KPS representation and completeness theorems

The top-level results of [HI13] / [KPS59]:

• ComparativeProbability.representable_of_card_lt_five — for |W| < 5, every FA model is representable by a finitely additive probability measure (FA = FP∞ below five worlds).
• ComparativeProbability.exists_nonrepresentable_of_five_le_card — for |W| ≥ 5, FA is strictly weaker than FP∞ (the KPS counterexample, padded with null atoms).
• ComparativeProbability.exists_qualAddMeasure_repr, exists_dominationLift_repr — qualitative completeness results ([vdH96]; [Hal03] Thm. 7.5.1a).
• ComparativeProbability.axiomA_iff_fa — Axiom A is equivalent to disjoint-union invariance (finite additivity).

theorem ComparativeProbability.representable_of_card_lt_five {W : Type u_1} [Fintype W] (sys : EpistemicSystemFA W) (hcard : Fintype.card W < 5) : Representable sys

Theorem 8a ([KPS59]; [HI13] Theorem 8): below five worlds every FA system is representable — FA and FP∞ coincide.

theorem ComparativeProbability.exists_nonrepresentable_of_five_le_card {W : Type u_1} [Fintype W] (hcard : 5 ≤ Fintype.card W) : ∃ (sys : EpistemicSystemFA W), ¬Representable sys

Theorem 8b ([KPS59] Theorem 8): at every cardinality ≥ 5 some FA system is non-representable, so FA is strictly weaker than FP∞.

theorem ComparativeProbability.exists_qualAddMeasure_repr {W : Type u_1} [Fintype W] (sys : EpistemicSystemFA W) : ∃ (m : QualAddMeasure ℚ W), ∀ (A B : Set W), sys.ge A B ↔ m.inducedGe A B

Theorem 6 completeness ([HI13], Theorem 6; [vdH96]): every FA system is representable by a qualitatively additive measure — the dominated-set count, affinely renormalised so μ(∅) = 0 and μ(Ω) = 1.

theorem ComparativeProbability.exists_dominationLift_repr {W : Type u_1} [Fintype W] (sys : EpistemicSystemW W) (hTran : ∀ (A B C : Set W), sys.ge A B → sys.ge B C → sys.ge A C) (hJ : RightUnion sys.ge) (hDS : DeterminedBySingletons sys.ge) : ∃ (ge_w : W → W → Prop) (_ : ∀ (w : W), ge_w w w), ∀ (A B : Set W), sys.ge A B ↔ dominationLift ge_w A B

Theorem 2 ([Hal03], Thm. 7.5.1a; [HI13]): an epistemic system satisfying R, T, Tran, J (right-union), and DS (determination by singletons) is representable by Lewis's l-lifting from a reflexive preorder on worlds.

The paper states this as a logic completeness theorem for WJR (K + BT + Tran + J + Mon + R). We prove the underlying per-model representation result, which is the model-theoretic core: the semantic hypotheses (R, T, Tran, J, DS) correspond to WJR's axioms evaluated on a single model, without formalizing the syntax or proof system.

Construction: ge_w u v := sys.ge {u} {v}.

theorem ComparativeProbability.axiomA_iff_fa {W : Type u_1} (ge : Set W → Set W → Prop) : (∀ (A B : Set W), ge A B ↔ ge (A \ B) (B \ A)) ↔ ∀ (A B C : Set W), (∀ x ∈ A, x ∉ C) → (∀ x ∈ B, x ∉ C) → (ge A B ↔ ge (A ∪ C) (B ∪ C))

Algebraic bridge: Axiom A and the finite additivity property of AdditiveScale are equivalent for any comparison on sets.