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 (@cite{charlow-2021}, Theorem 1)
• CardTest_u_distributive: cardinality tests ARE distributive
• exactlyN_u_cumulative: the composed meaning has cumulative truth conditions

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 × Semantics.Dynamic.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 × Semantics.Dynamic.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 × Semantics.Dynamic.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.exactlyN_u {W : Type u_1} {E : Type u_2} (v : ℕ) (P : E → Prop) (n : ℕ) [PartialOrder E] [Fintype E] : Core.StateCCP W E

Composed update-theoretic "exactly N" (equation 81): E^v_u; M_v_u; n_v_u

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] : ∃ (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. TODO: Prove by exhibiting a 2-element context where per-element maximization differs from whole-context maximization.

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_cumulative {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 meaning has cumulative truth conditions. TODO: Formalize.