Groenendijk & Stokhof (1991): Dynamic Predicate Logic

[GS91a]

Dynamic Predicate Logic. Linguistics and Philosophy 14(1): 39–100. The DPL substrate (DPL.Rel, Definition 2) lives in Semantics/Dynamic/DPL.lean; this file proves the paper's claims about it.

Main results

• scope_extension, donkey_equivalence: the two central equivalences — existentials bind across conjunction (∃xφ ∧ ψ ≃ ∃x[φ ∧ ψ]), and get universal force in conditional antecedents (∃xφ → ψ ≃ ∀x[φ → ψ]), both unconditional (they are the normal-binding-form equivalences of Fact 17, §3.6).
• Blocking (§2.5): neg, impl, disj, forall_ are tests — no binding escapes.
• §3.4's logical facts: conj_assoc, conj_not_comm, close_eq_neg_neg (♦φ ≃ ¬¬φ), the restricted double-negation law neg_neg_eq_self_iff_isTest (¬¬φ ≃ φ iff φ is a test), its anaphoric consequence dne_fails_anaphora, and the interdefinability of →, ∨, ∀ from ¬, ∧, ∃.
• closure_exists_eq_cylindrify and friends: the satisfaction-set computations from Fact 19's proof (§3.6), in cylindric-algebra vocabulary.
• The indexed reading: DPL's generators as context-extension arrows (testTransition, Transition.randomAssign), with clause 4 as transition composition and clause 7 factoring through the random-assignment arrow.

Scope extension (§2.1, §2.3)

"A man walks in the park. He whistles."

DPL translation: ∃x[man(x) ∧ walk(x)] ∧ whistle(x). Scope extension makes this equal to ∃x[man(x) ∧ walk(x) ∧ whistle(x)]: the existential binds across conjunction, unconditionally — a later conjunct with free x is simply captured. This accounts for Heim1982.Examples.indefinite_persists.

theorem GroenendijkStokhof1991.scope_extension {E : Type u_1} (x : ℕ) (φ ψ : DPL.Rel E) : DPL.Rel.exists_ x (φ.conj ψ) = (DPL.Rel.exists_ x φ).conj ψ

Scope extension: ∃xφ ∧ ψ ≃ ∃x[φ ∧ ψ] — one of the four normal-binding-form equivalences in Fact 17's proof (§3.6), and the formal content of cross-sentential anaphora (§2.1).

Donkey sentences (§2.4)

"If a farmer owns a donkey, he beats it."

DPL translation: ∃x[farmer(x) ∧ ∃y[donkey(y) ∧ own(x,y)]] → beat(x,y). By donkey_equivalence (twice), this equals ∀x∀y[farmer(x) ∧ donkey(y) ∧ own(x,y) → beat(x,y)] — the universal "strong" reading recorded for Geach1962.Examples.donkey_classic and Heim1982.Examples.conditional_donkey.

theorem GroenendijkStokhof1991.donkey_equivalence {E : Type u_1} (x : ℕ) (φ ψ : DPL.Rel E) : (DPL.Rel.exists_ x φ).impl ψ = DPL.Rel.forall_ x (φ.impl ψ)

The donkey equivalence: ∃xφ → ψ ≃ ∀x[φ → ψ]. An existential in the antecedent of an implication has universal force — donkey sentences are compositional without stipulating wide-scope ∀.

theorem GroenendijkStokhof1991.neg_exists_eq_forall_neg {E : Type u_1} (x : ℕ) (φ : DPL.Rel E) : (DPL.Rel.exists_ x φ).neg = DPL.Rel.forall_ x φ.neg

¬∃xφ ≃ ∀x¬φ: negation commutes with the quantifier switch, since negation turns anything into a test.

Blocking: the externally static constants (§2.5)

"Every man walked in. *He sat down." / "John didn't see a bird. *It was singing."

Negation, implication, disjunction, and the universal are tests: they force output = input, so no binding escapes them. This accounts for Heim1982.Examples.universal_blocks, standard_negation_blocks, and conditional_antecedent.

