A Cut−Free Sequent Calculus for Algebraic Dynamic Epistemic Logic
Mehrnoosh Sadrzadeh · 2010
We develop a cut-free sequent calculus for a Dynamic Epistemic Logic. The calculus is nested and represents a sub-structural action logic which acts on a propositional logic via a dynamic modality and its left adjoint update. Both logics are positive and have agent-indexed adjoint pairs of epistemic modalities. We prove admissibility (where appropriate) of Weakening and Contraction and Cut, as well as soundness and completeness theorems with regard to the algebraic semantics. To model epistemic protocols, we add assumption rules, prove that the admissibility results are preserved, and derive properties of a toy protocol that has honest and dishonest public and private announcements.