Lassiter (2015): Epistemic comparison, models of uncertainty, and the disjunction puzzle

Lassiter traces the disjunction puzzle, that φ is as likely as ψ and φ is as likely as χ entail φ is as likely as ψ or χ under Kratzer's comparative possibility, to Lewis's lift, by which the likelihood of a disjunction is that of its likeliest disjunct. Kratzer's revised lift keeps the puzzle for disjoint alternatives, and Holliday and Icard's m-lifting avoids it but, under Kratzer's must, refutes Yalcin's V6. A probability scale refutes the puzzle; symmetric fuzzy measures refute it too but also refute V13, which qualitative additivity restores. Three bridges from Kratzer's must to a probabilistic likely each fail, and the paper ends with three probabilistic replacements for the auxiliaries.

Main results

• disjunction_puzzle, lottery_collapse: §1.1, the puzzle and its lottery iteration.
• revised_escapes_collapse, revised_disjoint_puzzle, revised_countermodel_overlap: §1.4.
• mLift_refutes_V6: §1.5, the m-lifting against (35), which the l-lifting validates under the same must (Yalcin2010.kratzer_V6).
• prob_refutes_rightUnion, prob_rightUnion_of_half, lottery_bound: §2.1.
• fuzzy_refutes_V13, QualAddMeasure.eq_zero_of_union_le: §2.2, (48) and (49).
• bridge1_disjoint_puzzle, bridge1_thin_margin, bridge2_refutes_V6, bridge3_refutes_V6: §3.
• moreLikely_might, weak_refutes_moreLikely_might: §4.

Implementation notes

• Kratzer's must is human necessity over the empty base, as in Yalcin's study (Yalcin2010.must).
• The world-ordering countermodels share three worlds, the first alone best, with masses 0.4, 0.3, 0.3; BR3 holds there by Holliday and Icard's footnote-13 lemma.
• Probabilities are mathlib probability measures on a discrete space, compared on their real values; the models of §2.1 and §3 are finite sums of Dirac measures.
• The strong and weak auxiliaries are the positive forms of the probability scale, the preimages of Set.Ici for must and of Set.Ioi for might, with thresholds 1 and θ < 1.
• The ratio-modifier argument of §2.2 and the open problems of §4 are recorded as examples only.

References

• [Las15]
• [Kra91]
• [Kra12b]
• [Lew73b]
• [Hal97b]
• [Hal03]
• [HI13]
• [Yal10]
• [Ham59]
• [vFG10]

§1.1 The disjunction puzzle and the lottery

theorem Lassiter2015.disjunction_puzzle {W : Type u_1} (r : W → W → Prop) : ComparativeProbability.RightUnion (ComparativeProbability.LewisLift r)

The puzzle (11) is the right-union property, which Lewis's lift has, as Halpern shows.

theorem Lassiter2015.lottery_collapse {W : Type u_1} {r : Set W → Set W → Prop} (hJ : ComparativeProbability.RightUnion r) {ι : Type u_2} {s : Finset ι} (hs : s.Nonempty) {win : Set W} {wins : ι → Set W} (hcover : ⋃ i ∈ s, wins i = winᶜ) (h : ∀ i ∈ s, r win (wins i)) : r win winᶜ

Iterating the puzzle over the other ticket holders, whose winnings exhaust Sam's losing, makes Sam as likely to win as not, as in (13)–(14).

§1.4 Kratzer's revised comparative possibility

theorem Lassiter2015.kratzerLift_univ_iff {W : Type u_1} (r : W → W → Prop) (A : Set W) : ComparativeProbability.KratzerLift r A Set.univ ↔ A = Set.univ

The revised lift of (30) lets a proposition be as likely as its negation without being as likely as everything, escaping Yalcin's collapse, since it is as likely as the whole space only when the space is exhausted.

theorem Lassiter2015.revised_escapes_collapse : ¬ComparativeProbability.EquiprobabilityCollapse (ComparativeProbability.KratzerLift fun (x x_1 : Fin 2) => True)

Over two indiscriminate worlds {0} is as likely as its complement but not as everything.

theorem Lassiter2015.revised_countermodel_overlap {W : Type u_1} (r : W → W → Prop) {A B C : Set W} (hB : ComparativeProbability.KratzerLift r A B) (hC : ComparativeProbability.KratzerLift r A C) (hn : ¬ComparativeProbability.KratzerLift r A (B ∪ C)) : (∃ u ∈ B \ A, ∃ v ∈ A ∩ C, ¬(r u v ∧ ¬r v u)) ∨ ∃ u ∈ C \ A, ∃ v ∈ A ∩ B, ¬(r u v ∧ ¬r v u)

