What can we achieve by arbitrary announcements?

Abstract

Public announcement logic is an extension of multi-agent epistemic logic with dynamic operators to model the informational consequences of announcements to the entire group of agents. We propose an extension of public announcement logic with a dynamic modal operator that expresses what is true after any announcement: □φ expresses that φ is true after an arbitrary announcement ψ. As this includes the trivial announcement ⊤, one might as well say that □φ expresses what remains true after any announcement: it therefore corresponds to truth persistence after (definable) relativisation. The dual operation ⋄φ expresses that there is an announcement after which φ. This gives a perspective on Fitch's knowability issues: for which formulas φ does it hold that φ → ⋄Kφ? We give various semantic results, and we show completeness for a Hilbert-style axiomatisation of this logic.