Yalcin (2010): Probability operators

Yalcin asks what formal structure the semantics of probably, likely and the comparative at least as likely as requires, and runs three candidate semantics against a list of inference patterns: the intuitively valid V1–V12, the invalid I1–I3, and the questionable Conjunctivitis E1. Kratzer's relative likelihood account lifts the preorder an ordering source induces on worlds to propositions by Lewis's clause; Hamblin's possibility space account measures a proposition by its most possible world; the probability space account measures it by a finitely additive probability. In the paper's verdict Kratzer's account validates V1–V10 but fails positive form transfer and validates Halpern's union property I1, whose special case I2 collapses equiprobability into certainty; Hamblin's validates I1–I3 and Conjunctivitis; and the probability space account validates V1–V12 and none of I1–I3 or E1.

Implementation notes

• Each account is a likelihood relation on Set W with the comparative probability mixins, so most patterns come from Logic/ComparativeProbability/Patterns by instance resolution. V6 and V7 take Kratzer's human necessity and possibility for his account and the quantifiers A = Set.univ and A.Nonempty over the epistemic space for the other two; V8–V10 take Kratzer's restricted necessity or, for probability, entailment.
• The refutations are the paper's: footnote 8's two tied worlds against V11, the coin against I1 and I2, the twelve-sided die against E1.
• Two of the paper's verdicts do not survive formalization. V12, which the paper counts among Kratzer's failures, follows from I2, which the paper shows the account validates (kratzer_V12); for the same reason it is no point of Hamblin's account over Kratzer's. And Hamblin's account, which the paper credits with V11, refutes it (hamblin_refutes_V11). The paper's claim that Kratzer's account does not validate Conjunctivitis is confirmed by a four-world countermodel (kratzer_refutes_E1).
• Section numbers and example labels follow the author's June 2010 draft in Zotero and are unverified against the Philosophy Compass pagination.

References

• [Yal10]
• [Kra91]
• [Lew73b]
• [Ham59]
• [Hal03]

§3: the relative likelihood approach

The ordering source O induces the preorder v ≤[O] u, v at least as high as u; the comparative is Lewis's lift of it.

instance Yalcin2010.instIsPreorderLe_studies {W : Type u_1} (O : Set (W → Prop)) : IsPreorder W LE.le

@[reducible, inline]

abbrev Yalcin2010.likelihood {W : Type u_1} (O : Set (W → Prop)) : Set W → Set W → Prop

On Kratzer's account A is at least as likely as B when every world of B is matched by an at least as high world of A.

Equations

• Yalcin2010.likelihood O = ComparativeProbability.LewisLift LE.le

def Yalcin2010.must {W : Type u_1} (O : Set (W → Prop)) (A : Set W) (w : W) : Prop

Epistemic must at w is Kratzer's human necessity over the whole space.

Equations

• Yalcin2010.must O A w = Modality.humanNecessity ⊥ (fun (x : W) => O) (fun (x : W) => x ∈ A) w

def Yalcin2010.might {W : Type u_1} (O : Set (W → Prop)) (A : Set W) (w : W) : Prop

Epistemic might at w is human possibility, the dual of must.

Equations

• Yalcin2010.might O A w = Modality.humanPossibility ⊥ (fun (x : W) => O) (fun (x : W) => x ∈ A) w

def Yalcin2010.ifThen {W : Type u_1} (O : Set (W → Prop)) (A B : Set W) (w : W) : Prop

The indicative if A, B, with its tacit must, is human necessity over the base restricted by the antecedent, as in Kratzer's restrictor analysis.

Equations

• Yalcin2010.ifThen O A B w = Modality.humanNecessity (⊥.restrict fun (x : W) => x ∈ A) (fun (x : W) => O) (fun (x : W) => x ∈ B) w

theorem Yalcin2010.must_iff {W : Type u_1} (O : Set (W → Prop)) (A : Set W) (w : W) : must O A w ↔ ∀ (u : W), ∃ v ≤ u, ∀ z ≤ v, z ∈ A

theorem Yalcin2010.ifThen_iff {W : Type u_1} (O : Set (W → Prop)) (A B : Set W) (w : W) : ifThen O A B w ↔ ∀ u ∈ A, ∃ v ∈ A, v ≤ u ∧ ∀ z ∈ A, z ≤ v → z ∈ B

theorem Yalcin2010.kratzer_V1 {W : Type u_1} (O : Set (W → Prop)) : ComparativeProbability.ProbablyToNotProbablyNot (likelihood O)