In a countermodel to the puzzle for the revised lift, (31) of Appendix B, a world of one alternative outside the first proposition fails to dominate a world the first proposition shares with the other alternative.

theorem Lassiter2015.revised_disjoint_puzzle {W : Type u_1} (r : W → W → Prop) {A B C : Set W} (hB : Disjoint A B) (hC : Disjoint A C) (hAB : ComparativeProbability.KratzerLift r A B) (hAC : ComparativeProbability.KratzerLift r A C) : ComparativeProbability.KratzerLift r A (B ∪ C)

With the alternatives made disjoint, as in the lottery, the puzzle is valid for the revised lift, (32) of Appendix C.

§1.5 The m-lifting under Kratzer's must

theorem Lassiter2015.best_not_probably_of_ncard_lt {W : Type u_1} [Finite W] (r : W → W → Prop) {A : Set W} (h : A.ncard < Aᶜ.ncard) : ¬ComparativeProbability.Probably (ComparativeProbability.MatchingLift r) A

A proposition holding at fewer worlds than its complement cannot be probable under the m-lifting, since no injection matches its complement into it.

def Lassiter2015.bestFirst : Set (Fin 3 → Prop)

The ordering source of §1.5 and §3 makes the first of three worlds the sole best one.

Equations

• Lassiter2015.bestFirst = {fun (x : Fin 3) => x = 0}

theorem Lassiter2015.bestFirst_le (v u : Fin 3) : v ≤ u ↔ u = 0 → v = 0

theorem Lassiter2015.must_best : Yalcin2010.must bestFirst {0} 0

Kratzer's must of the sole best world holds.

theorem Lassiter2015.mLift_refutes_V6 : ¬ComparativeProbability.MustToProbably (ComparativeProbability.MatchingLift LE.le) fun (x : Set (Fin 3)) => Yalcin2010.must bestFirst x 0

Under Kratzer's must the m-lifting refutes (35), Yalcin's V6. The sole best world is necessary but not likelier than its complement, since one world matches no injection from two.

§2.1 Scales of probability

noncomputable def Lassiter2015.skewed : MeasureTheory.Measure (Fin 3)

Three disjoint alternatives with masses 0.4, 0.3, 0.3 refute the puzzle for probability, as in (46).

Equations

• Lassiter2015.skewed = ∑ i : Fin (Nat.succ 0).succ.succ, ENNReal.ofReal (![4 / 10, 3 / 10, 3 / 10] i) • MeasureTheory.Measure.dirac i

instance Lassiter2015.instIsProbabilityMeasureFinOfNatNatSkewed : MeasureTheory.IsProbabilityMeasure skewed

theorem Lassiter2015.skewed_real (A : Set (Fin 3)) : skewed.real A = ∑ i : Fin 3, A.indicator ![4 / 10, 3 / 10, 3 / 10] i

theorem Lassiter2015.prob_refutes_rightUnion : ¬ComparativeProbability.RightUnion skewed.inducedGe

theorem Lassiter2015.prob_rightUnion_of_half {W : Type u_1} [MeasurableSpace W] [DiscreteMeasurableSpace W] (P : MeasureTheory.Measure W) [MeasureTheory.IsProbabilityMeasure P] {A B C : Set W} (hA : 1 / 2 ≤ P.real A) (hB : B ⊆ Aᶜ) (hC : C ⊆ Aᶜ) : P.real (B ∪ C) ≤ P.real A

The premises are compatible with the conclusion, since when the first proposition holds at least half the mass, any alternatives outside it together weigh no more.

theorem Lassiter2015.lottery_bound {n k : ℕ} [NeZero n] {A : Set (Fin n)} (h : A.ncard ≤ k) : (ProbabilityTheory.uniformOn Set.univ).real A ≤ ↑k / ↑n ∧ (↑n - ↑k) / ↑n ≤ (ProbabilityTheory.uniformOn Set.univ).real Aᶜ

In the fair lottery a holder of at most k of n tickets wins with probability at most k / n and loses with probability at least (n - k) / n.

§2.2 Symmetric fuzzy measures and equal shares

structure Lassiter2015.SymmetricFuzzyMeasure (W : Type u_2) : Type u_2

A symmetric fuzzy measure (47) is normalized, symmetric under complement, and monotone.

• mu : Set W → ℝ

  mu A is the measure of A.

• mu_univ : self.mu Set.univ = 1
• symm (A : Set W) : self.mu A + self.mu Aᶜ = 1
• mono ⦃A B : Set W⦄ : A ⊆ B → self.mu A ≤ self.mu B

