Multi-type Display Calculus for Dynamic Epistemic Logic

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.

References in corpus (4)

• Multi-type display calculus for Propositional Dynamic Logic
• A Proof-Theoretic Semantic Analysis of Dynamic Epistemic Logic
• Epistemic Updates on Algebras
• Annotation-Free Sequent Calculi for Full Intuitionistic Linear Logic -- Extended Version

Cited by in corpus (12)

• Multi-type display calculus for Propositional Dynamic Logic
• A Proof-Theoretic Semantic Analysis of Dynamic Epistemic Logic
• Multi-type Sequent Calculi
• Algebraic proof theory for LE-logics
• The Logic of Resources and Capabilities
• Non normal logics: semantic analysis and proof theory
• Unified Correspondence as a Proof-Theoretic Tool
• Vector spaces as Kripke frames
• Completeness of Nominal PROPs
• Tool support for reasoning in display calculi
• First order logic properly displayed
• Non-normal logics: semantic analysis and proof theory (extended version)