Documentation

Linglib.Theories.Semantics.Modality.ProbabilityOrdering

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

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 => 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.

UNVERIFIED reference: Kratzer (2012) Modals and Conditionals, OUP — chapter and section number not checked against the original.

Polymorphic core #

source
@[reducible, inline]
abbrev Semantics.Modality.ProbabilityOrdering.ProbAssignment (W : Type u_1) :
Type u_1

A probability assignment maps worlds to rational probabilities.

Equations
Instances For
    source
    noncomputable def Semantics.Modality.ProbabilityOrdering.probToOrdering {W : Type u_1} [Fintype W] (prob : ProbAssignment W) :
    Core.Logic.Intensional.OrderingSource W

    Convert a probability assignment to a Kratzer ordering source over a finite world type.

    For each world v in Finset.univ, 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
    Instances For
      source
      theorem Semantics.Modality.ProbabilityOrdering.probToOrdering_const {W : Type u_1} [Fintype W] (prob : ProbAssignment W) (w w' : W) :
      probToOrdering prob w = probToOrdering prob w'

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

      source
      theorem Semantics.Modality.ProbabilityOrdering.higher_prob_dominates {W : Type u_1} [Fintype W] {prob : ProbAssignment W} {w1 w2 wEval : W} (hOrd : prob w1 ≥ prob w2) :
      w1 ≤[probToOrdering prob wEval] w2

      Convenience reducer: ordering relation reduces to probability comparison via transitivity over the threshold propositions. If prob w₁ ≥ prob w₂ then w₁ ≥_(probToOrdering prob w) w₂.

      source
      theorem Semantics.Modality.ProbabilityOrdering.uniform_all_equivalent {W : Type u_1} [Fintype W] [Inhabited W] (c : ℚ) (w z wEval : W) :
      w ≤[probToOrdering (fun (x : W) => c) wEval] z

      Uniform probability makes all worlds equivalent under the ordering.

      Concrete examples on Fin 4 #

      These examples instantiate the polymorphic core at Fin 4 (a 4-element world set) for direct demonstration.

      source
      @[reducible, inline]
      abbrev Semantics.Modality.ProbabilityOrdering.World :
      Type
      Equations
      Instances For
        source
        def Semantics.Modality.ProbabilityOrdering.skewedProb :
        ProbAssignment World

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

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

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

          Equations
          Instances For
            source
            theorem Semantics.Modality.ProbabilityOrdering.prob_ordering_best_w0 (w : World) :
            Kratzer.bestWorlds Core.Logic.Intensional.emptyBackground (probToOrdering skewedProb) w = {0}

            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 :
            0 ≤[probToOrdering skewedProb 0] 1

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

            source
            theorem Semantics.Modality.ProbabilityOrdering.prob_ordering_w1_ge_w2 :
            1 ≤[probToOrdering skewedProb 0] 2
            source
            theorem Semantics.Modality.ProbabilityOrdering.prob_ordering_w2_ge_w3 :
            2 ≤[probToOrdering skewedProb 0] 3
            source
            theorem Semantics.Modality.ProbabilityOrdering.prob_ordering_w0_strict_w1 :
            0 <[probToOrdering skewedProb 0] 1

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

            source
            theorem Semantics.Modality.ProbabilityOrdering.prob_necessity_at_best (p : World → Prop) (w : World) (hp : p 0) :
            Kratzer.necessity Core.Logic.Intensional.emptyBackground (probToOrdering skewedProb) p w

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