Abstract

This paper proposes non-labelled sequent calculi, G(K45PAL) and G(SK5PAL), for the public announcement expansions of modal logics K45 and S5. We transform each of the recursion axioms of PAL into left and right rules for the sequent calculi. For G(K45PAL), the cut elimination theorem is shown using the complexity measure introduced by van Ditmarsch et al. (2007). This measure was originally employed to establish semantic completeness via recursion axioms. While the cut elimination theorem fails in G(SK5PAL), we adopt Takano’s strategy (1992) to establish that the cut formula in G(SK5PAL) can be restricted to the set of suitably extended subformulas (i.e., closure) of the conclusion of the cut rule.