# Satisfiability of Quantified Boolean announcements

Hans van Ditmarsch, Tim French, Rustam Galimullin Open University of the
Netherlands<EMAIL_ADDRESS>of Western Australia, Perth,
Australia<EMAIL_ADDRESS>of Bergen, Bergen, Norway;
<EMAIL_ADDRESS>
###### Abstract

Dynamic epistemic logics consider formal representations of agents’ knowledge,
and how the knowledge of agents changes in response to informative events,
such as public announcements. Quantifying over informative events allows us to
ask whether it is possible to achieve some state of knowledge, and has
important applications in synthesising secure communication protocols.
However, quantifying over quite simple informative events, public
announcements, is not computable: such an arbitrary public announcement logic,
$\mathit{APAL}{}$, has an undecidable satisfiability problem. Here we consider
even simpler informative events called Boolean announcements, where
announcements are restricted to be a Boolean combination of atomic
propositions. The logic is called Boolean arbitrary public announcement logic,
$\mathit{BAPAL}{}$. A companion paper provides a complete finitary
axiomatization, and related expressivity results, for $\mathit{BAPAL}$. In
this work the satisfiability problem for $\mathit{BAPAL}{}$ is shown to
decidable, and also that $\mathit{BAPAL}{}$ does not have the finite model
property.

##  1 Introduction

Public announcement logic ($\mathit{PAL}$) [12, 14] extends epistemic logic
with operators for reasoning about the effects of specific public
announcements. The formula $[\psi]\varphi$ means that “$\varphi$ is true after
the truthful announcement of $\psi$.” This means that, when interpreted in a
Kripke model with a designated state, after submodel restriction to the states
where $\psi$ is true (this includes the designated state, ‘truthful’ here
means true), $\varphi$ is true in that restriction. Arbitrary public
announcement logic ($\mathit{APAL}$) [4] augments this with operators for
quantifying over public announcements. The formula $\Box\varphi$ means that
“$\varphi$ is true after the truthful announcement of any formula that does
not contain $\Box$.” It is known that satisfiability in $\mathit{APAL}$ is
undecidable [10] and also for some related logics [3] quantifying over less
than all public announcements.

One such restriction is only to permit quantification over announcements of
Boolean formulas (so-called Boolean announcements). This Boolean arbitrary
public announcement logic ($\mathit{BAPAL}$) has been reported in [17]. It
should be considered as a companion paper providing a background and
motivation for this logic $\mathit{BAPAL}$. It also provides a finitary
axiomatisation and several expressivity results. In the current paper we
further provide a computable procedure for testing the satisfiability of
$\mathit{BAPAL}{}$ formulas:

> $\mathit{BAPAL}$ is decidable.

As most such logics with quantification over information change are
undecidable [3, 16] or have trivial expressivity with respect to the logic
without quantifiers [13, 7, 8] this seems a remarkable result.

Additionally, we show in the current paper that:

> $\mathit{BAPAL}$ does not have the finite model property.

This is significant since given $\mathit{BAPAL}$ has a finitary axiomatisation
[17], a finite model property would have implied decidability [6]. A similar
lack of finite model property for other logics with quantification over
announcements is given in [18].

As the decidability result is a technical and complex result about
$\mathit{BAPAL}$, we will refer the reader to the companion paper [17] for
motivations, more comparisons to related work, and some proofs of technical
lemmas. However, the current paper will be self-contained as we will repeat
all necessary definitions and lemmas here.

In Section 2 we will give the necessary syntactic and semantic definitions for
$\mathit{BAPAL}{}$, we will also provide some foundational technical lemmas
that are required, and succinctly describe other results known about
$\mathit{BAPAL}$. Section 3 will provide the first of two main results:
$\mathit{BAPAL}{}$ does not have the finite model property. Section 4 presents
the second main result: the decidability of the satisfiability problem for
$\mathit{BAPAL}$. That is shown by finding a finite representation of
$\mathit{BAPAL}{}$ models and showing that all satisfiable formulas are
satisfied by some model with a representation of bounded size.

##  2 Boolean arbitrary public announcement logic

Given are a countable (finite or countably infinite) set of agents $A$ and a
countably infinite set of propositional variables $P$ (a.k.a. atoms, or
variables).

###  2.1 Syntax

We start with defining the logical language and some crucial syntactic
notions.

######  Definition 1 (Language).

The language of Boolean arbitrary public announcement logic is defined as
follows, where $a\in A$ and $p\in P$.

${\mathcal{L}}_{\mathit{bapal}}(A,P)\ \ni\ \varphi::=p\ |\ \neg\varphi\ |\
(\varphi\wedge\varphi)\ |\ K_{a}\varphi\ |\ [\varphi]\varphi\ |\ \Box\varphi$

$\dashv$

Other propositional connectives are defined by abbreviation. For
$K_{a}\varphi$ read ‘agent $a$ knows $\varphi$’. For $\Box\varphi$, read
‘after any Boolean announcement, $\varphi$ (is true)’. For $[\varphi]\psi$,
read ‘after public announcement of $\varphi$, $\psi$’. The dual modalities are
defined by abbreviation: $\hat{K}_{a}\varphi:=\neg K_{a}\neg\varphi$,
$\langle\varphi\rangle\psi:=\neg[\varphi]\neg\psi$, and
$\Diamond\varphi:=\neg\Box\neg\varphi$. Unless ambiguity results we often omit
one or both of the parameters $A$ and $P$ in
${\mathcal{L}}_{\mathit{bapal}}(A,P)$, and write
${\mathcal{L}}_{\mathit{bapal}}(P)$ or ${\mathcal{L}}_{\mathit{bapal}}$.
Unless ambiguity results we often omit parentheses occurring in formulas.
Formulas are denoted $\varphi,\psi$, possibly primed as in
$\varphi^{\prime},\varphi^{\prime\prime},\dots,\psi^{\prime},\dots$

We also distinguish the language ${\mathcal{L}}_{\mathit{el}}$ of _epistemic
logic_ (without the constructs $[\varphi]\varphi$ and $\Box\varphi$) and the
language ${\mathcal{L}}_{\mathit{pl}}$ of _propositional logic_ (without
additionally the construct $K_{a}\varphi$), also known as the _Booleans_.
Booleans are denoted $\varphi_{0},\psi_{0}$, etc.

The set of propositional variables that occur in a given formula $\varphi$ is
denoted $\mathit{var}(\varphi)$ (where one that does not occur in $\varphi$ is
called a fresh variable), its modal depth $d(\varphi)$ is the maximum nesting
of $K_{a}$ modalities, and its quantifier depth $D(\varphi)$ is the maximum
nesting of $\Box$ modalities. These notions are inductively defined as
follows.

  * •

$\mathit{var}(p)=\\{p\\}$,
$\mathit{var}(\neg\varphi)=\mathit{var}(K_{a}\varphi)=\mathit{var}(\Box\varphi)=\mathit{var}(\varphi)$,
$\mathit{var}(\varphi\wedge\psi)=\mathit{var}([\varphi]\psi)=\mathit{var}(\varphi)\cup\mathit{var}(\psi)$;

  * •

$D(p)=0$, $D(\neg\varphi)=D(K_{a}\varphi)=D(\varphi)$,
$D(\varphi\wedge\psi)=D([\varphi]\psi)=\max\\{D(\varphi),D(\psi)\\}$,
$D(\Box\varphi)=D(\varphi)+1$;

  * •

$d(p)=0$, $d(\neg\varphi)=d(\Box\varphi)=d(\varphi)$,
$d(\varphi\wedge\psi)=\max\\{d(\varphi),d(\psi)\\}$,
$d([\varphi]\psi)=d(\varphi)+d(\psi)$, $d(K_{a}\varphi)=d(\varphi)+1$.

Arbitrary announcement normal form is a syntactic restriction of
${\mathcal{L}}_{\mathit{bapal}}$ that pairs all public announcements with
arbitrary Boolean announcement operators. It plays a role in the decidability
proof. It is known that any formula in ${\mathcal{L}}_{\mathit{bapal}}$ is
equivalent to one in ${\mathcal{L}}_{\mathit{aanf}}$ [17].

######  Definition 2 (Arbitrary announcement normal form).

The language fragment ${\mathcal{L}}_{\mathit{aanf}}$ is defined by the
following syntax, where $a\in A$ and $p\in P$.

$\varphi::=p\ |\ \neg\varphi\ |\ (\varphi\wedge\varphi)\ |\ K_{a}\varphi\ |\
[\varphi]\Box\varphi$

$\dashv$

###  2.2 Structures

We consider the following structures and structural notions in this work.

######  Definition 3 (Model).

An (epistemic) model $M=(S,\sim,V)$ consists of a non-empty domain $S$ (or
${\mathcal{D}}(M)$) of states (or ‘worlds’), an accessibility function
$\sim:A\rightarrow{\mathcal{P}}(S\times S)$, where each $\sim_{a}$ is an
equivalence relation, and a valuation $V:P\rightarrow{\mathcal{P}}(S)$, where
each $V(p)$ represents the set of states where $p$ is true. For $s\in S$, a
pair $(M,s)$, for which we write $M_{s}$, is a pointed (epistemic) model.
$\dashv$

We will abuse the language and also call $M_{s}$ a model. We will occasionally
use the following disambiguating notation: if $M$ is a model, $S^{M}$ is its
domain, $\sim^{M}_{a}$ the accessibility relation for an agent $a$, and
$V^{M}$ its valuation.

######  Definition 4 (Bisimulation).

Let $M=(S,\sim,V)$ and $M^{\prime}=(S^{\prime},\sim^{\prime},V^{\prime})$ be
epistemic models. A non-empty relation $\mathfrak{R}\subseteq S\times
S^{\prime}$ is a bisimulation if for every $(s,s^{\prime})\in\mathfrak{R}$,
$p\in P$, and $a\in A$ the conditions atoms, forth and back hold.

  * •

atoms: $s\in V(p)$ iff $s^{\prime}\in V^{\prime}(p)$.

  * •

forth: for every $t\sim_{a}s$ there exists
$t^{\prime}\sim^{\prime}_{a}s^{\prime}$ such that
$(t,t^{\prime})\in\mathfrak{R}$.

  * •

back: for every $t^{\prime}\sim^{\prime}_{a}s^{\prime}$ there exists
$t\sim_{a}s$ such that $(t,t^{\prime})\in\mathfrak{R}$.

If there exists a bisimulation $\mathfrak{R}$ between $M$ and $M^{\prime}$
such that $(s,s^{\prime})\in\mathfrak{R}$, then $M_{s}$ and
$M^{\prime}_{s^{\prime}}$ are bisimilar, notation
$M_{s}{\raisebox{1.29167pt}[0.0pt][0.0pt]{$\medspace\underline{\\!\leftrightarrow\\!}\medspace$}}M^{\prime}_{s^{\prime}}$
(or
$\mathfrak{R}:M_{s}{\raisebox{1.29167pt}[0.0pt][0.0pt]{$\medspace\underline{\\!\leftrightarrow\\!}\medspace$}}M^{\prime}_{s^{\prime}}$,
to be explicit about the bisimulation).

Let $Q\subseteq P$. A relation $\mathfrak{R}$ between $M$ and $M^{\prime}$
satisfying atoms for all $p\in Q$, and forth and back, is a $Q$-bisimulation
(a bisimulation restricted to $Q$). The notation for $Q$-restricted
bisimilarity is
${\raisebox{1.29167pt}[0.0pt][0.0pt]{$\medspace\underline{\\!\leftrightarrow\\!}\medspace$}}_{Q}$.
$\dashv$

The notion of $n$-bisimulation, for $n\in\mathbb{N}$, is given by defining
relations $\mathfrak{R}^{0}\supseteq\dots\supseteq\mathfrak{R}^{n}$.

######  Definition 5 ($n$-Bisimulation).

Let $M=(S,\sim,V)$ and $M^{\prime}=(S^{\prime},\sim^{\prime},V^{\prime})$ be
epistemic models, and let $n\in\mathbb{N}$. A non-empty relation
$\mathfrak{R}^{0}\subseteq S\times S^{\prime}$ is a $0$-bisimulation if atoms
holds for pair $(s,s^{\prime})\in\mathfrak{R}$. Then, a non-empty relation
$\mathfrak{R}^{n+1}\subseteq S\times S^{\prime}$ is a $(n+1)$-bisimulation if
for all $p\in P$ and $a\in A$:

  * •

$(n+1)$-forth: for every $t\sim_{a}s$ there exists
$t^{\prime}\sim^{\prime}_{a}s^{\prime}$ such that
$(t,t^{\prime})\in\mathfrak{R}^{n}$;

  * •

$(n+1)$-back: for every $t^{\prime}\sim^{\prime}_{a}s^{\prime}$ there exists
$t\sim_{a}s$ such that $(t,t^{\prime})\in\mathfrak{R}^{n}$.

Similarly to $Q$-bisimulations we define $Q$-$n$-bisimulations, wherein atoms
is only required for $p\in Q\subseteq P$; $n$-bisimilarity is denoted
$M_{s}{\raisebox{1.29167pt}[0.0pt][0.0pt]{$\medspace\underline{\\!\leftrightarrow\\!}\medspace$}}^{n}M^{\prime}_{s^{\prime}}$,
and $Q$-$n$-bisimilarity is denoted
$M_{s}{\raisebox{1.29167pt}[0.0pt][0.0pt]{$\medspace\underline{\\!\leftrightarrow\\!}\medspace$}}^{n}_{Q}M^{\prime}_{s^{\prime}}$.
$\dashv$

###  2.3 Semantics

We continue with the semantics of our logic.

######  Definition 6 (Semantics).

The interpretation of formulas in ${\mathcal{L}}_{\mathit{bapal}}$ on
epistemic models is defined by induction on formulas.

Assume an epistemic model $M=(S,\sim,V)$, and $s\in S$.

$\begin{array}[]{lcl}M_{s}\models p&\mbox{iff}&s\in V(p)\\\
M_{s}\models\neg\varphi&\mbox{iff}&M_{s}\not\models\varphi\\\
M_{s}\models\varphi\wedge\psi&\mbox{iff}&M_{s}\models\varphi\text{ and
}M_{s}\models\psi\\\ M_{s}\models K_{a}\varphi&\mbox{iff}&\mbox{for all }t\in
S:s\sim_{a}t\text{ implies }M_{t}\models\varphi\\\
M_{s}\models[\varphi]\psi&\mbox{iff}&M_{s}\models\varphi\text{ implies
}M^{\varphi}_{s}\models\psi\\\ M_{s}\models\Box\psi&\mbox{iff}&\mbox{for all
}\varphi_{0}\in{\mathcal{L}}_{\mathit{pl}}:M_{s}\models[\varphi_{0}]\psi\end{array}$

where epistemic model $M^{\varphi}=(S^{\prime},\sim^{\prime},V^{\prime})$ is
such that: $S^{\prime}=[\\![\varphi]\\!]_{M}$,
${\sim^{\prime}_{a}}={\sim_{a}}\cap([\\![\varphi]\\!]_{M}\times[\\![\varphi]\\!]_{M})$,
and $V^{\prime}(p):=V(p)\cap[\\![\varphi]\\!]_{M}$, and where
$[\\![\varphi]\\!]_{M}:=\\{s\in S\mid M_{s}\models\varphi\\}$. For
$(M^{\varphi})^{\psi}$ we may write $M^{\varphi\psi}$. Formula $\varphi$ is
valid on model $M$, notation $M\models\varphi$, if for all $s\in S$,
$M_{s}\models\varphi$. Formula $\varphi$ is valid, notation $\models\varphi$,
if for all $M$, $M\models\varphi$. $\dashv$

