Framework-Independent Comparative Semantics

@cite{hoeksema-1983} @cite{rett-2026} @cite{schwarzschild-2008} @cite{von-stechow-1984}

Comparative semantics shared across all degree frameworks: the basic comparativeSem and equativeSem functions, antonymy as scale reversal, DE-ness of than-clauses (NPI licensing), and boundary dependence.

This module was extracted from Theories/Semantics/Lexical/Adjective/Comparative.lean (which now re-exports from here). The framework-specific content (MAX, ambidirectionality, manner implicature) is in Degree/Frameworks/Rett.lean.

Key Results

1. comparativeSem: "A is taller than B" iff μ(A) > μ(B) (positive) or μ(A) < μ(B) (negative).
2. Antonymy as scale reversal: "A taller than B" ↔ "B shorter than A".
3. DE-ness of than-clauses: universal quantification over the standard domain is anti-monotone.

@[reducible, inline]

abbrev Semantics.Degree.Comparative.ScaleDirection : Type

Comparative direction reuses scale polarity from Core. positive: "taller" — MAX picks the highest degrees. negative: "shorter" — MAX picks the lowest degrees.

Equations

• Semantics.Degree.Comparative.ScaleDirection = Core.Scale.ScalePolarity

def Semantics.Degree.Comparative.comparativeSem {Entity : Type u_1} {α : Type u_2} [LinearOrder α] (μ : Entity → α) (a b : Entity) (dir : ScaleDirection) : Prop

Comparative semantics (@cite{rett-2026} / @cite{schwarzschild-2008}): "A is Adj-er than B" iff μ(a) exceeds μ(b) on the directed scale.

Equations

• Semantics.Degree.Comparative.comparativeSem μ a b Core.Scale.ScalePolarity.positive = (μ a > μ b)
• Semantics.Degree.Comparative.comparativeSem μ a b Core.Scale.ScalePolarity.negative = (μ a < μ b)

def Semantics.Degree.Comparative.equativeSem {Entity : Type u_1} {α : Type u_2} [LinearOrder α] (μ : Entity → α) (a b : Entity) (dir : ScaleDirection) : Prop

Equative semantics: "A is as Adj as B" iff μ(a) ≥ μ(b) on the directed scale.

Equations

• Semantics.Degree.Comparative.equativeSem μ a b Core.Scale.ScalePolarity.positive = (μ a ≥ μ b)
• Semantics.Degree.Comparative.equativeSem μ a b Core.Scale.ScalePolarity.negative = (μ a ≤ μ b)

theorem Semantics.Degree.Comparative.comparativeSem_eq_MAX {Entity : Type u_1} {α : Type u_2} [LinearOrder α] (μ : Entity → α) (a b : Entity) : comparativeSem μ a b Core.Scale.ScalePolarity.positive ↔ ∃ m ∈ Core.Scale.maxOnScale (fun (x1 x2 : α) => x1 > x2) {μ b}, μ a > m

MAX–direct bridge: the direct comparison μ(a) > μ(b) is equivalent to the MAX-based formulation.

theorem Semantics.Degree.Comparative.taller_shorter_antonymy {Entity : Type u_1} {α : Type u_2} [LinearOrder α] (μ : Entity → α) (a b : Entity) : comparativeSem μ a b Core.Scale.ScalePolarity.positive ↔ comparativeSem μ b a Core.Scale.ScalePolarity.negative

"A taller than B" ↔ "B shorter than A" — antonymy is argument swap plus direction reversal.

theorem Semantics.Degree.Comparative.equative_antonymy {Entity : Type u_1} {α : Type u_2} [LinearOrder α] (μ : Entity → α) (a b : Entity) : equativeSem μ a b Core.Scale.ScalePolarity.positive ↔ equativeSem μ b a Core.Scale.ScalePolarity.negative

Equative antonymy: "A as tall as B" ↔ "B as short as A".

theorem Semantics.Degree.Comparative.comparative_boundary {α : Type u_3} [LinearOrder α] (μ_a μ_b : α) : (∃ m ∈ Core.Scale.maxOnScale (fun (x1 x2 : α) => x1 ≥ x2) {d : α | d ≤ μ_b}, μ_a > m) ↔ μ_a > μ_b

The comparative depends only on the boundary μ_b.

theorem Semantics.Degree.Comparative.equative_boundary {α : Type u_3} [LinearOrder α] (μ_a μ_b : α) : (∃ m ∈ Core.Scale.maxOnScale (fun (x1 x2 : α) => x1 ≥ x2) {d : α | d ≤ μ_b}, μ_a ≥ m) ↔ μ_a ≥ μ_b

