Hans Van Ditmarsch, Tim French

Research output: Contribution to journalArticleAcademicpeer-review


Various extensions of public announcement logic have been proposed with quantification over announcements. The best-known extension is called arbitrary public announcement logic, APAL. It contains a primitive language construct ☐φ intuitively expressing that “after every public announcement of a formula, formula φ is true”. The logic APAL is undecidable and it has an infinitary axiomatization. Now consider restricting the APAL quantification to public announcements of Boolean formulas only, such that ☐φ intuitively expresses that “after every public announcement of a Boolean formula, formula φ is true”. This logic can therefore be called Boolean arbitrary public announcement logic, BAPAL. The logic BAPAL is the subject of this work. Unlike APAL it has a finitary axiomatization. Also, BAPAL is not at least as expressive as APAL. A further claim that BAPAL is decidable is deferred to a companion paper.

Original languageEnglish
Article number20
Number of pages22
JournalLogical Methods in Computer Science
Issue number1
Publication statusPublished - 21 Jan 2022


Dive into the research topics of 'QUANTIFYING OVER BOOLEAN ANNOUNCEMENTS'. Together they form a unique fingerprint.

Cite this