Epistemic Comparative Likelihood — Main Theorems

@cite{holliday-icard-2013} @cite{halpern-2003} @cite{kraft-pratt-seidenberg-1959} @cite{van-der-hoek-1996}

Re-exports EpistemicScale.Defs (axioms, structures, semantics), EpistemicScale.Representability (KPS counterexample, Fin 0–3 proofs), and EpistemicScale.Cancellation88 (Fin 4 via Scott cancellation), then states the top-level KPS theorems (8a, 8b) and completeness results.

theorem Core.Scale.theorem8a {W : Type u_1} [Fintype W] (sys : EpistemicSystemFA W) (hcard : Fintype.card W < 5) : ∃ (m : FinAddMeasure W), ∀ (A B : Set W), sys.ge A B ↔ m.inducedGe A B

Theorem 8a: for |W| < 5, every FA model is representable by a finitely additive probability measure. Below 5 worlds, the logics FA and FP∞ coincide.

The proof transfers an arbitrary Fintype W to Fin n via Fintype.equivFin, applies the per-cardinality proof for n ∈ {0,1,2,3,4}, and transports the resulting measure back.

theorem Core.Scale.theorem8b : ∃ (W : Type) (x : Fintype W) (sys : EpistemicSystemFA W), Fintype.card W = 5 ∧ ¬∃ (m : FinAddMeasure W), ∀ (A B : Set W), sys.ge A B ↔ m.inducedGe A B

Theorem 8b: for |W| ≥ 5, FA is strictly weaker than FP∞ — there exists a 5-element type with an FA ordering admitting no finitely additive measure representation.

theorem Core.Scale.theorem6_completeness {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 (@cite{holliday-icard-2013}, Theorem 6; @cite{van-der-hoek-1996}): every EpistemicSystemFA is representable by a qualitatively additive measure.

Construction: define μ(A) = |{S : Finset W | ge A S}| / 2^|W|. Totality + transitivity of ge ensure μ A ≥ μ B ↔ ge A B; qualitative additivity then follows from Axiom A.

theorem Core.Scale.theorem2_completeness {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 : EpistemicAxiom.J sys.ge) (hDS : EpistemicAxiom.DS sys.ge) : ∃ (ge_w : W → W → Prop) (_ : ∀ (w : W), ge_w w w), ∀ (A B : Set W), sys.ge A B ↔ halpernLift ge_w A B

Theorem 2 (@cite{halpern-2003}, Thm. 7.5.1a; @cite{holliday-icard-2013}): 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 Core.Scale.axiomA_iff_fa {W : Type u_1} (ge : Set W → Set W → Prop) : EpistemicAxiom.A ge ↔ ∀ (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.

inductive Core.Scale.EpistemicTag : Type

Binary epistemic classification, parallel to MereoTag.

• finitelyAdditive : EpistemicTag
• qualitative : EpistemicTag

instance Core.Scale.instDecidableEqEpistemicTag : DecidableEq EpistemicTag

Equations

• Core.Scale.instDecidableEqEpistemicTag x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Core.Scale.instBEqEpistemicTag : BEq EpistemicTag

Equations

• Core.Scale.instBEqEpistemicTag = { beq := Core.Scale.instBEqEpistemicTag.beq }

def Core.Scale.instBEqEpistemicTag.beq : EpistemicTag → EpistemicTag → Bool

Equations

• Core.Scale.instBEqEpistemicTag.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Core.Scale.instReprEpistemicTag : Repr EpistemicTag

Equations

• Core.Scale.instReprEpistemicTag = { reprPrec := Core.Scale.instReprEpistemicTag.repr }

def Core.Scale.instReprEpistemicTag.repr : EpistemicTag → ℕ → Std.Format

Equations

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

instance Core.Scale.instLicensingPipelineEpistemicTag : LicensingPipeline EpistemicTag

Equations

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

theorem Core.Scale.epistemicFA_licensed : LicensingPipeline.isLicensed EpistemicTag.finitelyAdditive = true

theorem Core.Scale.epistemicQualitative_blocked : LicensingPipeline.isLicensed EpistemicTag.qualitative = false

theorem Core.Scale.five_frameworks_agree (m : MereoTag) (e : EpistemicTag) (h : LicensingPipeline.toBoundedness m = LicensingPipeline.toBoundedness e) : LicensingPipeline.isLicensed m = LicensingPipeline.isLicensed e

theorem Core.Scale.epistemicFA_eq_qua : LicensingPipeline.isLicensed EpistemicTag.finitelyAdditive = LicensingPipeline.isLicensed MereoTag.qua

theorem Core.Scale.epistemicQualitative_eq_cum : LicensingPipeline.isLicensed EpistemicTag.qualitative = LicensingPipeline.isLicensed MereoTag.cum