The equative depends only on the boundary μ_b.

theorem Semantics.Degree.Comparative.comparative_than_DE {α : Type u_3} (R : α → α → Prop) (μ_a : α) (D₁ D₂ : Set α) (h_sub : D₁ ⊆ D₂) (h : ∀ d ∈ D₂, R μ_a d) (d : α) : d ∈ D₁ → R μ_a d

The than-clause argument of a comparative is DE (@cite{hoeksema-1983}): universal quantification over a domain is anti-monotone in the domain.

structure Semantics.Degree.Comparative.MannerEffect : Type

Manner implicature triggered by EN in an ambidirectional construction. evaluative: the relation is noteworthy (large gap / early timing). atypical: the EN form is pragmatically marked (optional, stylistic).

• evaluative : Bool

  Does EN trigger an evaluative reading?

• atypical : Bool

  Is the EN form pragmatically marked (optional, stylistic)?

instance Semantics.Degree.Comparative.instDecidableEqMannerEffect : DecidableEq MannerEffect

Equations

• Semantics.Degree.Comparative.instDecidableEqMannerEffect = Semantics.Degree.Comparative.instDecidableEqMannerEffect.decEq

def Semantics.Degree.Comparative.instDecidableEqMannerEffect.decEq (x✝ x✝¹ : MannerEffect) : Decidable (x✝ = x✝¹)

Equations

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

instance Semantics.Degree.Comparative.instBEqMannerEffect : BEq MannerEffect

Equations

• Semantics.Degree.Comparative.instBEqMannerEffect = { beq := Semantics.Degree.Comparative.instBEqMannerEffect.beq }

def Semantics.Degree.Comparative.instBEqMannerEffect.beq : MannerEffect → MannerEffect → Bool

Equations

• Semantics.Degree.Comparative.instBEqMannerEffect.beq { evaluative := a, atypical := a_1 } { evaluative := b, atypical := b_1 } = (a == b && a_1 == b_1)
• Semantics.Degree.Comparative.instBEqMannerEffect.beq x✝¹ x✝ = false

instance Semantics.Degree.Comparative.instReprMannerEffect : Repr MannerEffect

Equations

• Semantics.Degree.Comparative.instReprMannerEffect = { reprPrec := Semantics.Degree.Comparative.instReprMannerEffect.repr }

def Semantics.Degree.Comparative.instReprMannerEffect.repr : MannerEffect → ℕ → Std.Format

Equations

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

def Semantics.Degree.Comparative.enEvaluativeEffect : MannerEffect

EN in ambidirectional constructions triggers evaluativity.

Equations

• Semantics.Degree.Comparative.enEvaluativeEffect = { evaluative := true, atypical := false }

theorem Semantics.Degree.Comparative.comparative_iff_posExt_ssubset {Entity : Type u_3} {D : Type u_4} [LinearOrder D] (μ : Entity → D) (a b : Entity) : comparativeSem μ a b Core.Scale.ScalePolarity.positive ↔ Core.Scale.posExt μ b ⊂ Core.Scale.posExt μ a

Comparative via extents: "A is taller than B" iff A's positive extent strictly contains B's. Bridges the point comparison to the algebraic posExt_ssubset_iff from Core.Scale.

def Semantics.Degree.Comparative.equativeViaExtent {Entity : Type u_3} {D : Type u_4} [Preorder D] (μ : Entity → D) (a b : Entity) : Prop

Equative via extents: "A is as tall as B" iff B's positive extent is a subset of A's.

Equations

• Semantics.Degree.Comparative.equativeViaExtent μ a b = (Core.Scale.posExt μ b ⊆ Core.Scale.posExt μ a)

theorem Semantics.Degree.Comparative.equativeViaExtent_iff {Entity : Type u_3} {D : Type u_4} [LinearOrder D] (μ : Entity → D) (a b : Entity) : equativeViaExtent μ a b ↔ μ a ≥ μ b

Equative-via-extents is equivalent to μ(a) ≥ μ(b).

theorem Semantics.Degree.Comparative.comparative_iff_negExt_ssubset {Entity : Type u_3} {D : Type u_4} [LinearOrder D] (μ : Entity → D) (a b : Entity) : comparativeSem μ a b Core.Scale.ScalePolarity.positive ↔ Core.Scale.negExt μ a ⊂ Core.Scale.negExt μ b

"A is taller than B" iff "B is shorter than A" — derived from the complementarity of positive and negative extents, not stipulated as a lexical property of antonym pairs.

This is @cite{kennedy-1999}'s central result: antonymy equivalence follows from the algebra of extents. Delegates to Core.Scale.antonymy_biconditional.