Given $M_{s}$ and $M^{\prime}_{s^{\prime}}$, if for all
$\varphi\in{\mathcal{L}}_{\mathit{bapal}}$, $M_{s}\models\varphi$ iff
$M^{\prime}_{s^{\prime}}\models\varphi$, we write $M_{s}\equiv
M^{\prime}_{s^{\prime}}$ (for “$M_{s}$ and $M^{\prime}_{s^{\prime}}$ are
modally equivalent”). Similarly, if this holds for all $\varphi$ with
$d(\varphi)\leq n$, we write $M_{s}\equiv^{n}M^{\prime}_{s^{\prime}}$, and if
this holds for all $\varphi$ with $\mathit{var}(\varphi)\in Q\subseteq P$, we
write $M_{s}\equiv_{Q}M^{\prime}_{s^{\prime}}$.

Note that the languages of $\mathit{APAL}$ and $\mathit{BAPAL}$ are the same,
but that their semantics are different. The only difference is the
interpretation of $\Box\varphi$. In $\mathit{APAL}$, this quantifies over the
$\Box$-free fragment [4], so that, given the eliminability of public
announcements from that fragment [14], this amounts to quantifying over
formulas of epistemic logic:

$\begin{array}[]{lcl}M_{s}\models\Box\psi&\mbox{iff}&\mbox{for all
}\varphi\in{\mathcal{L}}_{\mathit{el}}:M_{s}\models[\varphi]\psi\quad\quad\quad\quad\text{($\mathit{APAL}$\
semantics of }\Box\varphi)\end{array}$

Given any formula $\varphi\in{\mathcal{L}}_{\mathit{bapal}}$, we say $\varphi$
is satisfiable if there is some epistemic model $M=(S,\sim,V)$ and some $s\in
S$ such that $M_{s}\models\varphi$. The satisfiability problem is, given some
$\varphi\in{\mathcal{L}}_{\mathit{bapal}}$, to determine whether $\varphi$ is
satisfiable.

###  2.4 Results for BAPAL from the companion paper

We continue with basic semantic results for the logic which will be used in
the later sections. Various well-known results for any dynamic epistemic logic
with propositional quantification generalise straightforwardly to
$\mathit{BAPAL}$.

######  Lemma 7 ([17, Lemma 3.1]).

Let $M_{s},N_{s^{\prime}}$ be epistemic models. Then
$M_{s}{\raisebox{1.29167pt}[0.0pt][0.0pt]{$\medspace\underline{\\!\leftrightarrow\\!}\medspace$}}N_{s^{\prime}}$
implies $M_{s}\equiv N_{s^{\prime}}$. $\dashv$

This lemma states the bisimulation invariance of $\mathit{BAPAL}$.

######  Lemma 8 ([17, Lemma 3.3]).

Let $M_{s},N_{s^{\prime}}$ be epistemic models. Then
$M_{s}{\raisebox{1.29167pt}[0.0pt][0.0pt]{$\medspace\underline{\\!\leftrightarrow\\!}\medspace$}}^{n}N_{s^{\prime}}$
implies $M_{s}\equiv^{n}N_{s^{\prime}}$. $\dashv$

This lemma shows that the bisimulation invariance still holds when we restrict
to finite depth bisimulations and formula. This may look obvious but is
actually rather special: it holds for $\mathit{BAPAL}$ but not, for example,
for $\mathit{APAL}$, where the quantifiers are over formulas of arbitrarily
large modal depth.

Note that both for $\mathit{APAL}$ and $\mathit{BAPAL}$ restricted
bisimilarity does not imply restricted modal equivalence:

$M_{s}{\raisebox{1.29167pt}[0.0pt][0.0pt]{$\medspace\underline{\\!\leftrightarrow\\!}\medspace$}}_{Q}M^{\prime}_{s^{\prime}}\
\text{does not imply}\ M_{s}\equiv_{Q}M^{\prime}_{s^{\prime}}.$

In Section 4 on the decidability of the satisfiability problem for
$\mathit{BAPAL}$ we show in Lemma 22 that models that are restrictedly
bisimilar and additionally satisfy another structural requirements are after
all restrictedly modally equivalent. This result will play a crucial part in
the decidability proof.

We continue with required lemma for the arbitrary announcement normal form.

######  Lemma 9 ([17, Lemma 3.4]).

Every formula of ${\mathcal{L}}_{\mathit{bapal}}$ is semantically equivalent
to a formula of ${\mathcal{L}}_{\mathit{aanf}}$, that is, in arbitrary
announcement normal form. $\dashv$

These are the results for $\mathit{BAPAL}$ that we will also crucially use in
this paper. A notable result in [17] not used in this paper is that
$\mathit{BAPAL}$ is not at least as expressive as $\mathit{APAL}$ [17, Prop.
4.2], and another one is that $\mathit{BAPAL}$ has a finitary axiomatization
[17, Theorem 5.8]. For the convenience of the reader we reprint the
axiomatization below (given formula
$\psi\rightarrow[\varphi^{\prime}][p]\varphi$ in derivation rule ${\bf
R\Box}$, a ‘fresh’ atom $p$ is one not occurring in
$\psi,\varphi^{\prime},\varphi$).

$\begin{array}[]{llll}{\bf P}&\text{propositional tautologies}&{\bf
K}&K_{a}(\varphi\rightarrow\psi)\rightarrow(K_{a}\varphi\rightarrow
K_{a}\psi)\\\ {\bf T}&K_{a}\varphi\rightarrow\varphi&{\bf
4}&K_{a}\varphi\rightarrow K_{a}K_{a}\varphi\\\ {\bf 5}&\neg
K_{a}\varphi\rightarrow K_{a}\neg K_{a}\varphi&{\bf
AP}&[\varphi]p\leftrightarrow(\varphi\rightarrow p)\\\ {\bf
AN}&[\varphi]\neg\psi\leftrightarrow(\varphi\rightarrow\neg[\varphi]\psi)&{\bf
AC}&[\varphi](\psi\land\psi^{\prime})\leftrightarrow([\varphi]\psi\land[\varphi]\psi^{\prime})\\\
{\bf AK}&[\varphi]K_{a}\psi\leftrightarrow(\varphi\rightarrow
K_{a}[\varphi]\psi)&{\bf
AA}&[\varphi][\psi]\psi^{\prime}\leftrightarrow[\varphi\land[\varphi]\psi]\psi^{\prime}\\\
{\bf A\Box}&\Box\varphi\rightarrow[\psi_{0}]\varphi\text{ where
}\psi_{0}\\!\in\\!{\mathcal{L}}_{\mathit{pl}}&{\bf MP}&\varphi\text{ and
}\varphi\rightarrow\psi\text{ imply }\psi\\\ {\bf NecK}\\!\\!&\varphi\text{
implies }K_{a}\varphi&{\bf NecA}\\!\\!&\varphi\text{ implies }[\psi]\varphi\\\
&&{\bf R\Box}&\psi\rightarrow[\varphi^{\prime}][p]\varphi\text{ for $p$ fresh
implies }\psi\rightarrow[\varphi^{\prime}]\Box\varphi\end{array}$

##  3 BAPAL does not have the finite model property

In this section we show that $\mathit{BAPAL}$ does not have the finite model
property. That is, there are satisfiable formulas in
${\mathcal{L}}_{\mathit{bapal}}$ that are not satisfied by any finite model.
This is significant since, given the finite complete axiomatization presented
in [17], the finite model property would give decidability for free.
Essentially to check if a formula, $\varphi$, is satisfiable we could
enumerate all proofs in order of size looking for a proof of $\lnot\varphi$,
and alternately enumerate all models in order of size, looking for a model
that satisfies $\varphi$. One of the procedures must halt, and if
$\lnot\varphi$ is provable, $\varphi$ is not satisfiable, and if $\varphi$ has
a model, $\varphi$ is satisfiable (see [6] for a more formal treatment.) The
recent paper [18] applies a similar approach to show that group announcement
logic [1] and coalition announcement logic [2, 11] also lack the finite model
property, although the constructions given there are more complex than the
ones we require for $\mathit{BAPAL}{}$.

######  Theorem 10.

$\mathit{BAPAL}$ does not have the finite model property. $\dashv$

###### Proof.

We will give the proof by construction. Consider the following formula fmp.

