Algebraic Semantics and Model Completeness for Intuitionistic Public Announcement Logic

In this paper, we start studying epistemic updates using the standard toolkit of duality theory. We focus on public announcements. We give the dual characterization of the corresponding submodel-injection map, as a certain pseudo-quotient map between the complex algebras respectively associated with the given model and with its relativized submodel. The dual characterization we provide naturally generalizes to much wider classes of algebras, which include, but are not limited to, arbitrary BAOs and arbitrary modal expansions of Heyting algebras (HAOs). As an application, we axiomatize the intuitionistic analogue of PAL, which we refer to as IPAL, and prove soundness and completeness of IPAL w.r.t. both algebraic and relational models.