## Abstract

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 language | English |
---|---|

Article number | 20 |

Number of pages | 22 |

Journal | Logical Methods in Computer Science |

Volume | 18 |

Issue number | 1 |

DOIs | |

Publication status | Published - 21 Jan 2022 |