theorem Yalcin2010.kratzer_V2 {W : Type u_1} (O : Set (W → Prop)) : ComparativeProbability.ProbablyDistribInf (likelihood O)

theorem Yalcin2010.kratzer_V3 {W : Type u_1} (O : Set (W → Prop)) : ComparativeProbability.ChancyDisjunctionIntro (likelihood O)

theorem Yalcin2010.kratzer_V4 {W : Type u_1} (O : Set (W → Prop)) : ComparativeProbability.Minimality (likelihood O)

theorem Yalcin2010.kratzer_V5 {W : Type u_1} (O : Set (W → Prop)) : ComparativeProbability.Maximality (likelihood O)

theorem Yalcin2010.kratzer_V6 {W : Type u_1} (O : Set (W → Prop)) [Nonempty W] (w : W) : ComparativeProbability.MustToProbably (likelihood O) fun (x : Set W) => must O x w

V6 holds for Kratzer's modals. A necessary proposition is probable, since its complement is dominated by the witnesses of necessity and cannot dominate them.

theorem Yalcin2010.kratzer_V7 {W : Type u_1} (O : Set (W → Prop)) [Nonempty W] (w : W) : ComparativeProbability.ProbablyToMight (likelihood O) fun (x : Set W) => might O x w

V7 holds for Kratzer's modals, by V6 and V1.

theorem Yalcin2010.kratzer_V10 {W : Type u_1} (O : Set (W → Prop)) (w : W) : ComparativeProbability.ConditionalToComparative (likelihood O) fun (x1 x2 : Set W) => ifThen O x1 x2 w

V10 holds for the restricted necessity, since the antecedent's worlds are matched by the witnesses, which are consequent worlds.

theorem Yalcin2010.kratzer_V8 {W : Type u_1} (O : Set (W → Prop)) (w : W) : ComparativeProbability.ChancyModusPonens (likelihood O) fun (x1 x2 : Set W) => ifThen O x1 x2 w

V8 holds for the restricted necessity. A world outside the consequent is dominated through the antecedent, and a consequent world undominated by the complement is found above the antecedent world the probability of the antecedent leaves undominated.

theorem Yalcin2010.kratzer_V9 {W : Type u_1} (O : Set (W → Prop)) (w : W) : ComparativeProbability.ChancyModusTollens (likelihood O) fun (x1 x2 : Set W) => ifThen O x1 x2 w

V9 holds for the restricted necessity, as the contrapositive of V8.

theorem Yalcin2010.kratzer_I1 {W : Type u_1} (O : Set (W → Prop)) : ComparativeProbability.RightUnion (likelihood O)

The union property I1 is the lift's right-union closure.

theorem Yalcin2010.kratzer_I2 {W : Type u_1} (O : Set (W → Prop)) : ComparativeProbability.EquiprobabilityCollapse (likelihood O)

I2, the collapse of equiprobability into certainty, follows from I1 as the paper derives it.

theorem Yalcin2010.kratzer_V12 {W : Type u_1} (O : Set (W → Prop)) : ComparativeProbability.ComplementTransfer (likelihood O)

Complement transfer holds for the lift of every preorder, since I2 does. The paper lists V12 with V11 among Kratzer's failures; its footnote 8 countermodel refutes only V11.

theorem Yalcin2010.kratzer_refutes_V11 : ¬ComparativeProbability.PositiveFormTransfer (likelihood ∅)

Footnote 8's limit-assumption variant refutes V11. With two tied maximal worlds, the empty ordering source, p the whole space and q one world, p is probable and q as likely as p, but q is not probable, since its complement is as high as it.

theorem Yalcin2010.kratzer_refutes_E1 : ¬ComparativeProbability.Conjunctivitis (likelihood {fun (x : Fin 4) => x ∈ {0, 1}, fun (x : Fin 4) => x ∈ {2, 3}})

Two incomparable tied pairs of worlds refute Conjunctivitis for Kratzer's account, as the paper says. {0, 2, 3} and {1, 2, 3} are each probable, since the one world each lacks is tied with a world it has, but their conjunction {2, 3} is not, since it dominates neither 0 nor 1.

§4: the possibility space approach

structure Yalcin2010.Possibility (W : Type u_2) : Type u_2

Hamblin's plausibility is a possibility measure on a finite epistemic space, given by values on worlds that are at most 1 and attain 1, so that the whole space measures 1 and every proposition or its complement is fully possible.

