Documentation

Linglib.Semantics.Quantification.Quantifier

Generalized quantifiers: typed bridge #

[BC81] [KS86] [PW06]

The GQ substrate (concrete denotations like every_sem, most_sem, … plus their properties: conservativity, monotonicity, smoothness, quantity, proportionality, etc.) lives in Quantification.{Basic, Counting}.

This file is the typed layer: the Ty.det semantic type and the Type-Shifting bridge A_eq_some_sem. Toy-witnessed examples and counterexamples live in Studies/BarwiseCooper1981.lean and Studies/KeenanStavi1986.lean. The threshold-parametric GQT scale-model (gqtMeaning) is van Tiel's foil and lives in Studies/VanTielEtAl2021.lean.

Semantic-type alias #

source
def Quantification.Quantifier.Ty.det :
Intensional.Ty

The determiner type ⟨⟨e,t⟩,⟨⟨e,t⟩,t⟩⟩.

Equations
Instances For

    Existential-closure bridge: A (Partee existential closure) = some_sem #

    A (type-shifting bridge in Composition.TypeShifting) and some_sem are both Type*-polymorphic over the entity domain. The bridge is one direction.

    source
    theorem Quantification.Quantifier.A_eq_some_sem (E : Type) (domain : List E) (hComplete : ∀ (x : E), x ∈ domain) :
    Semantics.Composition.TypeShifting.A domain = some_sem

    Partee's A (existential closure) equals B&C's ⟦some⟧ over a complete finite domain. Both compute λR.λS. ∃x. R(x) ∧ S(x).