def Semantics.Dynamic.DPL.DPLRel (E : Type u_1) : Type u_1

DPL semantic type: relation between assignments.

⟦φ⟧(g, h) means: starting from assignment g, the formula φ can update to assignment h.

Equations

• Semantics.Dynamic.DPL.DPLRel E = ((ℕ → E) → (ℕ → E) → Prop)

def Semantics.Dynamic.DPL.DPLRel.atom {E : Type u_1} (p : (ℕ → E) → Prop) : DPLRel E

Atomic predicate in DPL: tests without changing assignment.

Equations

• Semantics.Dynamic.DPL.DPLRel.atom p g h = (g = h ∧ p g)

def Semantics.Dynamic.DPL.DPLRel.conj {E : Type u_1} (φ ψ : DPLRel E) : DPLRel E

DPL conjunction: relation composition.

⟦φ ∧ ψ⟧(g, h) iff ∃k. ⟦φ⟧(g, k) ∧ ⟦ψ⟧(k, h)

Equations

• φ.conj ψ g h = ∃ (k : ℕ → E), φ g k ∧ ψ k h

def Semantics.Dynamic.DPL.DPLRel.exists_ {E : Type u_1} (x : ℕ) (φ : DPLRel E) : DPLRel E

DPL existential: random assignment then scope.

⟦∃x.φ⟧(g, h) iff ∃d. ⟦φ⟧(g[x↦d], h)

Equations

• Semantics.Dynamic.DPL.DPLRel.exists_ x φ g h = ∃ (d : E), φ (fun (n : ℕ) => if n = x then d else g n) h

def Semantics.Dynamic.DPL.DPLRel.neg {E : Type u_1} (φ : DPLRel E) : DPLRel E

DPL negation: test without changing assignment.

⟦¬φ⟧(g, h) iff g = h ∧ ¬∃k. ⟦φ⟧(g, k)

Note: this does not validate DNE.

Equations

• φ.neg g h = (g = h ∧ ¬∃ (k : ℕ → E), φ g k)

theorem Semantics.Dynamic.DPL.dpl_dne_fails_anaphora {E : Type u_1} [Nontrivial E] : ∃ (x : ℕ), ∃ (φ : DPLRel E), (DPLRel.exists_ x φ).neg.neg ≠ DPLRel.exists_ x φ

DPL does not validate DNE for anaphora.

¬¬∃x.φ is not equivalent to ∃x.φ because negation resets the output assignment: neg(neg(exists_ x φ)) g h forces g = h (it's a test), while exists_ x φ can change the assignment to export a witness.

Requires Nontrivial E (at least 2 elements): for Unit, all assignments are identical and DNE holds vacuously.

theorem Semantics.Dynamic.DPL.scope_extension {E : Type u_1} (x : ℕ) (φ ψ : DPLRel E) (_hfree : ∀ (g h : ℕ → E) (d : E), ψ g h ↔ ψ (fun (n : ℕ) => if n = x then d else g n) fun (n : ℕ) => if n = x then d else h n) : DPLRel.exists_ x (φ.conj ψ) = (DPLRel.exists_ x φ).conj ψ

Scope extension theorem: ∃x(φ ∧ ψ) ≡ (∃xφ) ∧ ψ when x not free in ψ.

"Not free in ψ" means ψ is invariant under reassigning x in both input and output assignments. Under this condition, the existential can scope out past conjunction.

TODO: Prove by extensionality and reordering existential quantifiers.