Heim's Sentential Operator Approach

@cite{heim-2001} @cite{heim-2006}

@cite{heim-2001} "Degree Operators and Scope": the comparative morpheme -er is a sentential operator that introduces degree variables via λ-abstraction, rather than being a degree quantifier as in Kennedy's approach.

Key Differences from Kennedy

Feature	Kennedy	Heim
Type of -er	degree quantifier	sentential operator
Degree binding	-er binds degree var	λ-abstraction
Than-clause	degree clause (type d)	degree predicate (d → t)
Scope	DP-internal scope	clausal scope

Denotation

⟦-er⟧ = λD₂.λD₁. max(D₁) > max(D₂)

where D₁ and D₂ are degree predicates (sets of degrees):

• D₁ = the matrix degree clause (abstracting over d)
• D₂ = the than-clause degree predicate

Scope Predictions

The sentential operator approach predicts scope interactions with other operators (negation, modals, quantifiers) that the degree quantifier approach does not, because -er takes scope at the clause level.

def Semantics.Degree.Frameworks.Heim.DegreePredicate (D : Type u_1) : Type u_1

A degree predicate: a set of degrees. In Heim's framework, both the matrix clause and the than-clause denote degree predicates after degree abstraction.

Example: "John is d-tall" = λd. height(John) ≥ d This is the same as Kennedy's adjective denotation, but Heim treats it as the result of degree abstraction rather than the lexical entry of the adjective.

Equations

• Semantics.Degree.Frameworks.Heim.DegreePredicate D = (D → Prop)

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

The matrix degree predicate: abstracting over the degree variable in "A is d-tall" yields λd. μ(A) ≥ d. This is the degree set of A.

Equations

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

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

The than-clause degree predicate: abstracting over the degree variable in "B is d-tall" yields λd. μ(B) ≥ d. This is the degree set of B.

Equations

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

def Semantics.Degree.Frameworks.Heim.heimComparative {D : Type u_1} [LinearOrder D] (d1Max d2Max : D) : Prop

Heim's -er as a sentential operator over degree predicates.

⟦-er⟧(D₂)(D₁) = max(D₁) > max(D₂)

When D₁ and D₂ are degree sets of entities A and B, this yields: height(A) > height(B).

Equations

• Semantics.Degree.Frameworks.Heim.heimComparative d1Max d2Max = (d1Max > d2Max)

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

Heim comparative with measure function: same truth conditions as Kennedy, but different compositional derivation.

"A is taller than B" via Heim: ⟦-er⟧(λd. height(B) ≥ d)(λd. height(A) ≥ d) = height(A) > height(B)

Equations

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

inductive Semantics.Degree.Frameworks.Heim.ComparativeScopeReading : Type

Heim's approach predicts scope ambiguities with modals. "The paper is required to be longer than that."

• -er > required: there's a length d such that the paper must be at least d-long
• required > -er: for each requirement, the paper meets the length threshold

Kennedy's degree quantifier approach does not predict the wide-scope -er reading (because -er is DP-internal).

• wideScope : ComparativeScopeReading
• narrowScope : ComparativeScopeReading

instance Semantics.Degree.Frameworks.Heim.instDecidableEqComparativeScopeReading : DecidableEq ComparativeScopeReading

Equations

• Semantics.Degree.Frameworks.Heim.instDecidableEqComparativeScopeReading x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Degree.Frameworks.Heim.instBEqComparativeScopeReading.beq : ComparativeScopeReading → ComparativeScopeReading → Bool

Equations

• Semantics.Degree.Frameworks.Heim.instBEqComparativeScopeReading.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Degree.Frameworks.Heim.instBEqComparativeScopeReading : BEq ComparativeScopeReading

Equations

• Semantics.Degree.Frameworks.Heim.instBEqComparativeScopeReading = { beq := Semantics.Degree.Frameworks.Heim.instBEqComparativeScopeReading.beq }

instance Semantics.Degree.Frameworks.Heim.instReprComparativeScopeReading : Repr ComparativeScopeReading

Equations

• Semantics.Degree.Frameworks.Heim.instReprComparativeScopeReading = { reprPrec := Semantics.Degree.Frameworks.Heim.instReprComparativeScopeReading.repr }

def Semantics.Degree.Frameworks.Heim.instReprComparativeScopeReading.repr : ComparativeScopeReading → ℕ → Std.Format

Equations

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

theorem Semantics.Degree.Frameworks.Heim.kennedy_heim_extensional_equivalence {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (a b : Entity) : heimComparativeWithMeasure μ a b ↔ Kennedy.kennedyComparative μ a b

Extensional equivalence: Kennedy and Heim yield the same truth conditions for simple comparatives. They differ only in scope predictions with other operators.