Documentation

Linglib.Theories.Semantics.Composition.QuantifierComposition

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:

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

Note on Prop-valued .t #

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

source
def Semantics.Composition.QuantifierComposition.quantLex :
Montague.Lexicon Montague.toyModel
Equations
Instances For
    source
    def Semantics.Composition.QuantifierComposition.g₀ :
    Core.Assignment Montague.toyModel.Entity
    Equations
    Instances For
      source
      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.
      Instances For
        source
        theorem Semantics.Composition.QuantifierComposition.every_student_sleeps_false :
        ¬Quantification.Quantifier.every_sem Montague.toyModel Quantification.Quantifier.student_sem Montague.ToyLexicon.sleeps_sem

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

        source
        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.
        Instances For
          source
          theorem Semantics.Composition.QuantifierComposition.some_student_sleeps_true :
          Quantification.Quantifier.some_sem Montague.toyModel Quantification.Quantifier.student_sem Montague.ToyLexicon.sleeps_sem

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

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

          source
          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.
          Instances For
            source
            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.
            Instances For
              source
              @[reducible, inline]
              abbrev Semantics.Composition.QuantifierComposition.surfaceScopeProp :
              Prop

              Surface scope Prop.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                @[reducible, inline]
                abbrev Semantics.Composition.QuantifierComposition.inverseScopeProp :
                Prop

                Inverse scope Prop.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  theorem Semantics.Composition.QuantifierComposition.surface_scope_true :
                  surfaceScopeProp

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

                  source
                  theorem Semantics.Composition.QuantifierComposition.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.)

                  source
                  theorem Semantics.Composition.QuantifierComposition.scope_readings_differ :
                  surfaceScopeProp ≠ inverseScopeProp

                  The two scope readings differ: proof of genuine ambiguity.

                  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.

                  source
                  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.
                  Instances For