Holliday & Icard (2013): Measure semantics for epistemic comparatives

[HI13] ask which semantics for the epistemic comparative at least as likely as matches speakers' inference judgments. The benchmark is measure semantics: φ is at least as likely as ψ is true iff μ(φ) ≥ μ(ψ) for a probability measure μ over the worlds compatible with the relevant evidence.

The paper's argument, formalized on the Core/Scales/EpistemicScale substrate:

1. The disjunction problem (Fact 1). Kratzer-style world-ordering semantics — the l-lifting of a world order to propositions, due to [Lew73b] — validates the patterns I1–I3 that measure semantics refutes. I1 is the signature case: from φ ≿ ψ and φ ≿ χ it licenses φ ≿ ψ ∨ χ, predicting that a fair die's showing one is at least as likely as its showing an even number. (disjunction_problem, measures_refute_I_patterns)
2. The m-lifting repair (Fact 5). Requiring distinct dominating witnesses — an injection rather than a choice function — yields a lifting that agrees with measure semantics on every pattern in the paper's Figure 1. (mLift_validates_V11_V12_V13, mLift_refutes_I_patterns)
3. Completeness for qualitative additivity (Theorem 6; [vdH96]). The logic FA is sound and complete for qualitatively additive measures. (fa_qualAdd_complete)
4. FA vs. finite additivity (Theorem 8; [KPS59]). FA and the finitely-additive logic FP∞ coincide exactly below five worlds: the KPS ordering separates them at every |W| ≥ 5. (fa_representable_iff_card_lt_five)

See also [Yal10] for the inference-pattern inventory V1–V13/I1–I3 and [Hal03] for the l-lifting's completeness.

Fact 1: the disjunction problem

theorem HollidayIcard2013.disjunction_problem {W : Type u_1} (ge_w : W → W → Prop) (hRefl : ∀ (w : W), ge_w w w) : ComparativeProbability.patternI1 (ComparativeProbability.dominationLift ge_w) ∧ ComparativeProbability.patternI2 (ComparativeProbability.dominationLift ge_w) ∧ ComparativeProbability.patternI3 (ComparativeProbability.dominationLift ge_w)

Fact 1 (the disjunction problem): the l-lifting of any reflexive world order validates all three measure-invalid patterns I1–I3.

theorem HollidayIcard2013.measures_refute_I_patterns : (∃ (m : ComparativeProbability.FinAddMeasure ℚ (Fin 3)), ¬ComparativeProbability.patternI1 m.inducedGe) ∧ (∃ (m : ComparativeProbability.FinAddMeasure ℚ (Fin 3)), ¬ComparativeProbability.patternI2 m.inducedGe) ∧ ∃ (m : ComparativeProbability.FinAddMeasure ℚ (Fin 3)), ¬ComparativeProbability.patternI3 m.inducedGe

Measure semantics refutes each of I1–I3 (uniform measure on three worlds).

theorem HollidayIcard2013.lLift_refutes_V11_V13 : (∃ (W : Type) (ge_w : W → W → Prop), (∀ (w : W), ge_w w w) ∧ ¬ComparativeProbability.patternV11 (ComparativeProbability.dominationLift ge_w)) ∧ ∃ (W : Type) (ge_w : W → W → Prop), (∀ (w : W), ge_w w w) ∧ ¬ComparativeProbability.patternV13 (ComparativeProbability.dominationLift ge_w)

The l-lifting also misses two valid patterns: V11 and V13 fail.

Fact 5: the m-lifting matches measure semantics

theorem HollidayIcard2013.mLift_validates_V11_V12_V13 {W : Type u_1} [Finite W] (ge_w : W → W → Prop) (hRefl : ∀ (w : W), ge_w w w) (hTrans : ∀ (u v w : W), ge_w u v → ge_w v w → ge_w u w) : ComparativeProbability.patternV11 (ComparativeProbability.matchingLift ge_w) ∧ ComparativeProbability.patternV12 (ComparativeProbability.matchingLift ge_w) ∧ ComparativeProbability.patternV13 (ComparativeProbability.matchingLift ge_w)

Fact 5, validity half: on a finite preorder the m-lifting validates the distinctive patterns V11–V13 (V1–V7 hold for any world relation).

theorem HollidayIcard2013.mLift_refutes_I_patterns : (∃ (W : Type) (ge_w : W → W → Prop), (∀ (w : W), ge_w w w) ∧ ¬ComparativeProbability.patternI1 (ComparativeProbability.matchingLift ge_w)) ∧ (∃ (W : Type) (ge_w : W → W → Prop), (∀ (w : W), ge_w w w) ∧ ¬ComparativeProbability.patternI2 (ComparativeProbability.matchingLift ge_w)) ∧ ∃ (W : Type) (ge_w : W → W → Prop), (∀ (w : W), ge_w w w) ∧ ¬ComparativeProbability.patternI3 (ComparativeProbability.matchingLift ge_w)

Fact 5, invalidity half: the m-lifting refutes I1–I3, dissolving the disjunction problem.

Theorem 6: completeness for qualitatively additive measures

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

Theorem 6 ([vdH96]): every FA system is represented by a qualitatively additive measure.

Theorem 8: FA = FP∞ exactly below five worlds

theorem HollidayIcard2013.fa_representable_iff_card_lt_five (n : ℕ) : (∀ (sys : ComparativeProbability.EpistemicSystemFA (Fin n)), ComparativeProbability.Representable sys) ↔ n < 5

Theorem 8 ([KPS59]): every FA system on Fin n is representable by a finitely additive measure iff n < 5.