Dynamic Hypersequents for Public Announcement Logic

TL;DR

This paper introduces dynamic hypersequents, a new proof-theoretic framework for Public Announcement Logic, enabling syntactic modeling of epistemic updates with desirable proof properties.

Contribution

It extends hypersequent calculus with dynamic mechanisms to represent epistemic model transitions, achieving cut-elimination and rule admissibility.

Findings

Constructed a calculus for PAL using dynamic hypersequents

Proved admissibility of structural rules and cut-elimination

Demonstrated the calculus's desirable proof-theoretic properties

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. 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.