Representability of Epistemic Systems

[KPS59] [HI13]

FA systems on small domains (|W| ≤ 4) are representable by finitely additive probability measures (Theorem 8a, [KPS59]). For every |W| ≥ 5 this fails: padding the KPS counterexample with null atoms gives a non-representable FA system at each cardinality (Theorem 8b).

Contents

1. Representable: the representability predicate.
2. KPS counterexample (Fin 5): non-representable FA system (kpsSystemFA, kps_not_representable); null-atom padding (padFA, exists_nonrepresentable_fin) extends it to every Fin n with n ≥ 5.
3. Shared infrastructure: injection pullback (comapFA), null element reduction (null_elem_reduce), transport/permutation (transportFA, perm_repr)
4. Small-cardinality proofs: Fin 0 (no_fa_empty), Fin 1 (representable_fin1), Fin 2 (representable_fin2). Fin 3 and Fin 4 are derived from Scott cancellation in CancellationFin4.lean (representable_fin3, representable_fin4).

def ComparativeProbability.Representable {W : Type u_1} (sys : EpistemicSystemFA W) : Prop

An FA system is representable when some finitely additive probability measure induces exactly its comparison relation.

Equations

• ComparativeProbability.Representable sys = ∃ (m : ComparativeProbability.FinAddMeasure ℚ W), ∀ (A B : Set W), sys.ge A B ↔ m.inducedGe A B

noncomputable def ComparativeProbability.kpsSystemFA : EpistemicSystemFA (Fin 5)

Equations

• One or more equations did not get rendered due to their size.

theorem ComparativeProbability.kps_not_representable : ¬Representable kpsSystemFA

theorem ComparativeProbability.reduce_to_disjoint {W : Type u_1} (sys : EpistemicSystemFA W) (m : FinAddMeasure ℚ W) (h : ∀ (C D : Set W), Disjoint C D → (sys.ge C D ↔ m.inducedGe C D)) (A B : Set W) : sys.ge A B ↔ m.inducedGe A B

Agreement on disjoint pairs suffices for full representability (Axiom A reduces every comparison to a disjoint one).

theorem ComparativeProbability.null_removal_disjoint {W : Type u_1} (sys : EpistemicSystemFA W) (j : W) (hj : sys.ge ∅ {j}) (C D : Set W) (hdisj : Disjoint C D) : sys.ge C D ↔ sys.ge (C \ {j}) (D \ {j})

Removing a null element (sys.ge ∅ {j}) from both sides of a disjoint comparison preserves ge.

def ComparativeProbability.comapFA {α : Type u_1} {W : Type u_2} (f : α → W) (hf : Function.Injective f) (sys : EpistemicSystemFA W) (hnt : ¬sys.ge ∅ (Set.range f)) : EpistemicSystemFA α

Pull back an FA system along an injection: α-propositions compare via their images. Non-triviality requires a witness and must be supplied.

Equations

• ComparativeProbability.comapFA f hf sys hnt = { ge := fun (A B : Set α) => sys.ge (f '' A) (f '' B), refl := ⋯, mono := ⋯, bottom := ⋯, nonTrivial := ⋯, total := ⋯, trans := ⋯, additive := ⋯ }

theorem ComparativeProbability.null_elem_reduce {n : ℕ} (sys : EpistemicSystemFA (Fin (n + 2))) (hn0 : sys.ge ∅ {0}) (hnn : ∃ (i : Fin (n + 1)), ¬sys.ge ∅ {i.succ}) (sub_repr : ∀ (sys' : EpistemicSystemFA (Fin (n + 1))), Representable sys') : Representable sys

Null element reduction: if atom 0 is null in an FA system on Fin (n+2) and some atom is not, representability reduces along Fin.succ to Fin (n+1).

theorem ComparativeProbability.no_fa_empty (sys : EpistemicSystemFA (Fin 0)) : False

theorem ComparativeProbability.representable_fin1 (sys : EpistemicSystemFA (Fin 1)) : Representable sys

theorem ComparativeProbability.representable_fin2 (sys : EpistemicSystemFA (Fin 2)) : Representable sys

def ComparativeProbability.transportFA {W : Type u_1} {α : Type u_2} (e : W ≃ α) (sys : EpistemicSystemFA W) : EpistemicSystemFA α

Equations

• ComparativeProbability.transportFA e sys = ComparativeProbability.comapFA ⇑e.symm ⋯ sys ⋯

def ComparativeProbability.transportMeasure {W : Type u_1} {α : Type u_2} (e : W ≃ α) (m : FinAddMeasure ℚ α) : FinAddMeasure ℚ W

Equations

• ComparativeProbability.transportMeasure e m = { mu := fun (A : Set W) => m.mu (⇑e '' A), nonneg := ⋯, additive := ⋯, total := ⋯ }

theorem ComparativeProbability.transfer_repr {W : Type u_1} {α : Type u_2} (e : W ≃ α) (sys : EpistemicSystemFA W) (m : FinAddMeasure ℚ α) (hm : ∀ (A B : Set α), (transportFA e sys).ge A B ↔ m.inducedGe A B) (A B : Set W) : sys.ge A B ↔ (transportMeasure e m).inducedGe A B

theorem ComparativeProbability.perm_null_iff {n : ℕ} (σ : Fin n ≃ Fin n) (sys : EpistemicSystemFA (Fin n)) (j : Fin n) : (transportFA σ sys).ge ∅ {j} ↔ sys.ge ∅ {σ.symm j}

Null pattern transport: j is null in transportFA σ sys iff σ.symm j is null in sys.

theorem ComparativeProbability.perm_repr {W : Type u_1} {α : Type u_2} (σ : W ≃ α) (sys : EpistemicSystemFA W) (h : Representable (transportFA σ sys)) : Representable sys

Representability transports backward along any equivalence.

def ComparativeProbability.padFA {n : ℕ} (sys : EpistemicSystemFA (Fin n)) : EpistemicSystemFA (Fin (n + 1))

Pad an FA system with one null atom: comparisons on Fin (n + 1) are decided by the preimage restriction to the first n atoms.

Equations

• One or more equations did not get rendered due to their size.

theorem ComparativeProbability.padFA_last_null {n : ℕ} (sys : EpistemicSystemFA (Fin n)) : (padFA sys).ge ∅ {Fin.last n}

The padded atom is null.

theorem ComparativeProbability.representable_of_padFA {n : ℕ} {sys : EpistemicSystemFA (Fin n)} (h : Representable (padFA sys)) : Representable sys

Padding reflects representability: a measure for padFA sys assigns the padded atom measure zero, so its Fin.castSucc-image restriction represents sys.

theorem ComparativeProbability.exists_nonrepresentable_fin {n : ℕ} (h : 5 ≤ n) : ∃ (sys : EpistemicSystemFA (Fin n)), ¬Representable sys

Theorem 8b at every cardinality: for n ≥ 5 there is a non-representable FA system on Fin n — the KPS counterexample, padded with null atoms.