Update-Theoretic Dynamic Generalized Quantifiers

@cite{charlow-2021}

Same operators as DynamicGQ.Basic, but defined directly over StateCCP W E := State W E → State W E — @cite{charlow-2021}'s main contribution.

The key insight: Mvar_u (equation 78) maximizes over the entire context, not per-assignment. This makes it non-distributive, which is exactly what produces cumulative readings automatically.

Main results

• Mvar_u_nondistributive: M_v is not distributive (p. 33 of @cite{charlow-2021})
• CardTest_u_distributive: cardinality tests ARE distributive
• sentenceMeaning_u: the full two-quantifier composed meaning (eq. 82)
• exactlyN_u_distributive: the single-quantifier pipeline (no nuclear scope) is distributive

def Semantics.Dynamic.DynamicGQ.UpdateTheoretic.Evar_u {W : Type u_1} {E : Type u_2} (v : ℕ) (P : E → Prop) : Core.StateCCP W E

Existential dref introduction at the state level (equation 74): for each world-assignment pair in the context, non-deterministically extend the assignment at position v with some entity satisfying P.

Equations

• Semantics.Dynamic.DynamicGQ.UpdateTheoretic.Evar_u v P s = {p : W × Core.Assignment E | ∃ q ∈ s, p.1 = q.1 ∧ ∃ (x : E), P x ∧ p.2 = q.2.update v x}

def Semantics.Dynamic.DynamicGQ.UpdateTheoretic.Mvar_u {W : Type u_1} {E : Type u_2} (v : ℕ) (K : Core.StateCCP W E) [PartialOrder E] : Core.StateCCP W E

Mereological maximization at the state level (equation 78): apply K, then retain only those output pairs where v is maximal across the entire output state. This is the non-distributive operator.

Equations

• Semantics.Dynamic.DynamicGQ.UpdateTheoretic.Mvar_u v K s = {p : W × Core.Assignment E | p ∈ K s ∧ Mereology.isMaximal (fun (x : E) => ∃ q ∈ K s, q.2 v = x) (p.2 v)}

def Semantics.Dynamic.DynamicGQ.UpdateTheoretic.CardTest_u {W : Type u_1} {E : Type u_2} (v n : ℕ) [PartialOrder E] [Fintype E] : Core.StateCCP W E

Cardinality test at the state level (equation 75): filter the context for pairs where atomCount(v(g)) = n.

Equations

• Semantics.Dynamic.DynamicGQ.UpdateTheoretic.CardTest_u v n s = {p : W × Core.Assignment E | p ∈ s ∧ Mereology.atomCount E (p.2 v) = n}

def Semantics.Dynamic.DynamicGQ.UpdateTheoretic.dseq_u {W : Type u_1} {E : Type u_2} (L R : Core.StateCCP W E) : Core.StateCCP W E

Dynamic sequencing at the state level (equation 80): function composition. s[L;R] := R(L(s)).

Equations

• L ⨟ᵤ R = R ∘ L

def Semantics.Dynamic.DynamicGQ.UpdateTheoretic.«term_⨟ᵤ_» : Lean.TrailingParserDescr

Equations

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

def Semantics.Dynamic.DynamicGQ.UpdateTheoretic.RelTest {W : Type u_1} {E : Type u_2} (v₁ v₂ : ℕ) (R : E → E → Prop) : Core.StateCCP W E

Relational test at the state level (eq. 73 in @cite{charlow-2021}): filter for assignments where R(g(v₁), g(v₂)) holds. Used to encode verb meanings in the dynamic pipeline.

Equations

• Semantics.Dynamic.DynamicGQ.UpdateTheoretic.RelTest v₁ v₂ R s = {p : W × Core.Assignment E | p ∈ s ∧ R (p.2 v₁) (p.2 v₂)}

def Semantics.Dynamic.DynamicGQ.UpdateTheoretic.exactlyN_u {W : Type u_1} {E : Type u_2} (v : ℕ) (P : E → Prop) (n : ℕ) [PartialOrder E] [Fintype E] : Core.StateCCP W E

Single-quantifier "exactly N" pipeline (no nuclear scope): E^v P ; M_v(E^v P) ; n_v. This is the trivial-scope instantiation of @cite{charlow-2021}'s scope-taking GQ (eq. 81), with the nuclear scope set to identity.

Equations

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

def Semantics.Dynamic.DynamicGQ.UpdateTheoretic.sentenceMeaning_u {W : Type u_1} {E : Type u_2} (v u : ℕ) (P_subj P_obj : E → Prop) (R : E → E → Prop) (n_subj n_obj : ℕ) [PartialOrder E] [Fintype E] : Core.StateCCP W E

The full update-theoretic sentence meaning for "exactly n_subj P_subj R exactly n_obj P_obj" (eq. 82 in @cite{charlow-2021}).

Structure: M_v (E^v P_subj ; M_u (E^u P_obj ; R u v)) ; n_obj_u ; n_subj_v

The two maximization operators nest: the inner M_u maximizes the object dref within the scope of the outer subject dref, while the outer M_v maximizes over the entire state. The non-distributivity of M_v is what produces the cumulative reading.

Equations

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

theorem Semantics.Dynamic.DynamicGQ.UpdateTheoretic.Mvar_u_nondistributive {W : Type u_1} {E : Type u_2} [PartialOrder E] [Nonempty W] (a b : E) (hab : a < b) : ∃ (v : ℕ) (K : Core.StateCCP W E), ¬Core.IsDistributive (Mvar_u v K)

M_v is NOT distributive: it surveys the entire context to determine which assignments have maximal v-values.

Proof: with K = id and a context containing two pairs whose v-values are a < b, whole-context maximization keeps only the b-pair (a is not maximal), but per-element processing keeps both (each is trivially maximal in its singleton).

theorem Semantics.Dynamic.DynamicGQ.UpdateTheoretic.CardTest_u_distributive {W : Type u_1} {E : Type u_2} [PartialOrder E] [Fintype E] (v n : ℕ) : Core.IsDistributive (CardTest_u v n)

Cardinality tests ARE distributive: they only inspect one pair at a time.

theorem Semantics.Dynamic.DynamicGQ.UpdateTheoretic.exactlyN_u_distributive {W : Type u_1} {E : Type u_2} [PartialOrder E] [Fintype E] (v : ℕ) (P : E → Prop) (n : ℕ) : Core.IsDistributive (exactlyN_u v P n)

The update-theoretic composed "exactly N" is distributive.

Despite containing the non-distributive Mvar_u, the full pipeline Evar_u ; Mvar_u ∘ Evar_u ; CardTest_u is distributive because Evar_u normalizes the v-values: after Evar_u v P, the set of values at position v is always {x | P x} regardless of the input state. The maximization in Mvar_u therefore selects the same maximal P-elements whether processing the full state or per-element.

The cumulative reading (@cite{charlow-2021}) arises from the non-distributivity of Mvar_u itself (see Mvar_u_nondistributive), not from the composed pipeline.