Cylindric Algebra Bridges for Dynamic Semantics

@cite{henkin-monk-tarski-1971} @cite{groenendijk-stokhof-1991} @cite{muskens-1996}

Proves that the existential quantifiers and identity tests across DPL, CDRT, and DRS are all instances of the cylindric algebra operations cylindrify and diagonal from Core.CylindricAlgebra.

Bridges

Framework	Existential	= Cylindric
DPL	DPLRel.exists_ x φ	cylindrify x (closure φ)
CDRT	DProp.new n ;; φ	cylindrify n (closure φ)
DRS	box [n] [conds]	cylindrify n (interp conds)

Framework	Identity	= Cylindric
DPL	atom (g(x) = g(y))	diagonal x y
CDRT	eq' (dref n) (dref m)	diagonal n m
DRS	.is n m	diagonal n m

These are not analogies — they are algebraic identities under closure.

theorem Core.CylindricAlgebra.cdrt_register_eq_assignment {E : Type u_1} : Semantics.Dynamic.CDRT.Register E = Assignment E

CDRT registers ARE assignments.

theorem Core.CylindricAlgebra.cdrt_new_seq_eq_cylindrify {E : Type u_1} (n : ℕ) (φ : Semantics.Dynamic.CDRT.DProp E) : Semantics.Dynamic.Core.DynProp.closure (Semantics.Dynamic.CDRT.toDRS (Semantics.Dynamic.CDRT.DProp.new n ;; φ)) = cylindrify n (Semantics.Dynamic.Core.DynProp.closure (Semantics.Dynamic.CDRT.toDRS φ))

Discourse referent introduction under closure = cylindrification.

closure(new n ;; φ) = cₙ(closure(φ)): introducing dref n then continuing with φ equals cylindrifying φ at n.

theorem Core.CylindricAlgebra.cdrt_eq_dref_eq_diagonal {E : Type u_1} (i j : ℕ) : Semantics.Dynamic.Core.DynamicTy2.eq' (Semantics.Dynamic.CDRT.dref i) (Semantics.Dynamic.CDRT.dref j) = diagonal i j

CDRT equality condition on drefs = diagonal element.

theorem Core.CylindricAlgebra.charlow_static_eq_cylindrify {E : Type u_1} (x : ℕ) (body : Assignment E → Prop) (g : Assignment E) : Semantics.Dynamic.Charlow2019.trueAt (Semantics.Dynamic.Charlow2019.staticExists x body) g ↔ cylindrify x body g

Static existential truth = cylindrification.

Charlow's staticExists x body tests whether ∃ d, body(g[x↦d]), which is exactly cylindrify x body.

theorem Core.CylindricAlgebra.charlow_dynamic_eq_cylindrify {E : Type u_1} (x : ℕ) (body : Assignment E → Prop) (g : Assignment E) : Semantics.Dynamic.Charlow2019.trueAt (Semantics.Dynamic.Charlow2019.dynamicExists x body) g ↔ cylindrify x body g

Dynamic existential truth = cylindrification (same truth conditions).