Dynamic Predicate Logic

The DPL substrate ([groenendijk-stokhof-1991]): meanings are relations between total assignments (Rel, 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

• Rel with Definition 2's clauses: atom, conj, exists_, neg, impl, disj, forall_; close (Definition 17).
• agreeOn, reset: the agreement relations, with the existential factored through the reset (exists_eq_reset_conj).
• 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 (toDRS_conj, toDRS_neg, ...).

def DPL.Rel (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.Rel E = ((ℕ → E) → (ℕ → E) → Prop)

@[instance_reducible]

instance DPL.instCompleteLatticeRel {E : Type u_1} : CompleteLattice (Rel E)

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

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

def DPL.Rel.conj {E : Type u_1} (φ ψ : Rel E) : Rel 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.Rel.exists_ {E : Type u_1} (x : ℕ) (φ : Rel E) : Rel E

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

Equations

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

def DPL.Rel.neg {E : Type u_1} (φ : Rel E) : Rel 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.Rel.impl {E : Type u_1} (φ ψ : Rel E) : Rel 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.Rel.disj {E : Type u_1} (φ ψ : Rel E) : Rel 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.Rel.forall_ {E : Type u_1} (x : ℕ) (φ : Rel E) : Rel E

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

Equations

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

def DPL.Rel.close {E : Type u_1} (φ : Rel E) : Rel 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)

Agreement relations

def DPL.agreeOn {E : Type u_1} (V : Set ℕ) : Rel E

Agreement on V: relate the assignments equal on V ([Vis98], Definition 2.2).

Equations

• DPL.agreeOn V f g = Set.EqOn f g V

def DPL.reset {E : Type u_1} (x : ℕ) : Rel E

The random reset k[x]g of the existential clause: agree everywhere but x, [Vis98]'s [x].

Equations

• DPL.reset x = DPL.agreeOn {x}ᶜ

theorem DPL.le_agreeOn_conj {E : Type u_1} (R : Rel E) (V W : Set ℕ) : R ≤ (agreeOn V).conj (R.conj (agreeOn W))

A relation embeds in its composition with agreement on either side.

theorem DPL.agreeOn_conj_agreeOn {E : Type u_1} (V W : Set ℕ) : (agreeOn V).conj (agreeOn W) = agreeOn (V ∩ W)

Agreements compose to agreement on the intersection.

theorem DPL.agreeOn_inf_agreeOn {E : Type u_1} (V W : Set ℕ) : agreeOn V ⊓ agreeOn W = agreeOn (V ∪ W)

Agreements meet in agreement on the union.

theorem DPL.agreeOn_empty {E : Type u_1} : agreeOn ∅ = ⊤

Agreement on no variables is trivial.

Semantic notions (Definitions 3, 6, 9)

def DPL.Rel.trueAt {E : Type u_1} (φ : Rel 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.Rel.satisfactionSet {E : Type u_1} (φ : Rel E) : Set (ℕ → E)

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

Equations

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

def DPL.Rel.productionSet {E : Type u_1} (φ : Rel 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.

@[reducible, inline]

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

DPL extend is Function.update.

Equations

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

def DPL.toDRS {E : Type u_1} (φ : Rel E) : DynamicSemantics.Update (Assignment E)

A DPL relation is an Update over Assignment E.

Equations

• DPL.toDRS φ = φ

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

An Update is a DPL relation.

Equations

• DPL.ofDRS D = D

@[simp]

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

@[simp]

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

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

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

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

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

theorem DPL.exists_eq_reset_conj {E : Type u_1} (x : ℕ) (φ : Rel E) : Rel.exists_ x φ = (reset x).conj φ

The existential clause factored through the reset: ∃x φ is the random reset at x composed with the scope.

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

DPL implication is the test of dynamic implication.

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

DPL disjunction is the test of dynamic disjunction.

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

DPL closure is the test of existential closure.

theorem DPL.toDRS_agreeOn_univ {E : Type u_1} : toDRS (agreeOn Set.univ) = 1

Total agreement is the unit update — the trivial test.

theorem DPL.trueAt_iff_closure {E : Type u_1} (φ : Rel E) (g : Assignment E) : φ.trueAt g ↔ (toDRS φ).closure g

DPL truth is existential closure.