Pointwise Dynamic Generalized Quantifiers

@cite{brasoveanu-2007} @cite{charlow-2021}

@cite{muskens-1996}/@cite{brasoveanu-2007}-style dynamic GQ operators defined over the pointwise DRS S := S → S → Prop type. These correspond to @cite{charlow-2021} §2.

The key operators:

• Evar: existential dref introduction (equation 17)
• Mvar: mereological maximization (equation 18)
• CardTest: cardinality test (equation 19)
• exactlyN_pw: composed modified numeral "exactly N" (pointwise)

Charlow shows that in the pointwise setting, sequencing Mvar inside vs outside CardTest yields pseudo-cumulative vs cumulative readings — and the pointwise system can only derive pseudo-cumulative.

Cross-cutting smell: five dynamic-GQ variants, no "which to use" map

Quantification/Dynamic/ hosts five formalizations of dynamic generalized quantifiers, each coping with the cumulative-reading problem differently. They are not ranked or ordered; downstream consumers must pick by hand.

Variant	State type	Cumulative?	File
Pointwise (this file)	S → S → Prop	✗ pseudo-cumulative only	Quantification/Dynamic/Basic.lean
Update-theoretic	State W E → State W E	✓ via non-distributive Mvar_u	Quantification/Dynamic/UpdateTheoretic.lean
Higher-order tower	((DRS S → DRS S) → DRS S) → DRS S	✓ via LOWER placement	Quantification/Dynamic/HigherOrder.lean
Post-suppositional	Writer (DRS S) A	✓ via deferred cardinality tests	Quantification/Dynamic/PostSuppositional.lean
Subtype-polymorphic	DRS S with Completeness enum	rules out pseudo-cumulative by typing	Quantification/Dynamic/SubtypePolymorphism.lean

All five are @cite{charlow-2021}'s work — the paper canvasses them as alternative repairs to the pointwise system's failure on exactly 3 boys saw exactly 5 movies. The variants are not equivalent: Update-theoretic and Higher-order produce genuine cumulative readings operationally; Post-suppositional defers the cardinality test as conventional implicature; Subtype-polymorphic blocks the pseudo- cumulative reading by type discipline rather than by deriving the cumulative one. New consumers should pick based on what they need: flat state-threading (Update-theoretic), explicit scope (Higher-order), post-suppositional content (Post-suppositional), or static well- formedness (Subtype-polymorphic). Pointwise is the baseline and the empirical counterexample, kept here primarily as the reference against which the other four are measured.

def Phenomena.Plurals.Studies.Charlow2021.Basic.Evar {S : Type u_1} {E : Type u_2} [Semantics.Dynamic.Core.AssignmentStructure S E] (v : Semantics.Dynamic.Core.Dref S E) (P : E → Prop) : Semantics.Dynamic.Core.DRS S

Existential dref introduction (equation 17): introduce a new referent satisfying P into the assignment at dref v. Evar v P i j ⟺ ∃x. P(x) ∧ j = extend(i, v, x)

Equations

• Phenomena.Plurals.Studies.Charlow2021.Basic.Evar v P i j = ∃ (x : E), P x ∧ j = Semantics.Dynamic.Core.AssignmentStructure.extend i v x

def Phenomena.Plurals.Studies.Charlow2021.Basic.Mvar {S : Type u_1} {E : Type u_2} (v : Semantics.Dynamic.Core.Dref S E) (D : Semantics.Dynamic.Core.DRS S) [PartialOrder E] : Semantics.Dynamic.Core.DRS S

Mereological maximization (equation 18): retain only assignments where v is maximal in the output set of D. In the pointwise setting, this checks maximality of v(j) among all j reachable from i via D.

Equations

• Phenomena.Plurals.Studies.Charlow2021.Basic.Mvar v D i j = (D i j ∧ Mereology.isMaximal (fun (x : E) => ∃ (k : S), D i k ∧ v k = x) (v j))

def Phenomena.Plurals.Studies.Charlow2021.Basic.CardTest {S : Type u_1} {E : Type u_2} (v : Semantics.Dynamic.Core.Dref S E) (n : ℕ) [PartialOrder E] [Fintype E] : Semantics.Dynamic.Core.DRS S

Cardinality test (equation 19): test that atomCount of v equals n. Identity on assignments (a test in the dynamic sense).

Equations

• Phenomena.Plurals.Studies.Charlow2021.Basic.CardTest v n i j = (i = j ∧ Mereology.atomCount E (v j) = n)

def Phenomena.Plurals.Studies.Charlow2021.Basic.sawDRS {S : Type u_1} {E : Type u_2} (u v : Semantics.Dynamic.Core.Dref S E) (R : E → E → Prop) : Semantics.Dynamic.Core.DRS S

Transitive verb as DRS: test that R holds between two drefs.

Equations

• Phenomena.Plurals.Studies.Charlow2021.Basic.sawDRS u v R = [fun (i : S) => R (u i) (v i)]

def Phenomena.Plurals.Studies.Charlow2021.Basic.exactlyN_pw {S : Type u_1} {E : Type u_2} [Semantics.Dynamic.Core.AssignmentStructure S E] [PartialOrder E] [Fintype E] (v : Semantics.Dynamic.Core.Dref S E) (P : E → Prop) (n : ℕ) : Semantics.Dynamic.Core.DRS S

Composed pointwise "exactly N": E^v; M_v; n_v (equation 20).

Equations

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

def Phenomena.Plurals.Studies.Charlow2021.Basic.pseudoCumulative {S : Type u_1} {E : Type u_2} [Semantics.Dynamic.Core.AssignmentStructure S E] [PartialOrder E] [Fintype E] (v u : Semantics.Dynamic.Core.Dref S E) (boys movies : E → Prop) (saw' : E → E → Prop) : Semantics.Dynamic.Core.DRS S

Pseudo-cumulative formula (5): M_v scopes over the cardinality test on u. "Exactly 3 boys saw exactly 5 movies" with pseudo-cumulative reading: M_v(E^v boys; M_u(E^u movies; saw u v); 5_u); 3_v

Equations

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

def Phenomena.Plurals.Studies.Charlow2021.Basic.cumulative {S : Type u_1} {E : Type u_2} [Semantics.Dynamic.Core.AssignmentStructure S E] [PartialOrder E] [Fintype E] (v u : Semantics.Dynamic.Core.Dref S E) (boys movies : E → Prop) (saw' : E → E → Prop) : Semantics.Dynamic.Core.DRS S

Cumulative formula (6): cardinality tests scope outside both M operators. M_v(E^v boys; M_u(E^u movies; saw u v)); 5_u; 3_v

Equations

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