Epistemic Entailment Patterns ([HI13], Figure 1)

[HI13] [HTHI18] [Yal10] [Lew73b] [Hal03]

[HI13] Figure 1 lists 10 validity patterns (V1–V7, V11–V13) and 3 invalidity patterns (I1–I3) for epistemic comparatives. (V8–V10 are from [Yal10] 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 four 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": the l-lifting (due to [Lew73b]) 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). Completeness of the l-lifting logic is due to [Hal03].

Measure semantics (FP∞): I1–I3 counterexamples

Counterexample infrastructure: uniform measure on Fin 3 (μ {i} = 1/3).

theorem ComparativeProbability.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 ComparativeProbability.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 ComparativeProbability.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).

Qualitative additivity (FA)

theorem ComparativeProbability.fa_not_I1 : ∃ (W : Type) (sys : EpistemicSystemFA W), ¬patternI1 sys.ge

I1 is invalid for FA: every finitely additive measure induces an FA system via toSystemFA, so the measure counterexample transfers.

theorem ComparativeProbability.fa_not_I2 : ∃ (W : Type) (sys : EpistemicSystemFA W), ¬patternI2 sys.ge

I2 is invalid for FA.

theorem ComparativeProbability.fa_not_I3 : ∃ (W : Type) (sys : EpistemicSystemFA W), ¬patternI3 sys.ge

I3 is invalid for FA.

World-ordering semantics (l-lifting)

Recall: dominationLift is the l-lifting (due to [Lew73b]): dominationLift ge_w A B := ∀ b, b ∈ B → ∃ a, a ∈ A ∧ ge_w a b, i.e. every element of B is dominated by some element of A. The identifier dominationLift (defined in Defs) reflects [Hal03]'s completeness result; the lifting operation itself is due to [Lew73b].

The `V2`–`V7` proofs below (and their m-lift analogues) are deliberately
*not* routed through the abstract `patternV*_of` layer: the lifts validate
these patterns for **arbitrary** world relations, whereas the abstract route
would require reflexivity and transitivity of `ge_w` (the lift is monotone
only given reflexivity, transitive only given transitivity). The abstract
layer is consumed exactly where its hypotheses are genuinely needed
(`V11`/`V12` for the m-lift, via `matchingLift_isTrans` and
`matchingLift_isComplementReversing`). 

theorem ComparativeProbability.dominationLift_V1 {W : Type u_2} (ge_w : W → W → Prop) : patternV1 (dominationLift ge_w)

theorem ComparativeProbability.dominationLift_V2 {W : Type u_2} (ge_w : W → W → Prop) : patternV2 (dominationLift ge_w)

theorem ComparativeProbability.dominationLift_V3 {W : Type u_2} (ge_w : W → W → Prop) : patternV3 (dominationLift ge_w)

theorem ComparativeProbability.dominationLift_V4 {W : Type u_2} (ge_w : W → W → Prop) : patternV4 (dominationLift ge_w)

theorem ComparativeProbability.dominationLift_V5 {W : Type u_2} (ge_w : W → W → Prop) (hRefl : ∀ (w : W), ge_w w w) : patternV5 (dominationLift ge_w)

theorem ComparativeProbability.dominationLift_V6 {W : Type u_2} [Nonempty W] (ge_w : W → W → Prop) : patternV6 (dominationLift ge_w)

theorem ComparativeProbability.dominationLift_V7 {W : Type u_2} (ge_w : W → W → Prop) : patternV7 (dominationLift ge_w)

theorem ComparativeProbability.dominationLift_not_V11 : ∃ (W : Type) (ge_w : W → W → Prop), (∀ (w : W), ge_w w w) ∧ ¬patternV11 (dominationLift ge_w)

V11 is invalid for world-ordering semantics (Fact 1 in [HI13]). 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 ComparativeProbability.dominationLift_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 (dominationLift ge_w)

V12 is valid for world-ordering semantics with a preorder (Fact 1 in [HI13]). Requires transitivity for the case where y ∈ Bᶜ ∩ Aᶜ: chain through A via ge A Aᶜ, then through B via ge B A.

