QUANTIFYING OVER BOOLEAN ANNOUNCEMENTS

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.