Groenendijk & Stokhof (1991): Dynamic Predicate Logic #

Dynamic Predicate Logic. Linguistics and Philosophy 14(1): 39-100.

Key Claims Verified #

Cross-sentential anaphora (§2.1): Existential quantifiers bind variables across conjunction (scope_extension).
Donkey sentences (§2.4): Existential quantifiers in the antecedent of an implication have universal force (donkey_equivalence).
Blocking (§2.5): Universal quantifiers, negation, implication, and disjunction are externally static — they do not export bindings.
DNE failure (§3.4): Double negation elimination fails for anaphora (dpl_dne_fails_anaphora), because negation resets the output assignment.
Interdefinability (§3.4): →, ∨, ∀ are definable from ¬, ∧, ∃, but not vice versa — the DPL asymmetry.

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

DPL translation: ∃x[man(x) ∧ walk_in_park(x)] ∧ whistle(x)

The scope extension theorem shows this equals ∃x[man(x) ∧ walk_in_park(x) ∧ whistle(x)]: the existential quantifier's binding power extends across conjunction.

This accounts for Heim1982.Examples.indefinite_persists.

source

theorem GroenendijkStokhof1991.indefinite_persistence_predicted {E : Type u_1} (x : ℕ) (P Q R : Semantics.Dynamic.DPL.DPLRel E) (hfree : ∀ (g h : ℕ → E) (d : E), R g h ↔ R (fun (n : ℕ) => if n = x then d else g n) fun (n : ℕ) => if n = x then d else h n) :

Semantics.Dynamic.DPL.exists_ x ((P.conj Q).conj R) = (Semantics.Dynamic.DPL.exists_ x (P.conj Q)).conj R

DPL correctly predicts indefinite persistence: scope extension ensures ∃x in the first sentence binds x in the second.

"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, this is equivalent to: ∀x[farmer(x) ∧ ∃y[donkey(y) ∧ own(x,y)] → beat(x,y)]

And applying it again for y: ∀x∀y[farmer(x) ∧ donkey(y) ∧ own(x,y) → beat(x,y)]

This gives the universal "strong" reading recorded for Geach1962.Examples.donkey_classic and Heim1982.Examples.conditional_donkey.

source

theorem GroenendijkStokhof1991.donkey_universal_force {E : Type u_1} (x : ℕ) (φ ψ : Semantics.Dynamic.DPL.DPLRel E) :

(Semantics.Dynamic.DPL.exists_ x φ).impl ψ = Semantics.Dynamic.DPL.forall_ x (φ.impl ψ)

The donkey equivalence gives universal force to indefinites in conditional antecedents, matching the strong/universal reading of Heim1982.Examples.conditional_donkey.

"Every man walked in. *He sat down."

The universal quantifier is a test: ⟦∀xφ⟧(g,h) forces g = h. This means no new bindings are created — the pronoun "he" has no accessible antecedent.

This accounts for Heim1982.Examples.universal_blocks.

source

theorem GroenendijkStokhof1991.universal_blocks_anaphora {E : Type u_1} (x : ℕ) (φ : Semantics.Dynamic.DPL.DPLRel E) (g h : ℕ → E) (hfa : Semantics.Dynamic.DPL.forall_ x φ g h) :

g = h

Universal quantification is externally static: it cannot introduce discourse referents. Any formula following ∀xφ sees the same assignment as before.

source

theorem GroenendijkStokhof1991.negation_blocks_anaphora {E : Type u_1} (φ : Semantics.Dynamic.DPL.DPLRel E) (g h : ℕ → E) (hn : φ.neg g h) :

g = h

Negation is externally static: it blocks anaphora. Accounts for Heim1982.Examples.standard_negation_blocks.

source

theorem GroenendijkStokhof1991.implication_blocks_anaphora {E : Type u_1} (φ ψ : Semantics.Dynamic.DPL.DPLRel E) (g h : ℕ → E) (hi : φ.impl ψ g h) :

g = h

Implication is externally static: bindings in the antecedent or consequent don't escape. Accounts for Heim1982.Examples.conditional_antecedent.

"It is not the case that nobody walked in. *He sat down."

Double negation ¬¬∃xφ is a test (g = h), so it cannot export the witness introduced by ∃x. This contrasts with ∃xφ itself, which does export. Hence ¬¬∃xφ ≠ ∃xφ.

A known limitation of DPL: doubly negated indefinites do in fact license anaphora (ElliottSudo2025.Examples.double_negation is judged acceptable), so DPL underpredicts here. The divergence is stated as a theorem in Studies/ElliottSudo2025.lean (dpl_diverges_on_double_negation), where the later, comparing paper lives.

source

theorem GroenendijkStokhof1991.dne_blocks_anaphora_dpl_prediction {E : Type u_1} [Nontrivial E] :

∃ (x : ℕ), ∃ (φ : Semantics.Dynamic.DPL.DPLRel E), (Semantics.Dynamic.DPL.exists_ x φ).neg.neg ≠ Semantics.Dynamic.DPL.exists_ x φ

DPL predicts double negation blocks anaphora, contra the empirical judgment in ElliottSudo2025.Examples.double_negation. This is the well-known DPL limitation that [ES25a] and bilateral update semantics address.

In standard PL, any pair from {¬, ∧, ∨, →} plus quantifiers suffices to define the others. In DPL, only {¬, ∧, ∃} works as a basis — {¬, →, ∀} and {¬, ∨, ∀} cannot define conjunction or existential quantification, because ∧ and ∃ are the only connectives that are externally dynamic.

source