A cut-free labelled sequent calculus for dynamic epistemic logic. (17th February 2020) - Nomura, Shoshin; Ono, Hiroakira; Sano, Katsuhiko
Abstract: Dynamic epistemic logic is a logic that is aimed at formally expressing how a person's knowledge changes. We provide a cut-free labelled sequent calculus ($GDEL$ ) on the background of existing studies of Hilbert-style axiomatization $HDEL$ of dynamic epistemic logic and labelled calculi for public announcement logic. We first show that the $cut$ rule is admissible in $GDEL$ and show that $GDEL$ is sound and complete for Kripke semantics. Moreover, we show that the basis of $GDEL$ is extended from modal logic K to other familiar modal logics including S5 with keeping the admissibility of cut, soundness and completeness.