Framework Comparison: Where Kennedy and Heim Diverge

@cite{heim-2001} @cite{kennedy-2007} @cite{klein-1980} @cite{schwarzschild-2008}

Formal comparison of the degree semantic frameworks on shared empirical ground. By implementing all frameworks with the same type signatures, we can formally state where they agree and where they diverge.

Agreement

All degree-based frameworks agree on the truth conditions of simple comparatives: "A is taller than B" iff μ(A) > μ(B). Klein's degree-free framework agrees under the natural correspondence between delineation functions and measure functions.

Divergences

Question	Kennedy	Heim	Klein	Schwarzschild
Degrees in ontology?	Yes	Yes	No	Yes (intervals)
Scope of -er	DP	CP	N/A	DP
Measure phrases	Direct	Direct	Hard	Direct
Subcomparatives	Special	Special	Special	Natural

theorem Phenomena.Comparison.Comparative.Compare.heim_agrees {Entity : Type u_1} {D : Type u_2} [LinearOrder D] [BoundedOrder D] (μ : Entity → D) (a b : Entity) : Semantics.Degree.DegreeAbstraction.heimComparativeWithMeasure μ a b ↔ Semantics.Degree.Comparative.comparativeSem μ a b Core.Scale.ScalePolarity.positive

All degree-based frameworks agree on simple comparatives. Heim and Schwarzschild (intervals) both yield μ(A) > μ(B) for "A is taller than B" — the consensus comparativeSem at positive direction.

theorem Phenomena.Comparison.Comparative.Compare.schwarzschild_agrees {Entity : Type u_1} {D : Type u_2} [LinearOrder D] [BoundedOrder D] (μ : Entity → D) (a b : Entity) : Semantics.Degree.Intervals.intervalComparative μ a b ↔ Semantics.Degree.Comparative.comparativeSem μ a b Core.Scale.ScalePolarity.positive

Schwarzschild's interval comparative also agrees (reduces to point comparison on positive intervals).

theorem Phenomena.Comparison.Comparative.Compare.heim_extensional_scope_free {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (a b : Entity) : Semantics.Degree.Comparative.comparativeSem μ a b Core.Scale.ScalePolarity.positive = Semantics.Degree.DegreeAbstraction.heimComparativeWithMeasure μ a b

The key divergence between Kennedy and Heim is scope. Kennedy: -er is DP-internal → only narrow scope Heim: -er is sentential → wide scope available

We can't formalize the scope prediction directly (it's about LF movement), but we can state that Heim's denotation is extensionally equivalent to the consensus in scope-free contexts.

theorem Phenomena.Comparison.Comparative.Compare.klein_correspondence {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (a b : Entity) (delineation : Set Entity → Entity → Prop) (hdiscrim : μ a > μ b → ∃ (C : Set Entity), delineation C a ∧ ¬delineation C b) : Semantics.Degree.Comparative.comparativeSem μ a b Core.Scale.ScalePolarity.positive → Semantics.Comparison.Delineation.comparativeSem delineation a b

Klein's framework diverges fundamentally: it has no degrees at all. We cannot directly compare truth conditions because Klein's comparativeSem takes a delineation function, not a measure function.

However, under the natural correspondence — a delineation function that classifies entities as "tall in C" when they exceed some threshold determined by C — Klein's comparative follows from the degree-based analysis. If μ(a) > μ(b), then for the comparison class {a, b}, delineating at μ(b) puts a in the positive extension but not b.