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.
| Original language | English |
|---|---|
| Pages (from-to) | 2017-2065 |
| Number of pages | 49 |
| Journal | Journal of Logic and Computation |
| Volume | 26 |
| Issue number | 6 |
| DOIs | |
| Publication status | Published - 1 Jan 2016 |
| Externally published | Yes |
Funding
The research of G.G. and A.P. has been made possible by the NWO Vidi grant 016.138.314, by the NWO Aspasia grant 015.008.054 and by a Delft Technology Fellowship awarded in 2013 to A.P.
Keywords
- Display calculus
- Dynamic epistemic logic
- Modularity
- Multi-type system