Abstract

This thesis provides an analysis of the existing proof systems for dynamic epistemic logic from the viewpoint of proof-theoretic semantics. After an illustration of the basic principles of proof-theoretic semantics, we review some of the most significant proposals of proof systems for dynamic epistemic logics, and we critically reject on them in the light of proof-theoretic semantic principles. The main original contributions of the present thesis are: (a) a revised version of the display-style calculus D.EAK, which we argue to be more adequate from the proof-theoretic semantic viewpoint; the main feature of this revision is that a smoother proof (so-called Belnap-style) of cut-elimination holds for it, which is problematic for the original version of D.EAK. (b) The intro duction of a novel, multi-type display calculus for dynamic epistemic logic, which we refer to as Dynamic Calculus. The presence of types endows the language of the Dynamic Calculus with additional expressivity, and makes it possible to design rules with an even smoother behavior. We argue that this calculus paves the way towards a general methodology for the design of proof systems for the generality of dynamic logics, and certainly for proof systems beyond dynamic epistemic logic. We prove that the Dynamic Calculus adequately captures Baltag-Moss-Solecki's dynamic epistemic logic, and enjoys Belnap-style cut elimination.