Dynamic Hypersequents for Public Announcement Logic
Clara Lerouvillois, Francesca Poggiolesi
TL;DR
The paper develops a syntactic, proof-theoretic treatment of Public Announcement Logic by introducing dynamic hypersequents, an extension of hypersequent calculi for S5 that encodes updates caused by public announcements. It defines a calculus DHS$_{PAL}$ with dynamic, announcement, and merge rules, and proves hp-admissibility of structural rules, hp-invertibility of logical rules, soundness, completeness, and syntactic cut-elimination. A key contribution is the derivability of the announcement-composition axiom via a DHS-complexity framework and a derivability lemma, enabling full PAL derivability within the calculus. The results establish a robust, purely syntactic account of PAL dynamics and open paths to broader dynamic epistemic logics and decidability analyses.
Abstract
Dynamic Epistemic Logic extends classical epistemic logic by modeling not only static knowledge but also its evolution through information updates. Among its various systems, Public Announcement Logic (PAL) provides one of the simplest and most studied frameworks for representing epistemic change. While the semantics of PAL is well understood as transformation of Kripke models, the proof theory so far developed fails to represent this dynamism in purely syntactical terms. The aim of this paper is to repair this lack. In particular, building on a hypersequent calculus for S5, we extend it with a mechanism that models the transition between epistemic models induced by public announcements. We call these structures dynamic hypersequents. Using dynamic hypersequents, we construct a calculus for PAL and we show that it enjoys several desirable properties: admissibility of all structural rules (including contraction), invertibility of logical rules, as well as syntactic cut-elimination.