A cut-free labelled sequent calculus for dynamic epistemic logic. (17th February 2020)

• Record Type: Journal Article
• Authors: Nomura, Shoshin; Ono, Hiroakira; Sano, Katsuhiko
• Is Part Of: Journal of logic and computation. Volume 30:Number 1(2020)
• Page Start: 321
• Page End: 348
• Publication Date: 2020-02-17
• Subjects: Logic programming -- Periodicals; Logic, Symbolic and mathematical -- Periodicals; Computational complexity -- Periodicals; 005.115
• DOI: 10.1093/logcom/exaa014
• Languages: English
• ISSNs: 0955-792X

Abstract

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 ($\textbf{GDEL}$ ) on the background of existing studies of Hilbert-style axiomatization $\textbf{HDEL}$ of dynamic epistemic logic and labelled calculi for public announcement logic. We first show that the $cut$ rule is admissible in $\textbf{GDEL}$ and show that $\textbf{GDEL}$ is sound and complete for Kripke semantics. Moreover, we show that the basis of $\textbf{GDEL}$ is extended from modal logic K to other familiar modal logics including S5 with keeping the admissibility of cut, soundness and completeness.