Documentation

Linglib.Studies.Montague1973

Montague (1973): The Proper Treatment of Quantification in Ordinary English #

[Mon73], with the category-to-type correspondence in the form adopted by [dowty-wall-peters-1981] (Ch. 7, Bennett's simplification).

PTQ's two central moves, exercised over the shared Semantics.Montague toy fragment:

Grounding, not restipulation #

The category-to-type function f and the named PTQ categories come from the canonical Intensional.CategoryType (PtqCat/catToTy), so the IL types here are the paper's — verbs and common nouns take individual concepts ⟨s,e⟩, not bare entities. The two scope readings are the shared GQ-level operators Quantification.Polyadic.surfaceScope/inverseScope over the propositional denotations every_sem/some_sem, and the ambiguous string is a Semantics.Scope.ScopeDerivation. This makes PTQ's quantifying-in directly comparable to the QR (HeimKratzer1998), Glue (Asudeh2022), and RSA (ScontrasPearl2021) treatments of the same ambiguity, which target the same substrate.

PTQ's distinctive intensional payload — individual concepts doing semantic work in the temperature/price puzzle ("the temperature is ninety but it is rising") and the de dicto/de re ambiguity of "John seeks a unicorn" — needs a model with a nontrivial index set and is left to a dedicated intensional study; the toy fragment here is extensional (W = Unit), so the "sees" example exercises only the quantificational, not the intensional, side of PTQ.

Predication #

Compositional truth conditions by direct function application over the toy fragment.

Category-to-type correspondence #

PTQ assigns every syntactic category a unique IL type via f (catToTy in Intensional.CategoryType). The facts below anchor the categories relevant to quantification; the general machinery lives in the substrate.

A term phrase (category T, e.g. "every student", "John") denotes a generalized quantifier over property-intensions of individual concepts: f(T) = ⟨⟨s, ⟨⟨s,e⟩, t⟩⟩, t⟩. Treating "every student" as a function on (intensions of) VP-meanings rather than as an entity is exactly what lets scope be assigned by the grammar.

A determiner (category T/CN, e.g. "every", "a") combines with a common-noun intension to yield a term-phrase meaning.

Common nouns and intransitive verbs share the IL type of sets of individual concepts ⟨⟨s,e⟩, t⟩ — PTQ's device for the temperature/price puzzle, where a verb predicates of a concept whose value varies, not of a fixed individual.

Scope ambiguity via quantifying-in (S14) #

"Every student sees a person" has two readings, generated by quantifying the two term phrases in at different points (PTQ's S14). They are the two linear Polyadic readings of an every/some pair:

The paper's own non-intensional illustration is "a woman loves every man" (§4), introduced precisely to show "that ambiguity can arise even when there is no element of intensionality, simply because quantifying terms may be introduced in more than one order."

@[reducible, inline]

The toy "sees" relation as a subject-first binary predicate x sees y, read off the (object-first) fragment denotation sees_sem. abbrev so the Decidable (sees_sem _ _) instance below transports to seesRel.

Equations
Instances For
    @[implicit_reducible]

    Each concrete sees_sem a b reduces to True/False, mirroring the fragment's own DecidablePred pattern.

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

    ∃∀ ⊨ ∀∃. For an every/some pair, the inverse (wide-existential) reading entails the surface (wide-universal) reading, over any domain, restrictors, and relation. PTQ's S14 generates both readings; this is the one-directional entailment between them, and it is why a context can never make the inverse reading true without the surface reading being true too.

    "Every student sees a person" as a single syntactic form carrying both scope-indexed meanings, in the shared ScopeDerivation representation — the same type targeted by HeimKratzer1998 (QR), Asudeh2022 (Glue), and ScontrasPearl2021 (RSA).

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      def Montague1973.surfaceTruth :
      UnitBool

      Truth of the surface (∀∃) reading over the single extensional world. The Prop is written explicitly (rather than as everyStudentSeesAPerson.meaningAt .surface) so Decidable synthesises over ToyEntity; surfaceTruth_iff certifies it is the same reading.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        def Montague1973.inverseTruth :
        UnitBool

        Truth of the inverse (∃∀) reading; inverseTruth_iff ties it to the ScopeDerivation.

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

          The Bool surface truth function reflects the ScopeDerivation's surface meaning — certifying that the explicitly-written Prop in surfaceTruth is everyStudentSeesAPerson.meaningAt .surface, not merely asserted to be.

          The Bool inverse truth function reflects the ScopeDerivation's inverse meaning.

          In the shared ScopeEntailment vocabulary (cf. ScontrasPearl2021.every_not_scope_entailment, which gets surfaceEntailsInverse for "every…not"), the every/some pair classifies as inverseEntailsSurface: inverse ⊨ surface (held across the checked world), surface ⊭ inverse (the toy world makes surface true and inverse false). The general direction is every_some_inverse_entails_surface.