Dynamic Tableaux for Public Announcement Logic
Jonas De Vuyst · 2012
Public announcement logic (PAL) extends epistemic logic with ‘dynamic’ statements of the form [!A]B, which can be read as “After it becomes common knowledge that A is true, B holds”. Interestingly, PAL uses standard S5 n models. To wit, [!A]B is defined to be true at a world w if and only if (i) B holds at w in the model that remains when all the worlds at which A is false are deleted or (ii) w is one of the worlds that would be erased. In the literature on analytic tableaux for PAL two approaches can be distinguished. In [1] and [3] the mathematical structure of tableaux is ammended. Whereas tableaux for standard epistemic logic can be described as graphs whose nodes contain formulas, tableaux for public announcement logic that use this approach have nodes that contain formulas which hold when specific sequences of formulas have been announced. Rules are added that propagate formulas between related histories. In [2], on the other hand, the graph structure of tableaux is not changed. The trick used instead is to incorporate the reduction axioms from axiomatic proof systems for PAL as tableau rules. These rules rewrite dynamic formulas into the language of standard epistemic logic. In this talk I will present preliminary results of my attempt to develop a third approach. An approach that aims to restore some of the elegance that is lost when moving from tableaux for standard epistemic logic to the systems just mentioned. It does not add complexity to the tableau structure and adds only one simple rule. Its most novel feature is that tableaux containing formulas [!A]B are defined to be open only if certain tableaux for B exist that stand in an easy to understand relation to the original tableau.