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.
DPL existential = cylindrification.
closure(∃x.φ) = cₓ(closure(φ)): the truth-conditional content of
DPL's existential quantifier at variable x is exactly cylindrification
at register x. This is the defining correspondence between DPL
and cylindric set algebra (@cite{groenendijk-stokhof-1991}).
DPL identity test = diagonal element.
closure(atom(g(x) = g(y))) = Dxy: the truth condition of the DPL
atomic formula x = y is the diagonal element Dxy from cylindric
algebra.
DPL negation under closure is a test for non-cylindrifiability:
closure(¬φ)(g) iff no assignment update satisfies φ.
Discourse referent introduction under closure = cylindrification.
closure(new n ;; φ) = cₙ(closure(φ)): introducing dref n
then continuing with φ equals cylindrifying φ at n.
CDRT equality condition on drefs = diagonal element.