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.

翻译：动态认知逻辑通过建模信息更新来扩展经典认知逻辑，不仅描述静态知识，还刻画其动态演化过程。在众多系统中，公共宣告逻辑（PAL）为表示认知变化提供了最简单且研究最深入的框架之一。尽管PAL的语义在克里普克模型变换层面已得到充分理解，但迄今发展的证明理论未能以纯句法方式体现这种动态性。本文旨在弥补这一缺陷。具体而言，我们在S5的超序列演算基础上，引入一种机制来建模由公共宣告引发的认知模型间转换，称此类结构为动态超序列。利用动态超序列，我们构建了PAL的演算系统，并证明其具备若干理想性质：所有结构规则（包括收缩规则）的可接纳性、逻辑规则的可逆性，以及句法层面的切割消除性。