Dynamic Predicate Logic

This file formalizes the logical facts of Groenendijk and Stokhof's "Dynamic predicate logic", in which a formula denotes a relation between assignments. The paper's semantics is the update algebra of Semantics/Dynamic/Update.lean: conjunction is relational composition, the existential is a random reset followed by its scope, and negation, implication, disjunction, the universal, and closure are the tests of the conditions neg, impl, disj, dforall, and SetRel.dom, which is the content of the paper's translation of discourse representation theory. Only the quantifiers mention assignments, so the propositional laws are proved of updates over any state type and the quantifier laws over any register structure.

The notions of section 3.2 come first: s-equivalence and p-equivalence, which equivalence implies but which together do not imply it, and the tests, on which all three coincide. Section 3.4 then supplies the laws. The connectives are definable from negation, conjunction, and the existential but not conversely, since a negation is a test and an existential is one only over a contradictory scope (isTest_dexists_iff); double negation, commutativity, and idempotency of conjunction hold exactly of tests, while contraposition, currying, and the de Morgan laws hold outright. An existential binds without limit to its right because composition is associative (scope_extension), and it has universal force in an antecedent because implication curries (donkey_equivalence). Section 3.5's dynamic entailment (Entails) satisfies the deduction theorem and reduces s-entailment to entailment from the closed premiss, and it is neither reflexive nor transitive (not_entails_self, not_entails_trans), by the paper's own counterexamples: ¬¬∃x Px entails ∃x Px, which entails Px, but the first does not entail the third. The satisfaction set of an existential computed in the proof of Fact 19 is the cylindrification of its scope's, in the cylindric set algebra of Henkin, Monk and Tarski; that is the substrate's dom_dexists. The laws are then read off for the formulas of DPL/Syntax.lean under their interpretation DPL.Formula.eval, and the paper's opening contrast is computed: ∃x Px ∧ Qx binds the last occurrence of x, while its double negation and its alphabetic variant ∃y Py ∧ Qx do not. Section 4.1's normal binding form (nbf) is defined by structural recursion, Definition 24's rebracketing clauses being theorems of it; a formula is equivalent to its normal binding form, which is scope-bound, so that the dynamic truth conditions of any formula are the first-order satisfaction conditions of its normal binding form (mem_dom_eval_iff_realize_nbf). Conversely, eliminating conjunction, implication and the existential gives every formula a scope-bound equivalent in predicate logic (mem_dom_eval_staticForm_iff). Section 4.2's translation of discourse representation structures (DRT.DRS.toDPL, Definition 28) preserves meaning: a condition becomes the test of its verification and a box denotes its box relation (DRT.DRS.eval_toDPL, Fact 25).

Implementation notes

The paper quantifies over models; an Update S fixes one, so its equivalence is equality of relations, its contradiction is ∅, and its counterexamples are stated over assignments into a domain with two individuals, [Nontrivial E]. Truth with respect to an assignment and the satisfaction set are both SetRel.dom, and the production set is SetRel.cod. That conditions are tests, that tests are closed under conjunction, and that a test's production set is its satisfaction set are the substrate's isTest_test, IsTest.comp, and IsTest.cod_eq_dom; that closure and negation are idempotent on tests is dom_test. The paper lists idempotency of disjunction as unconditional, but a disjunction is a test by Definition 2, so φ ∨ φ is the closure of φ (disj_self) and the law holds exactly of tests. Fact 5, that a condition is a test, is the substrate's DPL.Formula.isTest_eval. Fact 6, that the tests are the conditions and the contradictions, holds up to equivalence, a test being equivalent to the condition ¬¬φ (neg_neg_eq_self_iff_isTest), and not of the syntactic class itself: x = y ∧ ∃x[x = y] is a test in every structure and has an active quantifier (isTest_eval_equal_conj_ex_equal).

References

• Groenendijk & Stokhof 1991, Dynamic Predicate Logic
• Henkin et al. 1971, Cylindric Algebras, Part I
• Kamp & Reyle 1993, From Discourse to Logic formalized

TODO

The remaining laws of section 3.4 with side conditions (the leftward scope extension, commutativity and idempotency of conjunction, contraposition, distribution), the restricted reflexivity and transitivity of dynamic entailment (Facts 15 and 16), Facts 26 and 27 on the translated conditions, and the translation to quantificational dynamic logic of section 4.3.