Quantifier Composition via Predicate Abstraction

Demonstrates that interp composes quantificational sentences end-to-end: lexicon → syntax tree (with QR traces and binders) → truth conditions.

H&K Pipeline (@cite{heim-kratzer-1998} 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 (∀>∃): every person scopes above some person
• Inverse scope (∃>∀): some person scopes above every person

The two trees differ only in which quantifier is raised higher.

def Semantics.Composition.QuantifierComposition.quantLex : Montague.Lexicon Montague.toyModel

Equations

• One or more equations did not get rendered due to their size.
• Semantics.Composition.QuantifierComposition.quantLex "sleeps" = some { ty := Semantics.Montague.Ty.e ⇒ Semantics.Montague.Ty.t, denot := Semantics.Montague.ToyLexicon.sleeps_sem }
• Semantics.Composition.QuantifierComposition.quantLex "laughs" = some { ty := Semantics.Montague.Ty.e ⇒ Semantics.Montague.Ty.t, denot := Semantics.Montague.ToyLexicon.laughs_sem }
• Semantics.Composition.QuantifierComposition.quantLex word = none

def Semantics.Composition.QuantifierComposition.g₀ : Montague.Variables.Assignment Montague.toyModel

Equations

• Semantics.Composition.QuantifierComposition.g₀ x✝ = Semantics.Montague.ToyEntity.john

def Semantics.Composition.QuantifierComposition.tree_everyStudentSleeps : Core.Tree.Tree Unit String

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

Equations

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

theorem Semantics.Composition.QuantifierComposition.every_student_sleeps_false : Tree.evalTree quantLex g₀ tree_everyStudentSleeps = some false

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

theorem Semantics.Composition.QuantifierComposition.every_student_sleeps_grounding : Tree.evalTree quantLex g₀ tree_everyStudentSleeps = some (Lexical.Determiner.Quantifier.every_sem Montague.toyModel Lexical.Determiner.Quantifier.student_sem Montague.ToyLexicon.sleeps_sem)

Grounding: tree interpretation = direct application of GQ.

def Semantics.Composition.QuantifierComposition.tree_someStudentSleeps : Core.Tree.Tree Unit String

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

Equations

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

theorem Semantics.Composition.QuantifierComposition.some_student_sleeps_true : Tree.evalTree quantLex g₀ tree_someStudentSleeps = some true

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

theorem Semantics.Composition.QuantifierComposition.some_student_sleeps_grounding : Tree.evalTree quantLex g₀ tree_someStudentSleeps = some (Lexical.Determiner.Quantifier.some_sem Montague.toyModel Lexical.Determiner.Quantifier.student_sem Montague.ToyLexicon.sleeps_sem)

Grounding: tree interpretation = direct application.

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

def Semantics.Composition.QuantifierComposition.tree_surface : Core.Tree.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 Semantics.Composition.QuantifierComposition.tree_inverse : Core.Tree.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.

theorem Semantics.Composition.QuantifierComposition.surface_scope_true : Tree.evalTree quantLex g₀ tree_surface = some true

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

theorem Semantics.Composition.QuantifierComposition.inverse_scope_value : Tree.evalTree quantLex g₀ tree_inverse = some false

Inverse scope is also true. (John is seen by everyone: both John and Mary see John? No — Mary sees John ✓, John sees Mary ✓, but John doesn't see John ✗. Check: is there ONE person that everyone sees?)

theorem Semantics.Composition.QuantifierComposition.scope_readings_differ : Tree.evalTree quantLex g₀ tree_surface ≠ Tree.evalTree quantLex g₀ tree_inverse

The two scope readings differ: proof of genuine ambiguity.

theorem Semantics.Composition.QuantifierComposition.surface_scope_grounding : Tree.evalTree quantLex g₀ tree_surface = some (Lexical.Determiner.Quantifier.every_sem Montague.toyModel Lexical.Determiner.Quantifier.person_sem fun (x : Montague.toyModel.interpTy Montague.Ty.e) => Lexical.Determiner.Quantifier.some_sem Montague.toyModel Lexical.Determiner.Quantifier.person_sem fun (y : Montague.toyModel.interpTy Montague.Ty.e) => Montague.ToyLexicon.sees_sem y x)

Surface scope tree = manual ∀>∃ computation.

theorem Semantics.Composition.QuantifierComposition.inverse_scope_grounding : Tree.evalTree quantLex g₀ tree_inverse = some (Lexical.Determiner.Quantifier.some_sem Montague.toyModel Lexical.Determiner.Quantifier.person_sem fun (y : Montague.toyModel.interpTy Montague.Ty.e) => Lexical.Determiner.Quantifier.every_sem Montague.toyModel Lexical.Determiner.Quantifier.person_sem fun (x : Montague.toyModel.interpTy Montague.Ty.e) => Montague.ToyLexicon.sees_sem y x)

Inverse scope tree = manual ∃>∀ computation.

def Semantics.Composition.QuantifierComposition.g₁ : Montague.Variables.Assignment Montague.toyModel

A different initial assignment yields the same result: closed sentences don't depend on the assignment.

Equations

• Semantics.Composition.QuantifierComposition.g₁ x✝ = Semantics.Montague.ToyEntity.mary

theorem Semantics.Composition.QuantifierComposition.assignment_independent : Tree.evalTree quantLex g₀ tree_everyStudentSleeps = Tree.evalTree quantLex g₁ tree_everyStudentSleeps

The same QR tree built 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 Semantics.Composition.QuantifierComposition.synTree_everyStudentSleeps : Core.Tree.Tree Core.Tree.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.

theorem Semantics.Composition.QuantifierComposition.synTree_every_student_sleeps_false : Tree.evalTree quantLex g₀ synTree_everyStudentSleeps = some false

Category-bearing tree yields the same result as category-free tree.

theorem Semantics.Composition.QuantifierComposition.catTree_agrees_with_unitTree : Tree.evalTree quantLex g₀ synTree_everyStudentSleeps = Tree.evalTree quantLex g₀ tree_everyStudentSleeps

Tree Cat String agrees with Tree Unit String.