Epistemic Comparative Likelihood

@cite{holliday-icard-2013} @cite{halpern-2003} @cite{van-der-hoek-1996}

Epistemic likelihood scales: the EpistemicScale arm of the categorical diagram in Core/Scale.lean.

@cite{holliday-icard-2013} study the logic of "at least as likely as" (≿) on propositions, defining a hierarchy of axiom systems (W ⊂ F ⊂ FA) whose qualitative additivity axiom is the epistemic counterpart of AdditiveScale.fa.

Axiom hierarchy (@cite{holliday-icard-2013}, Figure 3; axioms in Figures 4–6):

System	Axioms	Semantics
W	R, T	World-ordering + l-lifting
F	W + Bot, BT	+ bottom, non-triviality
FA	F + Tot, Tran, A	Qualitatively additive measures
FP∞	FA + Scott cancellation	Finitely additive measures

Bridge: Axiom A (epistemic qualitative additivity) and AdditiveScale.fa (mereological finite additivity) are algebraically equivalent — both express that a comparison factors through disjoint parts.

References:

• Holliday, W. & Icard, T. (2013). Measure Semantics and Qualitative Semantics for Epistemic Modals. SALT 23: 514–534.
• Halpern, J. (2003). Reasoning about Uncertainty. MIT Press.
• van der Hoek, W. (1996). Qualitative modalities. IJUFKS 4(1).

def Core.Scale.EpistemicAxiom.R {W : Type u_1} (ge : Set W → Set W → Prop) : Prop

Axiom R: reflexivity — A ≿ A.

Equations

• Core.Scale.EpistemicAxiom.R ge = ∀ (A : Set W), ge A A

def Core.Scale.EpistemicAxiom.T {W : Type u_1} (ge : Set W → Set W → Prop) : Prop

Axiom T: monotonicity — A ⊆ B → B ≿ A.

Equations

• Core.Scale.EpistemicAxiom.T ge = ∀ (A B : Set W), A ⊆ B → ge B A

def Core.Scale.EpistemicAxiom.F {W : Type u_1} (ge : Set W → Set W → Prop) : Prop

Axiom F: Ω ≿ ∅ — tautology is at least as likely as contradiction.

Equations

• Core.Scale.EpistemicAxiom.F ge = ge Set.univ ∅

def Core.Scale.EpistemicAxiom.BT {W : Type u_1} (ge : Set W → Set W → Prop) : Prop

Axiom BT: ¬(∅ ≿ Ω) — contradiction is NOT at least as likely as tautology. The non-triviality condition from @cite{holliday-icard-2013}. Without this, the degenerate ordering (all sets equivalent) would satisfy FA but admit no finitely additive measure representation (since μ(∅) = 0 but μ(Ω) = 1).

Equations

• Core.Scale.EpistemicAxiom.BT ge = ¬ge ∅ Set.univ

def Core.Scale.EpistemicAxiom.A {W : Type u_1} (ge : Set W → Set W → Prop) : Prop

Axiom A: qualitative additivity — A ≿ B ↔ (A \ B) ≿ (B \ A). The comparative likelihood factors through disjoint parts.

Equations

• Core.Scale.EpistemicAxiom.A ge = ∀ (A B : Set W), ge A B ↔ ge (A \ B) (B \ A)

def Core.Scale.EpistemicAxiom.J {W : Type u_1} (ge : Set W → Set W → Prop) : Prop

Axiom J (@cite{holliday-icard-2013}, Figure 4): right-union — φ ≿ ψ ∧ φ ≿ χ → φ ≿ (ψ ∨ χ).

Equations

• Core.Scale.EpistemicAxiom.J ge = ∀ (A B C : Set W), ge A B → ge A C → ge A (B ∪ C)

def Core.Scale.EpistemicAxiom.DS {W : Type u_1} (ge : Set W → Set W → Prop) : Prop

Axiom DS: determination by singletons (@cite{halpern-2003}, Thm. 7.5.1a) — A ≿ {b} → ∃ a ∈ A, {a} ≿ {b}. The comparison can be witnessed by a single element of the dominating set.

Equations

• Core.Scale.EpistemicAxiom.DS ge = ∀ (A : Set W) (b : W), ge A {b} → ∃ a ∈ A, ge {a} {b}

structure Core.Scale.EpistemicSystemW (W : Type u_1) : Type u_1

System W: the weakest epistemic likelihood logic. Reflexivity + monotonicity.

• ge : Set W → Set W → Prop
• refl : EpistemicAxiom.R self.ge
• mono : EpistemicAxiom.T self.ge

