Docs / Logic / ComparativeProbability / WorldOrdering

Comparative likelihood from an ordering of worlds

import Linglib.Logic.ComparativeProbability.WorldOrdering · namespace ComparativeProbability

This file reads comparative possibility as comparative likelihood. Lewis's comparative possibility is a monotone, transitive likelihood order with Halpern's two properties, right-union and determination by singletons, and a monotone, transitive relation on the subsets of a finite set is Lewis's comparative possibility of a reflexive relation on worlds exactly when it has both. Kratzer's revised notion is monotone and qualitatively additive. Holliday and Icard's m-lifting asks for an injective dominating map where Lewis's notion asks for any dominating map; the m-lifting of a preorder is a monotone, transitive likelihood order, and on a finite set it reverses complements.

Main definitions

ComparativeProbability.MatchingLift: the m-lifting.

Main statements

ComparativeProbability.lewis_iff_exists_dominating: Lewis's notion by a dominating map.
ComparativeProbability.MatchingLift.compl: the m-lifting of a finite preorder reverses complements.
ComparativeProbability.exists_eq_lewis_iff: the representation for Halpern's logic WJR.

Implementation notes

Complement reversal follows each point of A \ B along the dominating injection until it leaves A, the chain construction of Harrison-Trainor, Holliday and Icard's matching argument.

References

Lewis 1973b, Counterfactuals formalized
Kratzer 2012, Modals and Conditionals formalized
Holliday & Icard 2013, Measure Semantics and Qualitative Semantics for Epistemic Modals formalized
Harrison-Trainor et al. 2018, Inferring probability comparisons
Halpern 2003, Reasoning about Uncertainty

Lewis's comparative possibility as likelihood

A is at least as possible as B exactly when some map sends each world of B to a world of A that dominates it (Holliday and Icard, p. 524).

theorem lewis_iff_exists_dominating L69–75

{α : Type u_1} {r : α → α → Prop} {A B : Set α} :

ComparativePossibility.Lewis r A B ↔ ∃ (f : α → α), ∀ b ∈ B, f b ∈ A ∧ r (f b) b

Kratzer's revised comparative possibility as likelihood

L79

L81

L83–84

The m-lifting

The m-lifting MatchingLift r A B holds when some map injective on B sends each world of B to a world of A that dominates it (Holliday and Icard, p. 524), Harrison-Trainor, Holliday and Icard's injection extension (their Definition 3.1, p. 65).

def MatchingLift L88–92

{α : Type u_1} (r : α → α → Prop) (A B : Set α) :

Prop

MatchingLift r A B = ∃ (f : α → α), (∀ b ∈ B, f b ∈ A ∧ r (f b) b) ∧ Set.InjOn f B

Used by MatchingLift.lewis, matchingLift_empty, matchingLift_empty_left_iff, matchingLift_singleton_iff, matchingLift_of_subset, instReflSetMatchingLift, instIsLikelihoodMonoSetMatchingLiftOfRefl, instIsNontrivialSetMatchingLiftOfNonempty, MatchingLift.mono_left, MatchingLift.anti_right, MatchingLift.trans, instIsTransSetMatchingLift, MatchingLift.ncard_le, MatchingLift.compl, matchingLift_compl_compl, instIsComplementReversingSetMatchingLiftOfFiniteOfIsPreorder

Used in HollidayIcard2013, Lassiter2015

Complement reversal

A dominating injection f : A → B is followed from each point p ∈ A \ B: the chain p, f p, f (f p), … stays above p, cannot revisit A forever when α is finite, and chains from distinct origins never merge, because f is injective on A and no origin lies in the image B. Sending p to the first point of its chain outside A, and fixing the points outside A ∪ B, is a dominating injection Bᶜ → Aᶜ.

theorem MatchingLift.compl L207–226

{α : Type u_1} {r : α → α → Prop} {A B : Set α} [Finite α] [IsPreorder α r] (h : MatchingLift r B A) :

MatchingLift r Aᶜ Bᶜ

Built from

L228–230

L232–233

The WJR representation

A monotone, transitive relation on the subsets of a finite set is Lewis's comparative possibility of a reflexive relation on worlds exactly when it has right-union and is determined by singletons: the model-theoretic content of the soundness and completeness of Halpern's logic WJR over Lewis's comparative possibility (Holliday and Icard's Theorem 2, p. 520, citing Halpern's Theorem 7.5.1a).

theorem exists_eq_lewis_iff L251–265

{W : Type u_2} [Finite W] {ge : Set W → Set W → Prop} [IsLikelihoodMono ge] [IsTrans (Set W) ge] :

(∃ (r : W → W → Prop), Std.Refl r ∧ ComparativePossibility.Lewis r = ge) ↔ RightUnion ge ∧ DeterminedBySingletons ge