def Lassiter2015.SymmetricFuzzyMeasure.likelihood {W : Type u_1} (μ : SymmetricFuzzyMeasure W) (A B : Set W) : Prop

Under a symmetric fuzzy measure A is at least as likely as B when it measures at least as much.

Equations

• μ.likelihood A B = (μ.mu B ≤ μ.mu A)

noncomputable def Lassiter2015.SymmetricFuzzyMeasure.ofMeasure {W : Type u_1} [MeasurableSpace W] [DiscreteMeasurableSpace W] (P : MeasureTheory.Measure W) [MeasureTheory.IsProbabilityMeasure P] : SymmetricFuzzyMeasure W

Every probability measure is a symmetric fuzzy measure, through its real values.

Equations

• Lassiter2015.SymmetricFuzzyMeasure.ofMeasure P = { mu := P.real, mu_univ := ⋯, symm := ⋯, mono := ⋯ }

noncomputable def Lassiter2015.cutClass : SymmetricFuzzyMeasure (Fin 3)

In the scenario of (48) Sam may go to school (1), more likely to the movies (0), or elsewhere (2), and the movies alone measure 0.6, as much as the movies or school.

Equations

• One or more equations did not get rendered due to their size.

theorem Lassiter2015.fuzzy_refutes_V13 : ¬ComparativeProbability.StrictDisjunctionIntro cutClass.likelihood

Symmetric fuzzy measures refute V13. Under cutClass going to the movies is exactly as likely as going to school or to the movies, although going to school is possible (48).

theorem Lassiter2015.QualAddMeasure.eq_zero_of_union_le {W : Type u_1} (m : ComparativeProbability.QualAddMeasure ℝ W) {A B : Set W} (h : m (A ∪ B) ≤ m A) : m (B \ A) = 0

Qualitative additivity, (49) added to (47), gives V13, so a proposition as likely as a disjunction it is part of leaves the other disjunct no mass, and (48) forces school out.

§3 Bridging rules

def Lassiter2015.Bridge1 {W : Type u_1} (r : W → W → Prop) [MeasurableSpace W] (P : MeasureTheory.Measure W) : Prop

BR1 (57) requires the revised lift to constrain probability.

Equations

• Lassiter2015.Bridge1 r P = ∀ (A B : Set W), ComparativeProbability.KratzerLift r A B → P B ≤ P A

def Lassiter2015.Bridge2 {W : Type u_1} (r : W → W → Prop) [MeasurableSpace W] (P : MeasureTheory.Measure W) : Prop

BR2 (59) requires the world order to constrain probability on singletons.

Equations

• Lassiter2015.Bridge2 r P = ∀ (u v : W), r u v → P {v} ≤ P {u}

def Lassiter2015.Bridge3 {W : Type u_1} (r : W → W → Prop) [MeasurableSpace W] (P : MeasureTheory.Measure W) : Prop

BR3 (61) requires the m-lifting to constrain probability.

Equations

• Lassiter2015.Bridge3 r P = ∀ (A B : Set W), ComparativeProbability.MatchingLift r A B → P B ≤ P A

theorem Lassiter2015.bridge1_disjoint_puzzle {W : Type u_1} (r : W → W → Prop) [MeasurableSpace W] (P : MeasureTheory.Measure W) (h : Bridge1 r P) {A B C : Set W} (hB : Disjoint A B) (hC : Disjoint A C) (hAB : ComparativeProbability.KratzerLift r A B) (hAC : ComparativeProbability.KratzerLift r A C) : P (B ∪ C) ≤ P A

BR1 reimports the puzzle for disjoint alternatives ordered by the revised lift (58).

theorem Lassiter2015.bridge3_of_agree {W : Type u_1} (r : W → W → Prop) [MeasurableSpace W] (P : MeasureTheory.Measure W) [Fintype W] [MeasurableSingletonClass W] (h : ∀ (v u : W), r v u ↔ P {u} ≤ P {v}) : Bridge3 r P

BR2 makes the m-lifting sound for the measure, by Holliday and Icard's footnote 13, so BR3 follows from BR2 when the order agrees with the measure.

theorem Lassiter2015.bridge2_refutes_V6 : Bridge2 LE.le skewed ∧ ¬ComparativeProbability.MustToProbably skewed.inducedGe fun (x : Set (Fin 3)) => Yalcin2010.must bestFirst x 0

In the three-world model of §3, with masses 0.4, 0.3, 0.3, BR2 holds, yet under Kratzer's must V6 fails, since the necessary best world is less likely than its complement.

theorem Lassiter2015.bridge3_refutes_V6 : Bridge3 LE.le skewed ∧ ¬ComparativeProbability.MustToProbably skewed.inducedGe fun (x : Set (Fin 3)) => Yalcin2010.must bestFirst x 0