• poss : W → ℚ≥0

  poss w is the possibility of the world w.

• le_one (w : W) : self.poss w ≤ 1
• exists_eq_one : ∃ (w : W), self.poss w = 1

noncomputable def Yalcin2010.Possibility.measure {W : Type u_1} [Fintype W] (m : Possibility W) (A : Set W) : ℚ≥0

The possibility of a proposition is the greatest possibility of its worlds.

Equations

• m.measure A = {x : W | x ∈ A}.sup m.poss

theorem Yalcin2010.Possibility.measure_le_one {W : Type u_1} [Fintype W] (m : Possibility W) (A : Set W) : m.measure A ≤ 1

theorem Yalcin2010.Possibility.measure_eq_one_iff {W : Type u_1} [Fintype W] (m : Possibility W) (A : Set W) : m.measure A = 1 ↔ ∃ w ∈ A, m.poss w = 1

theorem Yalcin2010.Possibility.measure_mono {W : Type u_1} [Fintype W] (m : Possibility W) {A B : Set W} (h : A ⊆ B) : m.measure A ≤ m.measure B

theorem Yalcin2010.Possibility.measure_empty {W : Type u_1} [Fintype W] (m : Possibility W) : m.measure ∅ = 0

theorem Yalcin2010.Possibility.measure_univ {W : Type u_1} [Fintype W] (m : Possibility W) : m.measure Set.univ = 1

theorem Yalcin2010.Possibility.measure_singleton {W : Type u_1} [Fintype W] (m : Possibility W) (w : W) : m.measure {w} = m.poss w

theorem Yalcin2010.Possibility.measure_union {W : Type u_1} [Fintype W] (m : Possibility W) (A B : Set W) : m.measure (A ∪ B) = max (m.measure A) (m.measure B)

The measure of a union is the greater measure.

theorem Yalcin2010.Possibility.measure_eq_one_or_compl {W : Type u_1} [Fintype W] (m : Possibility W) (A : Set W) : m.measure A = 1 ∨ m.measure Aᶜ = 1

Every proposition or its complement is fully possible.

def Yalcin2010.Possibility.likelihood {W : Type u_1} [Fintype W] (m : Possibility W) (A B : Set W) : Prop

On Hamblin's account A is at least as likely as B when it is at least as possible.

Equations

• m.likelihood A B = (m.measure B ≤ m.measure A)

instance Yalcin2010.Possibility.instIsLikelihoodMonoSetLikelihood {W : Type u_1} [Fintype W] (m : Possibility W) : ComparativeProbability.IsLikelihoodMono m.likelihood

instance Yalcin2010.Possibility.instIsTransSetLikelihood {W : Type u_1} [Fintype W] (m : Possibility W) : IsTrans (Set W) m.likelihood

instance Yalcin2010.Possibility.instReflSetLikelihood {W : Type u_1} [Fintype W] (m : Possibility W) : Std.Refl m.likelihood

instance Yalcin2010.Possibility.instIsNontrivialSetLikelihood {W : Type u_1} [Fintype W] (m : Possibility W) : ComparativeProbability.IsNontrivial m.likelihood

theorem Yalcin2010.Possibility.measure_eq_one_of_probably {W : Type u_1} [Fintype W] (m : Possibility W) {A : Set W} (h : ComparativeProbability.Probably m.likelihood A) : m.measure A = 1 ∧ m.measure Aᶜ < 1

A probable proposition is fully possible and its complement is not.

theorem Yalcin2010.Possibility.hamblin_V1 {W : Type u_1} [Fintype W] (m : Possibility W) : ComparativeProbability.ProbablyToNotProbablyNot m.likelihood

theorem Yalcin2010.Possibility.hamblin_V2 {W : Type u_1} [Fintype W] (m : Possibility W) : ComparativeProbability.ProbablyDistribInf m.likelihood

theorem Yalcin2010.Possibility.hamblin_V3 {W : Type u_1} [Fintype W] (m : Possibility W) : ComparativeProbability.ChancyDisjunctionIntro m.likelihood

theorem Yalcin2010.Possibility.hamblin_V4 {W : Type u_1} [Fintype W] (m : Possibility W) : ComparativeProbability.Minimality m.likelihood

theorem Yalcin2010.Possibility.hamblin_V5 {W : Type u_1} [Fintype W] (m : Possibility W) : ComparativeProbability.Maximality m.likelihood

