World-ordering semantics: the l-lifting as a comparative-probability model

[lewis-1973]'s comparative possibility lifts an ordering of worlds to an ordering of propositions (dominationLift); [holliday-icard-2013] (§5) take it as a semantics for comparative epistemic modals with complete logic WJR ([halpern-2003] Thm. 7.5.1). This file gives the model-theoretic content of that completeness: a monotone, transitive comparison relation is an l-lifting of some reflexive world relation iff it satisfies right-union (axiom J) and determination by singletons.

Main statements

• strict_dominationLift_iff — over a total world relation the strict lift is Lewis's ∃∀ clause.
• exists_dominationLift_repr, dominationLift_repr_iff — the WJR representation and its round trip.

theorem ComparativeProbability.strict_dominationLift_iff {α : Type u_1} {r : α → α → Prop} (hTotal : ∀ (a b : α), r a b ∨ r b a) (A B : Set α) : Strict (dominationLift r) A B ↔ ∃ a ∈ A, ∀ b ∈ B, r a b ∧ ¬r b a

Over a total relation, the strict l-lifting collapses to Lewis's ∃∀ comparative possibility: some A-point strictly dominates every B-point.

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

Theorem 2 ([halpern-2003], Thm. 7.5.1a; [holliday-icard-2013]): a monotone, transitive comparison relation satisfying 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 correspond to WJR's axioms evaluated on a single model, without formalizing the syntax or proof system.

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

theorem ComparativeProbability.dominationLift_repr_iff {W : Type u_1} [Fintype W] {ge : Set W → Set W → Prop} (hMono : ∀ (A B : Set W), A ⊆ B → ge B A) (hTran : ∀ (A B C : Set W), ge A B → ge B C → ge A C) : (∃ (ge_w : W → W → Prop), (∀ (w : W), ge_w w w) ∧ ∀ (A B : Set W), ge A B ↔ dominationLift ge_w A B) ↔ RightUnion ge ∧ DeterminedBySingletons ge

Round trip of exists_dominationLift_repr: a monotone, transitive comparison relation is representable by Lewis's l-lifting iff it satisfies right-union and determination by singletons — the model-theoretic form of soundness and completeness for WJR ([holliday-icard-2013]; [halpern-2003] Thm. 7.5.1). Soundness transfers dominationLift_rightUnion and dominationLift_determinedBySingletons across the representation.