Heim 2001: Degree Operators and Scope

@cite{heim-2001} @cite{heim-1999} @cite{kennedy-1999}

Irene Heim. Degree Operators and Scope. In C. Féry & W. Sternefeld (eds.), Audiatur Vox Sapientiae, Akademie Verlag, pp. 214–239.

Core Claim

Degree phrases (DegPs) are generalized quantifiers over degrees that take scope by QR, analogous to DP quantifiers. The paper probes which scope configurations are empirically available.

Key Results

1. Monotone collapse (§2.1): with ↑monotone operators (∀, ∃, required, allowed), low-DegP and high-DegP are truth-conditionally equivalent — scope is undetectable for plain comparatives.

2. Negation (§2.1): high-DegP over negation yields presupposition failure (max of {d: ¬tall(x,d)} is undefined on unbounded scales).

3. Kennedy's generalization (§2.2): DegP cannot scope over a quantificational DP whose scope contains the DegP's trace.

4. Intensional verbs (§2.3): DegP CAN scope over require, allow, need, be able; but NOT over might, should, supposed to, want.

5. De re/de dicto ≠ DegP-scope (§2.4): the Russell ambiguity ("John thinks the yacht is longer than it is") is world-variable binding in the than-clause, not DegP movement.

6. Semantic ellipsis (§3.2): -est and too use their complement twice — evidence for DegP movement independent of VP-ellipsis.

