Multi-type Display Calculus for Dynamic Epistemic Logic
Logic
2018-05-22 v1
Abstract
In the present paper, 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
Cite
@article{arxiv.1805.07586,
title = {Multi-type Display Calculus for Dynamic Epistemic Logic},
author = {Sabine Frittella and Giuseppe Greco and Alexander Kurz and Alessandra Palmigiano and Vlasta Sikimić},
journal= {arXiv preprint arXiv:1805.07586},
year = {2018}
}