Heim 2001: Degree Operators and Scope

@cite{heim-2001} @cite{heim-1999} @cite{kennedy-1999} @cite{percus-2000} @cite{von-stechow-1984} @cite{fox-hackl-2006} @cite{schwarzschild-wilkinson-2002} @cite{beck-2001} @cite{kennedy-mcnally-2005} @cite{szabolcsi-1986}

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

Headline

Heim's central §2.1 observation — that the high-DegP and low-DegP LFs for ↑monotone operators are truth-conditionally equivalent — reduces to two lattice identities:

• sSup (⋃ᵢ Iic (μ i)) = ⨆ᵢ μ i (mathlib's sSup_iUnion_Iic)
• sSup (⋂ᵢ Iic (μ i)) = ⨅ᵢ μ i (sSup_iInter_Iic_eq_iInf below)

Heim's max-set semantics for -er (paper exs. (5)–(6)) computes the high-DegP truth condition as sSup (matrixSet) > threshold. The lattice identities reduce this to the low-DegP threshold form (with an attainment caveat for the ∀ direction; see heim_collapse_forall_low_to_high, paper fn. 6).

For the negation case (paper exs. 17–19), no_isGreatest_Ioi_of_noMaxOrder shows the high-DegP LF is undefined: the negated degree set Ioi (μ a) has no greatest element on any NoMaxOrder scale. This is the same mechanism behind @cite{fox-hackl-2006} negative islands.

Kennedy's generalization (paper ex. (27)) is formalized via the Heim-Kennedy Constraint substrate (Theories/Syntax/Minimalist/DegreeMovement.lean), re-exported below.

Section map

Paper	This file
§2.1 monotone collapse (8–16)	heim_collapse_exists, heim_collapse_forall_*
§2.1 negation (17–19)	no_isGreatest_Ioi_of_noMaxOrder, negation_high_DegP_undefined
§2.2 Kennedy's generalization (20–27)	nonMonotone_blocked_by_HKC
§2.3 intensional verbs (28–36)	intensionalVerbData + BhattPancheva2004 HKC bridge
§2.4 Russell ambiguity (37–42)	docstring only — see VonStechow1984.lean
§3.2 semantic ellipsis (58–64)	reference to Superlative.absoluteSuperlative

What this file does NOT formalize

• Heim's free-world-variable implementation of de re/de dicto (paper §2.4, ex. (40); Percus-style binding per @cite{percus-2000} and Abusch 1994 — paper fn. 16). The substrate's Theories/Semantics/Degree/Intensional.lean formalizes the alternative ACTUALLY-operator implementation (von Stechow 1984), used in VonStechow1984.lean. The two implementations agree on the diagnosis (Russell ambiguity is de re/de dicto, not DegP-scope) but differ on the LF mechanism.
• Typed ⟨dt,t⟩ DegP-as-generalized-quantifier denotations over arbitrary degree predicates. For monotone adjectives the max-set computation reduces to a measure-function form already in the substrate (Abstraction.heimComparativeWithMeasure = Comparative.comparativeSem, proved by Iff.rfl at Abstraction.heim_extensional_equivalence).

Recent literature this file does not engage

• @cite{schwarzschild-wilkinson-2002} interval semantics, which Heim's own fn. 21 flags as work that may force her to revise basic assumptions
• @cite{beck-2001} intervention effects, parallel to Kennedy's generalization
• @cite{kennedy-mcnally-2005} closed-scale adjective behavior under negation

theorem Heim2001.sSup_iInter_Iic_eq_iInf {α : Type u_1} [CompleteLinearOrder α] {ι : Type u_2} (f : ι → α) : sSup (⋂ (i : ι), Set.Iic (f i)) = ⨅ (i : ι), f i

sSup ∘ ⋂ ∘ Iic = ⨅ on a CompleteLinearOrder. The dual of mathlib's sSup_iUnion_Iic. Heim's high-DegP-over-∀ truth condition reduces to this two-step calculation (⋂Iic = Iic ⨅, then csSup_Iic).

theorem Heim2001.heim_collapse_exists {α : Type u_1} {D : Type u_2} [LinearOrder D] (R : α → Prop) (μ : α → D) (t : D) : Semantics.Degree.Abstraction.lowDegP_exists R μ t ↔ Semantics.Degree.Abstraction.highDegP_exists R μ t

Heim §2.1, ∃-side: high-DegP and low-DegP collapse for existentially quantified subjects ("Some girl is taller than 4 feet"). Re-export of the substrate identity; the underlying lattice content is sSup_iUnion_Iic: sSup (⋃ᵢ Iic (μ i)) > t ↔ ∃ i, μ i > t.

theorem Heim2001.highDegP_forall_lattice {α : Type u_1} [CompleteLinearOrder α] {ι : Type u_2} (μ : ι → α) (t : α) : sSup {d : α | ∀ (i : ι), d ≤ μ i} > t ↔ ⨅ (i : ι), μ i > t

Heim §2.1, ∀-side, lattice form: the high-DegP-over-∀ max-set {d | ∀ i, d ≤ μ i} has truth condition (⨅ᵢ μ i) > t.

theorem Heim2001.heim_collapse_forall_high_to_low {α : Type u_1} {D : Type u_2} [LinearOrder D] (R : α → Prop) (μ : α → D) (t : D) : Semantics.Degree.Abstraction.highDegP_forall R μ t → Semantics.Degree.Abstraction.lowDegP_forall R μ t

Heim §2.1, ∀-side collapse, forward direction (paper p. 218, discussion of ex. (10)): high-DegP entails low-DegP. Always holds. Substrate re-export.

theorem Heim2001.heim_collapse_forall_low_to_high {α : Type u_1} {D : Type u_2} [LinearOrder D] (R : α → Prop) (μ : α → D) (t : D) (w : α) (hw : R w) (hmin : ∀ (x : α), R x → μ x ≥ μ w) : Semantics.Degree.Abstraction.lowDegP_forall R μ t → Semantics.Degree.Abstraction.highDegP_forall R μ t

Heim §2.1, ∀-side collapse, reverse direction (paper fn. 6: holds "whenever these maxima are defined"): low-DegP entails high-DegP given an attaining witness — the "shortest girl" of Heim's prose. Substrate re-export.

theorem Heim2001.no_isGreatest_Ioi_of_noMaxOrder {α : Type u_1} [LinearOrder α] [NoMaxOrder α] (a : α) : ¬∃ (m : α), IsGreatest (Set.Ioi a) m

The lattice fact behind Heim's negation argument: on any NoMaxOrder linear order, the strict upper interval Ioi a has no greatest element. This is the same mechanism behind @cite{fox-hackl-2006} negative islands.

theorem Heim2001.negation_high_DegP_undefined {Entity : Type u_1} {D : Type u_2} [LinearOrder D] [NoMaxOrder D] (μ : Entity → D) (a : Entity) : ¬∃ (m : D), IsGreatest {d : D | Semantics.Degree.Abstraction.negatedDegreePredicate μ a d} m

Heim §2.1, ex. (17c): the high-DegP LF for "Mary isn't taller than 4 feet" computes max{d | ¬ tall(m,d)} > 4 = max(Ioi (μ m)) > 4, which is undefined on any NoMaxOrder scale. The high-DegP LF is therefore ruled out by presupposition failure.

Heim p. 220 generalizes this to at most n (ex. 18) and to implicitly negative verbs like refuse (ex. 19) — both classified as "implicitly negative or monotone decreasing operators", not as neg-raising verbs (which are §2.3, exs (34)–(36)).

theorem Heim2001.nonMonotone_blocked_by_HKC (degH qpH : ℕ) (h : degH < qpH) : ¬Minimalist.DegreeMovement.IsHeimKennedy { degHeight := degH, qpHeight := qpH, qpBasePosition := qpH, qpBindsDeg := true }

Kennedy's generalization (paper ex. (27)): "If the scope of a quantificational DP contains the trace of a DegP, it also contains that DegP itself." Equivalently: a high-DegP LF in which the QP binds into the DegP's restrictor is illicit.

Re-export of not_isHeimKennedy_QP_above_bound_DegP from the Minimalism–degree-semantics interface substrate. The exemplar binding ⟨degHeight := 0, qpHeight := 1, qpBindsDeg := true⟩ covers Heim's §2.2 examples uniformly: exactly-differentials (exs 20, 22), less-comparatives (24), and object-position quantifiers (25). @cite{bhatt-pancheva-2004} §4 is the dedicated formalization; see BhattPancheva2004.bp_hkc_matches_heim_intensional_data.

inductive Heim2001.IntensionalVerbClass : Type

Heim's classification of intensional verbs by whether they admit the high-DegP reading with exactly-differentials or less. Heim presents this 4-vs-4 split as descriptive, not explanatory: paper p. 226 ("I am unable to spell out any concrete explanations for the unambiguity of (33–36), and it is only a hope that it will follow without specific stipulations about DegP-movement").

@cite{bhatt-pancheva-2004} §5.2 derives the split from the Heim-Kennedy Constraint plus the assumption that intensional subjects bind into the degree predicate; see BhattPancheva2004.bp_hkc_matches_heim_intensional_data.

• deontic : IntensionalVerbClass

  Necessity / requirement modals. Heim §2.3 (28), (32b).

• possibility : IntensionalVerbClass

  Possibility / ability modals. Heim §2.3 (29), (32a).

• epistemic : IntensionalVerbClass

  Epistemic modals: high-DegP unavailable. Heim §2.3 (33).

• negRaising : IntensionalVerbClass

  Neg-raising verbs (should, supposed-to, want): high-DegP unavailable. Heim §2.3 (34)–(36), citing von Fintel & Iatridou 2001 in fn. 14. (Note: refuse from Heim §2.1 ex. (19) is implicitly negative, not neg-raising.)

@[implicit_reducible]

instance Heim2001.instDecidableEqIntensionalVerbClass : DecidableEq IntensionalVerbClass

Equations

• Heim2001.instDecidableEqIntensionalVerbClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Heim2001.instReprIntensionalVerbClass.repr : IntensionalVerbClass → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Heim2001.instReprIntensionalVerbClass : Repr IntensionalVerbClass

Equations

• Heim2001.instReprIntensionalVerbClass = { reprPrec := Heim2001.instReprIntensionalVerbClass.repr }

def Heim2001.IntensionalVerbClass.admitsHighDegP : IntensionalVerbClass → Bool

Per IntensionalVerbClass, predict whether high-DegP is admitted.

Equations

• Heim2001.IntensionalVerbClass.deontic.admitsHighDegP = true
• Heim2001.IntensionalVerbClass.possibility.admitsHighDegP = true
• Heim2001.IntensionalVerbClass.epistemic.admitsHighDegP = false
• Heim2001.IntensionalVerbClass.negRaising.admitsHighDegP = false

structure Heim2001.IntensionalVerbDatum : Type

A row of Heim's §2.3 intensional-verb table.

• sentence : String
• verb : String
• verbClass : IntensionalVerbClass
• highDegPAvailable : Bool

  Does the high-DegP reading exist for this verb (with exactly or less)? Determined by verbClass (see verbClass_predicts_highDegPAvailable).

@[implicit_reducible]

instance Heim2001.instReprIntensionalVerbDatum : Repr IntensionalVerbDatum

Equations

• Heim2001.instReprIntensionalVerbDatum = { reprPrec := Heim2001.instReprIntensionalVerbDatum.repr }

def Heim2001.instReprIntensionalVerbDatum.repr : IntensionalVerbDatum → ℕ → Std.Format

Equations

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

def Heim2001.intensionalVerbData : List IntensionalVerbDatum

Heim §2.3, exs. (28)–(36). The 4-vs-4 split is by verbClass; deontic and possibility admit high-DegP, epistemic and negRaising block it.

Equations

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

theorem Heim2001.verbClass_predicts_highDegPAvailable (d : IntensionalVerbDatum) : d ∈ intensionalVerbData → d.highDegPAvailable = d.verbClass.admitsHighDegP

Per-row drift sentry: each datum's highDegPAvailable flag matches its verbClass. Adding/removing a row keeps the witness localized. Replaces the previous aggregate-count theorem (length = 4 ∧ length = 4), which would silently go stale on any data edit.