theorem ComparativeProbability.dominationLift_not_V13 : ∃ (W : Type) (ge_w : W → W → Prop), (∀ (w : W), ge_w w w) ∧ ¬patternV13 (dominationLift 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 ComparativeProbability.dominationLift_I1 {W : Type u_2} (ge_w : W → W → Prop) : patternI1 (dominationLift ge_w)

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

theorem ComparativeProbability.dominationLift_I2 {W : Type u_2} (ge_w : W → W → Prop) (hRefl : ∀ (w : W), ge_w w w) : patternI2 (dominationLift ge_w)

I2 is valid for world-ordering semantics.

theorem ComparativeProbability.dominationLift_I3 {W : Type u_2} (ge_w : W → W → Prop) (hRefl : ∀ (w : W), ge_w w w) : patternI3 (dominationLift ge_w)

I3 is valid for world-ordering semantics.

m-lifting ([HI13], Fact 5)

The m-lifting validates all 13 validity patterns V1–V13 and invalidates I1–I3 (Fact 5 in [HI13]). 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 (`matchingLift_complement_reversal`). 

theorem ComparativeProbability.matchingLift_implies_dominationLift {W : Type u_2} {ge_w : W → W → Prop} {A B : Set W} (h : matchingLift ge_w A B) : dominationLift 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 ComparativeProbability.matchingLift_V1 {W : Type u_2} (ge_w : W → W → Prop) : patternV1 (matchingLift ge_w)

theorem ComparativeProbability.matchingLift_V2 {W : Type u_2} (ge_w : W → W → Prop) : patternV2 (matchingLift 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 ¬matchingLift (A∩B)ᶜ (A∩B). Symmetric for B.

theorem ComparativeProbability.matchingLift_V3 {W : Type u_2} (ge_w : W → W → Prop) : patternV3 (matchingLift ge_w)

theorem ComparativeProbability.matchingLift_V4 {W : Type u_2} (ge_w : W → W → Prop) : patternV4 (matchingLift ge_w)

theorem ComparativeProbability.matchingLift_V5 {W : Type u_2} (ge_w : W → W → Prop) (hRefl : ∀ (w : W), ge_w w w) : patternV5 (matchingLift ge_w)

theorem ComparativeProbability.matchingLift_V6 {W : Type u_2} [Nonempty W] (ge_w : W → W → Prop) : patternV6 (matchingLift ge_w)

theorem ComparativeProbability.matchingLift_V7 {W : Type u_2} (ge_w : W → W → Prop) : patternV7 (matchingLift ge_w)

V11–V13 require [Finite W] and reflexivity (and V11/V12 additionally need transitivity). The paper ([HI13]) assumes a finite poset (W, ≥). The proofs of V11 and V12 follow the companion paper [HTHI18]: the injection extension ≥ⁱ (= matchingLift) is a GFC order, which implies V12 directly. The key lemma is complement reversal: matchingLift ge_w B A → matchingLift ge_w Aᶜ Bᶜ (via an f-chain construction on elements of A ∩ Bᶜ). V12 then follows from complement reversal plus two applications of matchingLift transitivity.

Helper: matchingLift transitivity

Helper lemmas for the f-chain construction

Complement reversal

V11/V12 from transitivity and complement reversal

The m-lifting of a reflexive, transitive world ordering on finite W is transitive (matchingLift_trans) and complement-reversing (matchingLift_complement_reversal); V11 and V12 then follow from the abstract patternV11_of/patternV12_of with those registered as local IsTrans/IsComplementReversing instances. The injection extension ≿ⁱ (= matchingLift) is moreover the genuine generalized-finite-cancellation order of [HTHI18] (ComparativeProbability.GFCOrder).

def ComparativeProbability.matchingLift_isTrans {W : Type u_2} [Finite W] (ge_w : W → W → Prop) (hTrans : ∀ (u v w : W), ge_w u v → ge_w v w → ge_w u w) : IsTrans (Set W) (matchingLift ge_w)

The m-lift's transitivity, packaged for the abstract pattern layer.

Equations

• ⋯ = ⋯

def ComparativeProbability.matchingLift_isComplementReversing {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) : IsComplementReversing (matchingLift ge_w)

The m-lift's complement reversal, packaged for the abstract pattern layer.

Equations

• ⋯ = ⋯

theorem ComparativeProbability.matchingLift_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 (matchingLift ge_w)

V12 is valid for the m-lifting on finite posets (Fact 5 in [HI13]): the m-lift is transitive and complement-reversing, so patternV12_of supplies the pattern.

theorem ComparativeProbability.matchingLift_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 (matchingLift ge_w)

V11 is valid for the m-lifting on finite posets (Fact 5 in [HI13]): immediate from patternV11_of.

theorem ComparativeProbability.matchingLift_V13 {W : Type u_2} [Finite W] (ge_w : W → W → Prop) (hRefl : ∀ (w : W), ge_w w w) : patternV13 (matchingLift ge_w)

V13 is valid for the m-lifting on finite posets (Fact 5 in [HI13]). The ge half uses id on B (reflexivity); the Strict half uses pigeonhole (|A∪B| > |B| since A\B nonempty, finiteness).

theorem ComparativeProbability.matchingLift_not_I1 : ∃ (W : Type) (ge_w : W → W → Prop), (∀ (w : W), ge_w w w) ∧ ¬patternI1 (matchingLift ge_w)

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

theorem ComparativeProbability.matchingLift_not_I2 : ∃ (W : Type) (ge_w : W → W → Prop), (∀ (w : W), ge_w w w) ∧ ¬patternI2 (matchingLift ge_w)

I2 is invalid for the m-lifting (Fact 5 in [HI13]). Counterexample: W = Fin 3, ge_w total. A = {0,1}, B = univ. matchingLift A Aᶜ holds (|Aᶜ| = 1 ≤ 2 = |A|), but ¬matchingLift A univ since |A| = 2 < 3 = |univ|.

theorem ComparativeProbability.matchingLift_not_I3 : ∃ (W : Type) (ge_w : W → W → Prop), (∀ (w : W), ge_w w w) ∧ ¬patternI3 (matchingLift ge_w)

I3 is invalid for the m-lifting (Fact 5 in [HI13]). 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.

Non-totality of the m-lifting

theorem ComparativeProbability.matchingLift_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), ¬matchingLift ge_w A B ∧ ¬matchingLift 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).