Multi-type display calculus for dynamic epistemic logic
- 5 December 2014
- journal article
- research article
- Published by Oxford University Press (OUP) in Journal of Logic and Computation
- Vol. 26 (6) , 2017-2065
Abstract
In the present article, we introduce a multi-type display calculus for dynamic epistemic logic, which we refer to as Dynamic Calculus. The display approach is suitable to modularly chart the space of dynamic epistemic logics on weaker-than-classical propositional base. The presence of types endows the language of the Dynamic Calculus with additional expressivity, allows for a smooth proof-theoretic treatment, and paves the way towards a general methodology for the design of proof systems for the generality of dynamic logics, and certainly beyond dynamic epistemic logic. We prove that the Dynamic Calculus adequately captures Baltag–Moss–Solecki's dynamic epistemic logic, and enjoys Belnap-style cut elimination.Keywords
All Related Versions
This publication has 20 references indexed in Scilit:
- Algebraic semantics and model completeness for Intuitionistic Public Announcement LogicAnnals of Pure and Applied Logic, 2014
- Algebra, proof theory and applications for an intuitionistic logic of propositions, actions and adjoint modal operatorsACM Transactions on Computational Logic, 2013
- Dynamic Epistemic Logic DisplayedLecture Notes in Computer Science, 2013
- Algorithmic correspondence and canonicity for distributive modal logicAnnals of Pure and Applied Logic, 2012
- Logics of public communicationsSynthese, 2007
- Epistemic Actions as ResourcesJournal of Logic and Computation, 2007
- Sequent Systems for Modal Logics2002
- Dual Intuitionistic Logic Revisited2000
- Linear logic displayed.Notre Dame Journal of Formal Logic, 1989
- Display logicJournal of Philosophical Logic, 1982