Heim's Degree Operator Approach

@cite{heim-2001}

@cite{heim-2001} "Degree Operators and Scope": degree morphemes (-er, less, -est, too) are generalized quantifiers over degrees (type ⟨dt,t⟩) that take scope by QR, just like DP quantifiers. The key theoretical content is twofold:

1. Denotation: ⟦-er than P⟧ = λQ. max(Q) > max(P), where max is the maximality operator over degree predicates.
2. Scope: because DegPs QR, they interact scopally with other operators (quantifiers, negation, modals). The paper probes which scope configurations are empirically available.

Monotonicity and Scope Collapse

Adjective denotations are monotone: if tall(x,d) then tall(x,d') for all d' ≤ d. This means max{d: tall(x,d)} = μ(x). And for monotone increasing operators (∀, ∃), low-DegP and high-DegP yield equivalent truth conditions — scope is undetectable.

Comparison with Kennedy

Kennedy's -er is DP-internal (no QR needed), so it never takes wide scope. The two frameworks agree extensionally on simple comparatives but diverge on scope predictions with exactly-differentials, less, and intensional verbs.

Order-Theoretic Foundations

Heim's maximality operator IsMaxDeg is Mathlib's IsGreatest. The matrix predicate λd. μ(a) ≥ d and @cite{kennedy-1999}'s posExt μ a are both the principal downset Set.Iic (μ a) — the same mathematical object arrived at from different linguistic motivations. The scope collapse theorems factor through the degree image μ '' {x | R x}, connecting to gc_sSup_Iic under ConditionallyCompleteLattice.

def Semantics.Degree.Abstraction.DegreePredicate (D : Type u_1) : Type u_1

A degree predicate: a set of degrees (type ⟨d,t⟩ in Heim's terms). Both the matrix clause and the than-clause denote degree predicates after degree abstraction.

Equations

• Semantics.Degree.Abstraction.DegreePredicate D = (D → Prop)

def Semantics.Degree.Abstraction.IsMaxDeg {D : Type u_1} [LE D] (P : DegreePredicate D) (d : D) : Prop

Heim's maximality operator (paper def. (6)): max(P) := ιd. P(d) ∧ ∀d', P(d') → d' ≤ d

We define it relationally: d is the maximum of P when it satisfies P and is an upper bound.

Equations

• Semantics.Degree.Abstraction.IsMaxDeg P d = (P d ∧ ∀ (d' : D), P d' → d' ≤ d)

theorem Semantics.Degree.Abstraction.isMaxDeg_iff_isGreatest {D : Type u_1} [LE D] (P : DegreePredicate D) (d : D) : IsMaxDeg P d ↔ IsGreatest {d' : D | P d'} d

Heim's maximality = Mathlib's IsGreatest.

IsMaxDeg P d ("d is the maximum of predicate P") is IsGreatest {d | P d} d ("d is the greatest element of the set satisfying P"). The equivalence makes all of Mathlib.Order.Bounds available for degree-semantic reasoning.

def Semantics.Degree.Abstraction.matrixPredicate {Entity : Type u_1} {D : Type u_2} [Preorder D] (μ : Entity → D) (a : Entity) : DegreePredicate D

The matrix degree predicate for "A is d-tall": λd. μ(A) ≥ d.

Equations

• Semantics.Degree.Abstraction.matrixPredicate μ a d = (μ a ≥ d)

def Semantics.Degree.Abstraction.thanClausePredicate {Entity : Type u_1} {D : Type u_2} [Preorder D] (μ : Entity → D) (b : Entity) : DegreePredicate D

The than-clause degree predicate for "B is d-tall": λd. μ(B) ≥ d.

Equations

• Semantics.Degree.Abstraction.thanClausePredicate μ b d = (μ b ≥ d)

theorem Semantics.Degree.Abstraction.matrixPredicate_mem_iff_Iic {Entity : Type u_1} {D : Type u_2} [Preorder D] (μ : Entity → D) (a : Entity) (d : D) : matrixPredicate μ a d ↔ d ∈ Set.Iic (μ a)

Matrix predicate membership = Set.Iic membership.

theorem Semantics.Degree.Abstraction.matrixPredicate_mem_iff_posExt {Entity : Type u_1} {D : Type u_2} [Preorder D] (μ : Entity → D) (a : Entity) (d : D) : matrixPredicate μ a d ↔ d ∈ Core.Scale.posExt μ a

Matrix predicate membership = posExt membership (@cite{kennedy-1999}).

theorem Semantics.Degree.Abstraction.isMaxDeg_matrixPredicate {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (a : Entity) : IsMaxDeg (matrixPredicate μ a) (μ a)

The maximum of a monotone predicate λd. μ(a) ≥ d is μ(a) itself. This grounds the Heim–Kennedy equivalence: max{d: tall(a,d)} = μ(a).

This is Mathlib's isGreatest_Iic — the greatest element of {d | d ≤ μ(a)} is μ(a) — specialized to degree semantics.

def Semantics.Degree.Abstraction.IsMonotoneAdj {Entity : Type u_1} {D : Type u_2} [Preorder D] (adj : D → Entity → Prop) : Prop

An adjective denotation (type ⟨d,et⟩) is monotone iff tall(x,d) implies tall(x,d') for all d' ≤ d.

@cite{heim-2001}: a function f of type ⟨d,et⟩ is monotone iff ∀x∀d∀d'[f(d)(x) = 1 & d' < d → f(d')(x) = 1].

Named IsMonotoneAdj (not Monotone) to avoid shadowing mathlib's Monotone.

Equations

• Semantics.Degree.Abstraction.IsMonotoneAdj adj = ∀ (x : Entity) (d d' : D), adj d x → d' ≤ d → adj d' x

theorem Semantics.Degree.Abstraction.matrixPredicate_monotone {Entity : Type u_1} {D : Type u_2} [Preorder D] (μ : Entity → D) (a : Entity) (d d' : D) : matrixPredicate μ a d → d' ≤ d → matrixPredicate μ a d'

matrixPredicate μ a is always monotone (by construction).

def Semantics.Degree.Abstraction.erOnPredicates {D : Type u_1} [LE D] [LT D] (_P₁ _P₂ : DegreePredicate D) (d₁ d₂ : D) (_h₁ : IsMaxDeg _P₁ d₁) (_h₂ : IsMaxDeg _P₂ d₂) : Prop

Heim's -er operating on degree predicates (paper def. (6)): ⟦-er⟧(D₂)(D₁) = max(D₁) > max(D₂)

Takes two degree predicates and compares their maxima.

Equations

• Semantics.Degree.Abstraction.erOnPredicates _P₁ _P₂ d₁ d₂ _h₁ _h₂ = (d₁ > d₂)

def Semantics.Degree.Abstraction.lessOnPredicates {D : Type u_1} [LE D] [LT D] (_P₁ _P₂ : DegreePredicate D) (d₁ d₂ : D) (_h₁ : IsMaxDeg _P₁ d₁) (_h₂ : IsMaxDeg _P₂ d₂) : Prop

Heim's less operator (paper (23)): ⟦less than P⟧ = λQ. max(Q) < max(P)

Equations

• Semantics.Degree.Abstraction.lessOnPredicates _P₁ _P₂ d₁ d₂ _h₁ _h₂ = (d₁ < d₂)

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

Heim comparative with measure function: the result of composing -er with degree predicates derived from a monotone adjective.

"A is taller than B" = ⟦-er⟧(λd. μ(B) ≥ d)(λd. μ(A) ≥ d) = max{d: μ(A) ≥ d} > max{d: μ(B) ≥ d} = μ(A) > μ(B)

Equations

• Semantics.Degree.Abstraction.heimComparativeWithMeasure μ a b = (μ a > μ b)

def Semantics.Degree.Abstraction.lowDegP_forall {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (restrictor : Entity → Prop) (μ : Entity → D) (threshold : D) : Prop

Low-DegP truth conditions for "every girl is taller than 4ft": ∀x[girl(x) → max{d: tall(x,d)} > 4']

DegP scopes below the quantifier. Each girl's height exceeds 4'.

Equations

• Semantics.Degree.Abstraction.lowDegP_forall restrictor μ threshold = ∀ (x : Entity), restrictor x → μ x > threshold

def Semantics.Degree.Abstraction.highDegP_forall {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (restrictor : Entity → Prop) (μ : Entity → D) (threshold : D) : Prop

High-DegP truth conditions for "every girl is taller than 4ft": max{d: ∀x[girl(x) → tall(x,d)]} > 4'

DegP scopes above the quantifier. The maximal degree to which every girl is tall exceeds 4'. This equals the height of the shortest girl (by monotonicity).

Equations

• Semantics.Degree.Abstraction.highDegP_forall restrictor μ threshold = ∃ (d : D), (∀ (x : Entity), restrictor x → μ x ≥ d) ∧ d > threshold

def Semantics.Degree.Abstraction.lowDegP_exists {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (restrictor : Entity → Prop) (μ : Entity → D) (threshold : D) : Prop

Low-DegP for ∃: ∃x[girl(x) ∧ μ(x) > threshold].

Equations

• Semantics.Degree.Abstraction.lowDegP_exists restrictor μ threshold = ∃ (x : Entity), restrictor x ∧ μ x > threshold

def Semantics.Degree.Abstraction.highDegP_exists {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (restrictor : Entity → Prop) (μ : Entity → D) (threshold : D) : Prop

High-DegP for ∃: max{d: ∃x[girl(x) ∧ tall(x,d)]} > threshold. This equals the tallest girl's height.

Equations

• Semantics.Degree.Abstraction.highDegP_exists restrictor μ threshold = ∃ (d : D), (∃ (x : Entity), restrictor x ∧ μ x ≥ d) ∧ d > threshold

theorem Semantics.Degree.Abstraction.exists_scope_via_degreeImage {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (R : Entity → Prop) (μ : Entity → D) (t : D) : lowDegP_exists R μ t ↔ ∃ d ∈ μ '' {x : Entity | R x}, d > t

∃ scope collapse via degree image: both scope readings ask whether the degree image μ '' {x | R x} contains an element above t.

theorem Semantics.Degree.Abstraction.forall_scope_via_degreeImage {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (R : Entity → Prop) (μ : Entity → D) (t : D) : lowDegP_forall R μ t ↔ ∀ d ∈ μ '' {x : Entity | R x}, d > t

∀ scope collapse via degree image lower bounds: both scope readings ask whether t is strictly below every element of the degree image μ '' {x | R x}.

theorem Semantics.Degree.Abstraction.forall_more_high_to_low {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (restrictor : Entity → Prop) (μ : Entity → D) (threshold : D) : highDegP_forall restrictor μ threshold → lowDegP_forall restrictor μ threshold

Monotone collapse (Heim §2.1): for ∀ + more-comparatives, high-DegP → low-DegP (the reverse direction).

If there exists d > threshold s.t. every girl is d-tall, then every girl exceeds threshold (since μ(x) ≥ d > threshold).

theorem Semantics.Degree.Abstraction.forall_more_low_to_high {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (restrictor : Entity → Prop) (μ : Entity → D) (threshold : D) (w : Entity) (hw : restrictor w) (hmin : ∀ (x : Entity), restrictor x → μ x ≥ μ w) : lowDegP_forall restrictor μ threshold → highDegP_forall restrictor μ threshold

Monotone collapse (Heim §2.1): for ∀ + more-comparatives, low-DegP → high-DegP (given a witness).

If every girl is taller than threshold, pick any girl w — her height witnesses d > threshold with ∀x.tall(x,d) being vacuously weak (every girl is at least threshold-tall, and w is one of them).

theorem Semantics.Degree.Abstraction.exists_more_scope_collapse {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (restrictor : Entity → Prop) (μ : Entity → D) (threshold : D) : lowDegP_exists restrictor μ threshold ↔ highDegP_exists restrictor μ threshold

Monotone collapse for ∃ + more: low ↔ high. Both readings reduce to ∃ d ∈ μ '' {x | R x}, d > t (see exists_scope_via_degreeImage).

def Semantics.Degree.Abstraction.negatedDegreePredicate {Entity : Type u_1} {D : Type u_2} [Preorder D] (μ : Entity → D) (a : Entity) : DegreePredicate D

The degree set {d : ¬(μ(x) ≥ d)} = {d : d > μ(x)}. This set has no maximum on an unbounded scale. Heim (p. 220): high-DegP over negation is ruled out because max{d: ¬tall(m,d)} is undefined.

Equations

• Semantics.Degree.Abstraction.negatedDegreePredicate μ a d = ¬μ a ≥ d

theorem Semantics.Degree.Abstraction.negatedDegreePredicate_eq {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (a : Entity) (d : D) : negatedDegreePredicate μ a d ↔ d > μ a

The negated degree set is negExt (@cite{kennedy-1999}): the degrees entity a "lacks". The failure of IsMaxDeg for this predicate corresponds to negExt (= Set.Ioi) having no IsGreatest element — it is unbounded above.

theorem Semantics.Degree.Abstraction.heim_extensional_equivalence {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (a b : Entity) : heimComparativeWithMeasure μ a b ↔ Comparative.comparativeSem μ a b Core.Scale.ScalePolarity.positive

Extensional equivalence: Heim yields the same truth conditions as the consensus comparative semantics for simple comparatives. They differ only on scope predictions with exactly-differentials, less-comparatives, and intensional verbs (Heim §2.2–2.3).

theorem Semantics.Degree.Abstraction.heim_kennedy_via_galois {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (a b : Entity) : heimComparativeWithMeasure μ a b ↔ Core.Scale.posExt μ b ⊂ Core.Scale.posExt μ a

The Heim comparative and Kennedy's extent comparison are connected by the Galois connection: both factor through the same order on degrees.