The same model satisfies BR3, since the order agrees with the measure on singletons, so BR3 too allows a necessary proposition to be less likely than its negation.

noncomputable def Lassiter2015.thin : MeasureTheory.Measure (Fin 2)

thin is the two-world model of §3, with masses 0.5001 and 0.4999.

Equations

• Lassiter2015.thin = ∑ i : Fin (Nat.succ 0).succ, ENNReal.ofReal (![5001 / 10000, 4999 / 10000] i) • MeasureTheory.Measure.dirac i

instance Lassiter2015.instIsProbabilityMeasureFinOfNatNatThin : MeasureTheory.IsProbabilityMeasure thin

theorem Lassiter2015.thin_real (A : Set (Fin 2)) : thin.real A = ∑ i : Fin 2, A.indicator ![5001 / 10000, 4999 / 10000] i

def Lassiter2015.bestFirst₂ : Set (Fin 2 → Prop)

bestFirst₂ makes the first of two worlds the best.

Equations

• Lassiter2015.bestFirst₂ = {fun (x : Fin 2) => x = 0}

theorem Lassiter2015.bridge1_thin_margin : Bridge1 LE.le thin ∧ Yalcin2010.must bestFirst₂ {0} 0 ∧ thin.real {0} < 5002 / 10000

In thin BR1 holds and the sole best world is necessary, yet it is only barely likelier than its negation, so BR1 cannot deliver much more likely.

§4 Probability and the epistemic auxiliaries

def Lassiter2015.quantMust {W : Type u_1} (A : Set W) : Prop

Must as a quantifier over the epistemic space, Kratzer's auxiliary with an empty ordering source, holds of the whole space.

Equations

• Lassiter2015.quantMust A = (A = Set.univ)

def Lassiter2015.probMust {W : Type u_1} [MeasurableSpace W] (P : MeasureTheory.Measure W) (θ : ℝ) (A : Set W) : Prop

The probabilistic must with threshold θ holds when Pr(A) ≥ θ; it is strong at θ = 1 and weak below.

Equations

• Lassiter2015.probMust P θ A = (A ∈ P.real ⁻¹' Set.Ici θ)

def Lassiter2015.probMight {W : Type u_1} [MeasurableSpace W] (P : MeasureTheory.Measure W) (θ : ℝ) (A : Set W) : Prop

The dual might holds when Pr(A) > 1 - θ.

Equations

• Lassiter2015.probMight P θ A = (A ∈ P.real ⁻¹' Set.Ioi (1 - θ))

theorem Lassiter2015.quantMust_prob {W : Type u_1} [MeasurableSpace W] (P : MeasureTheory.Measure W) [MeasureTheory.IsProbabilityMeasure P] {A : Set W} (h : quantMust A) : P A = 1 ∧ P Aᶜ = 0

Under the quantificational auxiliaries a necessary proposition has all the mass, the largest possible margin over its negation, as (56) requires.

theorem Lassiter2015.probMust_one_iff {W : Type u_1} [MeasurableSpace W] (P : MeasureTheory.Measure W) [MeasureTheory.IsProbabilityMeasure P] (A : Set W) : probMust P 1 A ↔ P.real A = 1

The strong probabilistic must agrees with the quantificational one on the mass.

theorem Lassiter2015.probMight_iff_not_probMust_compl {W : Type u_1} [MeasurableSpace W] (P : MeasureTheory.Measure W) [MeasureTheory.IsProbabilityMeasure P] [DiscreteMeasurableSpace W] (θ : ℝ) (A : Set W) : probMight P θ A ↔ ¬probMust P θ Aᶜ

Might is the dual of must, since A might hold iff its complement is not a must.

theorem Lassiter2015.moreLikely_might {W : Type u_1} [MeasurableSpace W] (P : MeasureTheory.Measure W) [MeasureTheory.IsProbabilityMeasure P] {A B : Set W} (h : ComparativeProbability.Strict P.inducedGe A B) : probMight P 1 A

Under the strong probabilistic auxiliaries, what is more likely than something might be, since it has positive mass (64).

theorem Lassiter2015.weak_refutes_moreLikely_might : ∃ (P : MeasureTheory.Measure (Fin 100)), MeasureTheory.IsProbabilityMeasure P ∧ ∃ (A : Set (Fin 100)) (B : Set (Fin 100)), ComparativeProbability.Strict P.inducedGe A B ∧ ¬probMight P (9 / 10) A

Under a weak might two astronomically unlikely teams can be ordered without either being a live possibility (65).