Representability of Epistemic Systems

@cite{kraft-pratt-seidenberg-1959} @cite{holliday-icard-2013}

FA systems on small domains (|W| ≤ 4) are representable by finitely additive probability measures (Theorem 8a, @cite{kraft-pratt-seidenberg-1959}). For |W| ≥ 5, this fails: the KPS counterexample provides an FA system with no representing measure (Theorem 8b).

Contents

1. KPS counterexample (Fin 5): non-representable FA system (kpsSystemFA, kps_not_representable)
2. Shared infrastructure: null element reduction (null_elem_reduce), transport/permutation (transportFA, perm_repr)
3. Per-cardinality proofs: Fin 0 (no_fa_empty), Fin 1 (theorem8a_fin1), Fin 2 (theorem8a_fin2), Fin 3 (theorem8a_fin3)

noncomputable def Core.Scale.kpsSystemFA : EpistemicSystemFA (Fin 5)

Equations

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

theorem Core.Scale.kps_not_representable : ¬∃ (m : FinAddMeasure (Fin 5)), ∀ (A B : Set (Fin 5)), kpsSystemFA.ge A B ↔ m.inducedGe A B

theorem Core.Scale.measure_axiomA {W : Type u_1} (m : FinAddMeasure W) (A B : Set W) : m.inducedGe A B ↔ m.inducedGe (A \ B) (B \ A)

theorem Core.Scale.reduce_to_disjoint {W : Type u_1} (sys : EpistemicSystemFA W) (m : FinAddMeasure W) (h : ∀ (C D : Set W), (∀ x ∈ C, x ∉ D) → (sys.ge C D ↔ m.inducedGe C D)) (A B : Set W) : sys.ge A B ↔ m.inducedGe A B

theorem Core.Scale.null_removal_disjoint {W : Type u_1} (sys : EpistemicSystemFA W) (j : W) (hj : sys.ge ∅ {j}) (C D : Set W) (hdisj : ∀ x ∈ C, x ∉ D) : sys.ge C D ↔ sys.ge (C \ {j}) (D \ {j})

Removing a null element from both sides of a disjoint comparison preserves ge. When sys.ge ∅ {j} (j is null) and C, D are disjoint, sys.ge C D ↔ sys.ge (C\{j}) (D\{j}).

theorem Core.Scale.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))), ∃ (m : FinAddMeasure (Fin (n + 1))), ∀ (A B : Set (Fin (n + 1))), sys'.ge A B ↔ m.inducedGe A B) : ∃ (m : FinAddMeasure (Fin (n + 2))), ∀ (A B : Set (Fin (n + 2))), sys.ge A B ↔ m.inducedGe A B

Null element reduction: if element 0 is null in an FA system on Fin (n+2), reduce to Fin (n+1) via Fin.succ and delegate to a sub-theorem.

theorem Core.Scale.no_fa_empty (sys : EpistemicSystemFA (Fin 0)) : False

theorem Core.Scale.theorem8a_fin1 (sys : EpistemicSystemFA (Fin 1)) : ∃ (m : FinAddMeasure (Fin 1)), ∀ (A B : Set (Fin 1)), sys.ge A B ↔ m.inducedGe A B

theorem Core.Scale.theorem8a_fin2 (sys : EpistemicSystemFA (Fin 2)) : ∃ (m : FinAddMeasure (Fin 2)), ∀ (A B : Set (Fin 2)), sys.ge A B ↔ m.inducedGe A B

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

Equations

• Core.Scale.transportFA e sys = { ge := fun (A B : Set α) => sys.ge (⇑e.symm '' A) (⇑e.symm '' B), refl := ⋯, mono := ⋯, bottom := ⋯, nonTrivial := ⋯, total := ⋯, trans := ⋯, additive := ⋯ }

noncomputable def Core.Scale.transportMeasure {W : Type u_1} {α : Type u_2} (e : W ≃ α) (m : FinAddMeasure α) : FinAddMeasure W

Equations

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

theorem Core.Scale.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 Core.Scale.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 Core.Scale.perm_null_convert {n : ℕ} (σ : Fin n ≃ Fin n) (sys : EpistemicSystemFA (Fin n)) (j k : Fin n) (hk : σ.symm j = k) : (transportFA σ sys).ge ∅ {j} ↔ sys.ge ∅ {k}

Concrete null pattern conversion: if σ.symm j = k then null-at-j in transported system iff null-at-k in original.

theorem Core.Scale.perm_repr {n : ℕ} (σ : Fin n ≃ Fin n) (sys : EpistemicSystemFA (Fin n)) (h : ∃ (m : FinAddMeasure (Fin n)), ∀ (A B : Set (Fin n)), (transportFA σ sys).ge A B ↔ m.inducedGe A B) : ∃ (m : FinAddMeasure (Fin n)), ∀ (A B : Set (Fin n)), sys.ge A B ↔ m.inducedGe A B

Permutation transport for representability: if transportFA σ sys is representable, then so is sys.

theorem Core.Scale.perm_singleton_iff {n : ℕ} (σ : Fin n ≃ Fin n) (sys : EpistemicSystemFA (Fin n)) (i j : Fin n) : (transportFA σ sys).ge {i} {j} ↔ sys.ge {σ.symm i} {σ.symm j}

theorem Core.Scale.theorem8a_fin3 (sys : EpistemicSystemFA (Fin 3)) : ∃ (m : FinAddMeasure (Fin 3)), ∀ (A B : Set (Fin 3)), sys.ge A B ↔ m.inducedGe A B