theorem Yalcin2010.Possibility.hamblin_V6 {W : Type u_1} [Fintype W] (m : Possibility W) : ComparativeProbability.MustToProbably m.likelihood fun (x : Set W) => x = Set.univ

V6 holds for the quantificational must of §4, simple necessity over the whole space.

theorem Yalcin2010.Possibility.hamblin_V7 {W : Type u_1} [Fintype W] (m : Possibility W) : ComparativeProbability.ProbablyToMight m.likelihood Set.Nonempty

V7 holds for the quantificational might, simple possibility over the whole space.

theorem Yalcin2010.Possibility.hamblin_E1 {W : Type u_1} [Fintype W] (m : Possibility W) : ComparativeProbability.Conjunctivitis m.likelihood

Conjunctivitis holds, since the fully possible worlds of two probable propositions lie in both, and the complement of the conjunction is the join of two complements below 1.

theorem Yalcin2010.Possibility.hamblin_I1 {W : Type u_1} [Fintype W] (m : Possibility W) : ComparativeProbability.RightUnion m.likelihood

I1, the union property, holds since the measure of a union is the greater measure.

theorem Yalcin2010.Possibility.hamblin_I2 {W : Type u_1} [Fintype W] (m : Possibility W) : ComparativeProbability.EquiprobabilityCollapse m.likelihood

I2 holds as a consequence of the union property.

theorem Yalcin2010.Possibility.hamblin_I3 {W : Type u_1} [Fintype W] (m : Possibility W) : ComparativeProbability.HamblinCollapse m.likelihood

I3, Hamblin's collapse, holds, so a probable proposition is at least as possible as any.

theorem Yalcin2010.Possibility.hamblin_V12 {W : Type u_1} [Fintype W] (m : Possibility W) : ComparativeProbability.ComplementTransfer m.likelihood

V12, which the paper counts in Hamblin's favour, holds since I2 does.

def Yalcin2010.threeWorlds : Possibility (Fin 3)

threeWorlds makes the first two of three worlds fully possible and the third half possible. Here {0, 1} is probable and {0, 2} is as possible as it, yet {0, 2} is not probable, since its complement {1} is fully possible. The paper credits Hamblin's account with positive form transfer; it fails.

Equations

• Yalcin2010.threeWorlds = { poss := ![1, 1, 1 / 2], le_one := ⋯, exists_eq_one := Yalcin2010.threeWorlds._proof_3 }

theorem Yalcin2010.hamblin_refutes_V11 : ¬ComparativeProbability.PositiveFormTransfer threeWorlds.likelihood

§5: semantics with probability spaces

theorem Yalcin2010.prob_V1 {W : Type u_1} [MeasurableSpace W] (P : MeasureTheory.Measure W) : ComparativeProbability.ProbablyToNotProbablyNot P.inducedGe

theorem Yalcin2010.prob_V2 {W : Type u_1} [MeasurableSpace W] (P : MeasureTheory.Measure W) [DiscreteMeasurableSpace W] [MeasureTheory.IsProbabilityMeasure P] : ComparativeProbability.ProbablyDistribInf P.inducedGe

theorem Yalcin2010.prob_V3 {W : Type u_1} [MeasurableSpace W] (P : MeasureTheory.Measure W) [DiscreteMeasurableSpace W] [MeasureTheory.IsProbabilityMeasure P] : ComparativeProbability.ChancyDisjunctionIntro P.inducedGe

theorem Yalcin2010.prob_V4 {W : Type u_1} [MeasurableSpace W] (P : MeasureTheory.Measure W) [DiscreteMeasurableSpace W] [MeasureTheory.IsProbabilityMeasure P] : ComparativeProbability.Minimality P.inducedGe

theorem Yalcin2010.prob_V5 {W : Type u_1} [MeasurableSpace W] (P : MeasureTheory.Measure W) [DiscreteMeasurableSpace W] [MeasureTheory.IsProbabilityMeasure P] : ComparativeProbability.Maximality P.inducedGe

theorem Yalcin2010.prob_V6 {W : Type u_1} [MeasurableSpace W] (P : MeasureTheory.Measure W) [DiscreteMeasurableSpace W] [MeasureTheory.IsProbabilityMeasure P] : ComparativeProbability.MustToProbably P.inducedGe fun (x : Set W) => x = Set.univ

V6 holds for the quantificational must, since the whole space has probability one.

