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.

翻译：动态认知逻辑通过不仅建模静态知识，还建模信息更新引起的知识演化，拓展了经典认知逻辑。在其众多系统中，公共宣告逻辑（PAL）提供了表征认知变化的最简单且研究最深入的框架之一。尽管PAL的语义已通过克里普克模型的变换得到充分理解，但迄今发展的证明理论未能纯粹以句法术语表征这种动态性。本文朝着弥合这一差距迈出了一步。具体而言，基于S5的超矢列演算，我们扩展了一种机制来建模由公共宣告引发的认知模型间的转换。我们将这些结构称为动态超矢列。利用动态超矢列，我们为PAL构建了一个演算，并证明其享有多种理想性质：所有结构规则（包括压缩规则）的可容许性、逻辑规则的可逆性，以及句法切割消去性。