Keenan & Stavi (1986): A Semantic Characterization of Determiners

[KS86] characterize the possible determiner denotations of natural language as the conservative functions, and classify which determiners are existential. This file holds the toy-witnessed counterexamples to those properties for specific determiners: the artificial m_sem fails conservativity, and every/most fail existentiality. The witness type is the toy fragment's ToyEntity.

The property definitions (Conservative, Existential) live in Quantification; positive results for English determiners live there and in Studies/BarwiseCooper1981.lean.

theorem KeenanStavi1986.m_not_conservative : ¬Quantification.Conservative Quantification.m_sem

m_sem is not conservative: it inspects B outside A.

theorem KeenanStavi1986.every_not_existential : ¬Quantification.Existential Quantification.every_sem

⟦every⟧ is NOT existential (K&S §3.3).

theorem KeenanStavi1986.most_not_existential : ¬Quantification.Existential Quantification.most_sem

⟦most⟧ is NOT existential (K&S §3.3).