Framework-Independent Comparative Semantics

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

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

The set-of-degrees S-comparative sComparative (originally @cite{hoeksema-1983} §3.8 Def 7) lives here as the natural generalization of comparativeSem from a binary comparator to a degree-set comparator. Hoeksema's polarity-asymmetry consumers (Boolean-hom npComparativeGQ, the licensing-context registry connection) remain in Phenomena/Polarity/Studies/Hoeksema1983.lean.

Framework-specific content for Rett 2026 (MAX, ambidirectionality, manner implicature) lives in Phenomena/Negation/Studies/Rett2026.lean.

Key Results

1. comparativeSem: "A is taller than B" iff μ(A) > μ(B) (positive) or μ(A) < μ(B) (negative).
2. sComparative: degree-set generalization; anti-additive in the standard set (the algebraic source of S-comparative NPI licensing).
3. sComparative_eq_singleton_of_isGreatest: the S-comparative is determined by the supremum of its degree-set argument when one exists. Specializes to: a downward-closed than-clause denotation reduces to its maximum (@cite{bhatt-pancheva-2004} §3 reduction).
4. Antonymy as scale reversal: "A taller than B" ↔ "B shorter than A".
5. 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.

def Semantics.Degree.Comparative.sComparative {Entity : Type u_3} {D : Type u_4} [Preorder D] (μ : Entity → D) (Δ : Set D) : Set Entity

S-comparative on a set of degrees (@cite{hoeksema-1983} §3.8 Def 7): y ∈ sComparative μ Δ iff μ y strictly exceeds every degree in Δ. The than-clause supplies a set of degrees Δ (typically existentially closed). Generalizes the binary comparativeSem from a single standard to an arbitrary degree-set standard.

Equations

• Semantics.Degree.Comparative.sComparative μ Δ y = ∀ d ∈ Δ, d < μ y

theorem Semantics.Degree.Comparative.sComparative_isAntiAdditive {Entity : Type u_3} {D : Type u_4} [Preorder D] (μ : Entity → D) : Entailment.AntiAdditivity.IsAntiAdditive (sComparative μ)

@cite{hoeksema-1983} Fact 4: the S-comparative is anti-additive in its set-of-degrees argument. The algebraic source of NPI licensing in clausal than-comparatives.

theorem Semantics.Degree.Comparative.sComparative_atomic {Entity : Type u_3} {D : Type u_4} [Preorder D] (μ : Entity → D) (a b : Entity) : a ∈ sComparative μ {μ b} ↔ μ b < μ a

Atomic specialization: at the singleton {μ b}, S-comparative membership reduces to the binary "taller than b" relation. The bridge between the Hoeksema set-theoretic schema and the everyday μ b < μ a reading.

theorem Semantics.Degree.Comparative.sComparative_eq_singleton_of_isGreatest {Entity : Type u_3} {D : Type u_4} [Preorder D] (μ : Entity → D) {Δ : Set D} {m : D} (hm : IsGreatest Δ m) : sComparative μ Δ = sComparative μ {m}

Reduction lemma (@cite{bhatt-pancheva-2004} §3 in algebraic form): the S-comparative is determined by the greatest element of its degree-set argument. Passing a set whose supremum is m yields the same predicate as passing {m}.

The proof requires neither linearity nor density of the scale — only [Preorder D] and the IsGreatest witness. This is the generic order-theoretic content behind B&P's claim that the clausal-source than-clause denotation {d | d ≤ μ b} collapses to its maximum.

theorem Semantics.Degree.Comparative.sComparative_atomic_eq_comparativeSem {Entity : Type u_3} {α : Type u_4} [LinearOrder α] (μ : Entity → α) (a b : Entity) : a ∈ sComparative μ {μ b} ↔ comparativeSem μ a b Core.Scale.ScalePolarity.positive

Bridge: the atomic S-comparative coincides with the binary comparativeSem on a LinearOrder. The set-of-degrees schema is a strict generalization of the binary comparator.

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

Universal quantification over a domain is antitone in the domain. This is the generic monotonicity fact behind the surface observation that than-clauses are downward-entailing — not @cite{hoeksema-1983}'s specific anti-additivity / Boolean-homomorphism result, which is proved in Phenomena/Polarity/Studies/Hoeksema1983.lean.

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)?

@[implicit_reducible]

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.

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

Equations

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

@[implicit_reducible]

instance Semantics.Degree.Comparative.instReprMannerEffect : Repr MannerEffect

Equations

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

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.

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.

Strengthened, negated, and extent-theoretic equatives

@cite{kennedy-2007} @cite{rett-2020} @cite{schwarzschild-2008} @cite{thomas-deo-2020}

The literal semantics of the equative is "at least as" (equativeSem with .positive). The "exactly as" reading is derived by scalar implicature: choosing as tall as over the stronger taller than implicates that the comparative is false, yielding equality. A granularity-based alternative is in Degree.Granularity.

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

Equative strengthened semantics: "A is as tall as B" iff μ(A) = μ(B). The "exactly as" reading, derived by implicature.

Equations

• Semantics.Degree.Comparative.equativeStrengthened μ a b = (μ a = μ b)

theorem Semantics.Degree.Comparative.equativeStrengthened_entails_sem {Entity : Type u_3} {D : Type u_4} [LinearOrder D] (μ : Entity → D) (a b : Entity) (h : equativeStrengthened μ a b) : equativeSem μ a b Core.Scale.ScalePolarity.positive

The strengthened reading entails the literal ≥ reading.

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

Negated equative: "A is not as tall as B" iff μ(A) < μ(B).

Equations

• Semantics.Degree.Comparative.negatedEquative μ a b = (μ a < μ b)

theorem Semantics.Degree.Comparative.negatedEquative_iff_not_sem {Entity : Type u_3} {D : Type u_4} [LinearOrder D] (μ : Entity → D) (a b : Entity) : negatedEquative μ a b ↔ ¬equativeSem μ a b Core.Scale.ScalePolarity.positive

Negated equative is the negation of the literal equative.

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

Equative as positive extent inclusion (@cite{kennedy-1999}): "A is as tall as B" iff posExt(B) ⊆ posExt(A) — every degree B has, A also has.

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

Negated equative as strict extent inclusion: B has strictly more degrees than A.