Documentation

Linglib.Theories.Semantics.Modality.ProbabilityOrdering

Probability-Ordering Bridge — @cite{kratzer-2012} §2.4 #

Connects probability assignments to Kratzer ordering sources.

A probability assignment P over worlds induces an ordering source where more probable worlds are ranked higher. For each world v, the ordering source generates the proposition "at least as probable as v": λ w => decide (P(w) ≥ P(v))

This means w ≥_A z iff every probability threshold that z meets, w also meets, which reduces to P(w) ≥ P(z).

Key result #

When the probability assignment is uniform, the induced ordering is trivial (all worlds equivalent). When skewed, the best worlds are those with maximal probability.

Reference: Kratzer, A. (2012). Modals and Conditionals. OUP. Ch. 2 §2.4.

Probability assignment #

source
@[reducible, inline]
abbrev Semantics.Modality.ProbabilityOrdering.ProbAssignment :
Type

A probability assignment maps worlds to rational probabilities.

Equations
Instances For
    source
    def Semantics.Modality.ProbabilityOrdering.probToOrdering (prob : ProbAssignment) :
    Kratzer.OrderingSource

    Convert a probability assignment to a Kratzer ordering source.

    For each world v, generate the proposition "at least as probable as v": w satisfies this iff P(w) ≥ P(v). The resulting ordering ranks worlds by probability: w ≥_A z iff P(w) ≥ P(z).

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Semantics.Modality.ProbabilityOrdering.probToOrdering_const (prob : ProbAssignment) (w w' : Attitudes.Intensional.World) :
      probToOrdering prob w = probToOrdering prob w'

      probToOrdering is world-independent: the ordering source is the same regardless of which evaluation world is chosen.

      Concrete example #

      source
      def Semantics.Modality.ProbabilityOrdering.skewedProb :
      ProbAssignment

      A skewed probability assignment: P(w0) > P(w1) > P(w2) > P(w3).

      Equations
      Instances For
        source
        def Semantics.Modality.ProbabilityOrdering.uniformProb :
        ProbAssignment

        A uniform probability assignment: P(w) = 1/4 for all w.

        Equations
        Instances For

          Theorems #

          source
          theorem Semantics.Modality.ProbabilityOrdering.uniform_all_equivalent (w z : Attitudes.Intensional.World) :
          (w ≤[probToOrdering uniformProb Core.Proposition.World4.w0] z) = true

          Uniform probability makes all worlds equivalent under the ordering. Every world satisfies the same set of ordering propositions (all of them).

          source
          theorem Semantics.Modality.ProbabilityOrdering.prob_ordering_best_w0 (w : Attitudes.Intensional.World) :
          Kratzer.bestWorlds Kratzer.emptyBackground (probToOrdering skewedProb) w = [Core.Proposition.World4.w0]

          Under skewed P, best worlds (from universal base) = {w0}. w0 has the highest probability and dominates all others.

          source
          theorem Semantics.Modality.ProbabilityOrdering.prob_ordering_w0_ge_w1 :
          (Core.Proposition.World4.w0 ≤[probToOrdering skewedProb Core.Proposition.World4.w0] Core.Proposition.World4.w1) = true

          Probability ordering preserves ranking: w0 ≥ w1 ≥ w2 ≥ w3.

          source
          theorem Semantics.Modality.ProbabilityOrdering.prob_ordering_w1_ge_w2 :
          (Core.Proposition.World4.w1 ≤[probToOrdering skewedProb Core.Proposition.World4.w0] Core.Proposition.World4.w2) = true
          source
          theorem Semantics.Modality.ProbabilityOrdering.prob_ordering_w2_ge_w3 :
          (Core.Proposition.World4.w2 ≤[probToOrdering skewedProb Core.Proposition.World4.w0] Core.Proposition.World4.w3) = true
          source
          theorem Semantics.Modality.ProbabilityOrdering.prob_ordering_w0_strict_w1 :
          (Core.Proposition.World4.w0 <[probToOrdering skewedProb Core.Proposition.World4.w0] Core.Proposition.World4.w1) = true

          Strict ordering: w0 > w1 (w0 beats w1 but not vice versa).

          source
          theorem Semantics.Modality.ProbabilityOrdering.prob_necessity_at_best (p : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) (hp : p Core.Proposition.World4.w0 = true) :
          Kratzer.necessity Kratzer.emptyBackground (probToOrdering skewedProb) p w = true

          Necessity under probability ordering: with skewed P and universal base, any proposition true at w0 is necessary (since best = {w0}).