structure Core.Scale.EpistemicSystemF (W : Type u_1) extends Core.Scale.EpistemicSystemW W : Type u_1

System F: System W + Bot + BT. Bot (Ω ≿ ∅) is redundant with monotonicity. BT (¬(∅ ≿ Ω)) is the non-triviality condition that excludes degenerate orderings.

• ge : Set W → Set W → Prop
• refl : EpistemicAxiom.R self.ge
• mono : EpistemicAxiom.T self.ge
• bottom : EpistemicAxiom.F self.ge
• nonTrivial : EpistemicAxiom.BT self.ge

structure Core.Scale.EpistemicSystemFA (W : Type u_1) extends Core.Scale.EpistemicSystemF W : Type u_1

System FA: System F + totality + transitivity + qualitative additivity. Sound and complete for qualitatively additive measure semantics (@cite{holliday-icard-2013}, Theorem 6; @cite{van-der-hoek-1996}). Strictly weaker than FP∞ (finitely additive measures) for |W| ≥ 5 (Kraft, @cite{kraft-pratt-seidenberg-1959}, Theorem 8).

Totality and transitivity are part of the FA logic in @cite{holliday-icard-2013}: FA = Bot + BT + Tot + Tran + A.

• ge : Set W → Set W → Prop
• refl : EpistemicAxiom.R self.ge
• mono : EpistemicAxiom.T self.ge
• bottom : EpistemicAxiom.F self.ge
• nonTrivial : EpistemicAxiom.BT self.ge
• total (A B : Set W) : self.ge A B ∨ self.ge B A
• trans (A B C : Set W) : self.ge A B → self.ge B C → self.ge A C
• additive : EpistemicAxiom.A self.ge

structure Core.Scale.GFCPreorder (W : Type u_1) : Type u_1

A GFC preorder on propositions: a preorder on Set W that is monotone (supersets are at least as likely) and complement-reversing (A ≿ B → Bᶜ ≿ Aᶜ).

@cite{harrison-trainor-holliday-icard-2018} Definition 2.7. The acronym "GFC" reflects the three axiom groups: (G) preorder, (F) faithfulness (monotonicity), (C) complement reversal.

The m-lifting (≿ⁱ) of any reflexive, transitive world ordering is a GFC preorder (Theorem 3.2). Note that GFC preorders are NOT necessarily total — mLift_not_total gives a counterexample.

• ge : Set W → Set W → Prop
• refl : EpistemicAxiom.R self.ge
• trans (A B C : Set W) : self.ge A B → self.ge B C → self.ge A C
• mono : EpistemicAxiom.T self.ge
• complRev (A B : Set W) : self.ge A B → self.ge Bᶜ Aᶜ

def Core.Scale.GFCPreorder.toSystemW {W : Type u_1} (g : GFCPreorder W) : EpistemicSystemW W

Every GFC preorder yields System W (the weakest epistemic logic).

Equations

• g.toSystemW = { ge := g.ge, refl := ⋯, mono := ⋯ }

structure Core.Scale.FinAddMeasure (W : Type u_1) : Type u_1

A finitely additive probability measure on subsets of W.

• mu : Set W → ℚ

  The measure function

• nonneg (A : Set W) : 0 ≤ self.mu A

  Non-negativity

• additive (A B : Set W) : (∀ x ∈ A, x ∉ B) → self.mu (A ∪ B) = self.mu A + self.mu B

  Finite additivity: μ(A ∪ B) = μ(A) + μ(B) when A ∩ B = ∅

• total : self.mu Set.univ = 1

  Normalization

def Core.Scale.FinAddMeasure.inducedGe {W : Type u_1} (m : FinAddMeasure W) (A B : Set W) : Prop

Measure-induced comparative likelihood: A ≿ B ↔ μ(A) ≥ μ(B).

Equations

• m.inducedGe A B = (m.mu A ≥ m.mu B)

theorem Core.Scale.FinAddMeasure.inducedGe_axiomR {W : Type u_1} (m : FinAddMeasure W) : EpistemicAxiom.R m.inducedGe

Measure-induced ≿ is reflexive.

theorem Core.Scale.FinAddMeasure.inducedGe_axiomT {W : Type u_1} (m : FinAddMeasure W) : EpistemicAxiom.T m.inducedGe

Measure-induced ≿ satisfies monotonicity. A ⊆ B → B = A ∪ (B \ A) → μ(B) = μ(A) + μ(B \ A) ≥ μ(A).

theorem Core.Scale.FinAddMeasure.mu_empty {W : Type u_1} (m : FinAddMeasure W) : m.mu ∅ = 0

