Dynamic Quantification over Assignment E

@cite{groenendijk-stokhof-1991} @cite{muskens-1996}

Substrate operations specialized to the Tarski-style assignment state Assignment E := Nat → E (from Core.Assignment).

AssignmentStructure (in Dynamic/Core/DynamicTy2.lean) takes abstract drefs S → E, but only projection drefs (fun g => g n) make sense for the concrete Assignment E type — there's no canonical way to extend g : Assignment E along an arbitrary (λ g => g 0 + g 1) : Assignment ℕ → ℕ. So the typeclass cannot be instantiated for Assignment E directly.

This file provides the natural-number-indexed operators that DPL, CDRT, FCS, PLA, and ICDRT all use under different paper-anchored names. They're substrate because they're fully generic over E, taking any Nat index.

Operator	Paper-anchored alias	Type
randomAssignAt n	DPL [x_n], FCS file-card opening	DRS (Assignment E)
existsAt n φ	DPL ∃x_n.φ, CDRT [u_n]; φ	DRS (Assignment E) → DRS (Assignment E)
forallAt n φ	DPL ∀x_n.φ	DRS (Assignment E) → DRS (Assignment E)
closeAt φ	DPL ◇φ, K&R existential closure	DRS (Assignment E) → DRS (Assignment E)

The existsAt / forallAt decomposition is mathlib-style: existsAt n is dseq after randomAssignAt n; forallAt n is test ∘ dneg ∘ existsAt n ∘ test ∘ dneg. The decomposition lemmas are immediate by definitional unfolding.

def Semantics.Dynamic.Core.randomAssignAt {E : Type u_1} (n : ℕ) : DynProp.DRS (Core.Assignment E)

The "open file card n" operation: g[n↦?] non-deterministically.

Equations

• Semantics.Dynamic.Core.randomAssignAt n g h = ∃ (d : E), h = g.update n d

def Semantics.Dynamic.Core.existsAt {E : Type u_1} (n : ℕ) (φ : DynProp.DRS (Core.Assignment E)) : DynProp.DRS (Core.Assignment E)

existsAt n φ is dseq (randomAssignAt n) φ. Holds at (g, h) iff some witness d : E makes φ accept the input g[n↦d] and produce h.

Equations

• Semantics.Dynamic.Core.existsAt n φ = Semantics.Dynamic.Core.randomAssignAt n ⨟ φ

@[simp]

theorem Semantics.Dynamic.Core.existsAt_eq_dseq {E : Type u_1} (n : ℕ) (φ : DynProp.DRS (Core.Assignment E)) : existsAt n φ = randomAssignAt n ⨟ φ

The decomposition: existsAt = dseq ∘ randomAssignAt.

theorem Semantics.Dynamic.Core.existsAt_iff {E : Type u_1} (n : ℕ) (φ : DynProp.DRS (Core.Assignment E)) (g h : Core.Assignment E) : existsAt n φ g h ↔ ∃ (d : E), φ (g.update n d) h

Direct unfolding: existsAt n φ g h ↔ ∃ d : E, φ (g.update n d) h.

def Semantics.Dynamic.Core.forallAt {E : Type u_1} (n : ℕ) (φ : DynProp.DRS (Core.Assignment E)) : DynProp.DRS (Core.Assignment E)

forallAt n φ: a test that requires φ to succeed for every value at n. Definitionally test (dneg (existsAt n (test (dneg φ)))) — the standard DPL/Muskens reduction ∀ ≈ ¬∃¬.

Equations

• Semantics.Dynamic.Core.forallAt n φ = [∼Semantics.Dynamic.Core.existsAt n [∼φ]]

theorem Semantics.Dynamic.Core.forallAt_iff {E : Type u_1} (n : ℕ) (φ : DynProp.DRS (Core.Assignment E)) (g h : Core.Assignment E) : forallAt n φ g h ↔ g = h ∧ ∀ (d : E), ∃ (k : Core.Assignment E), φ (g.update n d) k

Direct truth condition: forallAt n φ g h ↔ g = h ∧ ∀ d, ∃ k, φ (g.update n d) k.

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

closeAt φ: a test that succeeds iff φ has any output. Equals test (closure φ) from Connectives.Defs.

Equations

• Semantics.Dynamic.Core.closeAt φ = [Semantics.Dynamic.Core.DynProp.closure φ]

@[simp]

theorem Semantics.Dynamic.Core.closeAt_eq {E : Type u_1} (φ : DynProp.DRS (Core.Assignment E)) : closeAt φ = [DynProp.closure φ]