Dynamic epistemic logic with branching temporal structures (Q1036059): Difference between revisions

The authors investigate the relationship between dynamic epistemic logics (DEL) as proposed by \textit{A. Baltag, L. S. Moss} and \textit{S. Solecki} in [``The logic of public announcements, common knowledge, and private suspicions'', in: I. Gilboa (ed.), Proceedings of the 7th conference on theoretical aspects of rationality and knowledge, TARK '98. San Francisco: Morgan Kaufmann. 43--56 (1998)] and epistemic temporal logics as proposed by \textit{R. Fagin, J. Y. Halpern, Y. Moses} and \textit{M. Y. Vardi} in their 1995 book [Reasoning about knowledge. Cambridge, MA: MIT Press (1995; Zbl 0839.68095)]. This is part of a research program launched by \textit{J. van Benthem, J. Gerbrandy} and \textit{E. Pacuit} in [``Merging frameworks for interaction: DEL and ETL'', in: D. Samet (ed.), Proceedings of the 11th conference on theoretical aspects of rationality and knowledge, TARK 2007. Louvain-la-neuve: Presses Universitaires de Louvain. 72--81 (2007)]. The present paper improves over the 2009 paper by \textit{J. van Benthem, J. Gerbrandy, T. Hoshi} and \textit{E. Pacuit} [J. Philos. Log. 38, No. 5, 491--526 (2009; Zbl 1185.03019)] in two ways: first, the reconstruction of DELs in ETL is extended from public announcement logic to general event models; second, a past operator indexed by an event model is added to the language, in a way similar to \textit{J. Sack}'s paper [J. Logic Lang. Inf. 17, No. 2, 183--216 (2008; Zbl 1184.03010)]. For both extensions, axiomatizations and completeness proofs are provided. For the former it is a straightforward adaptation of the axiomatics of the 2009 JPL paper. The latter is made up of (1) an axiom F5 stipulating that it cannot be the case that two different events just took place (where `different' here means `syntactically different'), (2) an axiom F6 that is equivalent to the conversion axioms of temporal logics, (3) the K-axiom (that is here formulated for the existential version of the past operator), (4) the necessitation rule and (5) a further, non-standard inference rule. The authors finally discuss some issues such as forgetting.