A Reduction-based Cut-free Gentzen Calculus for Dynamic Epistemic Logic

Wirsing, Martin and Knapp, Alexander (2022): A Reduction-based Cut-free Gentzen Calculus for Dynamic Epistemic Logic. In: Logic Journal of the Igpl, Vol. 31, No. 6: pp. 1047-1068

Abstract

Dynamic epistemic logic (DEL) is a multi-modal logic for reasoning about the change of knowledge in multi-agent systems. It extends epistemic logic by a modal operator for actions which announce logical formulas to other agents. In Hilbert-style proof calculi for DEL, modal action formulas are reduced to epistemic logic, whereas current sequent calculi for DEL are labelled systems which internalize the semantic accessibility relation of the modal operators, as well as the accessibility relation underlying the semantics of the actions. We present a novel cut-free ordinary sequent calculus, called G4(P,A)[], for propositional DEL. In contrast to the known sequent calculi, our calculus does not internalize the accessibility relations, but-similar to Hilbert style proof calculi-action formulas are reduced to epistemic formulas. Since no ordinary sequent calculus for full S5 modal logic is known, the proof rules for the knowledge operator and the Boolean operators are those of an underlying S4 modal calculus. We show the soundness and completeness of G4(P,A)[] and prove also the admissibility of the cut-rule and of several other rules for introducing the action modality.

• Item Type: Journal article
• Faculties: Mathematics, Computer Science and Statistics > Computer Science
• Subjects: 000 Computer science, information and general works > 004 Data processing computer science
• ISSN: 1367-0751
• Language: English