theorem Yalcin2010.prob_V7 {W : Type u_1} [MeasurableSpace W] (P : MeasureTheory.Measure W) [DiscreteMeasurableSpace W] [MeasureTheory.IsProbabilityMeasure P] : ComparativeProbability.ProbablyToMight P.inducedGe Set.Nonempty

V7 holds for the quantificational might, since the empty proposition is not probable.

theorem Yalcin2010.prob_V8 {W : Type u_1} [MeasurableSpace W] (P : MeasureTheory.Measure W) [DiscreteMeasurableSpace W] [MeasureTheory.IsProbabilityMeasure P] : ComparativeProbability.ChancyModusPonens P.inducedGe fun (x1 x2 : Set W) => x1 ⊆ x2

theorem Yalcin2010.prob_V9 {W : Type u_1} [MeasurableSpace W] (P : MeasureTheory.Measure W) [DiscreteMeasurableSpace W] [MeasureTheory.IsProbabilityMeasure P] : ComparativeProbability.ChancyModusTollens P.inducedGe fun (x1 x2 : Set W) => x1 ⊆ x2

theorem Yalcin2010.prob_V10 {W : Type u_1} [MeasurableSpace W] (P : MeasureTheory.Measure W) [DiscreteMeasurableSpace W] [MeasureTheory.IsProbabilityMeasure P] : ComparativeProbability.ConditionalToComparative P.inducedGe fun (x1 x2 : Set W) => x1 ⊆ x2

theorem Yalcin2010.prob_V11 {W : Type u_1} [MeasurableSpace W] (P : MeasureTheory.Measure W) [DiscreteMeasurableSpace W] [MeasureTheory.IsProbabilityMeasure P] : ComparativeProbability.PositiveFormTransfer P.inducedGe

theorem Yalcin2010.prob_V12 {W : Type u_1} [MeasurableSpace W] (P : MeasureTheory.Measure W) [DiscreteMeasurableSpace W] [MeasureTheory.IsProbabilityMeasure P] : ComparativeProbability.ComplementTransfer P.inducedGe

theorem Yalcin2010.prob_refutes_I1_I2 : ¬ComparativeProbability.RightUnion (ProbabilityTheory.uniformOn Set.univ).inducedGe ∧ ¬ComparativeProbability.EquiprobabilityCollapse (ProbabilityTheory.uniformOn Set.univ).inducedGe

The fair coin refutes I1 and I2. Heads is at least as likely as tails and as heads but not as heads or tails, and it is as likely as its complement without being as likely as everything.

theorem Yalcin2010.prob_refutes_I3 : ¬ComparativeProbability.HamblinCollapse (ProbabilityTheory.uniformOn Set.univ).inducedGe

Three equiprobable worlds refute Hamblin's collapse I3, since {0, 1} is probable but not as likely as everything.

theorem Yalcin2010.prob_refutes_E1 : ¬ComparativeProbability.Conjunctivitis (ProbabilityTheory.uniformOn Set.univ).inducedGe

The twelve-sided die of §4 refutes Conjunctivitis for the probability space semantics. A number below nine and a number above four are each probable, eight faces of twelve, but a number above four and below nine is not, four faces.

§6: scales

Probably as a relative adjective compares the probability with a contextual threshold n; V1 survives exactly the thresholds at or above one half.

def Yalcin2010.probablyAt {W : Type u_1} [MeasurableSpace W] (P : MeasureTheory.Measure W) (n : ℝ) (A : Set W) : Prop

Probably with threshold n holds when Pr(A) > n, the strict positive form of the probability scale.

Equations

• Yalcin2010.probablyAt P n A = (A ∈ P.real ⁻¹' Set.Ioi n)

theorem Yalcin2010.probablyAt_V1 {W : Type u_1} [MeasurableSpace W] (P : MeasureTheory.Measure W) [DiscreteMeasurableSpace W] [MeasureTheory.IsProbabilityMeasure P] {n : ℝ} (hn : 1 / 2 ≤ n) (A : Set W) : probablyAt P n A → ¬probablyAt P n Aᶜ

With a threshold of at least one half, a proposition and its complement are not both probable.

theorem Yalcin2010.probablyAt_refutes_V1 : probablyAt (ProbabilityTheory.uniformOn Set.univ) (1 / 3) {0} ∧ probablyAt (ProbabilityTheory.uniformOn Set.univ) (1 / 3) {0}ᶜ

Below one half the pattern fails. With the threshold one third, the fair coin's heads and tails are both probable.