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.