Dynamic Predicate Logic

[GS91a]

The DPL substrate: meanings are relations between total assignments (DPLRel, the paper's Definition 2), truth is having an output (Definition 3), and ♦ closes a meaning to its test (Definition 17). Conjunction is relational composition and the existential is random reassignment — the two externally dynamic constants; negation, implication, disjunction, and the universal are tests. The paper's results about the system (scope extension, donkey equivalence, the restricted double-negation laws, interdefinability) are proved in Studies/GroenendijkStokhof1991.lean.

Main definitions

• DPLRel with Definition 2's clauses: atom, conj, exists_, neg, impl, disj, forall_; close (Definition 17).
• trueAt, satisfactionSet, productionSet (Definitions 3, 6, 9).
• toDRS/ofDRS: a DPL relation is an Update over assignments — DPL embeds in dynamic Ty2 at S = Assignment E, each connective matching its spine combinator (conj_eq_dseq, neg_eq_test_dneg, ...).

def DPL.DPLRel (E : Type u_2) : Type u_2

DPL semantic type (Definition 2): ⟦φ⟧ g h means that starting from input assignment g, the formula φ can update to output h.

Equations

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

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

Atomic predicate (clauses 1–2): test the input without changing it.

Equations

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

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

Conjunction (clause 4): relation composition — ⟦φ ∧ ψ⟧ g h iff ∃k, ⟦φ⟧ g k ∧ ⟦ψ⟧ k h.

Equations

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

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

Existential quantification (clause 7): random assignment at x, then the scope — ⟦∃x φ⟧ g h iff ∃d, ⟦φ⟧ g[x↦d] h.

Equations

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

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

Negation (clause 3): the test that no output is reachable — ⟦¬φ⟧ g h iff g = h ∧ ¬∃k, ⟦φ⟧ g k. Not DNE-valid: see Studies/GroenendijkStokhof1991.lean.

Equations

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

def DPL.DPLRel.impl {E : Type u_1} (φ ψ : DPLRel E) : DPLRel E

Implication (clause 6): internally dynamic, externally static — every output of the antecedent can be extended by the consequent. The antecedent passes bindings to the consequent, giving its existentials universal force (donkey sentences).

Equations

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

def DPL.DPLRel.disj {E : Type u_1} (φ ψ : DPLRel E) : DPLRel E

Disjunction (clause 5): externally and internally static — no anaphoric relations across or out of the disjuncts.

Equations

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

def DPL.DPLRel.forall_ {E : Type u_1} (x : ℕ) (φ : DPLRel E) : DPLRel E

Universal quantification (clause 8): a test — for every value at x, the scope can be processed. Externally static.

Equations

• DPL.DPLRel.forall_ x φ g h = (g = h ∧ ∀ (d : E), ∃ (m : ℕ → E), φ (fun (n : ℕ) => if n = x then d else g n) m)

def DPL.DPLRel.close {E : Type u_1} (φ : DPLRel E) : DPLRel E

Closure (Definition 17): ⟦♦φ⟧ g h iff g = h and φ can be successfully processed — the test with φ's truth conditions.

Equations

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

Semantic notions (Definitions 3, 6, 9)

def DPL.DPLRel.trueAt {E : Type u_1} (φ : DPLRel E) (g : ℕ → E) : Prop

Truth (Definition 3): φ is true w.r.t. g iff it has an output.

Equations

• φ.trueAt g = ∃ (h : ℕ → E), φ g h

def DPL.DPLRel.satisfactionSet {E : Type u_1} (φ : DPLRel E) : Set (ℕ → E)

Satisfaction set (Definition 6): inputs from which φ succeeds.

Equations

• φ.satisfactionSet = {g : ℕ → E | ∃ (h : ℕ → E), φ g h}

def DPL.DPLRel.productionSet {E : Type u_1} (φ : DPLRel E) : Set (ℕ → E)

Production set (Definition 9): possible outputs of φ.

Equations

• φ.productionSet = {h : ℕ → E | ∃ (g : ℕ → E), φ g h}

DPL as dynamic Ty2

DPL embeds directly into dynamic Ty2 at S = Assignment E: DPL assignments are Ty2 states, DPL relations are Update meanings, and each connective matches its spine combinator.

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

DPL dref: projection function for variable n.

Equations

• DPL.dref n g = g n

@[reducible, inline]

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

DPL extend is Function.update.

Equations

• DPL.extend g n e = Function.update g n e

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

theorem 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 DPL.toDRS {E : Type u_1} (φ : DPLRel E) : DynamicSemantics.Update (Core.Assignment E)

A DPL relation is an Update over Assignment E.

Equations

• DPL.toDRS φ = φ

def DPL.ofDRS {E : Type u_1} (D : DynamicSemantics.Update (Core.Assignment E)) : DPLRel E

An Update is a DPL relation.

Equations

• DPL.ofDRS D = D

@[simp]

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

@[simp]

theorem DPL.ofDRS_toDRS {E : Type u_1} (D : DynamicSemantics.Update (Core.Assignment E)) : toDRS (ofDRS D) = D

theorem DPL.atom_eq_test {E : Type u_1} (p : Core.Assignment E → Prop) : toDRS (DPLRel.atom p) = DynamicSemantics.Update.test fun (g : Core.Assignment E) => p g

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

theorem DPL.neg_eq_test_dneg {E : Type u_1} (φ : DPLRel E) : toDRS φ.neg = DynamicSemantics.Update.test (toDRS φ).neg

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

theorem DPL.impl_eq_test_dimpl {E : Type u_1} (φ ψ : DPLRel E) : toDRS (φ.impl ψ) = DynamicSemantics.Update.test ((toDRS φ).impl (toDRS ψ))

DPL implication is the test of dynamic implication.

theorem DPL.disj_eq_test_ddisj {E : Type u_1} (φ ψ : DPLRel E) : toDRS (φ.disj ψ) = DynamicSemantics.Update.test ((toDRS φ).disj (toDRS ψ))

DPL disjunction is the test of dynamic disjunction.

theorem DPL.close_eq_test_closure {E : Type u_1} (φ : DPLRel E) : toDRS φ.close = DynamicSemantics.Update.test (toDRS φ).closure

DPL closure is the test of existential closure.

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

DPL truth is existential closure.