theorem GroenendijkStokhof1991.neg_isTest {E : Type u_1} (φ : DPL.Rel E) : (DPL.toDRS φ.neg).IsTest

Negation is a test.

theorem GroenendijkStokhof1991.impl_isTest {E : Type u_1} (φ ψ : DPL.Rel E) : (DPL.toDRS (φ.impl ψ)).IsTest

Implication is a test: antecedent bindings do not escape.

theorem GroenendijkStokhof1991.disj_isTest {E : Type u_1} (φ ψ : DPL.Rel E) : (DPL.toDRS (φ.disj ψ)).IsTest

Disjunction is a test: no anaphora across or out of disjuncts.

theorem GroenendijkStokhof1991.forall_isTest {E : Type u_1} (x : ℕ) (φ : DPL.Rel E) : (DPL.toDRS (DPL.Rel.forall_ x φ)).IsTest

The universal quantifier is a test: it introduces no referents.

Logical facts (§3.4)

theorem GroenendijkStokhof1991.conj_assoc {E : Type u_1} (φ ψ χ : DPL.Rel E) : (φ.conj ψ).conj χ = φ.conj (ψ.conj χ)

Conjunction is associative — despite the increased binding power of the existential (§3.4).

theorem GroenendijkStokhof1991.conj_not_comm {E : Type u_1} [Nontrivial E] : ∃ (φ : DPL.Rel E) (ψ : DPL.Rel E), φ.conj ψ ≠ ψ.conj φ

Conjunction is not commutative: binding is left-to-right (§3.4).

theorem GroenendijkStokhof1991.close_eq_neg_neg {E : Type u_1} (φ : DPL.Rel E) : φ.close = φ.neg.neg

♦φ ≃ ¬¬φ: closure is double negation (§3.4).

theorem GroenendijkStokhof1991.close_eq_self_iff_isTest {E : Type u_1} (φ : DPL.Rel E) : φ.close = φ ↔ ∀ (g h : ℕ → E), φ g h → g = h

Closure fixes exactly the tests: ♦φ ≃ φ iff φ is a test (§3.4).

theorem GroenendijkStokhof1991.neg_neg_eq_self_iff_isTest {E : Type u_1} (φ : DPL.Rel E) : φ.neg.neg = φ ↔ ∀ (g h : ℕ → E), φ g h → g = h

The paper's restricted double-negation law (§3.4): ¬¬φ ≃ φ exactly when φ is a test.

theorem GroenendijkStokhof1991.dne_fails_anaphora {E : Type u_1} [Nontrivial E] : ∃ (x : ℕ) (φ : DPL.Rel E), (DPL.Rel.exists_ x φ).neg.neg ≠ DPL.Rel.exists_ x φ

DNE fails for anaphora: ¬¬∃xφ ≠ ∃xφ, since the existential is not a test. The anaphoric consequence — doubly negated indefinites should not license anaphora — underpredicts (ElliottSudo2025.Examples.double_negation is acceptable); the divergence theorem lives with the comparing paper, in Studies/ElliottSudo2025.lean.

Interdefinability (§3.4)

→, ∨, ∀ are definable from ¬, ∧, ∃ — but not conversely: the latter contains the only externally dynamic constants (conj_not_comm separates ∧ from any test).

theorem GroenendijkStokhof1991.impl_interdefinable {E : Type u_1} (φ ψ : DPL.Rel E) : φ.impl ψ = (φ.conj ψ.neg).neg

φ → ψ ≃ ¬[φ ∧ ¬ψ].

theorem GroenendijkStokhof1991.disj_interdefinable {E : Type u_1} (φ ψ : DPL.Rel E) : φ.disj ψ = (φ.neg.conj ψ.neg).neg

φ ∨ ψ ≃ ¬[¬φ ∧ ¬ψ].

theorem GroenendijkStokhof1991.forall_interdefinable {E : Type u_1} (x : ℕ) (φ : DPL.Rel E) : DPL.Rel.forall_ x φ = (DPL.Rel.exists_ x φ.neg).neg

