A Cut-Free Labelled Sequent Calculus for Dynamic Epistemic Logic

摘要

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 by Baltag et al. (1989) and labelled calculi for Public Announcement Logic by Maffezioli et al. (2011) and Nomura et al. (2015). We first show that the cut rule is admissible in GDEL. Then we show GDEL is sound and complete for Kripke semantics. Lastly, we touch briefly on our on-going work of an automated theorem prover of GDEL.