一句话:提出 BAPAL,将 APAL 的公告量化限制为布尔公式,给出有穷公理化并证明其表达力弱于 APAL。
公开公告逻辑 APAL 允许对任意公式的公开公告进行量化,但该逻辑不可判定且仅有无穷公理化。本文将量化范围限制为布尔公式,定义布尔任意公开公告逻辑 BAPAL,其中 Box φ 表示任意布尔公式公开公告后 φ 为真。工作给出 BAPAL 的有穷公理化,并证明 BAPAL 不至少与 APAL 一样有表达力,即其表达力弱于 APAL。可判定性结论则留待姊妹篇。该结果为公告量化提供了一种受布尔限制的折中,降低了公理化的复杂度。
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 Box phi intuitively expressing that "after every public announcement of a formula, formula phi 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 Box phi intuitively expresses that "after every public announcement of a Boolean formula, formula phi is true". This logic can therefore 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.