About intuitionistic public announcement logic

Abstract

Public announcement logic (PAL) is a logic for reasoning about the dynamic of knowledge in a multi-agent system in which public announcements are made. Syntactically, public announcements are modal formulas. Semantically, they correspond to restrictions of models. Ma et al. (2014) use the standard toolkit of duality theory in modal logic to define an algebraic semantics for a combination of IPL and PAL into intuitionistic public announcement logic (IPAL). In this paper, grounding our approach on relational semantics rather than on algebraic semantics, we give a sound and complete axiomatization of IPAL and we consider a complete sequent calculus for the associated membership problem.