[HK98]: Type-Driven Composition of Quantifiers

End-to-end verification that the H&K engine (Composition/Tree.lean) composes quantificational sentences as advertised in Ch. 5: lexicon → QR-syntax tree (with traces and binders) → truth conditions. The engine implements TN/NN/FA/IFA/PM/PA; this file feeds it the textbook examples and checks the predictions over a toy model.

H&K Pipeline (Ch. 5)

After Quantifier Raising moves a DP to a higher position, it leaves a trace tₙ and creates a binder node n. Predicate Abstraction (PA) converts the binder + body into λx. ⟦body⟧^{g[n↦x]}, producing a predicate that the raised quantifier takes as its scope argument.

"Every student sleeps" after QR:

[S [DP [D every] [N student]] [1 [S [t₁] [VP sleeps]]]]

Evaluated as:

1. ⟦t₁⟧^g = g(1) (Traces rule)
2. ⟦sleeps⟧ = sleeps' (TN)
3. ⟦[t₁ sleeps]⟧^g = sleeps'(g(1)) (FA)
4. ⟦[1 [t₁ sleeps]]⟧^g = λx. sleeps'(x) (PA)
5. ⟦every student⟧ = every'(student') (FA)
6. ⟦S⟧ = every'(student')(λx. sleeps'(x)) (FA)

Scope ambiguity

"Everybody loves somebody" yields two readings from two QR structures — surface scope (∀>∃) and inverse scope (∃>∀) — that differ only in which quantifier is raised higher. scope_readings_differ certifies that the two trees compute genuinely distinct propositions in the toy model.

Note on Prop-valued .t

With interpTy .t = Prop, the engine produces Prop-valued truth conditions directly. Theorems verify these at the Prop level rather than via evalTree (which would demand a blanket Decidable (∀ p : Prop, p) instance).

Model and lexicon

def HeimKratzer1998.quantLex : Semantics.Montague.Lexicon Semantics.Montague.ToyEntity Unit

Equations

• HeimKratzer1998.quantLex "every" = some { ty := Quantification.Quantifier.Ty.det, denot := Quantification.every_sem }
• HeimKratzer1998.quantLex "some" = some { ty := Quantification.Quantifier.Ty.det, denot := Quantification.some_sem }
• HeimKratzer1998.quantLex "student" = some { ty := Intensional.Ty.e ⇒ Intensional.Ty.t, denot := Semantics.Montague.ToyLexicon.student_sem }
• HeimKratzer1998.quantLex "person" = some { ty := Intensional.Ty.e ⇒ Intensional.Ty.t, denot := Semantics.Montague.ToyLexicon.person_sem }
• HeimKratzer1998.quantLex "sleeps" = some { ty := Intensional.Ty.e ⇒ Intensional.Ty.t, denot := Semantics.Montague.ToyLexicon.sleeps_sem }
• HeimKratzer1998.quantLex "laughs" = some { ty := Intensional.Ty.e ⇒ Intensional.Ty.t, denot := Semantics.Montague.ToyLexicon.laughs_sem }
• HeimKratzer1998.quantLex "sees" = some { ty := Intensional.Ty.e ⇒ Intensional.Ty.e ⇒ Intensional.Ty.t, denot := Semantics.Montague.ToyLexicon.sees_sem }
• HeimKratzer1998.quantLex word = none

def HeimKratzer1998.g₀ : Core.Assignment Semantics.Montague.ToyEntity

Equations

• HeimKratzer1998.g₀ x✝ = Semantics.Montague.ToyEntity.john

"Every student sleeps"

def HeimKratzer1998.tree_everyStudentSleeps : Syntax.Tree Unit String

QR tree: [S [DP every student] [1 [S t₁ sleeps]]]

Equations

• HeimKratzer1998.tree_everyStudentSleeps = ((Syntax.Tree.leaf "every").bin (Syntax.Tree.leaf "student")).bin (Syntax.Tree.binder 1 ((Syntax.Tree.tr 1).bin (Syntax.Tree.leaf "sleeps")))

theorem HeimKratzer1998.every_student_sleeps_false : ¬Quantification.every_sem Semantics.Montague.ToyLexicon.student_sem Semantics.Montague.ToyLexicon.sleeps_sem

Every student sleeps is false (Mary is a student but doesn't sleep).

def HeimKratzer1998.tree_someStudentSleeps : Syntax.Tree Unit String

QR tree: [S [DP some student] [1 [S t₁ sleeps]]]

Equations

• HeimKratzer1998.tree_someStudentSleeps = ((Syntax.Tree.leaf "some").bin (Syntax.Tree.leaf "student")).bin (Syntax.Tree.binder 1 ((Syntax.Tree.tr 1).bin (Syntax.Tree.leaf "sleeps")))

theorem HeimKratzer1998.some_student_sleeps_true : Quantification.some_sem Semantics.Montague.ToyLexicon.student_sem Semantics.Montague.ToyLexicon.sleeps_sem

Some student sleeps = true (John is a student and sleeps).

Scope ambiguity: "Every person sees some person"

Two QR structures yield two scope readings. The trees differ only in which quantifier occupies the higher position.

def HeimKratzer1998.tree_surface : Syntax.Tree Unit String

Surface scope (∀>∃):

[S [DP every person] [1 [S [DP some person] [2 [S t₁ [VP sees t₂]]]]]]

∀x[person(x) → ∃y[person(y) ∧ sees(x,y)]]

Equations

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

def HeimKratzer1998.tree_inverse : Syntax.Tree Unit String

Inverse scope (∃>∀):

[S [DP some person] [2 [S [DP every person] [1 [S t₁ [VP sees t₂]]]]]]

∃y[person(y) ∧ ∀x[person(x) → sees(x,y)]]

Equations

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

@[reducible, inline]

abbrev HeimKratzer1998.surfaceScopeProp : Prop

Surface scope Prop.

Equations

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

@[reducible, inline]

abbrev HeimKratzer1998.inverseScopeProp : Prop

Inverse scope Prop.

Equations

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

theorem HeimKratzer1998.surface_scope_true : surfaceScopeProp

Surface scope is true in the toy model. (John sees Mary and Mary sees John — each person sees some person.)

theorem HeimKratzer1998.inverse_scope_false : ¬inverseScopeProp

Inverse scope is false. (No single person is seen by everyone — John doesn't see John, Mary doesn't see Mary.)

theorem HeimKratzer1998.scope_readings_differ : surfaceScopeProp ≠ inverseScopeProp

The two scope readings differ: proof of genuine ambiguity.

The engine computes the readings

The QR trees and the hand-written surfaceScopeProp/inverseScopeProp are linked by interp: running the engine on a tree yields exactly the corresponding reading. So the scope-ambiguity result is a fact about the engine's output, not a parallel re-implementation alongside it.

theorem HeimKratzer1998.interp_computes_surface : Semantics.Composition.Tree.interp Semantics.Montague.ToyEntity Unit quantLex g₀ tree_surface = some { ty := Intensional.Ty.t, val := surfaceScopeProp }

Surface scope: the engine computes the hand-written reading.

theorem HeimKratzer1998.interp_computes_inverse : Semantics.Composition.Tree.interp Semantics.Montague.ToyEntity Unit quantLex g₀ tree_inverse = some { ty := Intensional.Ty.t, val := inverseScopeProp }

Inverse scope: likewise.

theorem HeimKratzer1998.scope_ambiguity_computed : Semantics.Composition.Tree.interp Semantics.Montague.ToyEntity Unit quantLex g₀ tree_surface ≠ Semantics.Composition.Tree.interp Semantics.Montague.ToyEntity Unit quantLex g₀ tree_inverse

Scope ambiguity, stated about the engine: the two QR derivations interpret to genuinely different meanings.

Unified tree: the same sentence with UD categories

The QR tree as Tree Cat String — carrying real UD-grounded categories on every node. interp ignores the categories and produces identical truth conditions to the category-free Tree Unit String version.

def HeimKratzer1998.synTree_everyStudentSleeps : Syntax.Tree Syntax.Cat String

QR tree with UD categories: [S [DP [Det every] [N student]] [1 [S [t₁:NP] [VP sleeps]]]]

Equations

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

First-order reduction

The textbook trees are in the compiled FO fragment (Composition/Reduction.lean): they compile to mathlib FirstOrder.Language.Formulas, and by the agreement theorem the engine's truth conditions are model-theoretic realization over toyModel.

theorem HeimKratzer1998.interp_eq_realize {t : Syntax.Tree Unit String} {φ : Semantics.Montague.toyLang.Formula ℕ} (h : Semantics.Composition.compileFO { } Semantics.Montague.toyNaming t = some φ) (g : Core.Assignment Semantics.Montague.ToyEntity) : Semantics.Composition.Tree.interp Semantics.Montague.ToyEntity Unit (Semantics.Montague.toyModel.lexiconFO { } Semantics.Montague.toyNaming ()) g t = some { ty := Intensional.Ty.t, val := Semantics.Montague.toyModel.realizeAt () φ g }

The agreement theorem instantiated at the toy model: for any tree in the fragment, engine truth conditions are Realize of the compiled formula.

theorem HeimKratzer1998.someStudentSleeps_holds (g : Core.Assignment Semantics.Montague.ToyEntity) : Semantics.Composition.HoldsAt Semantics.Montague.toyModel (Semantics.Montague.toyModel.lexiconFO { } Semantics.Montague.toyNaming ()) g tree_someStudentSleeps

"Some student sleeps" holds in the toy model, via the engine.

def HeimKratzer1998.tree_conj : Syntax.Tree Unit String

"John sleeps and Mary laughs".

Equations

• HeimKratzer1998.tree_conj = ((Syntax.Tree.leaf "John").bin (Syntax.Tree.leaf "sleeps")).bin ((Syntax.Tree.leaf "and").bin ((Syntax.Tree.leaf "Mary").bin (Syntax.Tree.leaf "laughs")))

theorem HeimKratzer1998.conj_entails_first (g : Core.Assignment Semantics.Montague.ToyEntity) : Semantics.Composition.HoldsAt Semantics.Montague.toyModel (Semantics.Montague.toyModel.lexiconFO { } Semantics.Montague.toyNaming ()) g tree_conj → Semantics.Composition.HoldsAt Semantics.Montague.toyModel (Semantics.Montague.toyModel.lexiconFO { } Semantics.Montague.toyNaming ()) g ((Syntax.Tree.leaf "John").bin (Syntax.Tree.leaf "sleeps"))

Consequence transfer: conjunction elimination is a first-order consequence, so the entailment holds in the toy model — and by the same theorem in every composition model interpreting the signature.

Minimalist trace interpretation (relocated from Minimalist/TraceInterpretation.lean)

Traces left by movement are interpreted as variables bound by λ-abstraction at the landing site (H&K Ch. 5, 7).

Rules

1. Trace Interpretation: a trace t_n is interpreted as g(n) ⟦t_n⟧^g = g(n)

2. Predicate Abstraction (the λ-abstraction at the landing site) and the relative-clause denotation it feeds are framework-neutral composition rules, so they live in Semantics/Composition/Abstraction.lean; this section is the Minimalist trace machinery that applies them.

Trace convention

On the index-free SO carrier ([MCB25] Def 1.2.1, chain identity is workspace-level) a trace is the single bare trace leaf SO.traceLeaf, recognized by SO.isTrace. The semantic trace index n is not carried by the leaf: it is supplied by the binder (λ-abstraction) at the landing site, exactly as in the H&K rule ⟦t_n⟧^g = g(n). The interpretation functions below therefore take the index as an explicit argument.

@[reducible, inline]

abbrev HeimKratzer1998.interpTrace {E : Type} (n : ℕ) : Intensional.Variables.DenotG E Unit Intensional.Ty.e

Interpret a trace as a variable: ⟦t_n⟧^g = g(n).

Heim and Kratzer's trace interpretation rule: traces and pronouns are semantically identical, looked up via the assignment function. The trace index n matches the binder (λ-abstraction) at the landing site of movement.

abbrev because trace interpretation IS pronoun interpretation — the only difference is the syntactic source.

Equations

• HeimKratzer1998.interpTrace n = Intensional.Variables.interpPronoun n

def HeimKratzer1998.interpMovement {E W : Type} (n : ℕ) (bodyWithTrace : Intensional.Variables.DenotG E W Intensional.Ty.t) : Intensional.Variables.DenotG E W (Intensional.Ty.e ⇒ Intensional.Ty.t)

Interpret a simple movement configuration:

• A trace t_n in some position
• An operator binding that trace from a higher position

Returns the predicate λx. ⟦body(t_n := x)⟧

Equations

• HeimKratzer1998.interpMovement n bodyWithTrace = Intensional.Variables.lambdaAbsG n bodyWithTrace

structure HeimKratzer1998.InterpContext (E : Type) : Type

A semantic interpretation context pairs a model with an assignment.

• assignment : Core.Assignment E

def HeimKratzer1998.soSemanticType (so : Minimalist.SyntacticObject) : Option Intensional.Ty

The semantic type corresponding to a syntactic object.

• A trace leaf has type e (it denotes an entity)
• Other SOs need lexical lookup

Equations

• HeimKratzer1998.soSemanticType so = if Minimalist.SO.isTrace so then some Intensional.Ty.e else none

def HeimKratzer1998.interpSOTrace {E : Type} (n : ℕ) (so : Minimalist.SyntacticObject) : Option (Intensional.Variables.DenotG E Unit Intensional.Ty.e)

Interpret a trace leaf in a syntactic object at a given index.

On the index-free SO carrier the trace leaf carries no index; the binder at the landing site supplies n (H&K's ⟦t_n⟧^g = g(n)). Returns none when so is not the trace leaf.

Equations

• HeimKratzer1998.interpSOTrace n so = if Minimalist.SO.isTrace so then some (HeimKratzer1998.interpTrace n) else none

@[simp]

theorem HeimKratzer1998.soSemanticType_traceLeaf : soSemanticType Minimalist.SO.traceLeaf = some Intensional.Ty.e

The trace leaf is recognized as type e.

@[simp]

theorem HeimKratzer1998.soSemanticType_lexLeaf (tok : Minimalist.LIToken) : soSemanticType (Minimalist.SO.lexLeaf tok) = none

A lexical leaf is not a trace, so it gets no carrier-level type.

theorem HeimKratzer1998.trace_indices_independent {E : Type} (n₁ n₂ : ℕ) (h : n₁ ≠ n₂) (x : E) (g : Core.Assignment E) : interpTrace n₁ (Function.update g n₂ x) = interpTrace n₁ g

Different indices yield independent interpretations.

theorem HeimKratzer1998.abstraction_binds_correct_variable {E : Type} (n : ℕ) (g : Core.Assignment E) (x : E) : interpTrace n (Function.update g n x) = x

Predicate abstraction creates the right binding: the abstracted variable is bound, other variables are free.