Dynamic Hypersequents for Public Announcement Logic
It addresses the lack of a fully syntactic proof-theoretic representation of epistemic dynamics in PAL, which is a foundational problem for logicians working on dynamic epistemic logics.
The paper introduces dynamic hypersequents to provide a purely syntactic proof theory for Public Announcement Logic (PAL), demonstrating admissibility of structural rules, invertibility of logical rules, and syntactic cut-elimination.
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. In this paper we propose a step toward addressing this gap. 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.