Framework-Independent Comparative Semantics

[Ret26] [Sch08f] [vS84] [Hoe83]

Comparative semantics shared across all degree frameworks: the binary comparativeSem / equativeSem, antonymy as scale reversal, and downward-entailingness of than-clauses. Both binary comparators are measure-pullback predications of the reified Core.Order.Comparison (over at a point standard, overSet at a set standard); comparativeSem_positive_eq_over makes that an identity. The set-of-degrees S-comparative ([Hoe83]) is Comparison.gt.overSet μ directly — there is no separate clausal-comparison definition; its properties are stated about overSet here (anti-additivity) and reuse the Comparison.overSet/over API for the rest. Framework-specific content for [Ret26] (MAX, ambidirectionality, manner implicature) lives in Studies/Rett2026.lean; [Hoe83]'s polarity-asymmetry consumers in Studies/Hoeksema1983.lean.

Main declarations

• comparativeSem / equativeSem — "A is Adj-er / as-Adj-as B" via a directed measure on a scale.
• gtOverSet_isAntiAdditive — the S-comparative Comparison.gt.overSet μ ([Hoe83]) is anti-additive in its standard: the algebraic source of than-clause NPI licensing.
• mem_gtOverSet_iff_subset_Iio — the set-of-degrees comparative as Set.Iio interval inclusion (strict mirror of mathlib's mem_upperBounds_iff_subset_Iic), collapsing to the binary comparator at a singleton via Comparison.overSet_singleton.
• gtOverSet_eq_singleton_of_isGreatest — a than-clause with a greatest degree reduces to that degree ([BP04], order-theoretic form).
• taller_shorter_antonymy — antonymy is argument swap plus direction reversal.
• comparative_iff_posExt_ssubset — comparison as extent inclusion ([Ken99]).

Scale direction

@[reducible, inline]

abbrev Degree.ScaleDirection : Type

Comparative direction reuses scale polarity from Core.Order. positive ("taller") makes MAX pick the highest degrees; negative ("shorter") the lowest.

Equations

• Degree.ScaleDirection = Core.Order.ScalePolarity

Comparative and equative semantics

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

Comparative semantics ([Ret26], [Sch08f]): "A is Adj-er than B" iff μ a exceeds μ b on the directed scale.

Equations

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

def Degree.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

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

theorem Degree.comparativeSem_positive_eq_over {Entity : Type u_1} {α : Type u_2} [LinearOrder α] (μ : Entity → α) (a b : Entity) : comparativeSem μ a b Core.Order.ScalePolarity.positive ↔ a ∈ Core.Order.Comparison.gt.over μ (μ b)

Grounding: the positive binary comparative is the strict-> point predication of Core.Order.Comparison at the standard μ b — not a reinvention.

theorem Degree.equativeSem_positive_eq_over {Entity : Type u_1} {α : Type u_2} [LinearOrder α] (μ : Entity → α) (a b : Entity) : equativeSem μ a b Core.Order.ScalePolarity.positive ↔ a ∈ Core.Order.Comparison.ge.over μ (μ b)

Grounding: the positive equative is the ≥ point predication of Core.Order.Comparison at the standard μ b.

theorem Degree.comparativeSem_eq_MAX {Entity : Type u_1} {α : Type u_2} [LinearOrder α] (μ : Entity → α) (a b : Entity) : comparativeSem μ a b Core.Order.ScalePolarity.positive ↔ ∃ m ∈ maxOnScale Core.Order.Comparison.gt {μ b}, μ a > m

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

Antonymy as scale reversal

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

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

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

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

Boundary dependence

theorem Degree.comparative_boundary {α : Type u_1} [LinearOrder α] (μ_a μ_b : α) : (∃ m ∈ maxOnScale Core.Order.Comparison.ge {d : α | d ≤ μ_b}, μ_a > m) ↔ μ_a > μ_b

The comparative depends only on the boundary μ_b.

theorem Degree.equative_boundary {α : Type u_1} [LinearOrder α] (μ_a μ_b : α) : (∃ m ∈ maxOnScale Core.Order.Comparison.ge {d : α | d ≤ μ_b}, μ_a ≥ m) ↔ μ_a ≥ μ_b

The equative depends only on the boundary μ_b.

Set-of-degrees comparative

The S-comparative ([Hoe83] §3.8 Def 7) generalizes comparativeSem from a single standard to an arbitrary degree-set standard. It is Comparison.gt.overSet μ (μ ⁻¹' strictUpperBounds Δ) — the strict-> set-standard predication of Core.Order.Comparison — not a separate definition; the binary comparator is its singleton case (Comparison.overSet_singleton). The properties below are stated about Comparison.gt.overSet μ directly. Needs only [Preorder D].

theorem Degree.mem_gtOverSet_iff_subset_Iio {Entity : Type u_1} {D : Type u_2} [Preorder D] (μ : Entity → D) (Δ : Set D) (y : Entity) : y ∈ Core.Order.Comparison.gt.overSet μ Δ ↔ Δ ⊆ Set.Iio (μ y)

The set-of-degrees comparative Comparison.gt.overSet μ ([Hoe83]) as a strict-interval inclusion: y clears the than-clause iff every standard degree lies strictly below μ y. Strict mirror of mathlib's mem_upperBounds_iff_subset_Iic; both faces are Iff.rfl siblings.

theorem Degree.gtOverSet_isAntiAdditive {Entity : Type u_1} {D : Type u_2} [Preorder D] (μ : Entity → D) : Entailment.IsAntiAdditive (Core.Order.Comparison.gt.overSet μ)

[Hoe83] Fact 4: the S-comparative Comparison.gt.overSet μ is anti-additive in its set-of-degrees argument — the algebraic source of NPI licensing in clausal than-comparatives.

theorem Degree.gtOverSet_eq_singleton_of_isGreatest {Entity : Type u_1} {D : Type u_2} [Preorder D] (μ : Entity → D) {Δ : Set D} {m : D} (hm : IsGreatest Δ m) : Core.Order.Comparison.gt.overSet μ Δ = Core.Order.Comparison.gt.overSet μ {m}

Reduction lemma ([BP04] §3, order-theoretic form): the S-comparative Comparison.gt.overSet μ is determined by the greatest element of its degree-set argument. Needs neither linearity nor density — only [Preorder D] and the IsGreatest witness.

Downward-entailingness of than-clauses

theorem Degree.comparative_than_DE {α : Type u_1} (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 — the generic monotonicity fact behind than-clauses being downward-entailing (not [Hoe83]'s specific anti-additivity result, which is in Studies/Hoeksema1983.lean).

Comparison as extent inclusion

Three faces of the posExt / negExt correspondence ([Ken99]): the binary comparator equals strict extent inclusion, and antonymy follows from extent complementarity rather than being stipulated.

theorem Degree.gtOverSet_atomic_eq_comparativeSem {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (a b : Entity) : a ∈ Core.Order.Comparison.gt.overSet μ {μ b} ↔ comparativeSem μ a b Core.Order.ScalePolarity.positive

Bridge: the atomic S-comparative Comparison.gt.overSet μ {μ b} coincides with the binary comparativeSem on a LinearOrder. The set-of-degrees schema strictly generalizes the binary comparator, collapsing at a singleton via Comparison.overSet_singleton.

theorem Degree.comparative_iff_posExt_ssubset {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (a b : Entity) : comparativeSem μ a b Core.Order.ScalePolarity.positive ↔ posExt μ b ⊂ posExt μ a

"A is taller than B" iff A's positive extent strictly contains B's ([Ken99]). Bridges the point comparison to posExt_ssubset_iff.

theorem Degree.comparative_iff_negExt_ssubset {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (a b : Entity) : comparativeSem μ a b Core.Order.ScalePolarity.positive ↔ negExt μ a ⊂ negExt μ b

"A taller than B" iff "B shorter than A", derived from the complementarity of positive and negative extents rather than stipulated as a lexical property of antonym pairs ([Ken99]).

Strengthened, negated, and extent-theoretic equatives

[Ken07] [Ret20] [Sch08f] [TD20]

The literal equative is "at least as" (equativeSem .positive); the "exactly as" reading is derived by scalar implicature (choosing as tall as over the stronger taller than). A granularity-based alternative is in Degree.Granularity.

def Degree.equativeStrengthened {Entity : Type u_1} {D : Type u_2} [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

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

theorem Degree.equativeStrengthened_entails_sem {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (a b : Entity) (h : equativeStrengthened μ a b) : equativeSem μ a b Core.Order.ScalePolarity.positive

The strengthened reading entails the literal ≥ reading.

def Degree.negatedEquative {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (a b : Entity) : Prop

Negated equative: "A is not as tall as B" iff μ a < μ b.

Equations

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

theorem Degree.negatedEquative_iff_not_sem {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (a b : Entity) : negatedEquative μ a b ↔ ¬equativeSem μ a b Core.Order.ScalePolarity.positive

Negated equative is the negation of the literal equative.

theorem Degree.equativeSem_iff_posExt_subset {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (a b : Entity) : equativeSem μ a b Core.Order.ScalePolarity.positive ↔ posExt μ b ⊆ posExt μ a

Equative as positive extent inclusion ([Ken99]): "A is as tall as B" iff posExt μ b ⊆ posExt μ a — every degree B has, A also has.

theorem Degree.negatedEquative_iff_posExt_ssubset {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (a b : Entity) : negatedEquative μ a b ↔ posExt μ a ⊂ posExt μ b

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