A Cut−Free Sequent Calculus for Algebraic Dynamic Epistemic Logic

Abstract

We develop a cut-free sequent calculus for an algebraic semantics of a Dynamic Epistemic Logic. The calculus is nested and consists of an action linear logic which acts on a propositional logic via a dynamic modality and its left adjoint update. Both logics are positive and have adjoint epistemic modalities. We prove admssibility of cuts, contraction, and weakening (where appropriate), as well as soundness and completeness theorems with regard to the algebraic semantics. To model epistemic protocols, we add assumption rules, prove that they preserve the admissibility results, and derive properties of a toy protocol that has honest and dishonest public and private announcements.