∀xφ ≃ ¬∃x¬φ.

Equivalence notions and conditions (§3.2, §3.4)

def GroenendijkStokhof1991.sEquiv {E : Type u_1} (φ ψ : DPL.Rel E) : Prop

s-equivalence (Definition 7) at a fixed model: same satisfaction set. The paper quantifies over models; DPL.Rel fixes one.

Equations

• GroenendijkStokhof1991.sEquiv φ ψ = (φ.satisfactionSet = ψ.satisfactionSet)

def GroenendijkStokhof1991.pEquiv {E : Type u_1} (φ ψ : DPL.Rel E) : Prop

p-equivalence (Definition 10): same production set.

Equations

• GroenendijkStokhof1991.pEquiv φ ψ = (φ.productionSet = ψ.productionSet)

theorem GroenendijkStokhof1991.sEquiv_of_eq {E : Type u_1} {φ ψ : DPL.Rel E} (h : φ = ψ) : sEquiv φ ψ

Facts 1–2: equivalence implies s-equivalence and p-equivalence.

theorem GroenendijkStokhof1991.pEquiv_of_eq {E : Type u_1} {φ ψ : DPL.Rel E} (h : φ = ψ) : pEquiv φ ψ

theorem GroenendijkStokhof1991.sEquiv_pEquiv_ne {E : Type u_1} [Nontrivial E] : ∃ (φ : DPL.Rel E) (ψ : DPL.Rel E), sEquiv φ ψ ∧ pEquiv φ ψ ∧ φ ≠ ψ

Fact 3: joint s- and p-equivalence does not imply equivalence — the trivial test and the total relation agree on both sets.

theorem GroenendijkStokhof1991.conj_isTest {E : Type u_1} {φ ψ : DPL.Rel E} (hφ : (DPL.toDRS φ).IsTest) (hψ : (DPL.toDRS ψ).IsTest) : (DPL.toDRS (φ.conj ψ)).IsTest

Definition 12's semantic core, clause 2: a conjunction of tests is a test. With the static constants (neg_isTest, ..., Fact 5) this closes the conditions under the semantics.

theorem GroenendijkStokhof1991.sEquiv_iff_eq_of_isTest {E : Type u_1} {φ ψ : DPL.Rel E} (hφ : (DPL.toDRS φ).IsTest) (hψ : (DPL.toDRS ψ).IsTest) : sEquiv φ ψ ↔ φ = ψ

Fact 4: for tests, s-equivalence coincides with equivalence — a test is determined by its truth conditions (IsTest.eq_test_closure, the semantic form of Fact 6).

Entailment (§3.5)

The paper's two entailment notions, stated over the spine's carrier (Update S) at full generality. Facts 13–16 — the restricted reflexivity and transitivity laws — carry syntactic AQV/FV side conditions and await the syntax stratum.

def GroenendijkStokhof1991.valid {S : Type u_2} (D : DynamicSemantics.Update S) : Prop

An Update is valid iff satisfiable (closure) at every input.

Equations

• GroenendijkStokhof1991.valid D = ∀ (i : S), D.closure i

def GroenendijkStokhof1991.entails {S : Type u_2} (D₁ D₂ : DynamicSemantics.Update S) : Prop

Dynamic entailment (Definition 20): every output of D₁ can be extended by D₂.

Equations

• GroenendijkStokhof1991.entails D₁ D₂ = ∀ (i j : S), D₁ i j → D₂.closure j

def GroenendijkStokhof1991.«term_⊨_» : Lean.TrailingParserDescr

Equations

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

def GroenendijkStokhof1991.sEntails {S : Type u_2} (D₁ D₂ : DynamicSemantics.Update S) : Prop

s-entailment (Definition 18): truth is preserved from premiss to conclusion. Unlike ⊨, it sees no binding between them.

Equations

• GroenendijkStokhof1991.sEntails D₁ D₂ = ∀ (i : S), D₁.closure i → D₂.closure i

