Multi-type Display Calculus for Dynamic Epistemic Logic

TL;DR

This paper introduces a multi-type display calculus for dynamic epistemic logic, enhancing expressivity and modularity, and proves its soundness and cut elimination, advancing proof systems for dynamic logics.

Contribution

It presents a novel multi-type display calculus for dynamic epistemic logic, enabling modular and expressive proof-theoretic analysis.

Findings

Captures Baltag-Moss-Solecki's dynamic epistemic logic accurately

Achieves Belnap-style cut elimination

Provides a general methodology for dynamic logic proof systems

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.