theorem Phenomena.Comparison.Studies.Heim2001.heim_eq_kennedy_simple {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (a b : Entity) : Semantics.Degree.DegreeAbstraction.heimComparativeWithMeasure μ a b ↔ Semantics.Degree.Comparative.comparativeSem μ a b Core.Scale.ScalePolarity.positive

For simple comparatives, Heim and Kennedy yield the same truth conditions. The derivation differs (degree abstraction + max vs direct measure comparison), but the result is identical.

structure Phenomena.Comparison.Studies.Heim2001.ScopeInteractionDatum : Type

A scope interaction datum: does high-DegP yield a distinct, available reading?

• sentence : String
• operator : String

  The operator DegP interacts with

• scopeCollapse : Bool

  Are low-DegP and high-DegP truth-conditionally equivalent?

• highDegPAvailable : Bool

  Is the high-DegP reading empirically available?

• explanation : String

  Why (equivalence, presupposition failure, constraint)

def Phenomena.Comparison.Studies.Heim2001.instReprScopeInteractionDatum.repr : ScopeInteractionDatum → ℕ → Std.Format

Equations

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

instance Phenomena.Comparison.Studies.Heim2001.instReprScopeInteractionDatum : Repr ScopeInteractionDatum

Equations

• Phenomena.Comparison.Studies.Heim2001.instReprScopeInteractionDatum = { reprPrec := Phenomena.Comparison.Studies.Heim2001.instReprScopeInteractionDatum.repr }

def Phenomena.Comparison.Studies.Heim2001.monotoneCollapseData : List ScopeInteractionDatum

Heim §2.1: scope collapses with monotone increasing operators. For plain comparatives (no exactly, no less), low-DegP ↔ high-DegP with ∀, ∃, required, allowed. Scope is undetectable.

Equations

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

theorem Phenomena.Comparison.Studies.Heim2001.monotone_collapse_all_equivalent (d : ScopeInteractionDatum) : d ∈ monotoneCollapseData → d.scopeCollapse = true

All monotone collapse examples have scopeCollapse = true.

def Phenomena.Comparison.Studies.Heim2001.negationData : List ScopeInteractionDatum

Heim §2.1: high-DegP over negation → presupposition failure. max{d: ¬tall(m,d)} = max{d: d > μ(m)} is undefined on unbounded scales. The high-DegP LF is semantically deviant.

Equations

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

theorem Phenomena.Comparison.Studies.Heim2001.negation_presupposition_failure {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (a : Entity) (d : D) : Semantics.Degree.DegreeAbstraction.negatedDegreePredicate μ a d ↔ d > μ a

The negated degree set {d : d > μ(a)} has no maximum, confirming presupposition failure for high-DegP over negation.

def Phenomena.Comparison.Studies.Heim2001.nonMonotoneData : List ScopeInteractionDatum

Heim §2.1–2.2: with exactly and less, the two scope configurations are truth-conditionally DISTINCT. This is where Heim's approach makes testable predictions.

Equations

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

structure Phenomena.Comparison.Studies.Heim2001.IntensionalVerbDatum : Type

Heim §2.3: with exactly-differentials and less, some intensional verbs allow high-DegP (= DegP scopes over the modal), others don't.

This is NOT detectable with plain more comparatives — those collapse due to monotonicity (§2.1). Only exactly/less break the equivalence.

• sentence : String
• verb : String
• highDegPAvailable : Bool

  Does DegP scope over this verb (with exactly/less)?

• note : String

instance Phenomena.Comparison.Studies.Heim2001.instReprIntensionalVerbDatum : Repr IntensionalVerbDatum

Equations

• Phenomena.Comparison.Studies.Heim2001.instReprIntensionalVerbDatum = { reprPrec := Phenomena.Comparison.Studies.Heim2001.instReprIntensionalVerbDatum.repr }

def Phenomena.Comparison.Studies.Heim2001.instReprIntensionalVerbDatum.repr : IntensionalVerbDatum → ℕ → Std.Format

Equations

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

def Phenomena.Comparison.Studies.Heim2001.intensionalVerbData : List IntensionalVerbDatum

Equations

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

theorem Phenomena.Comparison.Studies.Heim2001.intensional_verb_pattern : (List.filter (fun (x : IntensionalVerbDatum) => x.highDegPAvailable) intensionalVerbData).length = 4 ∧ (List.filter (fun (x : IntensionalVerbDatum) => !x.highDegPAvailable) intensionalVerbData).length = 4

The pattern: deontic/ability modals allow high-DegP, epistemic/neg-raising verbs block it.

structure Phenomena.Comparison.Studies.Heim2001.RussellAmbiguityDatum : Type

Heim §2.4: the Russell ambiguity is NOT evidence for DegP-scope. "John thinks the yacht is longer than it is" has two readings from world-variable binding in the than-clause (de re vs de dicto), both compatible with narrow DegP-scope.

• sentence : String
• readings : List String
• isDegPScope : Bool
• explanation : String

instance Phenomena.Comparison.Studies.Heim2001.instReprRussellAmbiguityDatum : Repr RussellAmbiguityDatum

Equations

• Phenomena.Comparison.Studies.Heim2001.instReprRussellAmbiguityDatum = { reprPrec := Phenomena.Comparison.Studies.Heim2001.instReprRussellAmbiguityDatum.repr }

def Phenomena.Comparison.Studies.Heim2001.instReprRussellAmbiguityDatum.repr : RussellAmbiguityDatum → ℕ → Std.Format

Equations

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

def Phenomena.Comparison.Studies.Heim2001.russellAmbiguity : RussellAmbiguityDatum

Equations

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

structure Phenomena.Comparison.Studies.Heim2001.SuperlativeJudgment : Type

@cite{heim-1999} absolute vs relative superlative ambiguity. Absolute = narrow-scope -est, relative = wide-scope -est. Focus determines the comparison set for relative readings.

• sentence : String
• readings : List String
• focus : Option String
• note : String

def Phenomena.Comparison.Studies.Heim2001.instReprSuperlativeJudgment.repr : SuperlativeJudgment → ℕ → Std.Format

Equations

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

instance Phenomena.Comparison.Studies.Heim2001.instReprSuperlativeJudgment : Repr SuperlativeJudgment

Equations

• Phenomena.Comparison.Studies.Heim2001.instReprSuperlativeJudgment = { reprPrec := Phenomena.Comparison.Studies.Heim2001.instReprSuperlativeJudgment.repr }

def Phenomena.Comparison.Studies.Heim2001.superlativeExamples : List SuperlativeJudgment

Equations

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

theorem Phenomena.Comparison.Studies.Heim2001.heim_est_matches_absolute {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (C : Set Entity) (x : Entity) : Semantics.Degree.Superlative.absoluteSuperlative μ C x ↔ x ∈ C ∧ ∀ y ∈ C, y ≠ x → μ x > μ y

Bridge to Superlative.lean: Heim's -est denotation (59) λR⟨d,et⟩.λx. max{d: R(x,d)} > max{d: ∃y ≠ x. R(y,d)} matches absoluteSuperlative when R is a monotone adjective.

theorem Phenomena.Comparison.Studies.Heim2001.heim_exactly_matches_differential {Entity : Type u_1} (μ : Entity → ℚ) (a b : Entity) (diff : ℚ) : Semantics.Degree.Differential.differentialComparative μ a b diff ↔ μ a - μ b = diff

Bridge to Differential.lean: Heim's exactly-differential (5b) ⟦exactly 2" -er than 1'⟧ = λP. max(P) = 1' + 2" corresponds to differentialComparative with diff = 2.

theorem Phenomena.Comparison.Studies.Heim2001.scope_collapse_exists {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (restrictor : Entity → Prop) (μ : Entity → D) (threshold : D) : Semantics.Degree.DegreeAbstraction.lowDegP_exists restrictor μ threshold ↔ Semantics.Degree.DegreeAbstraction.highDegP_exists restrictor μ threshold

Bridge to scope theory: the monotone collapse for ∃ is a proper theorem (not Iff.rfl).