Multi-type display calculus for dynamic epistemic logic
Sabine Frittella (Aix Marseille Université)
Giuseppe Greco (TU Delft - Ethics & Philosophy of Technology)
Alexander Kurz (University of Leicester)
Alessandra Palmigiano (TU Delft - Ethics & Philosophy of Technology)
Vlasta Sikimić (University of Belgrade)
More Info
expand_more
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.