Kratzer–Epistemic–RSA Bridge

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

This file traces the dependency chain from Kratzer's ordering source semantics down to RSA's worldPrior, via @cite{holliday-icard-2013} epistemic likelihood logics:

Kratzer ordering source A : List (BProp World)
    ↓ atLeastAsGoodAs (subset inclusion on satisfied propositions)
World preorder ge_w : World → World → Prop
    ↓ halpernLift (Lewis's l-lifting)
EpistemicSystemW
    ↓ + totality, transitivity, additivity
EpistemicSystemFA
    ↓ theorem8a (|World4| = 4 < 5, so FA = FP∞)
FinAddMeasure
    ↓ mu {w} → worldPrior
RSAConfig.worldPrior

An alternative, more direct path is provided by @cite{fagin-halpern-1994}'s KripkeKP (see Modality/KnowledgeProbability.lean): a Kripke probability structure packages both the accessibility relation and the probability assignment. Under CONS, knowledge and probability-1 belief coincide (knows_implies_prob_one), giving a single structure that serves both the epistemic logic layer and the RSA prior.

§1 and §2 are definitions (no sorry). §3–§4 are conjectures (sorry) that state what additional conditions are needed to traverse the full pipeline.

def Comparisons.KratzerEpistemicRSA.kratzerWorldGe (A : List (BProp Semantics.Attitudes.Intensional.World)) (w z : Semantics.Attitudes.Intensional.World) : Prop

Convert Kratzer's Bool-valued atLeastAsGoodAs to a Prop-valued world preorder, suitable for halpernLift.

Equations

• Comparisons.KratzerEpistemicRSA.kratzerWorldGe A w z = ((w ≤[A] z) = true)

theorem Comparisons.KratzerEpistemicRSA.kratzerWorldGe_refl (A : List (BProp Semantics.Attitudes.Intensional.World)) (w : Semantics.Attitudes.Intensional.World) : kratzerWorldGe A w w

Kratzer's ordering is reflexive (Prop version).

def Comparisons.KratzerEpistemicRSA.kratzerToSystemW (A : List (BProp Semantics.Attitudes.Intensional.World)) : Core.Scale.EpistemicSystemW Semantics.Attitudes.Intensional.World

Applying Lewis's l-lifting to Kratzer's world ordering yields EpistemicSystemW. This connects Kratzer modal semantics to Holliday & Icard's weakest epistemic likelihood logic.

Equations

• Comparisons.KratzerEpistemicRSA.kratzerToSystemW A = Core.Scale.halpernSystemW (Comparisons.KratzerEpistemicRSA.kratzerWorldGe A) ⋯

theorem Comparisons.KratzerEpistemicRSA.kratzer_to_rsa_prior (A : List (BProp Semantics.Attitudes.Intensional.World)) (hFA : ∀ (A' B' : Set Semantics.Attitudes.Intensional.World), (kratzerToSystemW A).ge A' B' ∨ (kratzerToSystemW A).ge B' A') (hTrans : ∀ (A' B' C' : Set Semantics.Attitudes.Intensional.World), (kratzerToSystemW A).ge A' B' → (kratzerToSystemW A).ge B' C' → (kratzerToSystemW A).ge A' C') (hAdd : Core.Scale.EpistemicAxiom.A (kratzerToSystemW A).ge) (hBT : Core.Scale.EpistemicAxiom.BT (kratzerToSystemW A).ge) : ∃ (prior : Semantics.Attitudes.Intensional.World → ℚ), ∀ (w : Semantics.Attitudes.Intensional.World), 0 ≤ prior w

Conjecture: For World (= World4, 4 elements), if a Kratzer ordering source induces an l-lifted system that satisfies the FA axioms (totality, transitivity, qualitative additivity), then by Kraft–Pratt–Seidenberg (Theorem 8a, since |World4| = 4 < 5), the system is representable by a finitely additive measure, yielding an RSA world prior.

This states the full Kratzer → RSA pipeline for the concrete 4-world type used throughout linglib's modal and RSA formalizations.

The key gap is that not every Kratzer ordering source yields an l-lifted system satisfying FA — the hypothesis hFA captures the additional conditions needed (totality, transitivity, additivity of the lifted relation).

theorem Comparisons.KratzerEpistemicRSA.prob_ordering_roundtrip (P : Semantics.Modality.ProbabilityOrdering.ProbAssignment) (w₀ : Semantics.Attitudes.Intensional.World) (hPos : ∀ (w : Semantics.Attitudes.Intensional.World), 0 < P w) (hFA : ∀ (A B : Set Semantics.Attitudes.Intensional.World), (kratzerToSystemW (Semantics.Modality.ProbabilityOrdering.probToOrdering P w₀)).ge A B ∨ (kratzerToSystemW (Semantics.Modality.ProbabilityOrdering.probToOrdering P w₀)).ge B A) : ∃ (prior : Semantics.Attitudes.Intensional.World → ℚ), (∀ (w : Semantics.Attitudes.Intensional.World), 0 ≤ prior w) ∧ ∀ (w z : Semantics.Attitudes.Intensional.World), P w ≥ P z → prior w ≥ prior z

Conjecture: The probability-ordering round-trip is consistent.

Starting from a probability assignment P:

1. probToOrdering P yields a Kratzer ordering source
2. atLeastAsGoodAs gives a world preorder
3. halpernLift gives an epistemic system
4. If FA holds, representation theorem gives measure μ
5. toWorldPrior extracts μ({w})

The round-trip prior μ({w}) should be consistent with the original P(w) — not necessarily equal (since the l-lifting and representation may lose information), but preserving the same ordering: P(w) ≥ P(z) ↔ μ({w}) ≥ μ({z}).

This conjecture makes precise what "consistent" means: the probability ordering is preserved through the pipeline.

Note: probToOrdering is world-independent (probToOrdering_const), so the choice of evaluation world w₀ is arbitrary.