def GroenendijkStokhof1991.«term_⊨ₛ_» : Lean.TrailingParserDescr

Equations

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

theorem GroenendijkStokhof1991.sEntails_of_subset {S : Type u_2} {D₁ D₂ : DynamicSemantics.Update S} (h : ∀ ⦃i j : S⦄, D₁ i j → D₂ i j) : sEntails D₁ D₂

Meaning inclusion implies s-entailment (Fact 10); the converse fails.

theorem GroenendijkStokhof1991.entails_iff_valid_test_impl {S : Type u_2} (D₁ D₂ : DynamicSemantics.Update S) : entails D₁ D₂ ↔ valid (DynamicSemantics.Update.test (D₁.impl D₂))

The deduction theorem (Fact 11) in spine vocabulary: entailment is validity of the implication test.

theorem GroenendijkStokhof1991.sEntails_iff_test_closure_entails {S : Type u_2} (D₁ D₂ : DynamicSemantics.Update S) : sEntails D₁ D₂ ↔ entails (DynamicSemantics.Update.test D₁.closure) D₂

Fact 12, in closure form: s-entailment is entailment from the closed premiss.

theorem GroenendijkStokhof1991.deduction {E : Type u_1} (φ ψ : DPL.Rel E) : entails (DPL.toDRS φ) (DPL.toDRS ψ) ↔ valid (DPL.toDRS (φ.impl ψ))

The deduction theorem (Fact 11): φ ⊨ ψ iff ⊨ φ → ψ — DPL implication is the test of dynamic implication, so this is the generic deduction theorem read through the Ty2 embedding.

theorem GroenendijkStokhof1991.sEntails_iff_close_entails {E : Type u_1} (φ ψ : DPL.Rel E) : sEntails (DPL.toDRS φ) (DPL.toDRS ψ) ↔ entails (DPL.toDRS φ.close) (DPL.toDRS ψ)

Fact 12: s-entailment is dynamic entailment from the closed premiss ♦φ.

theorem GroenendijkStokhof1991.exists_atom_entails_atom {E : Type u_1} (x : ℕ) (p : E → Prop) : entails (DPL.toDRS (DPL.Rel.exists_ x (DPL.Rel.atom fun (g : ℕ → E) => p (g x)))) (DPL.toDRS (DPL.Rel.atom fun (g : ℕ → E) => p (g x)))

The flagship dynamic entailment (§3.5): ∃xPx ⊨ Px — the premiss's output binds the conclusion's free variable ("A man came in. So, he wore a hat."). Not an s-entailment.

theorem GroenendijkStokhof1991.atom_entails_exists {E : Type u_1} (x : ℕ) (p : E → Prop) : entails (DPL.toDRS (DPL.Rel.atom fun (g : ℕ → E) => p (g x))) (DPL.toDRS (DPL.Rel.exists_ x (DPL.Rel.atom fun (g : ℕ → E) => p (g x))))

Conversely Px ⊨ ∃xPx — so the pair entail each other, yet are not equivalent (the atom is a test, the existential is not): mutual dynamic entailment is weaker than equivalence (§3.5).

theorem GroenendijkStokhof1991.entails_not_refl {E : Type u_1} [Nontrivial E] : ∃ (φ : DPL.Rel E), ¬entails (DPL.toDRS φ) (DPL.toDRS φ)

Dynamic entailment is not reflexive (§3.5): Px ∧ ∃xQx does not entail itself — its outputs forget that the input satisfied Px. The restricted law (Fact 15) needs AQV(φ) ∩ FV(φ) = ∅.

Satisfaction sets and PL (§3.6)

Fact 19 (§3.6) relates DPL to PL through satisfaction sets: for formulas in normal binding form, \φ\ is the PL meaning. Its proof computes \∃xψ\ = {g | ∃k: k[x]g ∧ k ∈ \ψ\} — cylindrification of the satisfaction set. Under closure (= satisfactionSet, Definition 6) these computations are algebraic identities in the cylindric set algebra ([HMT71]).

