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.

def Semantics.Degree.DegreeAbstraction.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.DegreeAbstraction.DegreePredicate D = (D → Prop)

def Semantics.Degree.DegreeAbstraction.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.DegreeAbstraction.IsMaxDeg P d = (P d ∧ ∀ (d' : D), P d' → d' ≤ d)

def Semantics.Degree.DegreeAbstraction.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.DegreeAbstraction.matrixPredicate μ a d = (μ a ≥ d)

def Semantics.Degree.DegreeAbstraction.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.DegreeAbstraction.thanClausePredicate μ b d = (μ b ≥ d)

theorem Semantics.Degree.DegreeAbstraction.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).

def Semantics.Degree.DegreeAbstraction.Monotone {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.

Heim (p. 216, def. (3)): a function f of type ⟨d,et⟩ is monotone iff ∀x∀d∀d'[f(d)(x) = 1 & d' < d → f(d')(x) = 1].

Equations

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

theorem Semantics.Degree.DegreeAbstraction.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.DegreeAbstraction.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.DegreeAbstraction.erOnPredicates _P₁ _P₂ d₁ d₂ _h₁ _h₂ = (d₁ > d₂)

def Semantics.Degree.DegreeAbstraction.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.DegreeAbstraction.lessOnPredicates _P₁ _P₂ d₁ d₂ _h₁ _h₂ = (d₁ < d₂)

def Semantics.Degree.DegreeAbstraction.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.DegreeAbstraction.heimComparativeWithMeasure μ a b = (μ a > μ b)

def Semantics.Degree.DegreeAbstraction.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.DegreeAbstraction.lowDegP_forall restrictor μ threshold = ∀ (x : Entity), restrictor x → μ x > threshold

def Semantics.Degree.DegreeAbstraction.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.DegreeAbstraction.highDegP_forall restrictor μ threshold = ∃ (d : D), (∀ (x : Entity), restrictor x → μ x ≥ d) ∧ d > threshold

theorem Semantics.Degree.DegreeAbstraction.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.DegreeAbstraction.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).

def Semantics.Degree.DegreeAbstraction.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.DegreeAbstraction.lowDegP_exists restrictor μ threshold = ∃ (x : Entity), restrictor x ∧ μ x > threshold

def Semantics.Degree.DegreeAbstraction.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.DegreeAbstraction.highDegP_exists restrictor μ threshold = ∃ (d : D), (∃ (x : Entity), restrictor x ∧ μ x ≥ d) ∧ d > threshold

theorem Semantics.Degree.DegreeAbstraction.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.

def Semantics.Degree.DegreeAbstraction.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.DegreeAbstraction.negatedDegreePredicate μ a d = ¬μ a ≥ d

theorem Semantics.Degree.DegreeAbstraction.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 exactly {d : d > μ(a)}.

theorem Semantics.Degree.DegreeAbstraction.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).