Algebraic semantics and model completeness for Intuitionistic Public Announcement Logic

Minghui Ma, Alessandra Palmigiano*, Mehrnoosh Sadrzadeh

*Corresponding author for this work

Research output: Contribution to JournalArticleAcademicpeer-review


In the present paper, we start studying epistemic updates using the standard toolkit of duality theory. We focus on public announcements, which are the simplest epistemic actions, and hence on Public Announcement Logic (PAL) without the common knowledge operator. As is well known, the epistemic action of publicly announcing a given proposition is semantically represented as a transformation of the model encoding the current epistemic setup of the given agents; the given current model being replaced with its submodel relativized to the announced proposition. We dually characterize the associated submodel-injection map as a certain pseudo-quotient map between the complex algebras respectively associated with the given model and with its relativized submodel. As is well known, these complex algebras are complete atomic BAOs (Boolean algebras with operators). 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). Thanks to this construction, the benefits and the wider scope of applications given by a point-free, intuitionistic theory of epistemic updates are made available. As an application of this dual characterization, we axiomatize the intuitionistic analogue of PAL, which we refer to as IPAL, prove soundness and completeness of IPAL w.r.t. both algebraic and relational models, and show that the well known Muddy Children Puzzle can be formalized in IPAL.

Original languageEnglish
Pages (from-to)963-995
Number of pages33
JournalAnnals of Pure and Applied Logic
Issue number4
Publication statusPublished - 1 Apr 2014
Externally publishedYes


  • Algebraic models
  • Duality
  • Intuitionistic modal logic
  • Intuitionistic Public Announcement Logic
  • Pointfree semantics
  • Public Announcement Logic


Dive into the research topics of 'Algebraic semantics and model completeness for Intuitionistic Public Announcement Logic'. Together they form a unique fingerprint.

Cite this