theorem GroenendijkStokhof1991.closure_exists_eq_cylindrify {E : Type u_1} (x : ℕ) (φ : DPL.Rel E) : (DPL.toDRS (DPL.Rel.exists_ x φ)).closure = CylindricAlgebra.cylindrify x (DPL.toDRS φ).closure

DPL existential = cylindrification: \∃xφ\ = cₓ\φ\ — the existential case of Fact 19's computation.

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

DPL identity test = diagonal element: \x = y\ = Dxy.

theorem GroenendijkStokhof1991.closure_neg_eq {E : Type u_1} (φ : DPL.Rel E) : (DPL.toDRS φ.neg).closure = fun (g : Assignment E) => ¬(DPL.toDRS φ).closure g

DPL negation complements the satisfaction set: \¬φ\ = ∁\φ\.

The indexed reading: DPL generators as context extension

DPL meanings are relations on total assignments (Definition 2); the indexed substrate (Transition.lean) types them by the contexts they read and write, via the total–typed bridge Transition.ofTotal. Tests (clauses 1–3, 5, 6, 8 are all of this shape) become testTransitions X ⟶ X — the predecessor's DependsOn guard dissolved with the typing — and the random reset of clause 7 is Transition.randomAssign : X ⟶ insert x X. Sequencing is clause 4 (toTransition_comp), and the existential factors through the category unconditionally (randomAssign_comp_toTransition) — a DPL formula's indexed meaning is a composite of the generating arrows of DynamicSemantics.Ctx.

def GroenendijkStokhof1991.toTransition {E : Type u_1} {W : Type u_2} {X Y : Set ℕ} (h : X ⊆ Y) (φ : DPL.Rel E) : DynamicSemantics.Transition W E X Y

A DPL relation as a transition at contexts, worlds inert, via the substrate's total–typed bridge.

Equations

• GroenendijkStokhof1991.toTransition h φ = DynamicSemantics.Transition.ofTotal h fun (x : W) => φ

def GroenendijkStokhof1991.testTransition {E : Type u_1} {W : Type u_2} (X : Set ℕ) (C : (↑X → E) → Prop) : DynamicSemantics.Transition W E X X

A DPL test as a transition: a condition on the context, checked without changing the environment. Clauses 1–3, 5, 6, and 8 of Definition 2 are all of this form.

Equations

• GroenendijkStokhof1991.testTransition X C = { rel := fun (x : W) (e e' : ↑X → E) => e = e' ∧ C e, grow := ⋯ }

theorem GroenendijkStokhof1991.testTransition_apply {E : Type u_1} {W : Type u_2} {X : Set ℕ} {C : (↑X → E) → Prop} (T : Set (W × (↑X → E))) : (testTransition X C).apply T = {e : W × (↑X → E) | e ∈ T ∧ C e.2}

Applying a test filters the fiber — the indexed form of Definition 2's test clauses.

theorem GroenendijkStokhof1991.toTransition_comp {E : Type u_1} {W : Type u_2} {X Y Z : Set ℕ} (h₁ : X ⊆ Y) (h₂ : Y ⊆ Z) {φ ψ : DPL.Rel E} (hψ : DynamicSemantics.Transition.ReadsAt Y fun (x : W) => ψ) : (toTransition h₁ φ).comp (toTransition h₂ ψ) = toTransition ⋯ (φ.conj ψ)

Clause 4 is transition composition: with the second conjunct reading within its context, typed sequencing is DPL conjunction.

theorem GroenendijkStokhof1991.randomAssign_comp_toTransition {E : Type u_1} {W : Type u_2} {X Y : Set ℕ} {x : ℕ} (h : insert x X ⊆ Y) (φ : DPL.Rel E) : (DynamicSemantics.Transition.randomAssign X x).comp (toTransition h φ) = toTransition ⋯ (DPL.Rel.exists_ x φ)

Clause 7 factors through the category, unconditionally: composing the random-assignment arrow with a typed scope is the existential. The scope's transition reads only insert x X, which is what lets the reset's underspecification off x collapse to Definition 2's ∃d.