Docs / Logic / ComparativeProbability / Patterns

Validity patterns for comparative probability

import Linglib.Logic.ComparativeProbability.Patterns · namespace ComparativeProbability

Yalcin assesses semantics for probably and the comparative at least as likely as against inference patterns: the intuitively valid V1–V12, the invalid I1–I3, and the questionable Conjunctivitis E1. Holliday and Icard's Figure 1 keeps his labels for V1–V7, V11, V12 and I1–I3, leaves out the conditional patterns V8–V10 and E1, and adds V13, which Lassiter defends against symmetric fuzzy measures. Each pattern is a predicate on a likelihood relation r on a Boolean algebra, with the account's modals (V6, V7) and conditional (V8–V10) as parameters; I1 is RightUnion. Each valid pattern is derived once from the axioms in Defs.lean, so a model discharges it by instance resolution.

Main statements

mustToProbably_eq_top_iff, probablyToMight_ne_bot_iff: for the quantifiers a = ⊤ and a ≠ ⊥ over the epistemic space, V6 says that the tautology is probable and V7 that the contradiction is not.
strictDisjunctionIntro_iff: over a monotone order, V13 says that an event at least as likely as a disjunction it is part of leaves the rest no more likely than ⊥.
chancyModusTollens_iff: V9 is V8 by contraposition, whatever the conditional.
equiprobabilityCollapse_of_rightUnion, hamblinCollapse_of_equiprobabilityCollapse, complementTransfer_of_equiprobabilityCollapse: I1 gives I2, as Yalcin derives it, and I2 gives I3 and V12. This is why Holliday and Icard's Fact 1 finds V12 valid for the l-lifting although Yalcin counts it among the failures of Kratzer's account.

References

Yalcin 2010, Probability Operators formalized
Holliday & Icard 2013, Measure Semantics and Qualitative Semantics for Epistemic Modals formalized
Lassiter 2015, Epistemic Comparison, Models of Uncertainty, and the Disjunction Puzzle formalized

Declarations

V9 is V8 by contraposition, for any conditional.

theorem chancyModusTollens_iff L87–90

{α : Type u_1} [BooleanAlgebra α] {r ifThen : α → α → Prop} :

ChancyModusTollens r ifThen ↔ ChancyModusPonens r ifThen

Built from ,

V6 for the necessity modal a = ⊤ says exactly that the tautology is probable.

theorem mustToProbably_eq_top_iff L92–94

{α : Type u_1} [BooleanAlgebra α] {r : α → α → Prop} :

(MustToProbably r fun (x : α) => x = ⊤) ↔ Probably r ⊤

Built from

V7 for the possibility modal a ≠ ⊥ says exactly that the contradiction is not probable.

theorem probablyToMight_ne_bot_iff L96–99

{α : Type u_1} [BooleanAlgebra α] {r : α → α → Prop} :

(ProbablyToMight r fun (x : α) => x ≠ ⊥) ↔ ¬Probably r ⊥

Built from

I3 is I2 with a strict premise.

theorem hamblinCollapse_of_equiprobabilityCollapse L101–103

{α : Type u_1} [BooleanAlgebra α] {r : α → α → Prop} (h : EquiprobabilityCollapse r) :

Built from ,

Over a monotone order, V13 says that a proposition at least as likely as a disjunction it is part of leaves the rest of the disjunction no more likely than ⊥.

theorem strictDisjunctionIntro_iff L133–139

{α : Type u_1} [BooleanAlgebra α] {r : α → α → Prop} [IsLikelihoodMono r] :

StrictDisjunctionIntro r ↔ ∀ (a b : α), r b (a ⊔ b) → r ⊥ (a \ b)

Built from

L141–144

L152–153

L155–156

I2 makes V12 trivial, since a ≽ aᶜ already gives a ≽ bᶜ.

theorem complementTransfer_of_equiprobabilityCollapse L158–161

{α : Type u_1} [BooleanAlgebra α] {r : α → α → Prop} [IsTrans α r] (h : EquiprobabilityCollapse r) :

ComplementTransfer r

Built from ,

The union property gives I2, as Yalcin derives it, since I1 for a, a and aᶜ gives a ≽ ⊤ and V5 does the rest.

theorem equiprobabilityCollapse_of_rightUnion L163–167

{α : Type u_1} [BooleanAlgebra α] {r : α → α → Prop} [IsTrans α r] [IsLikelihoodMono r] (hJ : RightUnion r) :

EquiprobabilityCollapse r

Built from