Towards a Proof-Theoretic Semantics for Dynamic Logics
Vlasta Sikimic

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.