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.

def Semantics.Dynamic.DynamicGQ.Basic.Evar {S : Type u_1} {E : Type u_2} [Core.DynamicTy2.AssignmentStructure S E] (v : Core.DynamicTy2.Dref S E) (P : E → Prop) : Core.DynProp.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

• Semantics.Dynamic.DynamicGQ.Basic.Evar v P i j = ∃ (x : E), P x ∧ j = Semantics.Dynamic.Core.DynamicTy2.AssignmentStructure.extend i v x

def Semantics.Dynamic.DynamicGQ.Basic.Mvar {S : Type u_1} {E : Type u_2} (v : Core.DynamicTy2.Dref S E) (D : Core.DynProp.DRS S) [PartialOrder E] : Core.DynProp.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

• Semantics.Dynamic.DynamicGQ.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 Semantics.Dynamic.DynamicGQ.Basic.CardTest {S : Type u_1} {E : Type u_2} (v : Core.DynamicTy2.Dref S E) (n : ℕ) [PartialOrder E] [Fintype E] : Core.DynProp.DRS S

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

Equations

• Semantics.Dynamic.DynamicGQ.Basic.CardTest v n i j = (i = j ∧ Mereology.atomCount E (v j) = n)

def Semantics.Dynamic.DynamicGQ.Basic.sawDRS {S : Type u_1} {E : Type u_2} (u v : Core.DynamicTy2.Dref S E) (R : E → E → Prop) : Core.DynProp.DRS S

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

Equations

• Semantics.Dynamic.DynamicGQ.Basic.sawDRS u v R = [fun (i : S) => R (u i) (v i)]

def Semantics.Dynamic.DynamicGQ.Basic.exactlyN_pw {S : Type u_1} {E : Type u_2} [Core.DynamicTy2.AssignmentStructure S E] [PartialOrder E] [Fintype E] (v : Core.DynamicTy2.Dref S E) (P : E → Prop) (n : ℕ) : Core.DynProp.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 Semantics.Dynamic.DynamicGQ.Basic.pseudoCumulative {S : Type u_1} {E : Type u_2} [Core.DynamicTy2.AssignmentStructure S E] [PartialOrder E] [Fintype E] (v u : Core.DynamicTy2.Dref S E) (boys movies : E → Prop) (saw' : E → E → Prop) : Core.DynProp.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 Semantics.Dynamic.DynamicGQ.Basic.cumulative {S : Type u_1} {E : Type u_2} [Core.DynamicTy2.AssignmentStructure S E] [PartialOrder E] [Fintype E] (v u : Core.DynamicTy2.Dref S E) (boys movies : E → Prop) (saw' : E → E → Prop) : Core.DynProp.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.