Logics for information update

Logical languages define propositions that describe states of the world, represented by some suitably chosen model. The typical format for this is a semantic truth definition M, s vp saying that formula p is true at state s of model M. In terms of this schema, one can then define valid reasoning as all steps from formulas to formulas that preserve truth. The usual systems of epistemic logic follow this set-up, and the resulting account of reasoning is useful and well-known. But there is also a limitation to this perspective. It leaves out the 'logical dynamics' of many natural processes, such as communicating information. In that case, the basic phenomena are actions which change information states of speakers and hearers, and the locus of 'meaning' for a proposition is not its static content, but the dynamic change it induces from one model M, viewed as an information state for logical agents, to another: announcing p changes M, s into N, t. One now becomes interested in cognitive actions like informing, questioning, answering - with inference as an important, but by no means the only example. This Dynamic Turn has emerged in many areas: linguistics (Kamp, Heim, Groenendijk & Stokhof), philosophy and AI (Gardenfors, Harman), computational linguistics (Gross & Sidner, Gabbay, Kempson & Meyer Viol) and computer science (Fagin/Halpern/Moses/Vardi, Abramsky, Reiter). This tutorial presents an overview of update logics for communicative actions. The basic tool is: Hintikka-Kripke models for epistemic languages. The difficult questions are twofold. First, what precise updates are induced by various types of communicative action? One line in the literature has looked at examples of increasing complexity. Models and update procedures are simple for questions/answers, or public announcements, but they get much more complex as communication gets more 'private'. We follow one such line in current research, referring to work by Veltman, Groeneveld & Gerbrandy, and Baltag, Solecki & Moss on information update in conversation and games, whose current challenges include more complex linguistic expressions, defaults and cryptographic communication. This requires building sophisticated models in harmony with the observed phenomena. Our second topic concerns new logical issues in this setting. In a way, all relevant dynamics is contained in existing epistemic logics cum temporal models. But this observation is no more useful than saying we can do most of modern logic inside first-order logic, and all of it inside set theory. Instead, we survey new questions beyond the usual agenda. Examples are: (a) relating model-theoretic to syntactic views of update, (b) (non-)persistence of assertions under update, (c) calculi for short-term dynamic 'local inference', and connections with longer-term 'global inference'. References for the general program (1) J. van Benthem, 1996, "Exploring Logical Dynamics", CSLI Publications, Stanford. (2) R. Muskens & A. Visser, 'Dynamics', in J. van Benthem & A. ter Meulen, eds., 1997, "Hand-book of Logic & Language", Elsevier, Amsterdam. (3) J. van Benthem, 2000, 'Update Delights', http://turing.wins.uva.nl/~johan/Update.Delights.ps, ILLC, University of Amsterdam - for proofs and details. The rest of this paper is a brief tour of some technical issues in update logic, starting with a simple card game, which highlights some essential questions. The tutorial at TARK itself will be example-oriented.