$\textbf{fmp}=\left(\begin{array}[]{rlr}&K_{b}(x\land\hat{K}_{a}\lnot
x\land(K_{a}(\lnot x\rightarrow y)\lor K_{a}(\lnot x\rightarrow\lnot
y))&(1)\\\ \land&\hat{K}_{b}(x\land\hat{K}_{a}(\lnot x\land y))&(2)\\\
\land&\hat{K}_{b}(x\land\hat{K}_{a}(\lnot x\land\lnot y))&(3)\\\
\land&K_{b}((x\land\hat{K}_{a}(\lnot x\land y))\rightarrow\Diamond
K_{b}(x\land\hat{K}_{a}(\lnot x\land y)))&(4)\\\
\land&K_{b}\Box(K_{b}\hat{K}_{a}\lnot
x\rightarrow\hat{K}_{b}(x\land\hat{K}_{a}(\lnot x\land
y))&(5)\end{array}\right)$

It refers to two agents, $a$ and $b$, and to two propositional atoms, $x$ and
$y$. Agent $b$ knows $x$ to be true (the first conjunct of fmp), and also
agent $b$ knows agent $a$ does not know whether $x$ is true or not, and
finally agent $b$ knows that agent $a$ knows whether $y$ is true, given $x$ is
not true. The next two conjuncts establish that agent $b$ cannot distinguish
(at least) two types of worlds. The second conjunct says that agent $b$
considers possible that agent $a$ considers possible a world where $x$ is
false and $y$ is true. These worlds, which satisfy $x\land\hat{K}_{a}(\lnot
x\land y)$ are type A worlds. The third conjunct says that agent $b$ considers
possible that agent $a$ considers possible a world where $x$ and $y$ are
false. These worlds, which satisfy $x\land\hat{K}_{a}(\lnot x\land\lnot y)$
are type B worlds. The fourth conjunct says that agent $b$ knows that in every
type A world, there is some Boolean announcement after which agent $b$ knows
that the world is type A. That is, $b$ knows that in every type A world there
is an announcement that preserves that world, and removes every type B world.
The final fifth conjunct says that agent $b$ knows that after every Boolean
announcement, if $a$ always considers any type A or type B possible, then $b$
considers a type A world possible. That is, if a type B world is preserved by
a Boolean announcement, then a type A world is also preserved by that
announcement. The formula fmp says, in other words, that there is a Boolean
announcement that preserves a type $A$ world and not a type $B$ world, but
there is no Boolean announcement that preserves a type $B$ world and not a
type $A$ world.

$\underline{A}:x\overline{y}$$B:x\overline{y}$$\overline{x}y$$\overline{x}\overline{y}$$b$$a$$a$
Figure 1: A model that does not satisfy formula fmp. The names of the worlds
indicate which atoms are true there, e.g., $x$ means that atom $x$ is true and
$\overline{x}$ means that $x$ is false.

Now consider the model depicted in Figure 1. The depicted model does not
satisfy the fifth conjunct. We note that the bottom-left world is a type $A$
world and the bottom-right world is a type $B$ world. Let
$\varphi\in{\mathcal{L}}_{\mathit{pl}}$ be a Boolean announcement preserving
the type $A$ world (and such that it remains type $A$, so that therefore also
the top-left world is preserved) but not the type $B$ world. Now consider
Boolean $x\rightarrow\lnot\varphi$. When announced in the model of Figure 1,
this formula would preserve the $B$ world and the top-right world, so it would
preserve the type $B$ of the world named $B$. But it would obviously not
preserve the $A$ world.

We can extend this argument to a proof to show that no finite model can
satisfy this formula. We proceed by contradiction: suppose that $M_{s}$ is a
finite model where $M_{s}\models\textbf{fmp}$. We enumerate the type $A$
worlds and the type $B$ worlds as respectively

$\begin{array}[]{lllll}T_{A}&=&\\{t\mid s\sim_{b}t,\
M_{t}\models\hat{K}_{a}(\lnot x\land y)\\}&=&\\{A_{0},\ldots,A_{n}\\}\\\
T_{B}&=&\\{t\mid s\sim_{b}t,\ M_{t}\models\hat{K}_{a}(\lnot x\land\lnot
y)\\}&=&\\{B_{0},\ldots,B_{m}\\}\end{array}$

We can infer from the first conjunct of fmp that for all $t\in T_{A}\cup
T_{B}$, $M_{t}\models x$. From the fourth conjunct of fmp we obtain that for
each $t\in T_{A}$ there is a Boolean formula $\varphi_{t}$ such that
$M_{t}\models\varphi_{t}$ and for all $u\in T_{B}$,
$M_{u}\not\models\varphi_{t}$. Now consider the Boolean

$\Psi=x\rightarrow\bigwedge_{t\in T_{A}}\lnot\varphi_{t}.$

For each $t\in T_{A}$, we have $M_{t}\not\models\Psi$, since $M_{t}\models
x\land\varphi_{t}$, and for each $u\in T_{B}$, we will have
$M_{u}\models\Psi$, since $M_{u}\models x$ and for all $t\in T_{A}$,
$M_{u}\not\models\varphi_{t}$. After the announcement of $\Psi$, all worlds
satisfying $\lnot x$ are preserved, so $K_{b}\hat{K}_{a}\lnot x$ is true.
However, as every world $t\in T_{A}$ is removed, there is no world
$u\sim_{b}s$ such that $M^{\Psi}_{u}\models\hat{K}_{a}(\lnot x\land y)$.
Therefore, the fifth conjunct of $\Phi$ does not hold and therefore the model
$M_{s}$ does not satisfy fmp, giving the required contradiction.

$A_{0}:x\overline{y}p_{0}$$B_{0}:x\overline{y}$$\overline{x}y$$\overline{x}\overline{y}$$b$$a$$a$$A_{1}:x\overline{y}p_{1}$$B_{1}:x\overline{y}$$\overline{x}y$$\overline{x}\overline{y}$$b$$b$$a$$a$$A_{2}:x\overline{y}p_{2}$$B_{2}:x\overline{y}$$\overline{x}y$$\overline{x}\overline{y}$$b$$b$$a$$a$$\ldots$
Figure 2: A model that does satisfy formula fmp. For each world $A_{i}$ there
is some atom $p_{i}$ that is true only at $A_{i}$. All atoms other than $x$,
$y$ and all $p_{i}$ are false everywhere.

However, we can construct an infinite model that satisfies fmp. Consider the
model $M$ depicted in Figure 2. In this infinite model $M$, for every $A_{i}$
world there is a Boolean announcement, $\varphi_{i}=p_{i}\lor\lnot x$, that
will preserve just $A_{i}$ and all worlds in the top-row of the model $M$.
Therefore, $M_{A_{i}}^{\varphi_{i}}\models K_{b}\hat{K}_{a}(\lnot x\land y)$
will be true in designated world $A_{i}$. However, in any world
$s\sim_{b}A_{0}$, no Boolean announcement can remove all $A_{i}$ worlds
without also also removing all $B_{i}$ worlds. This is because given any
finite set of propositional atoms, $P^{\prime}$, there is some world $A_{i}$
such that for all $p\in P^{\prime}$: $A_{i}\in V(p)$ iff for all
$j\in\mathbb{N}$, $B_{j}\in V(p)$ (i.e., there must be an $A_{i}$ world such
that the valuation of all atoms in $P^{\prime}$ is the same in the single
world $A_{i}$ and in all $B$ worlds). That is

$M_{s}\models K_{b}\Box(K_{b}\hat{K}_{a}\lnot
x\rightarrow\hat{K}_{b}(x\land\hat{K}_{a}(\lnot x\land y)),$

so the fifth conjunct holds. It is easy to see the other conjuncts of formula
fmp also hold in this model. This demonstrates that fmp has an infinite model.

##  4 Decidability of the satisfiability problem

To show that $\mathit{BAPAL}$ is decidable (Theorem 29) we give a procedure to
find a model of any satisfiable formula. The correctness of this procedure is
shown by induction over the depth of the nesting of the $\Box$ operator. This
is complicated by the fact that $\mathit{BAPAL}$ does not have the finite
model property (Theorem 10). However, we are able to provide a finite
representation of some models, and show that every satisfiable formula is
satisfied by such a model.

###  4.1 Overview of the proof

Before we continue with the actual proof, let us present a high-level overview
of our argument. For a formula $\varphi$ of ${\mathcal{L}}_{\mathit{bapal}}$
we can construct a finite number of so-called $\varphi$-pseudo-models
(Definition 13) that are somewhat similar to filtrations [6, Section 2.3]. The
$\varphi$-pseudo-models finitely represent the sets of available Boolean
announcements with respect to the subformulas of $\varphi$. In such models,
states111 We will refer to the entities of pseudo-models as states rather than
worlds to distinguish them from actual models.  are subsets of subformulas of
$\varphi$ (the colour) along with the representation of available
announcements (the hue). The $\varphi$-pseudo-model is consistent if the hue
of every state agrees with formulas in its colour (Definition 16). Now, we are
ready to formulate the statement we are proving in this paper:

> Given $\varphi\in{\mathcal{L}}_{\mathit{bapal}}$, there is a consistent
> $\varphi$-pseudo-model with a state $\sigma$ such that $\varphi\in\sigma$ if
> and only if $\varphi$ is satisfiable. ($\ast$)

Let us first consider the left-to-right direction of ($\ast$). A graphic
representation of the main idea of the proof is depicted in Figure 3.

$\varphi$$\mathcal{M}^{1}_{\sigma}$$\mathcal{M}^{2}_{\sigma}$$\mathellipsis$$\mathcal{M}^{n}_{\sigma}$ptFinite
$\varphi$-pseudomodels (Def.
13)$\mathcal{N}^{1}_{\sigma}$$\mathcal{N}^{2}_{\sigma}$$\mathellipsis$$\mathcal{N}^{m}_{\sigma}$ptConsistentpseudo-
models (Def. 16)Consistencycheck (Lemma
18)$\overline{\mathcal{N}^{k}_{(\sigma,1)}}\models\varphi$$\varphi\in\sigma$Pick
$\mathcal{N}^{k}_{\sigma}$with $\varphi\in\sigma$ptActualisation(Def. 19)ptif
andonly if Figure 3: A roadmap to the left-to-right direction of the
decidability proof.

Given $\varphi$, we first construct all possible $\varphi$-pseudo-models.
While building up $\varphi$-pseudo-models, we use a finite set of fresh
propositional atoms (the hue atoms) to model all possible Boolean
announcements that can be made in the model. In such a way, we only need to
deal with announcements of atoms. To ensure that arbitrary announcements on
$\varphi$-pseudo-models (the hue) agree with the subformulas of $\varphi$ at
each state (the colour), we focus on the consistent  set of pseudo-models,
(Definition 16), and present a computable process for determining whether a
pseudo-model is consistent (Lemma 18).

To construct a model that will satisfy $\varphi$, we pick a consistent
$\varphi$-pseudo-model with a state $\sigma$ such that $\varphi\in\sigma$, and
transform it into an actualisation (Definition 19). An actualisation of a
$\varphi$-pseudo-model is an infinite model, where the valuation of the hue
atoms we added while constructing the pseudo-model is empty, and instead we
use a new, now infinite, set of fresh variables (the actualisation atoms) to
model the effect of arbitrary Boolean announcements. To establish a
relationship between pseudo-models and their actualisations we introduce a
special kind of a bisimulation that is called $X!$-bisimulation (Definition
20). This kind of bisimulation allows us to regard new propositional variables
introduced in the actualisation only to the extent that they influence the set
of available announcements. Finally, with the help of $X!$-bisimulation, we
show that a formula is in state $\sigma$ of a pseudo-model if and only if the
formula is satisfied by the corresponding actualisation (Lemma 26).

The right-to-left direction of ($\ast$) is a bit more straightforward. Having
a model satisfying $\varphi$, we construct a $\varphi$-pseudo-model out of it
in such a way that states of the pseudo-model are sets consisting of formulas
true at a state of the initial model and fresh propositional variables that
model arbitrary Boolean announcements (Definition 27). After that we show that
thus constructed pseudo-model is consistent (Lemma 28).

###  4.2 Pseudo-models

We commence the proof by defining pseudo-models. Given a formula
$\varphi\in{\mathcal{L}}_{\mathit{bapal}}$, we recall that $D(\varphi)$ is the
maximum nesting of $\Box$ operators in $\varphi$, that $d(\varphi)$ is the
maximum nesting of $K_{a}$ operators (for any $a\in A$) in $\varphi$, and that
$\mathit{var}(\varphi)$ is the set of propositional variables that occur in
$\varphi$.

Lemma 9 demonstrated that we may assume without loss of generality that any
formula $\varphi\in{\mathcal{L}}_{\mathit{bapal}}$ is in arbitrary
announcement normal form ($\varphi\in{\mathcal{L}}_{\mathit{aanf}}$), and
consequently that all $\Box$ operators are necessarily coupled with a public
announcement operator, and vice versa. This assumption will now be made
throughout this section. This means that $D(\varphi)$ now not only determines
the maximum nesting of $\Box$ modalities in $\varphi$, but also that of the
(same) maximum nesting of announcements. Let $\psi\subseteq\varphi$ denote
that $\psi$ is a subformula of $\varphi$ in ${\mathcal{L}}_{\mathit{aanf}}$
syntax (so that the subformulas of $[\varphi^{\prime}]\Box\varphi$ exclude
$\Box\varphi$) and let $|\varphi|$ denote the number of symbols in $\varphi$.
In this section, apart from $\varphi,\psi$ we also allow $\alpha,\beta$
(possibly primed) to denote formulas in ${\mathcal{L}}_{\mathit{bapal}}$, and
(in order to avoid too cumbersome notation) we also allow all of them to
denote Booleans, i.e., formulas in ${\mathcal{L}}_{\mathit{pl}}$.

To model arbitrary Boolean announcements we introduce a set of fresh atoms
(the hue atoms) to represent all the announcements that can be made within a
model (by way of associating a set of atoms to a state, such that a subset of
the domain will correspond to a set of sets of atoms). These fresh atoms are
with respect to a given formula $\varphi$.

######  Definition 11 (Closure).

  1. 1.

Given $\varphi\in{\mathcal{L}}_{\mathit{aanf}}$, we define $cl(\varphi)$, the
closure of $\varphi$, inductively so that:

     * •

$cl(\varphi)=\\{\psi,\neg\psi\ |\ \psi\subseteq\varphi\\}$ if $d(\varphi)=0$,
and

     * •

$cl(\varphi)=\\{\psi,\neg\psi\ |\
\psi\subseteq\varphi\\}\cup\\{K_{a}\psi^{\prime},\neg K_{a}\psi^{\prime}\ |\
K_{a}\psi\subseteq\varphi\ \text{and}\ \psi^{\prime}\in cl(\psi)\\}$ if
$d(\varphi)>0$.

Note that in the second clause, $d(\psi)<d(\varphi)$, so the definition is
well-founded.

  2. 2.

We define the extended closure of $\varphi$ be
$cl^{+}(\varphi):=cl(\varphi)\cup\\{p,\neg p\ |\
p\in\mathit{fresh}(\varphi)$}, where given $f(0)=|cl(\varphi)|$ and
$f(i+1)=2^{2^{f(i)}}$, $\mathit{fresh}(\varphi)=\\{p_{i}\ |\ 0\leq
i<f(D(\varphi))\\}$ are fresh atoms that do not appear in $cl_{n-1}(\varphi)$.

$\dashv$

Let $P^{\varphi}_{\mathrm{col}}=\mathit{var}(\varphi)$ be the atoms appearing
in $\varphi$, $P^{\varphi}_{\mathrm{hue}}=\mathit{fresh}(\varphi)$ be the
fresh atoms introduced in the closure, and
$P^{\varphi}_{\mathrm{act}}=P-(P^{\varphi}_{\mathrm{col}}\cup
P^{\varphi}_{\mathrm{hue}})$ be the remaining atoms in the language. The
extended closure of $\varphi$ describes a set of formulas that influence
whether $\varphi$ is satisfied by a model, along with a set of extra atoms,
$P^{\varphi}_{\mathrm{hue}}$, to simulate possible Boolean announcements. To
simulate a model of $\varphi$, we consider each state of the model being
described by the set of formulas that are true at that state (the
$\varphi$-colour) and the announcements that are available at that state (the
$\varphi$-hue).

######  Definition 12.

Given $\varphi\in{\mathcal{L}}_{\mathit{aanf}}$ a maximal $\varphi$-set is a
set $\sigma\subseteq cl^{+}(\varphi)$ such that:

  1. 1.

for all $\lnot\psi\in cl^{+}(\varphi)$, either $\psi\in\sigma$ or
$\lnot\psi\in\sigma$222 Note that if $\psi\in cl^{+}(\varphi)$ either
$\lnot\psi\in cl^{+}(\varphi)$ or $\psi=\lnot\psi^{\prime}$ and
$\psi^{\prime}\in cl^{+}(\varphi)$.

  2. 2.

for all $\psi\wedge\psi^{\prime}\in cl(\varphi)$,
$\psi\wedge\psi^{\prime}\in\sigma$ iff $\psi\in\sigma$ and
$\psi^{\prime}\in\sigma$.

  3. 3.

for all $K_{a}\psi\in cl(\varphi)$, $K_{a}\psi\in\sigma$ implies
$\psi\in\sigma$.

The set of maximal $\varphi$-sets is denoted $\Sigma_{\varphi}$. Given a
maximal $\varphi$-set $\sigma$ we say its colour is
$\mathrm{col}(\sigma)=\sigma\cap cl(\varphi)$ and its hue is
$\mathrm{hue}(\sigma)=\sigma-cl(\varphi)$ (i.e. the set of hue atoms or their
negation). $\dashv$

Note that in Definition 12, there is no clause corresponding to paired
announcement operators $[\alpha]\Box$. This is because there appears to be no
simple syntactic relationship between $[\alpha]\Box\psi$ and $\psi$, that will
provide a consistent set of formulas. A more complex approach is required to
deal with these formulas (see Definitions 14 – 16). Apart from $\sigma$,
maximal $\varphi$-sets are denoted $\tau,\rho$ (possibly primed). The hue
atoms introduced are intended to represent all the possible Boolean
announcements.

We now take the maximal $\varphi$-sets as the states of a model.

######  Definition 13.

Given $\varphi\in{\mathcal{L}}_{\mathit{aanf}}$, a $\varphi$-pseudo-model is a
triple $\mathcal{M}=(\mathcal{S},\approx,\mathcal{V})$ where for each $a\in
A$, $\approx\subset\mathcal{S}\times\mathcal{S}$ is an equivalence relation
and for all $p\in P$, $\mathcal{V}(p)\subset\mathcal{S}$ such that:

  1. 1.

$\mathcal{S}\subseteq\Sigma_{\varphi}$;

  2. 2.

for $\sigma,\tau\in\mathcal{S}$, $\sigma\approx_{a}\tau$ only if for all
$K_{a}\psi\in cl(\varphi)$, $K_{a}\psi\in\sigma$ iff $K_{a}\psi\in\tau$;

  3. 3.

for all $\sigma\in\mathcal{S}$, for all $\neg K_{a}\psi\in\sigma$, there is
some $\tau\in\mathcal{S}$ where $\tau\sim^{M}_{a}\sigma$ and
$\neg\psi\in\tau$;

  4. 4.

for all $p\in P^{\varphi}_{\mathrm{col}}\cup P^{\varphi}_{\mathrm{hue}}$, for
all $\sigma\in\mathcal{S}$, $\sigma\in\mathcal{V}(p)$ iff $p\in\sigma$; for
all $p\in P^{\varphi}_{\mathrm{act}}$, $\mathcal{V}(p)=\emptyset$.

  5. 5.

for all $\psi\in{\mathcal{L}}_{\mathit{pl}}(P^{\varphi}_{\mathrm{col}})$,
there is some $p\in P^{\varphi}_{\mathrm{hue}}$ such that
$\mathcal{V}(p)=\\{\sigma\ |\ \sigma\cap
P^{\varphi}_{\mathrm{col}}\models\psi\\}$333 Where Boolean satisfaction has
its standard interpretation: for $p\in P$, $X\models p$ iff $p\in X$;
$X\models\lnot\psi$ iff $X\not\models\psi$; and
$X\models\psi_{1}\wedge\psi_{2}$ iff $X\models\psi_{1}$ and
$X\models\psi_{2}$. .

  6. 6.

for all $p,q\in P^{\varphi}_{\mathrm{hue}}$, there is some $r\in
P^{\varphi}_{\mathrm{hue}}$ such that
$\mathcal{V}(r)=\mathcal{V}(p)\cup\mathcal{V}(q)$, and some $r^{\prime}\in
P^{\varphi}_{\mathrm{hue}}$ such that
$\mathcal{V}(r^{\prime})=\mathcal{V}(p)\cap\mathcal{V}(q)$.

$\dashv$

Definition 13 is similar to a standard bottom-up tableau construction for
showing decidability in modal logic [9]. However, rather than allowing
quantification over all announcements of Boolean propositions (which requires
an infinite number of states), quantification is only considered over positive
Boolean atoms. Furthermore, these simulated announcements are only considered
to the extent that they may influence the interpretation of subformulas of
$\varphi$. To allow the infinite number of possible Boolean announcements to
be simulated, the last two clauses of Definition 13 require that:

  * •

for any Boolean formula made of only propositional atoms appearing in
$\varphi$, there is some hue atom whose denotation agrees with that formula;

  * •

for any two hue atoms, there is a third whose denotation is the union of the
denotations or the first two; and

  * •

for any two hue atoms, there is a third whose denotation is the intersection
of the denotations or the first two.

The intent of these clauses is that the semantics need only consider the
announcement of propositional atoms, rather than complex formulas. Note, that
while the denotations of the hue atoms are closed under disjunctions and
conjunctions, there is no requirement that they are closed under
complementation. This is because, with respect to the colours of states,
announcements need not be closed under complementation, in the sense that even
if a state is preserved by some Boolean announcement $\beta$, a state of the
same colour may be preserved by the announcement of $\lnot\beta$. This is
formally shown in Lemma 24.

It follows that a $\varphi$-pseudo-model (wherein the valuation of all atoms
in $P^{\varphi}_{\mathrm{act}}$ is empty) can be seen as a finite
representation of an infinite set of models (wherein the valuation of such
atoms may vary), and given a pointed $\varphi$-pseudo-model
$\mathcal{M}_{\sigma}$, the intent is that every model represented by
$\mathcal{M}_{\sigma}$ will satisfy every formula in $\mathrm{col}(\sigma)$
(though not necessarily the formulas of $\mathrm{hue}(\sigma)$).

To ensure the announcement operators interpretation is respected in a
$\varphi$-pseudo-model, we will now refine the set of $\varphi$-pseudo-models
inductively with respect to the depth of nestings of announcement operators in
$\varphi$. As $\varphi$ is in announcement normal form, this is the same as
the depth $D(\varphi)$ of $\Box$-operators.

First, we require the notion of a witness for an announcement. To do this, we
use a syntactic variant of an announcement as follows:

######  Definition 14.

Given a $\varphi$-pseudo-model
$\mathcal{M}=(\mathcal{S},\approx,\mathcal{V})$, some formula $\alpha\in
cl(\varphi)$ and some $p\in P^{\varphi}_{\mathrm{hue}}$ with non-empty
denotation in $\mathcal{M}$, we define the syntactic $\alpha$-$p$-restriction,
$\mathcal{M}^{(\alpha,p)}=(\mathcal{S}^{\prime},\approx^{\prime},\mathcal{V}^{\prime})$,
where

  * •

$\mathcal{S}^{\prime}=\\{\tau\in\mathcal{S}\ |\ \alpha,p\in\tau\\}$,

  * •

for all $a\in A$,
${\approx^{\prime}_{a}}={{\approx_{a}}\cap{(\mathcal{S}^{\prime}\times\mathcal{S}^{\prime})}}$

  * •

and for all $q\in P$,
$\mathcal{V}^{\prime}(q)=\mathcal{V}(q)\cap\mathcal{S}^{\prime}$.

$\dashv$

Using this syntactic notion of an announcement, we can define a witness for an
announcement.

######  Definition 15.

Given a pointed $\varphi$-pseudo-model
$\mathcal{M}_{\sigma}=(\mathcal{S},\approx,\mathcal{V})_{\sigma}$, some
formulas $\alpha,\psi\in cl(\varphi)$ with non-empty denotation in
$\mathcal{M}$ and some propositional atom $p\in P^{\varphi}_{\mathrm{hue}}$,
we say a pointed $\varphi$-pseudo-model model $\mathcal{N}_{\tau}$ is a
$\alpha$-$p$-witness for $\psi$ at $\mathcal{M}_{\sigma}$ if
$\mathcal{N}_{\tau}{\raisebox{1.29167pt}[0.0pt][0.0pt]{$\medspace\underline{\\!\leftrightarrow\\!}\medspace$}}\mathcal{M}_{\sigma}^{(\alpha,p)}$
and $\psi\in\tau$.444 Where the standard definition of bisimulation
(Definition 4) is applied to $\varphi$-pseudo-models without change.  $\dashv$

Finally, we require that the Boolean announcements afforded by the hue of a
state are consistent with the colour of the state. That is, for every state
$\sigma$ in the pseudo-model, every formula $[\alpha]\Box\psi\sigma$ should
have a suitable set of witnesses.

######  Definition 16.

Given $\varphi\in{\mathcal{L}}_{\mathit{aanf}}$, and some $n$ where $0\leq
n\leq D(\varphi)$, a $\varphi$-pseudo-model
$\mathcal{M}=(\mathcal{S},\approx,\mathcal{V})$ is defined to be
$n$-consistent if:

  * •

$n=0$ or $\mathcal{M}$ is $(n-1)$-consistent; and

  * •

for every $\sigma\in\mathcal{S}$, for all $[\alpha]\Box\psi\in cl(\varphi)$
where $D([\alpha]\Box\psi)\leq n$, we have $[\alpha]\Box\psi\in\sigma$ if and
only if for every $p\in P^{\varphi}_{\mathrm{hue}}$ such that
$\alpha,p\in\sigma$, there is a $\alpha$-$p$-witness $\mathcal{N}_{\tau}$ for
$\psi$ at $\mathcal{M}_{\sigma}$, where $\mathcal{N}$ is $(n-1)$-consistent.

We will refer to a $D(\varphi)$-consistent $\varphi$-pseudo-model simply as a
consistent $\varphi$-pseudo-model. $\dashv$

If $\mathcal{M}$ is consistent and $\sigma\in{\mathcal{D}}(\mathcal{M})$, we
also call $\mathcal{M}_{\sigma}$ consistent.

Note that the consistency of the announcement operators depends only on the
announcement of propositional atoms, rather than complex Boolean formulas. We
will refer to these simple announcements as atomic announcements.

Now we will show that:

  * •

There is a bounded number of $\varphi$-pseudo-models. (Lemma 17)

  * •

We can test if a $\varphi$-pseudo-model is consistent. (Lemma 18)

In the next section we will show that:

  * •

From a consistent $\varphi$-pseudo-model,
$\mathcal{M}=(\mathcal{S},\approx,\mathcal{V})$, given any
$\sigma\in\mathcal{S}$, given any $\psi\in\sigma$ we can construct a model
$\overline{\mathcal{M}}_{\overline{\sigma}}$ such that
$\overline{\mathcal{M}}_{\overline{\sigma}}\models\psi$. (Lemma 26)

  * •

Given any pointed model $M_{s}$, we can construct a $D(\varphi)$-consistent
$\varphi$-pseudo-model $M^{\varphi}=(\mathcal{S},\approx,\mathcal{V})$ where
there is some $\sigma\in\mathcal{S}$ where $\\{\psi\in cl(\varphi)\ |\
M_{s}\models\psi\\}\subseteq\sigma$. (Lemma 28)

Finally, the satisfiability procedure is then to:

  * •

enumerate all $\varphi$-pseudo-models, test for $D(\varphi)$-consistency, and
then check to see if a state contains the formula $\varphi$. (Theorem 29).

######  Lemma 17.

There is a bounded number of $\varphi$-pseudo-models. $\dashv$

###### Proof.

This is clear from Definitions 11-13. The set $cl^{+}(\varphi)$ is finite
(albeit non-elementary in $D(\varphi)$), and consequently $\Sigma_{\varphi}$
is finite. As the elements of $\Sigma_{\varphi}$ define the states of a
$\varphi$-pseudo-model, there can only be a finite number of possibilities and
the number of $\varphi$-pseudo-models is finite.

Note that $cl^{+}(\varphi)$ is non-elementary, where every increase in
$D(\varphi)$ adds two exponentials to the complexity. However, this paper is
only concerned with the fact that the satisfiability problem for
$\mathit{BAPAL}{}$ is decidable, and complexity lower bounds are left to
future work.

######  Lemma 18.

There is a computable procedure to test if a $\varphi$-pseudo-model is
consistent. $\dashv$

###### Proof.

Given some $n\leq D(\varphi)$ and some $\varphi$-pseudo-model
$\mathcal{M}=(\mathcal{S},\approx,\mathcal{V})$, the procedure
$\mathtt{Consistent}(\mathcal{M},n)$ is as follows:

$\begin{array}[]{rl}&\mathtt{Consistent}(\mathcal{M},n):\\\
1.&\quad\texttt{for each }\sigma\in\mathcal{S}:\\\ 2.&\quad\quad\texttt{if}\
n=0,\ \texttt{return true}\\\ 3.&\quad\quad\texttt{if not
Consistent}(\mathcal{M},n-1)\ \texttt{return false}\\\
4.&\quad\quad\texttt{for each }[\alpha]\Box\psi\in cl(\varphi)\texttt{ where
}\alpha\in\sigma:\\\ 5.&\quad\qquad\texttt{for each }p\in
P^{\varphi}_{\mathrm{hue}}:\\\ 6.&\qquad\qquad\texttt{var
}\textrm{flag}\leftarrow\texttt{false}\\\ 7.&\qquad\qquad\texttt{for each
}\psi\textrm{-pseudo-model
}\mathcal{N}=(\mathcal{S}^{\prime},\approx^{\prime},\mathcal{V}^{\prime}):\\\
8.&\quad\qquad\qquad\texttt{if }\texttt{Consistent}(\mathcal{N},n-1):\\\
9.&\qquad\qquad\qquad\texttt{for each }\tau\in\mathcal{S}^{\prime}\texttt{
where }\psi\in\tau:\\\ 10.&\qquad\qquad\qquad\quad\texttt{if
}\mathcal{N}_{\tau}{\raisebox{1.29167pt}[0.0pt][0.0pt]{$\medspace\underline{\\!\leftrightarrow\\!}\medspace$}}\mathcal{M}^{(\alpha,p)}_{\sigma}:\\\
11.&\qquad\qquad\qquad\qquad\textrm{flag}\leftarrow\texttt{true}\\\
12.&\quad\qquad\quad\texttt{if not }\textrm{flag},\texttt{ return false}\\\
13.&\quad\texttt{return true}\end{array}$

Given the recursive nature of Definition 16, the procedure
$\mathtt{Consistent}$ is also recursive. The procedure directly checks the
conditions required for Definition 16. Line 7 exploits the fact the the set of
$\varphi$-pseudo-models are finite and may be enumerated (Lemma 17). Line 8
makes a recursive call to check if the $\varphi$-pseudo-model $\mathcal{N}$ is
$(n-1)$-consistent, and if it is, for each element $\tau\in S^{N}$ containing
$\psi$, line 10 applies Definition 14 to compute the syntactic
$\alpha$-$p$-restriction of $\mathcal{M}_{\sigma}$ and applies the standard
process to test whether two finite models are bisimilar [5]. If they are
bisimilar, line 11 updates the flag variable to indicate an $\alpha$-$p$
witness for $\psi$ has been found. If every $[\alpha]\Box\psi$ formula and
every atom $p$ has some $\alpha$-$p$-witness for $\psi$, then the algorithm
$\mathtt{Consistent}(\mathcal{M},n)$ returns true. Therefore,
$\mathtt{Consistent}(\mathcal{M},n)$ checks that every state $\sigma$ has
suitable $\alpha$-$p$-witnesses for every announcement in $cl(\varphi)$ and
that $\mathcal{M}$ is thus $n$-consistent.

This gives a computable syntactic condition on finite models.

###  4.3 Constructing models from pseudo-models

We now need to show that, given a pointed consistent $\varphi$-pseudo-model
$\mathcal{M}_{\sigma}$, we can generate a model
$\overline{\mathcal{M}}_{\overline{\sigma}}$ (see Definition 19) such that for
all $\psi\in\sigma$, $\overline{\mathcal{M}}_{\overline{\sigma}}\models\psi$.
The main complexity of this construction is that we need to engineer a model
such that the set of Boolean announcements agree with the atomic announcements
of the $\varphi$-pseudo-model. From Definition 13 (clause 6) we can see that
the atomic announcements in a $\varphi$-pseudo-model include the announcements
made from atoms from $P^{\varphi}_{\mathrm{hue}}$ and that are closed under
conjunctions and disjunctions but not closed under negation.

We first describe the transformation from a $\varphi$-pseudo-model to an
infinite model.

######  Definition 19.

Suppose that the hue atoms are
$P^{\varphi}_{\mathrm{hue}}=\\{p_{0},p_{1},\ldots,p_{k}\\}$, and that
$\pi_{0},\ldots,\pi_{k}$ are the first $k+1$ prime numbers. Given a positive
integer $n$ and a prime $\pi$, let $\textrm{deg}(\pi,n)=\max\\{i\ |\ \exists
m\in\mathbb{N}^{+},m\pi^{i}=n\\}$ be the highest power of $\pi$ that is a
factor of $n$. Finally suppose,
$P^{\varphi}_{\mathrm{act}}=\\{q^{0}_{1},\ldots,q^{k}_{1},q^{0}_{2},\ldots,q^{k}_{2},q^{0}_{3},\ldots\\}$
is an enumeration of all atoms not in $P^{\varphi}_{\mathrm{col}}\cup
P^{\varphi}_{\mathrm{hue}}$, indexed by the product of the sets
$\\{0,\ldots,k\\}$ and $\mathbb{N}^{+}$.Given these enumerations and a
consistent $\varphi$-pseudo-model
$\mathcal{M}=(\mathcal{S},\approx,\mathcal{V})$, an actualisation of
$\mathcal{M}$ is the model
$\overline{\mathcal{M}}=(\overline{\mathcal{S}},\overline{\approx},\overline{\mathcal{V}})$,
where:

  * •

$\overline{\mathcal{S}}=\mathcal{S}\times\mathbb{N}^{+}$

  * •

$(\sigma,n){\overline{\approx_{a}}}{(\tau,m)}$ if and only if
$\sigma\approx_{a}\tau$.

  * •

for all $p\in P^{\varphi}_{\mathrm{col}}$, for all
$(\sigma,n)\in\overline{\mathcal{S}}$,
$(\sigma,n)\in\overline{\mathcal{V}}(p)$ if and only if
$\sigma\in\mathcal{V}(p)$.

  * •

for all $p_{i}\in P^{\varphi}_{\mathrm{hue}}$,
$\overline{\mathcal{V}}(p_{i})=\emptyset$.

  * •

for all $q_{i}^{j}\in P^{\varphi}_{\mathrm{act}}$, for all
$(\sigma,n)\in\overline{\mathcal{S}}$,
$(\sigma,n)\in\overline{\mathcal{V}}(q_{i}^{j})$ if and only if:
$\sigma\in\mathcal{V}(p_{j})$, and
$\textrm{deg}(\pi_{j},i)=\textrm{deg}(\pi_{j},n)$.

$\dashv$

This construction essentially creates infinitely many copies of the finite
$\varphi$-pseudo-model, with infinitely many fresh atomic propositions to
create the available Boolean announcements. The use of the natural numbers and
the first $k+1$ primes is a convenient way to induce an infinite labelling of
the worlds with the properties we require: particularly, with respect to the
colours, the announcements corresponding to the labels should be closed under
disjunction and conjunction, but not closed under negation. For example the
Boolean announcement of $\neg q_{0}^{0}$ might remove every world
$(\sigma,n)$, where $n$ is odd, but the remaining worlds effectively contain a
complete copy of the original model, via the mapping of worlds
$f(\sigma,n)\mapsto(\sigma,2n)$, and mapping the atoms

$g(q_{i}^{j})\mapsto\left\\{\begin{array}[]{l}q_{i+1}^{j}\quad\textrm{ if
}j=2;\\\ q_{i}^{j}\quad\textrm{ otherwise.}\end{array}\right.$

Before proceeding to a proof of correctness, we will first give an example of
the construction. In this simplified example, suppose that we have a formula:

$\varphi=K_{1}\bigwedge\left[\begin{array}[]{l}\Diamond K_{1}K_{2}\lnot x\\\
\Diamond K_{1}K_{2}\lnot y\\\ \Box(\hat{K}_{1}K_{2}\lnot
x\lor\hat{K}_{1}K_{2}\lnot y)\end{array}\right]$

and a $\varphi$-pseudo-model $\mathcal{M}=(\mathcal{S},\approx,\mathcal{V})$
consisting of five worlds, $\mathcal{S}=\\{a,b,c,x,y\\}$, where atom $x$ is
true only at world $x$, and atom $y$ is true only at world $y$. We suppose
that $x\sim_{2}a\sim_{1}b\sim_{1}c\sim_{2}y$. Finally, we suppose that there
are two fresh atoms in $P^{\varphi}_{\mathrm{hue}}$, $p_{0}$ and $p_{1}$,
where $\mathcal{V}(p_{0})=\\{a,b,x\\}$ and $\mathcal{V}(p_{1})=\\{b,c,y\\}$.
This $\varphi$-pseudo-model is shown at the far left of Figure 4. The
actualisation $\overline{M}$ of this model is shown at the right of Figure 4
including the first three atoms from $P^{\varphi}_{\mathrm{act}}$ that are
included in the denotation of each state.

$x:\\{x,p_{0}\\}$$\mathbf{M}$$a:\\{p_{0}\\}$$b:\\{p_{0},p_{1}\\}$$c:\\{p_{1}\\}$$y:\\{y,p_{0},p_{1}\\}$$1$$1$$2$$2$$\mathbf{\overline{M}}$$\underline{(x,1):\\{q^{0}_{1},q^{0}_{3},q^{0}_{5}\\}}$$\underline{(a,1):\\{q^{0}_{1},q^{0}_{3},q^{0}_{5}\\}}$$\underline{(b,1):\left\\{\begin{array}[]{l}q^{0}_{1},q^{0}_{3},q^{0}_{5}\\\
q^{1}_{1},q^{1}_{2},q^{1}_{4}\end{array}\right\\}}$$(c,1):\\{q^{1}_{1},q^{1}_{2},q^{1}_{4}\\}$$(y,1):\\{q^{1}_{1},q^{1}_{2},q^{1}_{4}\\}$$1$$1$$2$$2$$(x,2):\\{q^{0}_{2},q^{0}_{6},q^{0}_{10}\\}$$(a,2):\\{q^{0}_{2},q^{0}_{6},q^{0}_{10}\\}$$(b,2):\left\\{\begin{array}[]{l}q^{0}_{2},q^{0}_{6},q^{0}_{10}\\\
q^{1}_{1},q^{1}_{2},q^{1}_{4}\end{array}\right\\}$$(c,2):\\{q^{1}_{1},q^{1}_{2},q^{1}_{4}\\}$$(y,2):\\{q^{1}_{1},q^{1}_{2},q^{1}_{4}\\}$$2$$1$$2$$1$$2$$1$$2$$1$$2$$1$$1$$1$$2$$2$$\underline{(x,3):\\{q^{0}_{1},q^{0}_{1},q^{0}_{5}\\}}$$\underline{(a,3):\\{q^{0}_{1},q^{0}_{1},q^{0}_{5}\\}}$$\underline{(b,3):\left\\{\begin{array}[]{l}q^{0}_{1},q^{0}_{3},q^{0}_{5}\\\
q^{1}_{3},q^{1}_{6},q^{1}_{12}\end{array}\right\\}}$$(c,3):\\{q^{1}_{3},q^{1}_{6},q^{1}_{12}\\}$$(y,3):\\{q^{1}_{3},q^{1}_{6},q^{1}_{12}\\}$$2$$1$$2$$1$$2$$1$$2$$1$$2$$1$$2$$1$$1$$2$$2$$\ldots$$\ldots$$\ldots$$\ldots$$\ldots$

Figure 4: A representation of the construction of $\overline{M}$ from the
$\varphi$-pseudo-model $M$. The underlined worlds are the worlds that would
remain after an announcement of $q^{0}_{1}$, while the worlds not underlined
would remain after an announcement of $\lnot q^{0}_{1}$. The accessibility
links for agent $1$ are solid and those for agent $2$ are dashed. We assume
transitivity of access.

The underlined worlds indicate the worlds that would remain after an
announcement of $q^{0}_{1}$ and the worlds not underlined are the worlds that
would remain after an announcement of $\lnot q^{0}_{1}$. As the $0^{th}$ prime
is 2, $q^{0}_{1}$ is true at all states $(\sigma,n)$, where $p_{0}\in\sigma$
and where $\deg(2,n)=1$ (i.e. n is divisible by 2, but not divisible by 4). We
can see that while the underlined states only contain an $a$ state, a $b$
state and an $x$ state, all types of states are retained by an announcement of
$\lnot q^{0}_{1}$.

The variables $q^{i}_{j}$ simply facilitate potential Boolean announcements,
and do not feature explicitly in $cl(\varphi)$. The following variation of
bisimulation allows these variables to be ignored, so long as the set of
available announcements remains the same.

######  Definition 20 (X!-Bisimulation).

Let $M=(S^{M},\sim^{M},V^{M})$ and $N=(S^{N},\sim^{N},V^{N})$ be epistemic
models and $X\subseteq P$ a set of atoms. A non-empty relation
$\mathfrak{R}\subseteq S^{M}\times S^{N}$ paired with a permutation555 A
permutation on a set $A$ is injective and surjective function
$\rho:A\longrightarrow A$ $\rho:(P\setminus X)\longrightarrow(P\setminus X)$
is an $X$-announcement bisimulation, or $X!$-bisimulation, if for every
$(u,v)\in\mathfrak{R}$ the conditions $X$-atoms, $X$!-atoms, forth and back
hold.

  * •

$X$-atoms: for all $p\in X$, $u\in V^{M}(p)$ iff $v\in V^{N}(p)$;

  * •

$X!$-atoms: for all $x\in P\setminus X$, $u\in V^{M}(x)$ iff $v\in
V^{N}(\rho(x))$;

  * •

forth: for all $a\in A$, for all $u^{\prime}$ where $u\sim^{M}_{a}u^{\prime}$,
there exists $v^{\prime}$ where $v\sim^{N}_{a}v^{\prime}$ and
$(u^{\prime},v^{\prime})\in\mathfrak{R}$;

  * •

back: for all $a\in A$, for all $v^{\prime}$ where $v\sim^{N}_{a}v^{\prime}$,
there exists $u^{\prime}$ where $u\sim^{M}_{a}u^{\prime}$ and
$(u^{\prime},v^{\prime})\in\mathfrak{R}$.

If there exists a $X!$-bisimulation $(\mathfrak{R},\rho)$ between $M$ and $N$
such that $(s,t)\in\mathfrak{R}$, then $M_{s}$ and $N_{t}$ are $X!$-bisimilar,
notation
$M_{s}{\raisebox{1.29167pt}[0.0pt][0.0pt]{$\medspace\underline{\\!\leftrightarrow\\!}\medspace$}}_{X!}N_{t}$
(or
$(\mathfrak{R},\rho):M_{s}{\raisebox{1.29167pt}[0.0pt][0.0pt]{$\medspace\underline{\\!\leftrightarrow\\!}\medspace$}}_{X!}N_{t}$).
$\dashv$

Recalling Definition 4 of bisimulation and $X$-restricted bisimulation, it is
clear that an $X$-announcement bisimulation is an $X$-restricted bisimulation
with additional requirements on the atoms not in $X$, formalised in the clause
$X!$-atoms relative to the permutation $\rho$.

We require the following three technical lemmas. The first technical lemma
says that $X$-announcement bisimilarity is an equivalence relation.

######  Lemma 21.

Given any $X\subseteq P$, $X!$-announcement bisimilarity is an equivalence
relation. $\dashv$

###### Proof.

Reflexivity follows because the identity relations $\rho$ and $\mathfrak{R}$
satisfy the requirements of $X!$-bisimulation. Symmetry follows by noting that
the first two clauses of $X!$-bisimulation are symmetric, given that the
inverse of a permutation is a permutation, and the last two are a symmetric
pair. Finally, transitivity follows by noting that given
$(\mathfrak{R}_{1},\rho_{1}):M_{s}{\raisebox{1.29167pt}[0.0pt][0.0pt]{$\medspace\underline{\\!\leftrightarrow\\!}\medspace$}}_{1}^{X}N_{t}$
and
$(\mathfrak{R}_{2},\rho_{2}):N_{t}{\raisebox{1.29167pt}[0.0pt][0.0pt]{$\medspace\underline{\\!\leftrightarrow\\!}\medspace$}}_{2}^{X}O_{u}$,
we may define the permutation $(\mathfrak{R},\rho)$ where:
$\mathfrak{R}=\\{(s^{\prime},o^{\prime})\mid\exists u^{\prime}\in S^{N},\
(s^{\prime},u^{\prime})\in\mathfrak{R}_{1}\ \text{and}\
(u^{\prime},o^{\prime})\in\mathfrak{R}_{2}\\}$ and for all $x\in P\setminus
X$, $\rho(x)=\rho_{2}(\rho_{1}(x))$. It is straightforward to show that these
relations meet the criteria of Definition 20.

The second technical lemma says that $X$-announcement bisimilarity implies
$X$-restricted modal equivalence in $\mathit{BAPAL}$ (Subsection 2.4). That is
significant since $X$-restricted bisimilarity does not imply $X$-restricted
modal equivalence in $\mathit{BAPAL}$.

######  Lemma 22.

Let models $M_{s}$ and $N_{t}$ be given. If
$M_{s}{\raisebox{1.29167pt}[0.0pt][0.0pt]{$\medspace\underline{\\!\leftrightarrow\\!}\medspace$}}_{X!}N_{t}$,
then $M_{s}\equiv_{X}N_{t}$. $\dashv$

###### Proof.

This is given by induction over the complexity of formulas
$\alpha\in{\mathcal{L}}_{\mathit{aanf}}$. The cases of propositional atoms,
Boolean operations and epistemic modalities are all standard for bisimulation
invariance, see also Lemma 7 on bisimulation invariance for $\mathit{BAPAL}$
and the corresponding proof in [17].

Therefore, suppose that $\alpha=[\beta]\Box\gamma$, and for all
$X!$-announcement bisimilar pointed models $M_{u}$, $N_{v}$, for all proper
${\mathcal{L}}_{\mathit{aanf}}$ subformulas $\alpha^{\prime}\subset\alpha$,
$M_{u}\models\alpha^{\prime}$ iff $N_{v}\models\alpha^{\prime}$. Suppose
$M_{s}\models\alpha$, and
$(\mathfrak{R},\rho):M_{s}{\raisebox{1.29167pt}[0.0pt][0.0pt]{$\medspace\underline{\\!\leftrightarrow\\!}\medspace$}}_{X!}N_{t}$.
By the induction hypothesis, for all $u\in S^{M}$ and all $v\in S^{N}$ where
$M_{u}{\raisebox{1.29167pt}[0.0pt][0.0pt]{$\medspace\underline{\\!\leftrightarrow\\!}\medspace$}}_{X!}N_{v}$,
we have $M_{u}\models\beta$ if and only if $N_{v}\models\beta$. It follows
that the relation $\mathfrak{R}^{\beta}$ defined as
$(u^{\prime},v^{\prime})\in\mathfrak{R}^{\beta}$ iff
$(u^{\prime},v^{\prime})\in\mathfrak{R}$ and $M_{u^{\prime}}\models\beta$, is
an $X!$-announcement bisimulation between $M^{\beta}$ and $N^{\beta}$
(containing $(u,v)$). Similarly, it follows that for all
$\theta\in{\mathcal{L}}_{\mathit{pl}}$ such that $M^{\beta}_{u}\models\theta$
we have $M^{\beta\theta}_{u}\models\gamma$. Let $\theta^{\prime}$ be the
formula that results from substituting all instances of all propositional
atoms $x\in P\setminus{X}$ in $\theta$ with $\rho^{-1}(x)$. It follows that
for all $(u,v)\in\mathfrak{R}^{\beta}$, $M^{\beta}_{u}\models\theta^{\prime}$
iff $N^{\beta}_{v}\models\theta$. Therefore
$(\mathfrak{R},\rho):M_{u}^{\beta\theta^{\prime}}{\raisebox{1.29167pt}[0.0pt][0.0pt]{$\medspace\underline{\\!\leftrightarrow\\!}\medspace$}}_{X!}N_{v}^{\beta\theta}$,
and since $\theta^{\prime}\in{\mathcal{L}}_{\mathit{pl}}$ we must
$M_{u}^{\beta\theta^{\prime}}\models\gamma$. By the induction hypothesis it
follows $N_{v}^{\beta\theta}\models\gamma$ for all
$\theta\in{\mathcal{L}}_{\mathit{pl}}$. Therefore,
$N_{t}^{\beta}\models\Box\gamma$, and hence $N_{t}\models[\beta]\Box\gamma$.
The reverse direction follows from the symmetry of $X!$-bisimulation (Lemma
21).

The third technical lemma shows that given bisimilar $\varphi$-pseudo-models,
Definition 19 will generate $P^{\varphi}_{\mathrm{col}}$-bisimilar
actualisations.

######  Lemma 23.

Let consistent $\varphi$-pseudo-models
$\mathcal{M}_{\sigma}=(\mathcal{S},\approx,\mathcal{V})$ and
$\mathcal{N}_{\tau}=(\mathcal{S}^{\prime},\approx^{\prime},\mathcal{V}^{\prime})$
be given. If
$\mathcal{M}_{\sigma}{\raisebox{1.29167pt}[0.0pt][0.0pt]{$\medspace\underline{\\!\leftrightarrow\\!}\medspace$}}\mathcal{N}_{\tau}$,
then
$\overline{\mathcal{M}}_{(\sigma,1)}{\raisebox{1.29167pt}[0.0pt][0.0pt]{$\medspace\underline{\\!\leftrightarrow\\!}\medspace$}}_{P^{\varphi}_{\mathrm{col}}!}\overline{\mathcal{N}}_{(\tau,1)}$.
$\dashv$

###### Proof.

Let $\mathfrak{R}\subset\mathcal{S}\times\mathcal{S}^{\prime}$ be a
bisimulation between $\mathcal{M}$ and $\mathcal{N}$, where
$(\sigma,\tau)\in\mathfrak{R}$, and suppose that $\\{q^{0}_{1},\ldots\\}$ was
the enumeration of $P^{\varphi}_{\mathrm{act}}$ used in the actualisation
$\overline{\mathcal{M}}$, and that $\\{r^{0}_{1},\ldots\\}$ was the
enumeration of $P^{\varphi}_{\mathrm{act}}$ used in the actualisation
$\overline{\mathcal{N}}$ (Definition 19). We define the
$P^{\varphi}_{\mathrm{col}}!$-announcement bisimulation
$(\mathfrak{R}^{\prime},\rho^{\prime})$ where

$\mathfrak{R}^{\prime}=\\{((\sigma^{\prime},x),(\tau^{\prime},x))\ |\
(\sigma^{\prime},\tau^{\prime})\in\mathfrak{R},x\in\mathbb{N}^{+}\\},\quad\forall
p\in P^{\varphi}_{\mathrm{hue}},\rho(p)=p,\textrm{ and}\ \forall
i,j\in\mathbb{N},\rho(q^{i}_{j})=r^{i}_{j}.$

It can be shown that $\mathfrak{R}^{\prime}$ and $\rho^{\prime}$ satisfy the
clauses $X$-atoms, $X!$-atoms, forth and back of Definition 20 as follows:

  * •

$X$-atoms: if
$((\sigma^{\prime},x),(\tau^{\prime},x))\in\mathfrak{R}^{\prime}$ then
$(\sigma^{\prime},\tau^{\prime})\in\mathfrak{R}$ and by Definition 4 for all
$p\in P^{\varphi}_{\mathrm{col}}$, $\sigma^{\prime}\in\mathcal{V}(p)$ if and
only if $\tau^{\prime}\in\mathcal{V}^{\prime}(p)$. It follows from Definition
19 that $(\sigma^{\prime},x)\in\overline{\mathcal{V}}(p)$ if and only if
$(\tau,x)\in\overline{\mathcal{V}^{\prime}}(p)$.

  * •

$X!$-atoms: if
$((\sigma^{\prime},x),(\tau^{\prime},x))\in\mathfrak{R}^{\prime}$ then from
Definition 19, for all $p\in P^{\varphi}_{\mathrm{hue}}$,
$\overline{\mathcal{V}}(p)=\overline{\mathcal{V}^{\prime}}(p)=\emptyset$, so
$(\sigma^{\prime},x)\in\overline{\mathcal{V}}(p)$ if and only if
$(\tau^{\prime},x)\in\overline{\mathcal{V}^{\prime}}(p)$. Likewise for all
$q^{i}_{j}\in P^{\varphi}_{\mathrm{act}}$,
$(\sigma^{\prime},x)\in\overline{\mathcal{V}}(q^{i}_{j})$ if and only if
$\sigma^{\prime}\in\mathcal{V}(x_{i})$ and $\deg(\pi_{i},j)=\deg(\pi_{i},n)$.
Since $(\sigma^{\prime},\tau^{\prime})\in\mathfrak{R}$ it follows that
$\tau^{\prime}\in\mathcal{V}(x_{i})$, and therefore
$(\tau^{\prime},x)\in\overline{\mathcal{V}^{\prime}}(r^{i}_{j})=\overline{\mathcal{V}^{\prime}}(\rho(q^{i}_{j}))$
as required.

  * •

forth: for all $a\in A$, for all
$((\sigma^{\prime},x),(\tau^{\prime},x))\in\mathfrak{R}^{\prime}$, if
$(\sigma^{\prime},x)\overline{\approx}(\sigma^{\prime\prime},y)$, then by
Definition 20, $(\sigma^{\prime},\tau^{\prime})\in\mathfrak{R}$ and by
Definition 19, $\sigma^{\prime}\approx\sigma^{\prime\prime}$. Therefore, there
is some $\tau^{\prime\prime}$ such that
$(\sigma^{\prime\prime},\tau^{\prime\prime})\in\mathfrak{R}$, and
$\tau^{\prime}\approx^{\prime}\tau^{\prime\prime}$. By Definition 19,
$(\tau^{\prime\prime},y)\in\overline{\mathcal{S}^{\prime}}$ and
$((\sigma^{\prime\prime},y),(\tau^{\prime\prime},y))\in\mathfrak{R}^{\prime}$
as required.

  * •

back: this may be shown in the same manner as forth.

Figure 5 shows how the denotations of $P^{\varphi}_{\mathrm{hue}}$ atoms in
$\mathcal{M}$ correspond to the denotation of $P^{\varphi}_{\mathrm{act}}$
atoms in $\overline{\mathcal{M}}$.

$\mathcal{M}$$\sigma_{1}$$\sigma_{2}^{*}$$\sigma_{3}^{*}$$\sigma_{4}$$\sigma_{5}^{*}$$\sigma_{6}$$\sigma_{7}$$\alpha$$\overline{\mathcal{M}}$$1$$\overline{\circ}$$\underline{\overline{\bullet}}^{\prime}$$\underline{\overline{\bullet}}^{\prime}$$\underline{\circ}^{\prime}$$\underline{\overline{\bullet}}^{\prime}$$\underline{\overline{\circ}}$$\underline{\overline{\circ}}$$2$$\circ^{\prime}$$\circ^{\prime}$$\circ^{\prime}$$\circ^{\prime}$$\circ^{\prime}$$\circ$$\circ$$3$$\circ^{\prime}$$\underline{\circ}^{\prime}$$\underline{\circ}^{\prime}$$\underline{\circ}^{\prime}$$\underline{\circ}^{\prime}$$\underline{\circ}$$\underline{\circ}$$4$$\overline{\circ}$$\overline{\circ}$$\overline{\circ}$$\circ^{\prime}$$\overline{\circ}$$\overline{\circ}$$\overline{\circ}$$5$$\circ^{\prime}$$\underline{\circ}^{\prime}$$\underline{\circ}^{\prime}$$\underline{\circ}^{\prime}$$\underline{\circ}^{\prime}$$\underline{\circ}$$\underline{\circ}$$6$$\circ^{\prime}$$\circ^{\prime}$$\circ^{\prime}$$\circ^{\prime}$$\circ^{\prime}$$\circ$$\circ$$7$$\overline{\circ}$$\underline{\overline{\bullet}}^{\prime}$$\underline{\overline{\bullet}}^{\prime}$$\underline{\circ}^{\prime}$$\underline{\overline{\bullet}}^{\prime}$$\underline{\overline{\circ}}$$\underline{\overline{\circ}}$$\ldots$

Figure 5: A representation of the correspondence between
$\overline{\mathcal{M}}$ and the $\varphi$-pseudo-model $\mathcal{M}$. In this
figure the model $\mathcal{M}$ is on the left, the top five worlds of
$\mathcal{M}$ satisfy $\alpha$, and the model $\overline{\mathcal{M}}$ is on
the right. The states that correspond to $p\in P^{\varphi}_{\mathrm{hue}}$ are
overlined and the states that correspond to $q\in P^{\varphi}_{\mathrm{hue}}$
are underlined. The states that correspond to $\alpha\land p\land q$ are
represented as $\bullet$ and the states that correspond to
$\alpha\land(p\rightarrow q)$ are primed. In the model $\mathcal{M}$, there is
some atom $r\in P^{\varphi}_{\mathrm{hue}}$ that corresponds to $p\land q$ and
the states satisfying $r$ are marked with an ∗.

Consider a Boolean formula $\beta=p\land q$. In the Figure 5 the states that
will be preserved in $\overline{\mathcal{M}}^{\alpha\land\beta}$ are
represented by $\bullet$, and correspond to some propositional atom in
$P^{\varphi}_{\mathrm{hue}}$ (represented by the ∗ in the $\varphi$-pseudo-
model $\mathcal{M}$, on the left). If instead we considered the formula
$\gamma=p\rightarrow q$, all the primed states would remain, and thus every
state containing $\alpha$ in the $\varphi$-pseudo-model $\mathcal{M}$ would
have a corresponding state in the model
$\overline{\mathcal{M}}^{\alpha\land\gamma}$.

We require the following lemmas establishing the correspondence between the
announcement of Boolean formulas in $\overline{\mathcal{M}}$ and the syntactic
restriction to $P^{\varphi}_{\mathrm{hue}}$ atoms in $\mathcal{M}$. The first
shows that for every Boolean formula in the actualisation of $\varphi$-pseudo-
model we can find a corresponding $P^{\varphi}_{\mathrm{hue}}$ atom in the
$\varphi$-pseudo-model such that the announcement of the Boolean formula in
$\overline{\mathcal{M}}$ preserves the same set of colours as the syntactic
restriction of $\mathcal{M}$ to the atom.

The second lemma shows that the syntactic restriction to each
$P^{\varphi}_{\mathrm{hue}}$ atom in the $\varphi$-pseudo-model $\mathcal{M}$
corresponds to the announcement of some Boolean formula in its actualisation
$\overline{\mathcal{M}}$. As these lemmas will be applied in the inductive
proof of Lemma 26, they are qualified with respect to the announcement depth
of formulas $x$, and where $D(\alpha)>x$, presume that $\alpha\in\sigma$
coincides with $\overline{\mathcal{M}}_{(\sigma,n)}\models\alpha$.

######  Lemma 24.

Suppose $\mathcal{M}_{\sigma}=(\mathcal{S},\approx,\mathcal{V})_{\sigma}$ is
an $x$-consistent $\varphi$-pseudo-model, $\alpha\in cl_{0}(\varphi)$ where
$D(\alpha)<x$, and suppose that $\alpha\in\sigma$ if and only if for all
$n\in\mathbb{N}^{+}$, $\overline{\mathcal{M}}_{(\sigma,n)}\models\alpha$. Then
for every Boolean formula $\beta\in{\mathcal{L}}_{\mathit{pl}}{}$, there is
some $p\in P^{\varphi}_{\mathrm{hue}}$ such that for all $n\in\mathbb{N}^{+}$,
where $\overline{\mathcal{M}}_{(\sigma,n)}\models\alpha\land\beta$,
$\overline{\mathcal{M}}_{(\sigma,n)}^{\alpha\land\beta}{\raisebox{1.29167pt}[0.0pt][0.0pt]{$\medspace\underline{\\!\leftrightarrow\\!}\medspace$}}_{P^{\varphi}_{\mathrm{col}}!}\overline{\mathcal{M}^{(\alpha,p)}}_{(\sigma,n)}$.
$\dashv$

###### Proof.

Any Boolean formula $\beta\in{\mathcal{L}}_{\mathit{pl}}{}$ may be converted
into the following form:

$\bigwedge\left[\begin{array}[]{l}\lambda_{1}^{1}\lor\ldots\lor\lambda_{1}^{j_{1}}\lor\mu_{1}^{1}\lor\ldots\lor\mu_{1}^{k_{1}}\lor\nu_{1}^{1}\lor\ldots\lor\nu_{1}^{\ell_{1}}\\\
\lambda_{2}^{1}\lor\ldots\lor\lambda_{2}^{j_{2}}\lor\mu_{2}^{1}\lor\ldots\lor\mu_{2}^{k_{2}}\lor\nu_{2}^{1}\lor\ldots\lor\nu_{2}^{\ell_{2}}\\\
\ldots\\\
\lambda_{m}^{1}\lor\ldots\lor\lambda_{m}^{j_{m}}\lor\mu_{m}^{1}\lor\ldots\lor\mu_{m}^{k_{m}}\lor\nu_{m}^{1}\lor\ldots\lor\nu_{m}^{\ell_{m}}\end{array}\right]$

where each formula $\lambda_{i}^{j}\in\\{p,\lnot p\ |p\in
P^{\varphi}_{\mathrm{col}}\\}$ is either a colour atom or a negated colour
atom, each formula $\mu_{i}^{j}\in\\{p,\lnot p\ |p\in
P^{\varphi}_{\mathrm{hue}}\\}$ is either a hue atom or a negated hue atom, and
each formula $\nu_{i}^{j}\in\\{p,\lnot p\ |p\in P^{\varphi}_{\mathrm{act}}\\}$
is either an actualisation atom or a negated actualisation atom. The model
$\overline{\mathcal{M}}_{(\sigma,n)}^{\alpha\land\beta}$ will consist of all
worlds $(\sigma,n)$, where $\alpha\in\sigma$, and where for all $i\leq m$,
$(\sigma,n)$ satisfies one of the literals on the $i^{th}$ line of the above
form. Let us represent the disjunctive normal form above by
$\delta_{1}\wedge\dots\wedge\delta_{m}$. For each such disjunct $\delta_{i}$,
we claim it is possible to define some set of atoms $X_{i}\subset
P^{\varphi}_{\mathrm{hue}}$ such that for all $\tau\in\mathcal{S}$,
$\overline{\mathcal{M}}_{(\tau,n)}\models\delta_{i}$ for some $n$ if and only
if $X_{i}\cap\tau\neq\emptyset$. The existence of $X$ follows from Definitions
13 and 19:

  1. 1.

From Definition 19 we obtain that, for all $p\in P^{\varphi}_{\mathrm{hue}}$,
$p$ is false everywhere in $\overline{\mathcal{M}}$, so if $\lnot p$ appears
in $\delta_{i}$ then $\overline{M}_{(\tau,n)}\models\delta_{i}$ for all $n$,
so we may suppose that $X_{i}=P^{\varphi}_{\mathrm{hue}}$, since at least one
such atom is always guaranteed to be present in $\tau$. Otherwise $p$ will
never be satisfied in $\overline{\mathcal{M}}$ and it may be ignored.

  2. 2.

Each $\nu_{i}^{j}$ is equivalent to some atom $q^{\ell}_{k}$ or its negation,
and from Definition 19, for all $(\tau,n)\in\overline{\mathcal{S}}$,
$(\tau,n)\in\overline{\mathcal{V}}(q^{\ell}_{k})$ if and only if there is some
$x_{\ell}\in P^{\varphi}_{\mathrm{hue}}$ where $x_{\ell}\in\tau$ and
$\deg(\pi_{\ell},k)=\deg(\pi_{\ell},n)$. For all $\tau\in\mathcal{S}^{M}$, a
negative occurrence of $q^{\ell}_{k}$ will be satisfied by $(\tau,n)$ for
infinitely many $n$, so if $\lnot q^{\ell}_{k}$ appears in $\delta_{i}$, we
may suppose that $X_{i}=P^{\varphi}_{\mathrm{hue}}$. Otherwise if
$q^{\ell}_{k}$ appears positively in $\delta_{i}$, then for all
$\tau\in\mathcal{S}^{M}$, there will be infinitely many $n$ where
$\deg(\pi_{\ell},k)=\deg(\pi_{\ell},n)$666 For example, $mk$ for any
$m\in\mathbb{N}^{+}$ where $\pi_{\ell}$ does not divide $m$. , so we will
require that $x_{\ell}\in X_{i}$.

  3. 3.

Finally each $\lambda_{i}^{j}$ that appears in $\delta_{i}$ is either $p$ or
$\lnot p$ for some $p\in P^{\varphi}_{\mathrm{col}}$, so from the fifth clause
of Definition 13 there is some $x\in P^{\varphi}_{\mathrm{hue}}$, where
$x\in\tau$ if and only if
$\overline{\mathcal{M}}_{(\tau,n)}\models\lambda_{i}^{j}$, so each such $x$ is
included in $X_{i}$.

Thus the claim is shown and there is a set of atoms $X_{i}\subset
P^{\varphi}_{\mathrm{hue}}$ such that for all $\tau\in\mathcal{S}$,
$\overline{\mathcal{M}}_{(\tau,n)}\models\delta_{i}$ for some $n$ if and only
if $X_{i}\cap\tau\neq\emptyset$. Furthermore, from the sixth clause of
Definition 13, there is an atom $x^{i}\in P^{\varphi}_{\mathrm{hue}}$ which
has a denotation in $\mathcal{M}$ that is equivalent to the denotation of the
disjunction of the atoms in $X_{i}$. Therefore, for all $\tau\in\mathcal{S}$,
$\overline{\mathcal{M}}_{(\tau,n)}\models\delta_{i}$ for some $n$ if and only
if $x^{i}\in\tau$. Also, by the sixth clause of Definition 13, the denotations
of atoms in $P^{\varphi}_{\mathrm{hue}}$ are closed under intersection, so
there is some atom $p\in P^{\varphi}_{\mathrm{hue}}$ with denotation in
$\mathcal{M}$ equivalent to $\bigwedge_{i=1}^{m}x^{i}$.

Given $p\in P^{\varphi}_{\mathrm{hue}}$, and the formula $\alpha$, it remains
to show that
$\overline{\mathcal{M}}_{(\sigma,n)}^{\alpha\land\beta}{\raisebox{1.29167pt}[0.0pt][0.0pt]{$\medspace\underline{\\!\leftrightarrow\\!}\medspace$}}_{P^{\varphi}_{\mathrm{col}}!}\overline{\mathcal{M}^{(\alpha,p)}}_{(\sigma,n)}$.
Suppose that the construction of $\overline{M^{(\alpha,p)}}_{(\sigma,n)}$
(Definition 19) uses the enumeration of $P^{\varphi}_{\mathrm{act}}$,
$r^{0}_{1},\ldots,r^{k}_{1},r^{0}_{2},\ldots r^{k}_{2},\ldots$, where the
elements of $P^{\varphi}_{\mathrm{hue}}$ are $x_{1},\ldots,x_{k}$. Also,
suppose $\overline{\mathcal{M}}$ was defined using the enumeration of
$P^{\varphi}_{\mathrm{act}}$, $q^{0}_{1},\ldots,q^{k}_{1},q^{0}_{2},\ldots
q^{k}_{2},\ldots$ We define the $P^{\varphi}_{\mathrm{col}}!$-announcement
bisimulation $(\mathfrak{R},\rho)$ between
$\overline{\mathcal{M}}^{\alpha\wedge\beta}=(S^{\prime},\sim^{\prime},V^{\prime})$
and
$\overline{\mathcal{M}^{(\alpha,p)}}=(S^{\prime\prime},\sim^{\prime\prime},V^{\prime\prime})$,
where $\mathfrak{R}\subset S^{\prime}\times S^{\prime\prime}$ by

$((\tau,m),(\tau^{\prime},m^{\prime}))\in\mathfrak{R}\quad\text{iff}\quad\tau=\tau^{\prime}\
\text{and}\ m=m^{\prime},$

and

$\forall x\in
P^{\varphi}_{\mathrm{hue}},\rho(x)=x\quad\textrm{and}\quad\forall q^{i}_{j}\in
P^{\varphi}_{\mathrm{act}},\rho(q^{i}_{j})=r^{i}_{j}.$

To verify that $(\mathfrak{R},\rho)$ is an
$P^{\varphi}_{\mathrm{col}}!$-announcement bisimulation between
$\overline{\mathcal{M}}_{(\sigma,n)}^{\alpha\land\beta}$ and
$\overline{\mathcal{M}^{(\alpha,p)}}_{(\sigma,n)}$ via $\rho$ it is required
to show the follow clauses of Definition 20 hold:

  * •

$X$-atoms: this is immediate since $\mathfrak{R}$ is the identity relation,
and $\overline{\mathcal{M}}^{\alpha\wedge\beta}$ and
$\overline{\mathcal{M}^{(\alpha,p)}}$ have a common valuation function.

  * •

$X!$-atoms: this follows since for all $p\in P^{\varphi}_{\mathrm{hue}}$,
$\rho$ is the identity function, and for atoms in
$P^{\varphi}_{\mathrm{act}}$, $\rho$ relates $q^{i}_{j}$ to $r^{i}_{j}$. In
both cases Definition 20 assigns $V^{\prime}(p)=V^{\prime\prime}(\rho(p))$.

  * •

forth: Since $S^{\prime}\subset\mathcal{S}\times\mathbb{N}^{+}$,
$S^{\prime\prime}\subset\mathcal{S}\times\mathbb{N}^{+}$, and
$(\tau,x)\sim^{\prime}(\tau^{\prime},y)\sim^{\prime\prime}(\tau,x)$ if and
only if $\tau\approx\tau^{\prime}$, forth trivially holds if for every
$(\tau,x)\in S^{\prime}$, there is some $y\in\mathbb{N}^{+}$, such
$(\tau,y)\in S^{\prime\prime}$. This follows from the reasoning above: that
there is some $p\in P^{\varphi}_{\mathrm{hue}}$ where for all
$\tau\in\mathcal{S}$, $\overline{\mathcal{M}}_{(\tau,n)}\models\beta$ for some
$n$ if and only if $p\in\tau$; and the assumption that $\alpha\in\tau$ if and
only if $\overline{\mathcal{M}}_{(\tau,n)}\models\alpha$.

  * •

back: This may be shown similarly to forth.

Therefore,
$\overline{\mathcal{M}}_{(\sigma,n)}^{\alpha\land\beta}{\raisebox{1.29167pt}[0.0pt][0.0pt]{$\medspace\underline{\\!\leftrightarrow\\!}\medspace$}}_{P^{\varphi}_{\mathrm{col}}!}\overline{\mathcal{M}_{\sigma}^{(\alpha,p)}}$.

Conversely, it is required to show that for every hue atom, $p\in
P^{\varphi}_{\mathrm{hue}}$, there is a corresponding Boolean announcement in
$\overline{\mathcal{M}}$.

######  Lemma 25.

Suppose $\mathcal{M}_{\sigma}=(\mathcal{S},\approx,\mathcal{V})$ is an
$x$-consistent $\varphi$-pseudo-model, and $\alpha\in cl_{0}(\varphi)$ where
$D(\alpha)<x$. Suppose also that for all $\sigma\in\mathcal{S}$,
$\alpha\in\sigma$ if and only if for all $n\in\mathbb{N}^{+}$,
$\overline{M}_{(\sigma,n)}\models\alpha$. Then for every $p\in
P^{\varphi}_{\mathrm{hue}}$, for all $n\in\mathbb{N}^{+}$, there is some
Boolean formula $\beta\in{\mathcal{L}}_{\mathit{pl}}{}$, and some $m$ such
that
$\overline{\mathcal{M}^{(\alpha,p)}}_{(\sigma,n)}{\raisebox{1.29167pt}[0.0pt][0.0pt]{$\medspace\underline{\\!\leftrightarrow\\!}\medspace$}}_{P^{\varphi}_{\mathrm{col}}!}\overline{\mathcal{M}}_{(\sigma,m)}^{\alpha\land\beta}$.
$\dashv$

###### Proof.

Suppose in the construction of $\overline{\mathcal{M}}$ (Definition 19) the
primes $\pi_{0},\ldots,\pi_{\ell}$ correspond to the atoms in
$P^{\varphi}_{\mathrm{hue}}$ and particularly, the atom $p\in
P^{\varphi}_{\mathrm{hue}}$ corresponds to some such prime $\pi_{y}$. For all
$n\in\mathbb{N}^{+}$, there is an atom $q^{y}_{k}\in
P^{\varphi}_{\mathrm{act}}$ such that
$(\tau,n)\in\overline{\mathcal{V}}(q^{y}_{k})$ if and only if $p\in\tau$ and
$\deg(\pi_{y},n)=k$. Suppose in the definition of $\overline{M}$ the atoms in
$P^{\varphi}_{\mathrm{act}}$ were enumerated as
$q^{0}_{1},\ldots,q^{k}_{1},q^{0}_{2},\ldots q^{k}_{2},\ldots$ (where
$0,\ldots,k$ indexes $P^{\varphi}_{\mathrm{hue}}$), and in the definition of
$\overline{\mathcal{M}^{(\alpha,p)}}$ the atoms of
$P^{\varphi}_{\mathrm{act}}$ were indexed as
$r^{0}_{1},\ldots,r^{k}_{1},r^{0}_{2},\ldots r^{k}_{2},\ldots$. For every
$z\in\mathbb{N}^{+}$, the model $\overline{\mathcal{M}}^{\alpha\land
q^{y}_{z}}_{(\sigma,n)}$ is $P^{\varphi}_{\mathrm{col}}!$-bisimilar to the
model $\overline{\mathcal{M}^{(\alpha,p)}}_{(\sigma,\frac{n}{\pi_{y}^{z}})}$
via the pair $(\mathfrak{R},\rho)$ where

$\mathfrak{R}=\\{((\tau,m),(\tau,m^{\prime}))\ |\
\tau\in\mathcal{S}^{\alpha},m^{\prime}=m\cdot\pi_{y}^{z}\\},$

and $\forall x\in P^{\varphi}_{\mathrm{hue}},\ \rho(x)=x$ (noting that these
atoms have the empty denotation), and $\forall q^{i}_{j}\in
P^{\varphi}_{\mathrm{act}},\ \rho(q_{i}^{j})=r^{i}_{j}$.

It is straightforward to show that $\mathfrak{R}$ is an
$P^{\varphi}_{\mathrm{col}}$-announcement bisimulation, via $\rho$.

###  4.4 The correspondence of models and pseudo-models

The following lemma establishes the correspondence between the
$\varphi$-pseudo-model and the satisfiability of $\varphi$.

######  Lemma 26.

Suppose that $\mathcal{M}_{\sigma}=(\mathcal{S},\approx,\mathcal{V})$ is a
consistent $\varphi$-pseudo-model. Then for all $\sigma\in\mathcal{S}$, for
all $\psi\in cl_{0}(\varphi)$, $\psi\in\sigma$ if and only if
$\overline{\mathcal{M}}_{(\sigma,1)}\models\psi$. $\dashv$

###### Proof.

We proceed by induction over the complexity of formulas. The induction
hypothesis is:

  * $\mathbf{IH}_{\psi}$

Given the formula $\psi\in cl_{0}(\varphi)$, where  $D(\psi)\leq x$, given any
$x$-consistent $\varphi$-pseudo-model $\mathcal{N}_{\tau}$, then $\psi\in\tau$
if and only if for all $n>0$, $\overline{\mathcal{N}}_{(\tau,n)}\models\psi$.

The induction proceeds to show if for all $\psi\subseteq\varphi^{\prime}$,
$\mathbf{IH}_{\psi}$ holds, then $\mathbf{IH}_{\varphi^{\prime}}$ holds. The
base of this induction corresponds to the atomic propositions, and this, along
with the inductive cases, is presented below. Suppose that
$\varphi^{\prime}\in cl_{0}(\varphi)$ and $D(\varphi^{\prime})\leq x$.

  * •

If $\varphi^{\prime}=p$, then for all pointed $x$-consistent $\varphi$-pseudo-
models $\mathcal{M}_{\sigma}$, $p\in\sigma$ if and only if
$(\sigma,n)\in\overline{\mathcal{V}}(p)$ (by Definition 19) and therefore
$M_{(\sigma,n)}\models p$ by Definition 6.

  * •

if $\varphi^{\prime}=\lnot\psi$, then, as $\mathbf{IH}_{\psi}$ holds, we have
for all pointed $x$-consistent $\varphi$-pseudo-models $\mathcal{M}_{\sigma}$,
$\psi\in\sigma$ if and only for all $n>0$,
$\overline{\mathcal{M}}_{(\sigma,n)}\models\psi$. By Definition 13,
$\psi\in\sigma$ if and only if $\lnot\psi\notin\sigma$, so it follows that
$\lnot\psi\in\sigma$ if and only for all $n>0$,
$\mathcal{M}_{(\sigma,n)}\models\lnot\psi$.

  * •

if $\varphi^{\prime}=\psi_{1}\land\psi_{2}$, then by $\mathbf{IH}_{\psi_{1}}$
and $\mathbf{IH}_{\psi_{2}}$ we have that for all $x$-consistent pointed
$\varphi$-pseudo-models: $\psi_{1}\in\sigma$ if and only if for all $n>0$,
$\overline{\mathcal{M}}_{(\sigma,n)}\models\psi_{1}$, and $\psi_{2}\in\sigma$
if and only if for all $n>0$,
$\overline{\mathcal{M}}_{(\sigma,n)}\models\psi_{2}$. It follows from
Definition 13 that for all $x$-consistent pointed $\varphi$-pseudo-models
$\mathcal{M}_{\sigma}$, $\psi_{1}\land\psi_{2}\in\sigma$ if and only if for
all $n>0$, $\overline{\mathcal{M}}_{(\sigma,n)}\models\psi_{1}\land\psi_{2}$.

  * •

If $\varphi^{\prime}=K_{a}\psi$, then by $\mathbf{IH}_{\psi}$, for all
$x$-consistent pointed $\varphi$-pseudo-models $\mathcal{M}_{\tau}$, we have
$\psi\in\tau$ if and only if for all $n>0$,
$\overline{\mathcal{M}}_{(\tau,n)}\models\psi$. If for some $x$-consistent
pointed $\varphi$-pseudo-model $\mathcal{M}_{\sigma}$ we have
$K_{a}\psi\in\sigma$, then by the second clause of Definition 13 we obtain
that for all $\tau\in\mathcal{S}$ where $\sigma\approx_{a}\tau$, we have
$\psi\in\tau$. Applying the induction hypothesis, it follows that for all
$\tau\in\mathcal{S}$ where $\sigma\approx_{a}\tau$, for all $n>0$,
$\overline{\mathcal{M}}_{(\tau,n)}\models\psi$. Given
$\overline{M}=(S,\sim,V)$, by Definition 19, for all $n>0$, for all
$(\tau^{\prime},n^{\prime})\in S$ with
$(\sigma,n)\sim_{a}(\tau^{\prime},n^{\prime})$, we must have
$\sigma\approx_{a}\tau^{\prime}$, so it follows that for all
$(\tau^{\prime},n^{\prime})\in S$ with $(\sigma,n)\sim
a(\tau^{\prime},n^{\prime})$, we have
$\overline{\mathcal{M}}_{(\tau^{\prime},n^{\prime})}\models\psi$. It follows
that for all $n>0$, $\overline{\mathcal{M}}_{(\sigma,n)}\models K_{a}\psi$.

Conversely, if for some $x$-consistent $\varphi$-pseudo-model
$\mathcal{M}=(\mathcal{S},\approx,\mathcal{V})$ with $\sigma\in\mathcal{S}$,
we have $K_{a}\psi\notin\sigma$, then by the third clause of Definition 13,
there is some $\tau\in\mathcal{S}$ with $\sigma\approx_{a}\tau$ and
$\psi\notin\tau$. As above, it follows from Definition 19 that for all $n>0$,
there is some $n^{\prime}>0$ such that $(\tau,n^{\prime})\sim_{a}(\sigma,n)$,
and $\psi\notin\tau$. From the induction hypothesis, we have
$\overline{\mathcal{M}}_{(\tau,n^{\prime})}\not\models\psi$, and thus
$\overline{\mathcal{M}}_{(\sigma,n)}\not\models K_{a}\psi$.

  * •

If $\varphi^{\prime}=[\alpha]\Box\psi$, then for some $x$-consistent
$\varphi$-pseudo-model
$\mathcal{M}_{\sigma}=(\mathcal{S},\approx,\mathcal{V})$, suppose that
$\varphi^{\prime}\in\sigma\in\mathcal{S}$. If $\alpha\notin\sigma$, then as
$\alpha$ is a subformula of $\varphi^{\prime}$, the induction hypothesis
$\mathbf{IH}_{\alpha}$ holds. It follows that for all $n>0$,
$\overline{\mathcal{M}}_{(\sigma,n)}\not\models\alpha$, and so
$\overline{\mathcal{M}}_{(\sigma,n)}\models\varphi^{\prime}$ is vacuously
true.

So now suppose that $\alpha\in\sigma$. From Lemma 24 we have that for every
$\beta\in{\mathcal{L}}_{\mathit{pl}}{}$ there is some $p^{\prime}\in
P^{\varphi}_{\mathrm{hue}}$ such that for all $n\in\mathbb{N}^{+}$,
$\overline{\mathcal{M}}^{\alpha\land\beta}_{(\sigma,n)}{\raisebox{1.29167pt}[0.0pt][0.0pt]{$\medspace\underline{\\!\leftrightarrow\\!}\medspace$}}_{P^{\varphi}_{\mathrm{col}}!}\overline{\mathcal{M}^{(\alpha,p^{\prime})}}_{(\sigma,n)}$.
As $p^{\prime}\in P^{\varphi}_{\mathrm{hue}}$, from Definition 16, there is
some $(x-1)$-consistent $\varphi$-pseudo-model $\mathcal{N}$ with
$\tau\in{\mathcal{D}}(N)$, $\psi\in\tau$ and
$\mathcal{N}_{\tau}{\raisebox{1.29167pt}[0.0pt][0.0pt]{$\medspace\underline{\\!\leftrightarrow\\!}\medspace$}}\mathcal{M}_{\sigma}^{(\alpha,p^{\prime})}$.
As $D(\psi)\leq x-1$, we may apply the induction hypothesis
$\mathbf{IH}_{\psi}$ to infer, for all $n\in\mathbb{N}^{+}$,
$\overline{\mathcal{N}}_{(\tau,n)}\models\psi$. From Lemma 23 it follows that
$\overline{\mathcal{N}}_{(\tau,n)}{\raisebox{1.29167pt}[0.0pt][0.0pt]{$\medspace\underline{\\!\leftrightarrow\\!}\medspace$}}_{P^{\varphi}_{\mathrm{col}}!}\overline{\mathcal{M}^{(\alpha,p^{\prime})}}_{(\sigma,n)}$,
and therefore, with the already obtained
$\overline{\mathcal{M}^{(\alpha,p^{\prime})}}_{(\sigma,n)}{\raisebox{1.29167pt}[0.0pt][0.0pt]{$\medspace\underline{\\!\leftrightarrow\\!}\medspace$}}_{P^{\varphi}_{\mathrm{col}}!}\overline{\mathcal{M}}_{(\sigma,n)}^{\alpha\land\beta}$,
we may infer that
$\overline{\mathcal{N}}_{(\tau,n)}{\raisebox{1.29167pt}[0.0pt][0.0pt]{$\medspace\underline{\\!\leftrightarrow\\!}\medspace$}}_{P^{\varphi}_{\mathrm{col}}!}\overline{\mathcal{M}}_{(\sigma,n)}^{\alpha\land\beta}$.
From that, $\overline{\mathcal{N}}_{(\tau,n)}\models\psi$ and Lemma 22 we now
obtain that for every $\beta\in{\mathcal{L}}_{\mathit{pl}}{}$,
$\overline{\mathcal{M}}_{(\sigma,n)}^{\alpha\land\beta}\models\psi$. Therefore
$\overline{\mathcal{M}}_{(\sigma,n)}\models[\alpha]\Box\psi$, as required.

Conversely, suppose that $\varphi^{\prime}\notin\sigma$. From Definition 16 it
follows that there is some $(x-1)$-consistent $\varphi$-pseudo-model
$\mathcal{N}=(\mathcal{S}^{\prime},\approx^{\prime},\mathcal{V}^{\prime})$
with $\tau\in\mathcal{S}^{\prime}$ and some $p\in P^{\varphi}_{\mathrm{hue}}$
such that
$\mathcal{N}_{\tau}{\raisebox{1.29167pt}[0.0pt][0.0pt]{$\medspace\underline{\\!\leftrightarrow\\!}\medspace$}}\mathcal{M}_{\sigma}^{(\alpha,p)}$
where $\psi\notin\tau$ (see Definition 15). As $D(\psi)\leq x-1$, from the
induction hypothesis $\mathbf{IH}_{\psi}$ we have that for all
$n\in\mathbb{N}^{+}$, $\overline{\mathcal{N}}_{(\tau,n)}\models\lnot\psi$.
From Lemma 25 we obtain that there is some
$\beta\in{\mathcal{L}}_{\mathit{pl}}{}$ such that
$\overline{\mathcal{M}^{(\alpha,p)}}_{(\sigma,n)}{\raisebox{1.29167pt}[0.0pt][0.0pt]{$\medspace\underline{\\!\leftrightarrow\\!}\medspace$}}_{P^{\varphi}_{\mathrm{col}}!}\overline{\mathcal{M}}_{(\sigma,n)}^{\alpha\land\beta}$,
and by Lemma 23 we have
$\overline{\mathcal{N}}_{(\tau,n)}{\raisebox{1.29167pt}[0.0pt][0.0pt]{$\medspace\underline{\\!\leftrightarrow\\!}\medspace$}}_{P^{\varphi}_{\mathrm{col}}!}\overline{\mathcal{M}^{(\alpha,p)}}_{(\sigma,n)}{\raisebox{1.29167pt}[0.0pt][0.0pt]{$\medspace\underline{\\!\leftrightarrow\\!}\medspace$}}_{P^{\varphi}_{\mathrm{col}}!}\overline{\mathcal{M}}_{(\sigma,n)}^{\alpha\wedge\beta}$.
Therefore, from Lemma 22 we have that for some $\beta$,
$\overline{\mathcal{M}}_{(\sigma,n)}^{\alpha\land\beta}\models\lnot\psi$, and
hence $\overline{\mathcal{M}}_{(\sigma,1)}\not\models[\alpha]\Box\psi$, as
required.

Now we turn to the opposite direction of our decidability proof: we are
required to show that every model can be projected to a consistent
$\varphi$-pseudo-model. The construction is as follows, where we first need to
introduce the auxiliary notion of ‘$\varphi$-image of a model’.

######  Definition 27.

Let $M=(S,\sim,V)$ be a model. A $0$-$\varphi$-projection of $M$ is a function
$\pi_{0}:S\longrightarrow\wp(cl_{0}(\varphi))$ where:

$\forall s\in S,\ \pi_{0}(s)=\\{\psi\in cl_{0}(\varphi)\ |\
M_{s}\models\psi\\}.$

For $0<n\leq D(\varphi)$, an $n$-$\varphi$-projection of $M$ is a function
$\pi_{n}:S\longrightarrow\wp(cl_{n}(\varphi))$ where there is an
$(n-1)$-$\varphi$-projection of $M$, $\pi_{n-1}$, and a mapping from a set of
fresh propositional atoms $P_{n}=\\{p_{i}^{n}\ |\ 0\leq
i<2^{2^{|cl_{n-1}(\varphi)|}}\\}$ to subsets of $cl_{n-1}(\varphi)$,
$\lambda:P_{n}\longrightarrow\wp(cl_{n-1}(\varphi))$, such that:

$\forall s\in S,\ \pi_{n}(s)=\pi_{n-1}(s)\cup\\{p\in P_{n}\ |\
\exists\psi\in{\mathcal{L}}_{\mathit{pl}}(P),\\{\pi_{n-1}(s)\
|M_{s}\models\psi\\}=\lambda(p)\\}.$

Let $P^{\varphi}_{\mathrm{col}}=\mathit{var}(\varphi)$ and
$P^{\varphi}_{\mathrm{hue}}=\bigcup_{n=0}^{D(\varphi)}P_{n}$. A
$n$-$\varphi$-image of $M$ is the $\varphi$-pseudo-model
$\mathcal{M}=(\mathcal{S},\approx,\mathcal{V})$ where:

  * •

$\mathcal{S}=\\{\pi_{n}(s)\ |\ s\in S\\}$ for some $n$-$\varphi$-projection of
$M$, $\pi_{D(\varphi)}$;

  * •

for $\sigma,\tau\in\mathcal{S}$, $\sigma\approx_{a}\tau$ iff for all
$K_{a}\psi\in cl(\varphi)$, it is the case that $K_{a}\psi\in\sigma$ iff
$K_{a}\psi\in\tau$;

  * •

for all $\sigma\in\mathcal{S}$, for all $\neg K_{a}\psi\in\sigma$, there is
some $\tau\in\mathcal{S}$ where $\tau\approx_{a}\sigma$ and $\neg\psi\in\tau$;

  * •

for all $p\in P^{\varphi}_{\mathrm{col}}\cup P^{\varphi}_{\mathrm{hue}}$, for
all $\sigma\in\mathcal{S}$, $\sigma\in\mathcal{V}(p)$ iff $p\in\sigma$; for
all $p\not\in P^{\varphi}_{\mathrm{col}}\cup P^{\varphi}_{\mathrm{hue}}$,
$\mathcal{V}(p)=\emptyset$.

Where $n=D(\varphi)$ we simply say $\varphi$-image, rather than
$n$-$\varphi$-image. $\dashv$

This is an intuitive definition where the $\varphi$-image of a model is the
$\varphi$-pseudo-model consisting of sets of formulas true at a state, along
with atomic propositions representing the Boolean announcements available at
that state.

The final lemma shows that the $\varphi$-image of a model is consistent.

######  Lemma 28.

The $\varphi$-image $\mathcal{M}=(\mathcal{S},\approx,\mathcal{V})$ of a model
$M=(S,\sim,V)$ is consistent. $\dashv$

###### Proof.

For $\varphi$-image $\mathcal{M}$ to be consistent we must first show that
$\mathcal{M}$ is a $\varphi$-pseudo-model (Definition 16). This follows
directly from the construction, noting that for the final two clauses of
Definition 13, the set of Boolean formulas used to define the denotation of
the atoms in Definition 27 will include all Boolean formulas over
$\mathit{var}(\varphi)$ and that these are closed under disjunctions and
conjunctions. We now show that $\mathcal{M}$ is consistent, by induction,
where the induction hypothesis is that for all models $M$, for all $x<n$, the
$x$-$\varphi$-image of $M$ is $x$-consistent. The base case of this induction
clearly holds, since all $\varphi$-pseudo-models are $0$-consistent. Now,
suppose that the induction hypothesis holds for $n-1$, we must show that the
$n$-$\varphi$-image $\mathcal{M}=(\mathcal{S},\approx,\mathcal{V})$ of $M$ is
$n$-consistent. To do this, we will show for every $\sigma\in\mathcal{S}$, for
every $[\alpha]\Box\varphi\in\sigma$ and for every $p\in
P^{\varphi}_{\mathrm{hue}}$, we can construct a $\alpha$-$p$-witness for
$\psi$ at $\mathcal{M}_{\sigma}$ (Definition 15). Since
$[\alpha]\Box\psi\in\sigma$, there must be some $s\in S$ where
$\pi_{D(\varphi)}(s)=\sigma$, and $M_{s}\models[\alpha]\Box\psi$. Given any
$\beta\in{\mathcal{L}}_{\mathit{pl}}{}$, it follows on condition that
$M_{s}\models\alpha\wedge\beta$, that $M_{s}^{\alpha\land\beta}\models\psi$.
By Definition 27, for every such $\beta$ there is some atom $p$ such that
$\mathcal{M}^{(\alpha,p)}_{\sigma}$ is bisimilar to a $(n-1)$-$\varphi$-image
of $M_{s}^{\alpha\land\beta}$. Let this $(n-1)$-$\varphi$-image of
$M_{s}^{\alpha\land\beta}$ be denoted
$\mathcal{M}^{\prime}_{\sigma^{\prime}}$. Assume that $\pi_{n}$ is the
$n$-$\varphi$-projection of $M$, and is defined with respect to the map
$\lambda_{n}$, and that $\pi^{\prime}_{n-1}$ is the
$(n-1)$-$\varphi$-projection of $M^{\alpha\land\beta}$ defined with respect to
the map $\lambda^{\prime}_{(n-1)}$, where for all
$p\in\mathit{var}^{*}(\varphi)$, if $\lambda_{n}(p)=\\{\pi_{n-1}(s)\mid s\in
S\\}$ then $\lambda^{\prime}_{(n-1)}(p)=\\{\pi_{n-1}(s)\mid s\in
S\cap{\mathcal{D}}(M^{\alpha\land\beta})\\}$. A bisimulation
$\mathfrak{R}\subseteq{\mathcal{D}}(\mathcal{M}^{(\alpha,p)})\times{\mathcal{D}}(\mathcal{M}^{\prime})$
between $\mathcal{M}^{(\alpha,p)}_{\sigma}$ and
$\mathcal{M}^{\prime}_{\sigma^{\prime}}$ is then defined by
$(\sigma,\tau)\in\mathfrak{R}$ if and only if for some $t\in S$,
$\pi_{n}(t)=\sigma$ and $\pi^{\prime}_{n-1}(t)=\tau$. Therefore,
$\mathcal{M}^{\prime}_{\sigma^{\prime}}$ is an adequate $\alpha$-$p$-witness
for $\psi$ at $\mathcal{M}_{\sigma}$, so it follows that $\mathcal{M}$ is
consistent.

######  Theorem 29.

The logic $\mathit{BAPAL}$ is decidable. $\dashv$

###### Proof.

This follows as we can enumerate all $\varphi$-pseudo-models (Lemma 17) and
test which of those models are consistent (Lemma 18). If a consistent
$\varphi$-pseudo-model contains a state $\sigma$ where $\varphi\in\sigma$,
from Lemma 26 it follows that $\varphi$ is satisfiable. Conversely, if
$\varphi$ is satisfiable, it follows from Lemma 28 that there is a consistent
$\varphi$-pseudo-model containing some state $\sigma$ where
$\varphi\in\sigma$.

##  5 Conclusions and further research

We have shown that $\mathit{BAPAL}$ has a decidable satisfiability problem,
although it does not have the finite model property. This is the first time a
quantified announcement logic has been shown to be decidable.

For further research we wish to report the decidability of the satisfiability
problem of yet another logic with quantification over announcements, called
positive arbitrary public announcement logic, $\mathit{APAL+}$. It has a
primitive modality “after every public announcement of a positive formula,
$\varphi$ is true.” The positive formulas correspond to the universal fragment
in first-order logic. These are the formulas where negations do not bind
modalities. It has been reported in [15], and the decidability of the
satisfiability problem remains to be shown.

## References

  * [1] T. Ågotnes, P. Balbiani, H. van Ditmarsch, and P. Seban.  Group announcement logic.  Journal of Applied Logic, 8:62–81, 2010.
  * [2] T. Ågotnes and H. van Ditmarsch.  Coalitions and announcements.  In Proc. of 7th AAMAS, pages 673–680. IFAAMAS, 2008.
  * [3] T. Ågotnes, H. van Ditmarsch, and T. French.  The undecidability of quantified announcements.  Studia Logica, 104(4):597–640, 2016.
  * [4] P. Balbiani, A. Baltag, H. van Ditmarsch, A. Herzig, T. Hoshi, and T. De Lima.  ‘Knowable’ as ‘known after an announcement’.  Review of Symbolic Logic, 1(3):305–334, 2008.
  * [5] Jon Barwise and Johan Van Benthem.  Interpolation, preservation, and pebble games.  The Journal of Symbolic Logic, 64(2):881–903, 1999.
  * [6] P. Blackburn, M. de Rijke, and Y. Venema.  Modal Logic.  Cambridge University Press, Cambridge, 2001.
  * [7] L. Bozzelli, H. van Ditmarsch, T. French, J. Hales, and S. Pinchinat.  Refinement modal logic.  Information and Computation, 239:303–339, 2014.
  * [8] T. Charrier and F. Schwarzentruber.  Arbitrary public announcement logic with mental programs.  In Proc. of AAMAS, pages 1471–1479. ACM, 2015.
  * [9] Melvin Fitting.  Tableau methods of proof for modal logics.  Notre Dame Journal of Formal Logic, 13(2):237–247, 1972.
  * [10] T. French and H. van Ditmarsch.  Undecidability for arbitrary public announcement logic.  In Advances in Modal Logic 7, pages 23–42. College Publications, 2008.
  * [11] R. Galimullin.  Coalition announcements.  PhD thesis, University of Nottingham, UK, 2019.
  * [12] J.D. Gerbrandy and W. Groeneveld.  Reasoning about information change.  Journal of Logic, Language, and Information, 6:147–169, 1997.
  * [13] J. Hales.  Arbitrary action model logic and action model synthesis.  In Proc. of 28th LICS, pages 253–262. IEEE, 2013.
  * [14] J.A. Plaza.  Logics of public communications.  In Proc. of the 4th ISMIS, pages 201–216. Oak Ridge National Laboratory, 1989.
  * [15] H. van Ditmarsch, T. French, and J. Hales.  Positive announcements.  Studia Logica, 2020.  https://doi.org/10.1007/s11225-020-09922-1, https://arxiv.org/abs/1803.01696.
  * [16] H. van Ditmarsch, W. van der Hoek, and L.B. Kuijer.  The undecidability of arbitrary arrow update logic.  Theor. Comput. Sci., 693:1–12, 2017.
  * [17] Hans van Ditmarsch and Tim French.  Quantifying over Boolean announcements.  Logical Methods in Computer Science, Volume 18, Issue 1, January 2022.
  * [18] Hans van Ditmarsch, Tim French, and Rustam Galimullin.  No finite model property for logics of quantified announcements.  In Proceedings of the 18th Conference on Theoretical Aspects of Rationality and Knowledge, TARK 2021, number 335 in Electronic Proceedings in Theoretical Computer Science, pages 129––138, 2021.