Heim 2001: Degree Operators and Scope

[Hei01] [Hei99] [Ken99] [Per00] [vS84] [FH06b] [SW02a] [Bec01] [KMcN05] [Sza86]

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 [FH06b] negative islands.

Kennedy's generalization (paper ex. (27)) is formalized via the Heim-Kennedy Constraint substrate (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 Degree.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 [Per00] and Abusch 1994 — paper fn. 16). The alternative ACTUALLY-operator implementation (von Stechow 1984) is formalized in VonStechow1984.lean over the substrate's Semantics/Intensional/Rigidity.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 the substrate's measure-function comparative Degree.comparativeSem (via isGreatest_Iic).

Recent literature this file does not engage

• [SW02a] interval semantics, which Heim's own fn. 21 flags as work that may force her to revise basic assumptions
• [Bec01] intervention effects, parallel to Kennedy's generalization
• [KMcN05] closed-scale adjective behavior under negation

Degree-scope configurations

Heim's DegP-scope LFs for quantified subjects, and the §2.1 monotone collapse arguments.

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

Low-DegP for ∀ ("every girl is taller than 4ft"): each restrictor entity exceeds the threshold.

Equations

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

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

High-DegP for ∀: the maximal degree to which every restrictor entity measures exceeds the threshold.

Equations

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

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

Low-DegP for ∃: some restrictor entity exceeds the threshold.

Equations

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

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

High-DegP for ∃: some degree above the threshold is reached by some restrictor entity.

Equations

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

theorem Heim2001.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 (§2.1), ∀ + more: high-DegP entails low-DegP.

theorem Heim2001.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 (§2.1), ∀ + more: low-DegP entails high-DegP given a minimal witness.

theorem Heim2001.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, ∃ + more: the two scope readings coincide.

def Heim2001.negatedDegreePredicate {Entity : Type u_1} {D : Type u_2} [Preorder D] (μ : Entity → D) (a : Entity) (d : D) : Prop

The negated degree predicate {d : ¬(μ(a) ≥ d)} — the degrees a lacks (p. 220); extensionally Set.Ioi (μ a).

Equations

• Heim2001.negatedDegreePredicate μ a d = ¬μ a ≥ d

theorem Heim2001.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 Set.Ioi (μ a).

Lattice substrate (the Galois identity)

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).

Heim §2.1: monotone collapse (exs 8–16)

theorem Heim2001.heim_collapse_exists {α : Type u_1} {D : Type u_2} [LinearOrder D] (R : α → Prop) (μ : α → D) (t : D) : lowDegP_exists R μ t ↔ 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) : highDegP_forall R μ t → 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) : lowDegP_forall R μ t → 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.

Heim §2.1: negation (exs 17–19)

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 [FH06b] 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 | 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)).

Heim §2.2: Kennedy's generalization (exs 20–27)

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). [BP04] §4 is the dedicated formalization; see BhattPancheva2004.bp_hkc_matches_heim_intensional_data.

Heim §2.3: intensional verb data (exs 28–36)

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").

[BP04] §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.)

@[instance_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.

@[instance_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).

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

Equations

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

@[instance_reducible]

instance Heim2001.instReprIntensionalVerbDatum : Repr IntensionalVerbDatum

Equations

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

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.

Heim §2.4: Russell ambiguity ≠ DegP-scope (exs 37–42)

Heim §3.2: superlative semantic ellipsis (exs 58–64)