Differential Comparative Semantics #

@cite{schwarzschild-2005} @cite{solt-2015} @cite{winter-2005}

Compositional semantics for measure phrase differentials in comparatives: "3 inches taller", "twice as tall as".

Measure Phrase Composition #

@cite{schwarzschild-2005}: measure phrases modify the degree argument of the comparative, specifying the gap between matrix and standard degrees.

"A is 3 inches taller than B" iff height(A) - height(B) = 3 inches

This requires a ratio scale (with a meaningful zero point and unit), not just an ordinal or interval scale. Hence "3 inches taller" ✓ but "*3 units more beautiful" ✗.

source

def Semantics.Degree.Differential.differentialComparative {Entity : Type u_1} {D : Type u_2} [Sub D] (μ : Entity → D) (a b : Entity) (diff : D) :

Prop

Differential comparative: "A is d-much Adj-er than B" iff the difference μ(A) - μ(B) = d.

Requires a type with subtraction (ring-like structure), not just ordering. This is what makes measure phrase differentials more restrictive than bare comparatives.

Equations

Semantics.Degree.Differential.differentialComparative μ a b diff = (μ a - μ b = diff)

Instances For

source

theorem Semantics.Degree.Differential.differential_positive_iff {Entity : Type u_1} (μ : Entity → ℚ) (a b : Entity) (diff : ℚ) (hdiff : 0 < diff) :

differentialComparative μ a b diff → μ b < μ a

The differential is positive iff the comparative holds. Stated on ℚ; generalizing requires ordered-group machinery ([AddCommGroup D] [LinearOrder D] [IsStrictOrderedAddMonoid D]) that mathlib's current taxonomy splits across multiple unbundled classes — see e.g. Mathlib/Algebra/Order/Field/Defs.lean for the analogous LinearOrderedField → Field + LinearOrder + IsStrictOrderedRing migration. Consumers (Intensional, VonStechow1984) instantiate at ℚ.

source

inductive Semantics.Degree.Differential.MeasurementLevel :

Type

Measurement level: what kind of scale an adjective's degrees live on. Measure phrase differentials require at least interval scale; factor phrases require ratio scale.

Instances For

source

@[implicit_reducible]

instance Semantics.Degree.Differential.instDecidableEqMeasurementLevel :

DecidableEq MeasurementLevel

Equations

Semantics.Degree.Differential.instDecidableEqMeasurementLevel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

@[implicit_reducible]

instance Semantics.Degree.Differential.instReprMeasurementLevel :

Repr MeasurementLevel

Equations

Semantics.Degree.Differential.instReprMeasurementLevel = { reprPrec := Semantics.Degree.Differential.instReprMeasurementLevel.repr }

source

def Semantics.Degree.Differential.instReprMeasurementLevel.repr :

MeasurementLevel → ℕ → Std.Format

Equations

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

Instances For

source

def Semantics.Degree.Differential.admitsMeasurePhrase :

MeasurementLevel → Bool

Does this measurement level admit measure phrase differentials?

Equations

Instances For

source

def Semantics.Degree.Differential.admitsFactorPhrase :

MeasurementLevel → Bool

Does this measurement level admit factor phrases ("twice as tall")?

Equations

Instances For

source

def Semantics.Degree.Differential.factorEquative {Entity : Type u_1} {D : Type u_2} [Mul D] (μ : Entity → D) (a b : Entity) (factor : D) :

Prop

Factor phrase equative: "A is n times as tall as B" iff μ(A) = n × μ(B). Requires ratio scale: a meaningful zero point.

Equations

Semantics.Degree.Differential.factorEquative μ a b factor = (μ a = factor * μ b)

Instances For

source

inductive Semantics.Degree.Differential.MeasurementLevelExt :

Type

Extensive measurement level: a ratio scale that additionally permits cross-dimensional comparison. Spatial extent is the canonical example: height, width, length, and depth all map onto the same underlying extensive scale (cm, inches, etc.), so "the ladder is shorter than the house is high" is meaningful.

@cite{buring-2007} (p. 2, footnote 2): "spatial extent is the only scale I know of that has measurements in different dimensions mapped onto it." This makes cross-polar nomalies possible — they require comparing two different measure functions on a shared scale.

Temperature (°C vs °F) has meaningful differences (interval) and no meaningful zero (not ratio). Beauty has only ordering (ordinal). Spatial extent has all three: ordering, differences, ratios, AND cross-dimensional commensurability.

Instances For

source

@[implicit_reducible]

instance Semantics.Degree.Differential.instDecidableEqMeasurementLevelExt :

DecidableEq MeasurementLevelExt

Equations

Semantics.Degree.Differential.instDecidableEqMeasurementLevelExt x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

@[implicit_reducible]

instance Semantics.Degree.Differential.instReprMeasurementLevelExt :

Repr MeasurementLevelExt

Equations

Semantics.Degree.Differential.instReprMeasurementLevelExt = { reprPrec := Semantics.Degree.Differential.instReprMeasurementLevelExt.repr }

source

def Semantics.Degree.Differential.instReprMeasurementLevelExt.repr :

MeasurementLevelExt → ℕ → Std.Format

Equations

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

Instances For

source

def Semantics.Degree.Differential.admitsSubcomparative :

MeasurementLevelExt → Bool

Cross-dimensional comparison (subcomparative) requires extensive commensurability. Two measure functions μ₁, μ₂ must share a common extensive unit for "μ₁(a) > μ₂(b)" to be meaningful.

This explains why "shorter than high" ✓ (both spatial extent), "??hotter than expensive" ✗ (temperature ≠ price).

Equations

Instances For

source

theorem Semantics.Degree.Differential.extensive_admits_measure :

admitsMeasurePhrase MeasurementLevel.ratio = true

Extensive scales admit everything lower scales do.

source

theorem Semantics.Degree.Differential.extensive_admits_factor :

admitsFactorPhrase MeasurementLevel.ratio = true

source

structure Semantics.Degree.Differential.SubcomparativeAdmissibilityDatum :