μ(∅) = 0 for any finitely additive measure. Follows from additivity: μ(∅ ∪ ∅) = μ(∅) + μ(∅), but ∅ ∪ ∅ = ∅.

def Core.Scale.FinAddMeasure.toSystemFA {W : Type u_1} (m : FinAddMeasure W) : EpistemicSystemFA W

Every finitely additive measure satisfies the FA axioms. A fortiori from @cite{holliday-icard-2013} Theorem 6 soundness, since every finitely additive measure is qualitatively additive.

Equations

• m.toSystemFA = { ge := m.inducedGe, refl := ⋯, mono := ⋯, bottom := ⋯, nonTrivial := ⋯, total := ⋯, trans := ⋯, additive := ⋯ }

noncomputable def Core.Scale.FinAddMeasure.toWorldPrior {W : Type u_1} (m : FinAddMeasure W) : W → ℚ

Extract a world prior from a finitely additive measure by evaluating μ on singletons: prior(w) = μ({w}).

This bridges the epistemic likelihood representation theorem to RSA's worldPrior field. The resulting function maps each world to a non-negative rational, suitable for use as an unnormalized prior.

Equations

• m.toWorldPrior w = m.mu {w}

theorem Core.Scale.FinAddMeasure.toWorldPrior_nonneg {W : Type u_1} (m : FinAddMeasure W) (w : W) : 0 ≤ m.toWorldPrior w

Singleton measures are non-negative.

structure Core.Scale.QualAddMeasure (W : Type u_1) : Type u_1

A qualitatively additive measure on subsets of W. Unlike FinAddMeasure, this does NOT require μ(A ∪ B) = μ(A) + μ(B) for disjoint A, B. Instead it requires the weaker qualitative additivity condition: μ(A) ≥ μ(B) ↔ μ(A \ B) ≥ μ(B \ A).

@cite{holliday-icard-2013} Theorem 6: System FA is sound and complete with respect to qualitatively additive measure models.

Note: the paper's definition of qualitatively additive measures includes μ(∅) = 0, but we omit it here because the completeness proof (Theorem 6) constructs a measure with μ(∅) > 0 (belowCount counts ∅ itself via reflexivity). The soundness direction (toSystemFA) takes mu_empty as an explicit hypothesis.

• mu : Set W → ℚ

  The measure function

• nonneg (A : Set W) : 0 ≤ self.mu A

  Non-negativity

• total : self.mu Set.univ = 1

  Normalization

• qualAdd (A B : Set W) : self.mu A ≥ self.mu B ↔ self.mu (A \ B) ≥ self.mu (B \ A)

  Qualitative additivity: μ(A) ≥ μ(B) ↔ μ(A \ B) ≥ μ(B \ A)

def Core.Scale.QualAddMeasure.inducedGe {W : Type u_1} (m : QualAddMeasure W) (A B : Set W) : Prop

Measure-induced comparative likelihood: A ≿ B ↔ μ(A) ≥ μ(B).

Equations

• m.inducedGe A B = (m.mu A ≥ m.mu B)

theorem Core.Scale.QualAddMeasure.inducedGe_axiomT {W : Type u_1} (m : QualAddMeasure W) (h_empty : m.mu ∅ = 0) : EpistemicAxiom.T m.inducedGe

Monotonicity for qualitatively additive measures with μ(∅) = 0: A ⊆ B → μ(B) ≥ μ(A). Follows from qualAdd + μ(∅) = 0 + nonneg.

def Core.Scale.QualAddMeasure.toSystemFA {W : Type u_1} (m : QualAddMeasure W) (h_empty : m.mu ∅ = 0) : EpistemicSystemFA W

A qualitatively additive measure with μ(∅) = 0 induces System FA. Soundness direction of @cite{holliday-icard-2013} Theorem 6: every qualitatively additive measure model (with μ(∅) = 0) satisfies the FA axioms.

The h_empty hypothesis is needed for monotonicity and non-triviality; it is NOT a field on QualAddMeasure because the completeness proof constructs a measure where μ(∅) > 0.

Equations

• m.toSystemFA h_empty = { ge := m.inducedGe, refl := ⋯, mono := ⋯, bottom := ⋯, nonTrivial := ⋯, total := ⋯, trans := ⋯, additive := ⋯ }

noncomputable def Core.Scale.FinAddMeasure.toQualAdd {W : Type u_1} (m : FinAddMeasure W) : QualAddMeasure W

Every finitely additive measure is qualitatively additive. Proof: μ(A) = μ(A \ B) + μ(A ∩ B) and μ(B) = μ(B \ A) + μ(A ∩ B), so μ(A) ≥ μ(B) ↔ μ(A \ B) ≥ μ(B \ A).

