def Semantics.Dynamic.DPL.dref {E : Type u_1} (n : ℕ) : Core.DynamicTy2.Dref (Core.Assignment E) E

DPL dref: projection function for variable n

Equations

• Semantics.Dynamic.DPL.dref n g = g n

@[reducible, inline]

abbrev Semantics.Dynamic.DPL.extend {E : Type u_1} (g : Core.Assignment E) (n : ℕ) (e : E) : Core.Assignment E

DPL extend is Assignment.update.

Equations

• Semantics.Dynamic.DPL.extend g n e = g.update n e

theorem Semantics.Dynamic.DPL.extend_at {E : Type u_1} (g : Core.Assignment E) (n : ℕ) (e : E) : dref n (extend g n e) = e

theorem Semantics.Dynamic.DPL.extend_other {E : Type u_1} (g : Core.Assignment E) (n m : ℕ) (e : E) (h : n ≠ m) : dref m (extend g n e) = dref m g

def Semantics.Dynamic.DPL.toDRS {E : Type u_1} (φ : DPLRel E) : Core.DynProp.DRS (Core.Assignment E)

DPL relation IS a DRS

Equations

• Semantics.Dynamic.DPL.toDRS φ = φ

def Semantics.Dynamic.DPL.ofDRS {E : Type u_1} (D : Core.DynProp.DRS (Core.Assignment E)) : DPLRel E

DRS IS a DPL relation

Equations

• Semantics.Dynamic.DPL.ofDRS D = D

@[simp]

theorem Semantics.Dynamic.DPL.toDRS_ofDRS {E : Type u_1} (φ : DPLRel E) : ofDRS (toDRS φ) = φ

@[simp]

theorem Semantics.Dynamic.DPL.ofDRS_toDRS {E : Type u_1} (D : Core.DynProp.DRS (Core.Assignment E)) : toDRS (ofDRS D) = D

theorem Semantics.Dynamic.DPL.atom_eq_test {E : Type u_1} (p : Core.Assignment E → Prop) : toDRS (atom p) = [fun (g : Core.Assignment E) => p g]

theorem Semantics.Dynamic.DPL.conj_eq_dseq {E : Type u_1} (φ ψ : DPLRel E) : toDRS (φ.conj ψ) = toDRS φ ⨟ toDRS ψ

theorem Semantics.Dynamic.DPL.neg_eq_test_dneg {E : Type u_1} (φ : DPLRel E) : toDRS φ.neg = [∼toDRS φ]

theorem Semantics.Dynamic.DPL.exists_eq {E : Type u_1} (x : ℕ) (φ : DPLRel E) : toDRS (exists_ x φ) = fun (g h : Core.Assignment E) => ∃ (d : E), toDRS φ (extend g x d) h

DPL as a cylindric set algebra

The fundamental observation of @cite{groenendijk-stokhof-1991}: DPL's existential quantifier IS cylindrification. DPL's identity test IS a diagonal element. These are not analogies — they are algebraic identities under closure.

theorem Semantics.Dynamic.DPL.closure_exists_eq_cylindrify {E : Type u_1} (x : ℕ) (φ : DPLRel E) : Core.DynProp.closure (toDRS (exists_ x φ)) = Core.CylindricAlgebra.cylindrify x (Core.DynProp.closure (toDRS φ))

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.

theorem Semantics.Dynamic.DPL.closure_identity_eq_diagonal {E : Type u_1} (x y : ℕ) : Core.DynProp.closure (toDRS (atom fun (g : Core.Assignment E) => g x = g y)) = Core.CylindricAlgebra.diagonal x y

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.

theorem Semantics.Dynamic.DPL.closure_neg_eq {E : Type u_1} (φ : DPLRel E) : Core.DynProp.closure (toDRS φ.neg) = fun (g : Core.Assignment E) => ¬Core.DynProp.closure (toDRS φ) g

DPL negation under closure is a test for non-cylindrifiability: closure(¬φ)(g) iff no assignment update satisfies φ.

theorem Semantics.Dynamic.DPL.impl_eq_test_dimpl {E : Type u_1} (φ ψ : DPLRel E) : toDRS (φ.impl ψ) = [Core.DynProp.dimpl (toDRS φ) (toDRS ψ)]

DPL implication = test of dynamic implication.

toDRS(φ → ψ) = test(dimpl(toDRS φ)(toDRS ψ))

theorem Semantics.Dynamic.DPL.disj_eq_test_ddisj {E : Type u_1} (φ ψ : DPLRel E) : toDRS (φ.disj ψ) = [Core.DynProp.ddisj (toDRS φ) (toDRS ψ)]

DPL disjunction = test of dynamic disjunction.

toDRS(φ ∨ ψ) = test(ddisj(toDRS φ)(toDRS ψ))

theorem Semantics.Dynamic.DPL.close_eq_test_closure {E : Type u_1} (φ : DPLRel E) : toDRS φ.close = [Core.DynProp.closure (toDRS φ)]

DPL closure = test of existential closure.

toDRS(◇φ) = test(closure(toDRS φ))

theorem Semantics.Dynamic.DPL.trueAt_eq_closure {E : Type u_1} (φ : DPLRel E) (g : Core.Assignment E) : φ.trueAt g ↔ Core.DynProp.closure (toDRS φ) g

DPL truth = existential closure.

trueAt φ g ↔ closure(toDRS φ) g

Importing DPL.Bridge gives access to both the DPL-specific operations (from Basic) and the shared dynamic algebra (from DynProp/DynamicTy2). This avoids the need to separately import Core.DynProp or Core.CCP for standard DPL work.