Dynamic Semantics

This file formalizes Predicate Logic with Anaphora, the system of Dekker 1994 as consolidated in Dekker 2012: a Tarskian satisfaction semantics for a first-order language with pronouns, in which the dynamics of anaphora lives in one extra parameter, the sequence of witnesses, rather than in the notion of content. A pronoun is an index into that sequence, an existential prepends its witness to it, the second conjunct of a conjunction is evaluated after the first conjunct's witnesses, and negation quantifies witnesses away, Definition 4. The domain and range of a formula, Definition 3, count the witnesses it contributes and demands, and satisfaction reads the sequence no further than their sum. Implication then reads the antecedent's existentials universally, Observation 3, the discourse (9) and the donkey sentence (12) come out equivalent to their pronoun-free renderings, and on pronoun-free formulas truth obeys the classical clauses, Observation 4. Conjunction is neither idempotent nor commutative, Observation 9, with the book's example (14) as witness. Dynamic entailment, Definition 6, passes the premises' witnesses to the conclusion: it is classical on pronoun-free conclusions, Observation 10, validates Heim's inference (15) and the deduction theorem, Observation 11, and though neither reflexive nor monotone it obeys the acute identity and monotonicity rules of Observation 12 once pronouns are updated for the witnesses that intervene, Definition 7. Chapter 3 lifts the system to worlds with witnesses as individual concepts: contents, updates and support are each defined recursively, Definitions 1 to 3 of that chapter, and coincide, Observation 15 reducing contents to satisfaction world by world, Observation 16 making an update the intersection with the content and Observation 17 making support inclusion in it, so that supported updates never corrupt a hearer's information, Observation 18.

Implementation notes

The book's witness sequences are finite and long enough for the formula; here a sequence is a Stream', and sat_congr shows that satisfaction reads only its first domain + range entries, so length bookkeeping disappears while the finite blocks of witnesses a formula contributes stay lists of the right length. Pronoun pron i is the book's pᵢ₊₁, the i-th most recent witness. Relation and constant symbols are strings interpreted by the model. Observations 5 to 8, the α-conversion and binding algorithm that eliminate pronouns, and the cut rule of Observation 13 are not formalized; neither are the conceptual covers of Chapter 3 nor Chapter 4.

TODO

Observation 12's monotonicity rule inserts a premise χ before the last j premises and updates only the conclusion's pronouns, leaving those premises to be read against χ's witnesses instead of the ones they had; with ∃x Px, Q p₁ ⊨ Q p₁ and χ = ∃y Ry the rule so stated fails, since the middle premise now says Q of χ's witness. entails_update_of_entails states the rule with those premises updated as well, which the proof of the book's rule needs; the end-of-sequence case j = 0 is unaffected.

References

• Dekker 2012, Dynamic Semantics
• Dekker 1994, Predicate Logic with Anaphora
• Groenendijk & Stokhof 1991, Dynamic Predicate Logic formalized
• Heim 1982, The Semantics of Definite and Indefinite Noun Phrases formalized
• Stalnaker 1978, Assertion formalized