Equations

• m.toQualAdd = { mu := m.mu, nonneg := ⋯, total := ⋯, qualAdd := ⋯ }

def Core.Scale.halpernLift {W : Type u_1} (ge_w : W → W → Prop) (A B : Set W) : Prop

The l-lifting: a preorder on worlds induces a comparison on propositions. A ≿ B iff for every b ∈ B, ∃ a ∈ A with a ≥_w b. @cite{holliday-icard-2013} Definition 6; see also their injection-based m-lifting (Definition 7), which yields a complete logic for world-ordering models.

Equations

• Core.Scale.halpernLift ge_w A B = ∀ b ∈ B, ∃ a ∈ A, ge_w a b

theorem Core.Scale.halpernLift_axiomR {W : Type u_1} {ge_w : W → W → Prop} (hRefl : ∀ (w : W), ge_w w w) : EpistemicAxiom.R (halpernLift ge_w)

Halpern lift from a reflexive relation satisfies Axiom R.

theorem Core.Scale.halpernLift_axiomT {W : Type u_1} {ge_w : W → W → Prop} (hRefl : ∀ (w : W), ge_w w w) : EpistemicAxiom.T (halpernLift ge_w)

Halpern lift from a reflexive relation satisfies Axiom T. If A ⊆ B and b ∈ A, then b ∈ B, so take a = b.

def Core.Scale.halpernSystemW {W : Type u_1} (ge_w : W → W → Prop) (hRefl : ∀ (w : W), ge_w w w) : EpistemicSystemW W

The l-lifting from a reflexive preorder yields System W. Soundness direction: world-ordering models with the l-lifting validate System W (@cite{halpern-2003}; @cite{holliday-icard-2013}).

Equations

• Core.Scale.halpernSystemW ge_w hRefl = { ge := Core.Scale.halpernLift ge_w, refl := ⋯, mono := ⋯ }

theorem Core.Scale.halpernLift_axiomJ {W : Type u_1} {ge_w : W → W → Prop} : EpistemicAxiom.J (halpernLift ge_w)

Halpern lift satisfies Axiom J (right-union). If every b ∈ B is dominated and every c ∈ C is dominated, then every element of B ∪ C is dominated.

theorem Core.Scale.halpernLift_axiomDS {W : Type u_1} {ge_w : W → W → Prop} : EpistemicAxiom.DS (halpernLift ge_w)

Halpern lift satisfies Axiom DS (determination by singletons). If A ≿ {b} via the lift, some a ∈ A has ge_w a b, so {a} ≿ {b}.

def Core.Scale.mLift {W : Type u_1} (ge_w : W → W → Prop) (A B : Set W) : Prop

The m-lifting (@cite{holliday-icard-2013}, Definition 7): an injection-based alternative to halpernLift. A ≿ B iff there exists an injection f : B ↪ A such that f(b) ≥_w b for all b ∈ B.

The key difference from halpernLift (l-lifting) is that dominators must be distinct: each element of B is matched to a unique element of A. This avoids the "disjunction problem" (I1–I3 become invalid), while validating all 13 validity patterns V1–V13 (Fact 5).

Equations

• Core.Scale.mLift ge_w A B = ∃ (f : W → W), (∀ b ∈ B, f b ∈ A ∧ ge_w (f b) b) ∧ ∀ (b₁ b₂ : W), b₁ ∈ B → b₂ ∈ B → f b₁ = f b₂ → b₁ = b₂

theorem Core.Scale.mLift_axiomR {W : Type u_1} {ge_w : W → W → Prop} (hRefl : ∀ (w : W), ge_w w w) : EpistemicAxiom.R (mLift ge_w)

m-lift from a reflexive relation satisfies Axiom R.

theorem Core.Scale.mLift_axiomT {W : Type u_1} {ge_w : W → W → Prop} (hRefl : ∀ (w : W), ge_w w w) : EpistemicAxiom.T (mLift ge_w)

m-lift from a reflexive relation satisfies Axiom T. If A ⊆ B and b ∈ A, then b ∈ B, so take f = id.

def Core.Scale.mLiftSystemW {W : Type u_1} (ge_w : W → W → Prop) (hRefl : ∀ (w : W), ge_w w w) : EpistemicSystemW W

m-lifting from a reflexive preorder yields System W.

Equations

• Core.Scale.mLiftSystemW ge_w hRefl = { ge := Core.Scale.mLift ge_w, refl := ⋯, mono := ⋯ }