Epistemic Entailment Patterns (@cite{holliday-icard-2013}, Figure 1)

@cite{holliday-icard-2013} @cite{harrison-trainor-holliday-icard-2018} @cite{yalcin-2010}

@cite{holliday-icard-2013} Figure 1 lists 10 validity patterns (V1–V7, V11–V13) and 3 invalidity patterns (I1–I3) for epistemic comparatives. (V8–V10 are from @cite{yalcin-2010} and omitted from H&I's condensed figure.) This file defines each pattern as a Prop-valued predicate on a comparison relation ge, then proves which patterns hold (or fail) in each of three semantic classes:

Pattern	Measure (FP∞)	Qualitative (FA)	l-lifting (W)	m-lifting
V1	✓	✓	✓	✓
V2	✓	✓	✓	✓
V3	✓	✓	✓	✓
V4	✓	✓	✓	✓
V5	✓	✓	✓	✓
V6	✓	✓	✓	✓
V7	✓	✓	✓	✓
V11	✓	✓	✗	✓
V12	✓	✓	✓ (preorder)	✓
V13	✓	✓	✗	✓
I1	✗	✗	✓ (disj. bug)	✗
I2	✗	✗	✓ (disj. bug)	✗
I3	✗	✗	✓ (disj. bug)	✗

The world-ordering column illustrates the "disjunction problem": Halpern's l-lifting validates patterns (I1–I3) that are invalid under measure semantics, showing that world-ordering semantics is strictly stronger than intended. V11 and V13 are invalid for l-lifting (Fact 1 in the paper).

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

Strict comparative: A ≻ B iff A ≿ B but not B ≿ A.

Equations

• Core.Scale.strict ge A B = (ge A B ∧ ¬ge B A)

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

"Probably A" — A is strictly more likely than its complement.

Equations

• Core.Scale.probably ge A = Core.Scale.strict ge A Aᶜ

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

"Possibly A" — A is not certainly impossible (¬(∅ ≿ A)).

Equations

• Core.Scale.possibly ge A = ¬ge ∅ A

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

V1: △A → ¬△Aᶜ (probably A implies not probably not-A).

Equations

• Core.Scale.patternV1 ge = ∀ (A : Set W), Core.Scale.probably ge A → ¬Core.Scale.probably ge Aᶜ

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

V2: △(A ∩ B) → △A ∧ △B (probably conjunction implies probably each conjunct).

Equations

• Core.Scale.patternV2 ge = ∀ (A B : Set W), Core.Scale.probably ge (A ∩ B) → Core.Scale.probably ge A ∧ Core.Scale.probably ge B

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

V3: △A → △(A ∪ B) (probably A implies probably any disjunction containing A).

Equations

• Core.Scale.patternV3 ge = ∀ (A B : Set W), Core.Scale.probably ge A → Core.Scale.probably ge (A ∪ B)

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

V4: A ≿ ∅ (every proposition is at least as likely as absurdity).

Equations

• Core.Scale.patternV4 ge = ∀ (A : Set W), ge A ∅

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

V5: ⊤ ≿ A (tautology is at least as likely as anything).

Equations

• Core.Scale.patternV5 ge = ∀ (A : Set W), ge Set.univ A

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

V6: □A → △A (necessarily A implies probably A). □A is ¬◇¬A = ge ∅ Aᶜ in the set-theoretic framework (@cite{holliday-icard-2013}, Figure 1).

Equations

• Core.Scale.patternV6 ge = ∀ (A : Set W), ge ∅ Aᶜ → Core.Scale.probably ge A

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

V7: △A → ◇A (probably implies possibly).

Equations

• Core.Scale.patternV7 ge = ∀ (A : Set W), Core.Scale.probably ge A → Core.Scale.possibly ge A

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

V11: B ≿ A → △A → △B (if B is at least as likely as a probable set, then B is probable). Uses the comparative ≿, not set inclusion ⊆. Invalid for l-lifting (Fact 1 in @cite{holliday-icard-2013}).

Equations

• Core.Scale.patternV11 ge = ∀ (A B : Set W), ge B A → Core.Scale.probably ge A → Core.Scale.probably ge B

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

V12: B ≿ A → A ≿ Aᶜ → B ≿ Bᶜ (if B is at least as likely as a set that is more likely than not, then B is more likely than not). Uses the comparative ≿, not set inclusion ⊆.

Equations

• Core.Scale.patternV12 ge = ∀ (A B : Set W), ge B A → ge A Aᶜ → ge B Bᶜ

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

V13: (A \ B) ≻ ∅ → (A ∪ B) ≻ B (positive excess implies strict increase).

Equations

• Core.Scale.patternV13 ge = ∀ (A B : Set W), Core.Scale.strict ge (A \ B) ∅ → Core.Scale.strict ge (A ∪ B) B

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

I1: A ≿ B → A ≿ C → A ≿ (B ∪ C) (additivity of upper bound — INVALID for measures).

Equations

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

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

I2: A ≿ Aᶜ → A ≿ B (more-likely-than-not implies universally maximal — INVALID for measures).

Equations

• Core.Scale.patternI2 ge = ∀ (A B : Set W), ge A Aᶜ → ge A B

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

I3: △A → A ≿ B (probably implies universally maximal — INVALID for measures).

Equations

• Core.Scale.patternI3 ge = ∀ (A B : Set W), Core.Scale.probably ge A → ge A B

theorem Core.Scale.measure_V1 {W : Type u_1} (m : FinAddMeasure W) : patternV1 m.inducedGe

theorem Core.Scale.measure_V2 {W : Type u_1} (m : FinAddMeasure W) : patternV2 m.inducedGe

theorem Core.Scale.measure_V3 {W : Type u_1} (m : FinAddMeasure W) : patternV3 m.inducedGe

theorem Core.Scale.measure_V4 {W : Type u_1} (m : FinAddMeasure W) : patternV4 m.inducedGe

theorem Core.Scale.measure_V5 {W : Type u_1} (m : FinAddMeasure W) : patternV5 m.inducedGe

theorem Core.Scale.measure_V6 {W : Type u_1} (m : FinAddMeasure W) : patternV6 m.inducedGe

theorem Core.Scale.measure_V7 {W : Type u_1} (m : FinAddMeasure W) : patternV7 m.inducedGe

theorem Core.Scale.measure_V11 {W : Type u_1} (m : FinAddMeasure W) : patternV11 m.inducedGe

theorem Core.Scale.measure_V12 {W : Type u_1} (m : FinAddMeasure W) : patternV12 m.inducedGe

theorem Core.Scale.measure_V13 {W : Type u_1} (m : FinAddMeasure W) : patternV13 m.inducedGe

theorem Core.Scale.measure_not_I1 : ¬∀ (m : FinAddMeasure (Fin 3)), patternI1 m.inducedGe

I1 is invalid for measure semantics: with uniform measure on Fin 3, {0} ≿ {1} and {0} ≿ {2} but ¬({0} ≿ {1,2}).

theorem Core.Scale.measure_not_I2 : ¬∀ (m : FinAddMeasure (Fin 3)), patternI2 m.inducedGe

I2 is invalid for measure semantics: with uniform measure on Fin 3, {0,1} ≿ {0,1}ᶜ but ¬({0,1} ≿ univ).

theorem Core.Scale.measure_not_I3 : ¬∀ (m : FinAddMeasure (Fin 3)), patternI3 m.inducedGe

I3 is invalid for measure semantics: with uniform measure on Fin 3, probably({0,1}) but ¬({0,1} ≿ univ).

theorem Core.Scale.fa_V1 {W : Type u_1} (sys : EpistemicSystemFA W) : patternV1 sys.ge

theorem Core.Scale.fa_V2 {W : Type u_1} (sys : EpistemicSystemFA W) : patternV2 sys.ge

theorem Core.Scale.fa_V3 {W : Type u_1} (sys : EpistemicSystemFA W) : patternV3 sys.ge

theorem Core.Scale.fa_V4 {W : Type u_1} (sys : EpistemicSystemFA W) : patternV4 sys.ge

theorem Core.Scale.fa_V5 {W : Type u_1} (sys : EpistemicSystemFA W) : patternV5 sys.ge

theorem Core.Scale.fa_V6 {W : Type u_1} (sys : EpistemicSystemFA W) : patternV6 sys.ge

theorem Core.Scale.fa_V7 {W : Type u_1} (sys : EpistemicSystemFA W) : patternV7 sys.ge

theorem Core.Scale.fa_V11 {W : Type u_1} (sys : EpistemicSystemFA W) : patternV11 sys.ge

theorem Core.Scale.fa_V12 {W : Type u_1} (sys : EpistemicSystemFA W) : patternV12 sys.ge

theorem Core.Scale.fa_V13 {W : Type u_1} (sys : EpistemicSystemFA W) : patternV13 sys.ge

theorem Core.Scale.fa_not_I1 : ¬∀ (W : Type) (sys : EpistemicSystemFA W), patternI1 sys.ge

I1 is invalid for FA: the measure-induced FA system on Fin 3 is a counterexample (every finitely additive measure induces an FA system via toSystemFA).

theorem Core.Scale.fa_not_I2 : ¬∀ (W : Type) (sys : EpistemicSystemFA W), patternI2 sys.ge

I2 is invalid for FA.

theorem Core.Scale.fa_not_I3 : ¬∀ (W : Type) (sys : EpistemicSystemFA W), patternI3 sys.ge

I3 is invalid for FA.

Recall: halpernLift ge_w A B := ∀ b, b ∈ B → ∃ a, a ∈ A ∧ ge_w a b. So halpernLift ge_w A B means every element of B is dominated by some element of A.

theorem Core.Scale.halpern_V1 {W : Type u_2} (ge_w : W → W → Prop) : patternV1 (halpernLift ge_w)

theorem Core.Scale.halpern_V2 {W : Type u_2} (ge_w : W → W → Prop) : patternV2 (halpernLift ge_w)

theorem Core.Scale.halpern_V3 {W : Type u_2} (ge_w : W → W → Prop) : patternV3 (halpernLift ge_w)

theorem Core.Scale.halpern_V4 {W : Type u_2} (ge_w : W → W → Prop) : patternV4 (halpernLift ge_w)

theorem Core.Scale.halpern_V5 {W : Type u_2} (ge_w : W → W → Prop) (hRefl : ∀ (w : W), ge_w w w) : patternV5 (halpernLift ge_w)

theorem Core.Scale.halpern_V6 {W : Type u_2} [Nonempty W] (ge_w : W → W → Prop) : patternV6 (halpernLift ge_w)

theorem Core.Scale.halpern_V7 {W : Type u_2} (ge_w : W → W → Prop) : patternV7 (halpernLift ge_w)

theorem Core.Scale.halpern_not_V11 : ∃ (W : Type) (ge_w : W → W → Prop), (∀ (w : W), ge_w w w) ∧ ¬patternV11 (halpernLift ge_w)

V11 is invalid for world-ordering semantics (Fact 1 in @cite{holliday-icard-2013}). Counterexample: W = Fin 2, ge_w total. A = W (probably, since W ≿ ∅ and ¬(∅ ≿ W)). B = {0} (B ≿ A since ge_w is total, but Bᶜ = {1} ≿ B since ge_w is total — not strictly).

theorem Core.Scale.halpern_V12 {W : Type u_2} (ge_w : W → W → Prop) (hTrans : ∀ (u v w : W), ge_w u v → ge_w v w → ge_w u w) : patternV12 (halpernLift ge_w)

V12 is valid for world-ordering semantics with a preorder (Fact 1 in @cite{holliday-icard-2013}). Requires transitivity for the case where y ∈ Bᶜ ∩ Aᶜ: chain through A via ge A Aᶜ, then through B via ge B A.

theorem Core.Scale.halpern_not_V13 : ∃ (W : Type) (ge_w : W → W → Prop), (∀ (w : W), ge_w w w) ∧ ¬patternV13 (halpernLift ge_w)

V13 is invalid for world-ordering semantics. Counterexample: W = Fin 2, ge_w = total (everything related). A = {0}, B = {1}. Then (A \ B) ≻ ∅ holds but (A ∪ B) ≻ B fails because ge B (A ∪ B).

theorem Core.Scale.halpern_I1 {W : Type u_2} (ge_w : W → W → Prop) : patternI1 (halpernLift ge_w)

I1 is valid for world-ordering semantics: the "disjunction problem".

theorem Core.Scale.halpern_I2 {W : Type u_2} (ge_w : W → W → Prop) (hRefl : ∀ (w : W), ge_w w w) : patternI2 (halpernLift ge_w)

I2 is valid for world-ordering semantics.

theorem Core.Scale.halpern_I3 {W : Type u_2} (ge_w : W → W → Prop) (hRefl : ∀ (w : W), ge_w w w) : patternI3 (halpernLift ge_w)

I3 is valid for world-ordering semantics.

The m-lifting validates all 13 validity patterns V1–V13 and invalidates I1–I3 (Fact 5 in @cite{holliday-icard-2013}). This avoids the "disjunction problem" that plagues the l-lifting.

V1, V3–V7 follow from the l-lifting proofs (since m-lifting implies
l-lifting). V2, V11–V13 use the injection structure directly;
V11–V12 rely on complement reversal (`mLift_complement_reversal`). 

theorem Core.Scale.mLift_implies_halpernLift {W : Type u_2} {ge_w : W → W → Prop} {A B : Set W} (h : mLift ge_w A B) : halpernLift ge_w A B

Every m-lift entails an l-lift: if there is an injection from B to A with each image dominating its preimage, then in particular every element of B is dominated by some element of A.

theorem Core.Scale.mLift_V1 {W : Type u_2} (ge_w : W → W → Prop) : patternV1 (mLift ge_w)

theorem Core.Scale.mLift_V2 {W : Type u_2} (ge_w : W → W → Prop) (_hRefl : ∀ (w : W), ge_w w w) : patternV2 (mLift ge_w)

V2 is valid for the m-lifting: △(A ∩ B) → △A ∧ △B.

Proof: restrict the injection f : (A∩B)ᶜ ↪ A∩B to Aᶜ ⊆ (A∩B)ᶜ to get the ge half. For the strict half, any reverse injection g : A ↪ Aᶜ restricts to A∩B ↪ (A∩B)ᶜ (since Aᶜ ⊆ (A∩B)ᶜ), contradicting the hypothesis ¬mLift (A∩B)ᶜ (A∩B). Symmetric for B.

theorem Core.Scale.mLift_V3 {W : Type u_2} (ge_w : W → W → Prop) : patternV3 (mLift ge_w)

theorem Core.Scale.mLift_V4 {W : Type u_2} (ge_w : W → W → Prop) : patternV4 (mLift ge_w)

theorem Core.Scale.mLift_V5 {W : Type u_2} (ge_w : W → W → Prop) (hRefl : ∀ (w : W), ge_w w w) : patternV5 (mLift ge_w)

theorem Core.Scale.mLift_V6 {W : Type u_2} [Nonempty W] (ge_w : W → W → Prop) : patternV6 (mLift ge_w)

theorem Core.Scale.mLift_V7 {W : Type u_2} (ge_w : W → W → Prop) : patternV7 (mLift ge_w)

theorem Core.Scale.mLift_V12 {W : Type u_2} [Finite W] (ge_w : W → W → Prop) (hRefl : ∀ (w : W), ge_w w w) (hTrans : ∀ (u v w : W), ge_w u v → ge_w v w → ge_w u w) : patternV12 (mLift ge_w)

V12 is valid for the m-lifting on finite posets (Fact 5 in @cite{holliday-icard-2013}; proof via @cite{harrison-trainor-holliday-icard-2018}, Lemma 3.7). The proof decomposes into complement reversal (mLift ge_w B A → mLift ge_w Aᶜ Bᶜ) and two applications of mLift transitivity: B ≿ A ≿ Aᶜ ≿ Bᶜ.

theorem Core.Scale.mLift_V11 {W : Type u_2} [Finite W] (ge_w : W → W → Prop) (hRefl : ∀ (w : W), ge_w w w) (hTrans : ∀ (u v w : W), ge_w u v → ge_w v w → ge_w u w) : patternV11 (mLift ge_w)

V11 is valid for the m-lifting on finite posets (Fact 5 in @cite{holliday-icard-2013}). The ge half follows from V12; the strict half uses complement reversal + transitivity to derive a contradiction with the "probably A" hypothesis.

theorem Core.Scale.mLift_V13 {W : Type u_2} [Finite W] (ge_w : W → W → Prop) (_hRefl : ∀ (w : W), ge_w w w) : patternV13 (mLift ge_w)

V13 is valid for the m-lifting on finite posets (Fact 5 in @cite{holliday-icard-2013}). The ge half uses id on B (reflexivity); the strict half uses pigeonhole (|A∪B| > |B| since A\B nonempty, finiteness).

theorem Core.Scale.mLift_not_I1 : ∃ (W : Type) (ge_w : W → W → Prop), (∀ (w : W), ge_w w w) ∧ ¬patternI1 (mLift ge_w)

I1 is invalid for the m-lifting (Fact 5 in @cite{holliday-icard-2013}). Counterexample: W = Fin 2, ge_w total. A = {0}, B = {0}, C = {1}. mLift A B and mLift A C both hold (singleton ↪ singleton), but ¬mLift A (B ∪ C) since |A| = 1 < 2 = |B ∪ C| (no injection).

theorem Core.Scale.mLift_not_I2 : ∃ (W : Type) (ge_w : W → W → Prop), (∀ (w : W), ge_w w w) ∧ ¬patternI2 (mLift ge_w)

I2 is invalid for the m-lifting (Fact 5 in @cite{holliday-icard-2013}). Counterexample: W = Fin 3, ge_w total. A = {0,1}, B = univ. mLift A Aᶜ holds (|Aᶜ| = 1 ≤ 2 = |A|), but ¬mLift A univ since |A| = 2 < 3 = |univ|.

theorem Core.Scale.mLift_not_I3 : ∃ (W : Type) (ge_w : W → W → Prop), (∀ (w : W), ge_w w w) ∧ ¬patternI3 (mLift ge_w)

I3 is invalid for the m-lifting (Fact 5 in @cite{holliday-icard-2013}). Same counterexample as I2: W = Fin 3, ge_w total, A = {0,1}, B = univ. A ≿ Aᶜ (injection {2} → {0,1}) and ¬(Aᶜ ≿ A) (no injection {0,1} → {2}), so probably A. But ¬(A ≿ univ) by cardinality.

theorem Core.Scale.mLift_not_total : ∃ (W : Type) (ge_w : W → W → Prop), (∀ (w : W), ge_w w w) ∧ (∀ (u v w : W), ge_w u v → ge_w v w → ge_w u w) ∧ (∀ (u v : W), ge_w u v ∨ ge_w v u) ∧ ∃ (A : Set W) (B : Set W), ¬mLift ge_w A B ∧ ¬mLift ge_w B A

The m-lifting is NOT total, even for total preorders on worlds. Counterexample: W = Fin 4, ge_w = (· ≥ ·), A = {3, 0}, B = {2, 1}. Neither A ≿ⁱ B (only 3 dominates 2, leaving nothing for 1) nor B ≿ⁱ A (nothing in B dominates 3).

def Core.Scale.mLift_toGFCPreorder {W : Type u_2} [Finite W] (ge_w : W → W → Prop) (hRefl : ∀ (w : W), ge_w w w) (hTrans : ∀ (u v w : W), ge_w u v → ge_w v w → ge_w u w) : GFCPreorder W

The m-lifting of a reflexive, transitive world ordering on finite W is a GFC preorder (@cite{harrison-trainor-holliday-icard-2018}, Theorem 3.2).

This is the key structural result connecting world-ordering semantics to the axiomatic hierarchy: the injection extension ≿ⁱ (= mLift) satisfies all three GFC axiom groups — preorder (G), monotonicity (F), and complement reversal (C).

Equations

• Core.Scale.mLift_toGFCPreorder ge_w hRefl hTrans = { ge := Core.Scale.mLift ge_w, refl := ⋯, trans := ⋯, mono := ⋯, complRev := ⋯ }