Almost APAL

Hans van Ditmarsch, Mo Liu, Louwe Kuijer, Igor Sedlar

► To cite this version:

Hans van Ditmarsch, Mo Liu, Louwe Kuijer, Igor Sedlar. Almost APAL. Journal of Logic and Com- putation, 2022, 33 (6), pp.1350-1378. 10.1093/logcom/exac012. hal-04238177

HAL Id: hal-04238177

https://hal.science/hal-04238177v1

Submitted on 12 Oct 2023

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
# Almost APAL

HANS VAN DITMARSCH, *Open University, the Netherlands, PO Box 2960, 6401 DL Heerlen, Netherlands*.

E-mail: hans.vanditmarsch@ou.nl

MO LIU, *CNRS, LORIA, University of Lorraine, BP 239 54506 Vandoeuvre-lès-Nancy, France*.

E-mail: mo.liu@loria.fr

LOUWE B. KUIJER, *University of Liverpool, Ashton Street Liverpool, L69 3BX, United Kingdom*.

E-mail: lbkuijer@liverpool.ac.uk

IGOR SEDLAR, *Institute of Computer Science, Czech Academy of Sciences, Pod Vodárenskou věži 27/1/2 182 07 Praha 8, Czech Republic*.

E-mail: sedlar@cs.cas.cz

## Abstract

Arbitrary public announcement logic (APAL) is a logic of change of knowledge with modalities representing quantification over announcements. We present two rather different versions of APAL wherein this quantification is restricted to formulas only containing a subset of all propositional variables: SAPAL and SCAPAL. Such restrictions are relevant in principle for the specification of multi-agent system dynamics. We also present another version of APAL, quantifying over all announcements implied by or implying a given formula: IPAL. We then determine the relative expressivity of all these logics and APAL. We also present complete axiomatizations of SAPAL and SCAPAL and show undecidability of satisfiability for all logics involved, by arguments nearly identical to those for APAL. We show that the IPAL quantifier, motivated by the satisfaction clause for substructural implication, yields a new substructural dynamic consequence relation.

**Keywords:** APAL, quantification over announcements, substructural logic, expressivity

## 1 Introduction

The modal logic of knowledge was originally proposed to give a relational semantics for the perceived properties of knowledge, such as that what you know is true, and that you know what you know, and to contrast this with the properties of other epistemic notions such as belief [27]. Already in [27] the analysis of paradoxical phenomena that you cannot be informed of factual ignorance while ‘losing’ that ignorance, the so-called Moorean phenomena [33], played an important role. On the heels of the logic of (single agent) knowledge came the multi-agent logics of knowledge, wherein similar phenomena are not so paradoxical: there is no issue with my knowledge of your ignorance. This led on the one hand to the development of group epistemic notions such as common knowledge [6, 32] and distributed knowledge [26], topics that we will bypass in this contribution. On the other hand this led to increased interest in the analysis of multiple agents informing each other of their ignorance and knowledge, often inspired by logic puzzles [32, 34]. This culminated in Plaza’s public announcement logic (PAL) [36], wherein such informative actions became full members of the logical language besides the knowledge modalities; parallel developments of dynamic but not epistemic logics of information change are [43, 50].

Vol. 33, No. 6, © The Author(s) 2022. Published by Oxford University Press.

This is an Open Access article distributed under the terms of the Creative Commons Attribution License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted reuse, distribution, and reproduction in any medium, provided the original work is properly cited.

Advance Access Publication on 11 March 2022 https://doi.org/10.1093/logcom/exac012
The logic PAL contains a dynamic operator representing the consequences of information change that is similarly observed by all agents, the so-called public (and truthful) announcement. We let [ψ]φ stand for ‘after truthful public announcement of ψ, φ (is true)’. Every PAL formula is equivalent to a formula without public announcements, so that PAL is as expressive as epistemic logic EL (a.k.a. the logic S5) [36].

From PAL there were various directions for further generalization. One could consider public announcements in the presence of group epistemic operators such as common knowledge, or non-public information change such as private or secret announcements to some agents while other agents do not or only partially observe that. Both were simultaneously realized in action model logic [10]; parallel, now lesser known, developments are [23].

A different direction of generalizing PAL is to consider quantifying over announcements. Arbitrary public announcement logic APAL was proposed in [8] and contains a construct [!]φ standing for ‘after any truthful public announcement, φ (is true)’, i.e. for all ψ, [ψ]φ. In order to avoid circularity, the APAL quantifier is only over announcements not containing [!] modalities. There is an infinitary (not RE) axiomatization for the logic [9], where an open question remains whether there is a finitary (RE) axiomatization. APAL is undecidable [20], and the complexity of model checking is PSPACE-complete [1]. There are versions of APAL with finitary axiomatizations or decidable satisfiability problems [11, 17, 46], or that model aspects of agency [1, 2, 22]. APAL is more expressive than PAL [8]. The relative expressivity of versions of APAL is rather intricate, and most relevant in view of potential applications. For example, group announcement logic GAL and APAL are incomparable in expressivity [22], and in GAL we can formalize goal reachability in finite two-principal security protocols [1].

In this contribution we investigate some novel versions of APAL. If we quantify over announcements only using atoms in subsets $Q \subseteq P$ we obtain the logic SAPAL, and if these subsets are required to be *finite* we get FSAPAL. If we quantify over announcements only using atoms occurring in the formula under the *scope* of the quantifier, we obtain the logic SCAPAL. If we quantify over announcements *implying* a given formula $\psi$ or *implied by* a given formula $\psi$ and if such $\psi$ may also contain quantifiers we obtain logic QIPAL and if they are not allowed to contain quantifiers we obtain IPAL.

Note that there is a strong, but not well-known, relation between quantification over public announcements and epistemic planning [15]. In the latter, we wish to satisfy some epistemic goal φ by finding a sequence of actions, which could be public announcements, successively transforming multi-agent models for the system until ultimately leading to a model satisfying goal φ. In the former, we wish to satisfy (¡)φ (for ‘there is an announcement, or a sequence of announcements, after which φ’) by finding a sequence of announcements (successively transforming multi-agent models) after which φ. In both, undecidability can only be tamed by restricting what can be announced. The way to obtain decidability in epistemic planning is often to restrict the number of actions [5, 16]. This goes beyond merely restricting the number of atoms. Such an action may have a precondition of certain modal depth. But therefore, we no longer quantify over arbitrary modal depth as in the APAL versions considered here, but over bounded modal depth.

The common factor in each of the APAL variants considered in this paper is that they restrict the domain of quantification to certain formulas that are considered relevant or permissible in some context. In APAL, [!]φ means that φ holds after any truthful public announcement, including announcements that are completely irrelevant to the matter at hand. While it may be fun to read about Sherlock Holmes determining the identity of the killer based on, say, the weather in Berlin three days ago, such (seemingly) irrelevant announcements are not very useful in practice. Each of the variants under consideration here tries to solve this ‘irrelevant announcements’ problem in some way.
For SAPAL and FSAPAL, whenever we use an arbitrary announcement operator, we need to specify the relevant domain of discourse $Q \subseteq P$ for that operator. We then consider only those announcements that are considered relevant by virtue of pertaining to this domain of discourse. Think of an expert witness who is only allowed to opine on matters within their area of expertise. For a more technical example, suppose that we want to allow users to query a database in limited ways, while keeping a certain fact $p$ secret. One way to do this is to allow queries only about domain $Q$. We can then verify that $p$ remains unknown after the answer to the query is given by checking that $[Q](\neg Kp \wedge \neg K\neg p)$ holds.

More generally, when modelling dynamics of a multi-agent system it is often the case that the vocabulary is finite. In particular, often only a finite number of atomic propositions are considered relevant for each given subtask of a problem to solve, where this vocabulary might vary between subtasks. In such cases, FSAPAL might be more suitable modelling tools than ‘generic’ APAL. For example, consider distributed systems wherein agents may communicate about their own local state value [29]. Similarly, in gossip protocols [28], the protocols wherein agents merely exchange their secrets are less powerful than those wherein they are permitted to exchange other information, such as who they previously communicated with [18, 25].

In SCAPAL we also restrict announcements to some domain of discourse, but instead of adding this domain as a parameter to the operator, we consider a propositional variable $p$ to be in the domain of discourse if it occurs inside the scope of the announcement operator. This is not always a good idea; in the database query example above, the secret $p$ should definitely not be in the domain $Q$ of queries. The assumption that variables are relevant because they appear in the scope does make sense in a conversational context, however, if we are debating the truth of $\varphi$, then announcements regarding the truth of any variable that occurs in $\varphi$ are clearly relevant.

In IPAL, we do not restrict the domain of discourse, but instead limit (from below or above) how informative the announcement must be. An announcement $[\psi]$ eliminates all $\neg \psi$ states from consideration. As such, if $\chi$ is implied by $\psi$, and therefore holds at least on every state where $\psi$ holds, then $[\chi]$ is at most as informative as $[\psi]$. Likewise, if $\xi$ implies $\psi$ then $[\xi]$ is at least as informative as $[\psi]$. Like SAPAL and FAPAL, this has applications in security protocols, where communications by principals need to satisfy information goals towards other principals as well as safety goals against eavesdroppers and other intruders [31, 37]. In such protocols, we may wonder whether it is possible to be at least as informative as $\psi$ while not giving eavesdropper $e$ knowledge of $p$, represented by the formula $\langle\psi^{\downarrow}\rangle(\neg K_e p \wedge \neg K_e \neg p)$, or whether every communication at most as informative as $\psi$ is safe, represented by the formula $[\psi^{\uparrow}](\neg K_e p \wedge \neg K_e \neg p)$.

IPAL can also be useful in situations where disclosing certain information is required (by law, by company policy or simply by social obligation), but disclosing more than the strict requirement is possible. Or, of course, in situations where disclosing certain information is forbidden.

For IPAL we were additionally motivated by the dynamic consequence relation based on PAL proposed in [44], and how the IPAL quantification (that like the PAL announcement is parametrized with a formula) can be seen as the condition for a substructural implication. See Section 7 for more details.

In addition to these applications, we were also originally motivated by the search for ‘tameable’ versions of APAL. Ideally, a ‘tame’ version of APAL would be decidable. Or, if not decidable, we could hope for a logic that is at least recursively enumerable (RE), and that therefore admits a finitary axiomatization. The reason that APAL is so poorly behaved is that its distinctive $[!]$ operator is extremely powerful. The corresponding operators $[Q]$ and $[\subseteq]$ in FSAPAL and SCAPAL intuitively seem less powerful, suggesting that these logics might be tameable. Unfortunately, this turns out not to be the case. A pretty minor modification to the undecidability proof for APAL shows that FSAPAL and SCAPAL are undecidable, see Section 5. Even so, we hoped that the smaller domain of
<figure><img src="image_2.png" /><figcaption>FIGURE 1. Expressivity hierarchy of logics presented in this work. An arrow means larger expressivity. Assume transitivity. Absence of an arrow means incomparability.</figcaption></figure>

quantification would allow for a finitary axiomatization. While the domain of quantification for the arbitrary announcement operators in FSAPAL and SCAPAL is still infinite, and naive introduction rules for [Q] and [⊆] are therefore infinitary, we had hoped to find introduction axioms for [Q] and [⊆] using a finite (but unbounded) subset of the domain. There, too, we were frustrated, however; while we do present axiomatizations in Section 6 these use an infinitary introduction rule, similar to the corresponding rule in APAL.

In fact, even the intuition that [Q] and [⊆] are less powerful than [!] turns out to be only partially true. The domain of quantification of [Q] and [⊆] is smaller than that of [!], and, as a result, there are properties that can be expressed in APAL but not in FSAPAL or SCAPAL. But the smaller domain of quantification can also be used to express things in FSAPAL and SCAPAL that are unexpressible in APAL, see Section 4. So the expressive power of FSAPAL and SCAPAL is incomparable to, as opposed to strictly lower than, that of APAL.

With regard to SAPAL and IPAL, since it is possible to embed APAL in either of these logics, they are trivially at least as expressive as APAL, and their satisfiability problem is at least as hard as that of APAL. In Section 4 we show that both are in fact strictly more expressive than APAL.

So we did not strike gold in our search for tameable variants of APAL. Still, keeping in mind the applications discussed above, we argue that these logics are interesting in their own right. The expressivity results, which we consider the principal focus of our contribution, give a thorough overview of how these various attempts to limit the arbitrary announcement quantifier to some kind of relevant domain compare to each other. These results we consider of interest and non-trivial, so perhaps we did strike silver. Furthermore, that FSAPAL and SCAPAL are not tameable is a result in itself.

In Section 2 we introduce the syntax and semantics. In Section 3 we prove some modal properties of these quantifiers. Section 4 determines the expressivity hierarchy for the reported logics. It is shown in Figure 1. Let $<$ mean ‘strictly less expressive’ and $\asymp$ ‘incomparable’, then the results are that PAL is strictly less expressive than any of the logics with quantifiers, and that SCAPAL $<$ FSAPAL, APAL $\asymp$ SCAPAL, APAL $\asymp$ FSAPAL, IPAL $\asymp$ SCAPAL, IPAL $\asymp$ FSAPAL and APAL $<$ IPAL. Section 5 shows the undecidability of satisfiability of our APAL versions, and Section 6 provides complete axiomatizations for SAPAL and SCAPAL; these are similar to that for APAL. We conclude with Section 7 reinterpreting dynamic consequence in the IPAL setting.

## 2 Syntax and semantics: SAPAL, SCAPAL, QIPAL

Throughout this contribution, let a countable set *P* of propositional atoms and a finite set *A* of agents be given.

DEFINITION 2.1
(Language).
The logical language $\mathcal{L}$ is defined inductively as:

$$ \varphi ::= \top | p | \neg \varphi | (\varphi \land \varphi) | K_a \varphi | [\varphi] \varphi | [!] \varphi | [Q] \varphi | [\subseteq] \varphi | [\varphi \downarrow] \varphi | [\varphi \uparrow] \varphi $$

where $p \in P$, $a \in A$ and $Q \subseteq P$. The propositional sublanguage is $\mathcal{L}_{PL}$, with additionally the modalities $K_a$ we get the epistemic formulas $\mathcal{L}_{EL}$, with additionally the construct $[\varphi] \varphi$ it is $\mathcal{L}_{PAL}$, and adding one of the quantifiers $[!]$, $[Q]$, $[\subseteq]$, $[\varphi \downarrow] \psi$ and $[\varphi \uparrow] \psi$ we obtain, respectively, $\mathcal{L}_{APAL}$, $\mathcal{L}_{SAPAL}$ and $\mathcal{L}_{SCAPAL}$, $\mathcal{L}_{QIPAL \downarrow}$ and $\mathcal{L}_{QIPAL \uparrow}$. Adding both $[\varphi \downarrow] \psi$ and $[\varphi \uparrow] \psi$ we obtain $\mathcal{L}_{QIPAL}$, and if the $\varphi$ in $[\varphi \downarrow] \psi$ and $[\varphi \uparrow] \psi$ is restricted to $\mathcal{L}_{PAL}$, we get $\mathcal{L}_{IPAL}$. If the $Q$ in $[Q] \varphi$ are (always) finite we get $\mathcal{L}_{FSAPAL}$.

The meaning of all constructs will be explained after defining the semantics. The dual modalities for $[!]$, $[Q]$, $[\subseteq]$, $[\varphi \downarrow]$, and $[\varphi \uparrow]$ are, respectively, $\langle!\rangle$, $\langle Q \rangle$, $\langle \subseteq \rangle$, $\langle \varphi \downarrow \rangle$, and $\langle \varphi \uparrow \rangle$. Instead of $\varphi \in \mathcal{L}_X$ we also say that $\varphi$ is an $X$ formula. For any language $\mathcal{L}$, $\mathcal{L}|Q$ is the sublanguage only containing atoms in $Q \subseteq P$. Given $\varphi \in \mathcal{L}$, $P(\varphi)$ denotes the set of atoms occurring in $\varphi$. For $\{p_1, \dots, p_n\} \varphi$ we may write $[p_1 \dots p_n] \varphi$. The modal depth $d(\varphi)$ of a formula is the maximum stack of epistemic modalities; it is defined as: $d(\bot) = d(p) = 0$, $d(\varphi \land \psi) = \max\{d(\varphi), d(\psi)\}$, $d(K_a \varphi) = d(\varphi) + 1$, $d([\varphi] \psi) = d([\varphi \downarrow] \psi) = d([\varphi \uparrow] \psi) = d(\varphi) + d(\psi)$, and $d([!] \varphi) = d([\subseteq] \varphi) = d([Q] \varphi) = d(\neg \varphi) = d(\varphi)$.

We let $\Gamma$, $\Sigma$ and $\Delta$ denote finite sequences of formulas, where $(\Gamma, \Delta)$ denotes the concatenation of sequences (the parentheses are often omitted), and $|\Gamma|$ the length of a sequence. By induction on the length of $\Gamma$ (and where $\varphi, \psi$ are formulas) we define $[\Gamma]\varphi := \varphi$ when $|\Gamma| = 0$, and $[\psi, \Gamma]\varphi := [\psi][\Gamma]\varphi$ when $|\psi, \Gamma| = n+1$; similarly, $[\Gamma \downarrow]\varphi := \varphi$ when $|\Gamma| = 0$, and $[(\psi, \Gamma) \downarrow]\varphi := [\psi \downarrow][\Gamma \downarrow]\varphi$ when $|\psi, \Gamma| = n+1$.

## DEFINITION 2.2

(Structures).

An epistemic model (or *model*) is a triple $M = (S, \sim, V)$ where $S$ is a domain of states, $\sim$ is a set of binary relations $\sim_a \subseteq S \times S$ that are all equivalence relations, and $V : P \to \mathcal{P}(S)$ maps each atom $p \in P$ to its denotation $V(p)$.

Given a model $M$, we may refer to its domain, relations and valuation as $S^M$, $\sim_a^M$ and $V^M$, respectively, and we also refer to the domain of $M$ as $D(M)$. Bisimulation to compare models will be defined later. A model $N$ is a *submodel* of $M$, notation $N \subseteq M$, if $S^N \subseteq S^M$, for all $a \in A$, $\sim_a^N = \sim_a^M \cap (S^N \times S^M)$, and for all $p \in P$, $V^N(p) = V^M(p) \cap S^N$.

## DEFINITION 2.3

(Semantics).

Given model $M = (S, \sim, V)$, $s \in S$ and $\varphi \in \mathcal{L}$ we inductively define $M, s \models \varphi$ ($\varphi$ is true in state $s$ of model $M$) as:

$$
\begin{array}{lclcl}
M, s \models p & \text{iff} & s \in V(p) & & \\
M, s \models \neg \varphi & \text{iff} & M, s \models \varphi & & \\
M, s \models \varphi \land \psi & \text{iff} & M, s \models \varphi \text{ and } M, s \models \psi & & \\
M, s \models K_a \varphi & \text{iff} & \text{for all } t \in S, s \sim_a t \text{ implies } M, t \models \varphi & & \\
M, s \models [\psi] \varphi & \text{iff} & M, s \models \psi \text{ implies } M|\psi, s \models \varphi & & \\
M, s \models [!] \varphi & \text{iff} & \text{for any } \psi \in \mathcal{L}_{PAL} : M, s \models [\psi] \varphi & & \\
M, s \models [Q] \varphi & \text{iff} & \text{for any } \psi \in \mathcal{L}_{PAL} | Q M, s \models [\psi] \varphi & & \\
M, s \models [\subseteq] \varphi & \text{iff} & \text{for any } \psi \in \mathcal{L}_{PAL} | P(\varphi) : M, s \models [\psi] \varphi & & \\
M, s \models [\chi \downarrow] \varphi & \text{iff} & \text{for any } \psi \in \mathcal{L}_{PAL} \text{ implying } \chi : M, s \models [\psi] \varphi & & \\
M, s \models [\chi \uparrow] \varphi & \text{iff} & \text{for any } \psi \in \mathcal{L}_{PAL} \text{ implied by } \chi : M, s \models [\psi] \varphi & &
\end{array}
$$
where $M|\varphi = (S', \sim', V')$ is such that $S' = [[\varphi]]_M = \{s \in S \mid M, s \models \varphi\}, \sim'_a = \sim_a \cap ([[\varphi]]_M \times [[\varphi]]_M)$, and $V'(p) = V(p) \cap [[\varphi]]_M$.

A formula $\varphi$ is valid on model $M$, notation $M \models \varphi$, iff for all $s \in S$, $M, s \models \varphi$ and $\varphi$ is valid, notation $\models \varphi$, iff $\varphi$ is valid on all models $M$. A formula $\varphi$ is a distinguishing formula of a subset $S' \subseteq S$ of $M$ (or $S'$ is definable by $\varphi$) if for all $t \in S'$, $M, t \models \varphi$ and for all $t \notin S'$, $M, t \not\models \varphi$.

In the dual existential reading of the semantics of the quantifiers, the $\psi$ in 'there is a $\psi \in \mathcal{L}_{PAL}'$ is the witness of the quantifier. In the semantics of the last two, '$\psi$ implies $\chi$' means $\models \psi \rightarrow \chi$ and '$\psi$ is implied by $\chi$' means $\models \chi \rightarrow \psi$.

**PAL and APAL** *Public announcement logic PAL and arbitrary public announcement logic APAL* were already introduced.

**SAPAL and FSAPAL** The logic with construct $[Q]\varphi$, for 'after any announcement only containing atoms in $Q \subseteq P'$, is called SAPAL, for APAL with quantification over formulas restricted to *subsets* of variables. If those subsets are required to be *finite* we get FSAPAL.

**SCAPAL** The logic with construct $[\subseteq]\varphi$, for 'after any announcement only containing atoms occurring in $\varphi'$, is called SCAPAL (where $\varphi$ is the formula under the *scope* of the quantifier $[\subseteq]$).

**QIPAL** The logic with constructs $[\psi\downarrow]\varphi$ and $[\psi\uparrow]\varphi$ is called QIPAL, where $[\psi\downarrow]\varphi$ stands for 'after every announcement implying $\psi$, $\varphi$ is true', and $[\psi\uparrow]\varphi$ stands for 'after every announcement implied by $\psi$, $\varphi$ is true'. In QIPAL we can reason over restrictions of a given model $M$ that are submodels of $M|\psi$, or over restrictions that contain $M|\psi$ as a submodel.

**Bisimulation** We define several notions of bisimulation between models and obtain some elementary invariance results for our logics. They will be used much in the expressivity Section 4.

**DEFINITION 2.4**

(Bisimulation).

Let $M$ and $N$ be epistemic models. A non-empty relation $Z \subseteq S^M \times S^N$ is a *bisimulation* between $M$ and $N$ if for all $Zst, p \in P$ and $a \in A$:

- **atoms**: $s \in V^M(p)$ iff $t \in V^N(p)$.

- **forth**: if $s \sim_a^M s'$, then there is a $t' \in S^N$ such that $t \sim_a^N t'$ and $Zs't'$.

- **back**: if $t \sim_a^N t'$, then there is a $s' \in S^M$ such that $s \sim_a^M s'$ and $Zs't'$.

If there exists a bisimulation $Z$ between $M$ and $N$ we write $M \unfrown N$, to indicate the relation), and if it contains pair $(s,t)$, we write $(M,s) \unfrown (N,t)$. If the **atoms** clause is only satisfied for atoms $Q \subseteq P$, we write $M \unfrown^Q N$ and $Z$ is called a **Q-bisimulation** or a (**Q-**restricted bisimulation).

**DEFINITION 2.5**

(Bounded bisimulation).

Let $M$ and $N$ be epistemic models. For $n \in \mathbb{N}$ we define a sequence $Z^0 \supseteq \dots \supseteq Z^n$ of relations on $S^M \times S^N$.

A non-empty relation $Z^0$ is a 0-bisimulation if for all $Z^0st$ and $p \in P$:

- **atoms**: $s \in V^M(p)$ iff $t \in V^N(p)$.

A non-empty relation $Z^{n+1}$ is an $(n+1)$-bisimulation if for all $Z^{n+1}st, a \in A$:

- **$(n+1)$-forth**: if $s \sim_a^M s'$, then there is a $t' \in S^N$ s.t. $t \sim_a^N t'$ and $Z^{n}s't'$.

- **$(n+1)$-back**: if $t \sim_a^N t'$, then there is a $s' \in S^M$ s.t. $s \sim_a^M s'$ and $Z^{n}s't'$.

If there exists a *n*-bisimulation $Z^n$ between $M$ and $N$ we write $M \unfrown^n N$. (We also combine the notations $\unfrown^Q$ and $\unfrown^n$ in the obvious way, writing $\unfrown^{Q,n}$.)
Given pointed models $(M,s)$ and $(N,t)$ and a logic $L$ with language $\mathcal{L}_L$, $(M,s) \equiv_L (N,t)$ (for ‘$(M,s)$ and $(N,t)$ are modally equivalent’) denotes: for all $\varphi \in \mathcal{L}_L$, $M,s \models \varphi$ iff $N,t \models \varphi$. Given $Q \subseteq P$ and $n \in \mathbb{N}$, annotations $\equiv_L^n$ and $\equiv_L^Q$ restrict the evaluated formulas $\varphi \in \mathcal{L}_L$ to those of modal depth $d(\varphi) \le n$ and (resp.) to $\varphi \in \mathcal{L}_L|Q$. APAL is invariant for bisimilarity, but not for restricted bisimilarity or bounded bisimilarity: $(M,s) \unfrown (N,t)$ implies $(M,s) \equiv_{APAL} (N,t)$, whereas $(M,s) \unfrown^n (N,t)$ may not imply $(M,s) \equiv_{APAL}^n (N,t)$, and $(M,s) \unfrown^Q (N,t)$ may not imply $(M,s) \equiv_{APAL}^Q (N,t)$ [8, 47]. This is because the APAL modality [!] implicitly quantifies over formulas of arbitrarily large modal depth and over infinitely many atoms. All logics we consider in this paper are invariant for bisimilarity.

**LEMMA 2.6**

For any $L$ considered, $(M,s) \unfrown (N,t)$ implies $(M,s) \equiv_L (N,t)$.

**PROOF.** For $L = EL$, PAL, this is known from the literature [14] for EL, and for PAL because EL and PAL are equally expressive [36]. For the other logics, let us for example consider SAPAL; the proof for all remaining logics is similar. By induction on the structure of $\varphi$ we show that

For all $\varphi \in \mathcal{L}_{SAPAL}$ and for all pointed models $(M,s), (N,t)$:

$(M,s) \unfrown (N,t)$ implies $M,s \models \varphi$ iff $N,t \models \varphi$.

All inductive cases are elementary except ‘public announcement’ and ‘quantifier’.

**Case quantifier**

$M,s \models [Q]\psi$, iff $M,s \models [\varphi]\psi$ for all $\varphi \in \mathcal{L}_{PAL}|Q$, iff $M,s \models \varphi$ implies $M|\varphi,s \models \psi$ for all $\varphi \in \mathcal{L}_{PAL}|Q$, iff (*) $N,t \models \varphi$ implies $M|\varphi,s \models \psi$ for all $\varphi \in \mathcal{L}_{PAL}|Q$, iff (**) $N,t \models \varphi$ implies $N|\varphi,t \models \psi$ for all $\varphi \in \mathcal{L}_{PAL}|Q$, iff $N,t \models [\varphi]\psi$ for all $\varphi \in \mathcal{L}_{PAL}|Q$, iff $N,t \models [Q]\psi$.

(*): By bisimulation invariance of PAL, we obtain $M,s \models \varphi$ iff $N,t \models \varphi$.

(**): Let $Z : (M,s) \unfrown (N,t)$

Define $Z'$ between $M|\varphi$ and $N|\varphi$ as follows: $Z'uv$ iff (Zuv and $M,u \models \varphi$). By bisimulation invariance for $\varphi \in \mathcal{L}_{PAL}$ it follows that also $N,v \models \varphi$, so that $Z'$ is indeed a relation between $M|\varphi$ and $N|\varphi$. We now show that $Z' : (M|\varphi,s) \unfrown (N|\varphi,t)$.

$(N|\varphi,t)$. The clause **atoms** is obviously satisfied. Concerning **forth** for some agent $a$, take any pair $(v, v')$ such that $Z'vv'$ and let $u$ in the domain of $M|\varphi$ be such that $v \sim_a u$. As $u$ is in the domain of $M|\varphi$, $M,u \models \varphi$. From $Z'vv'$ follows $Zvv'$. As $v \sim_a u$ in $M|\varphi$, also $v \sim_a u$ in $M$. From $Zvv'$, $v \sim_a u$ in $M$, and **forth** (for $Z$) it follows that there is $u'$ in the domain of $N$ such that $Zuu'$ and $v' \sim_a u'$. From $Zuu'$, $M,u \models \varphi$, and bisimulation invariance for $\varphi \in \mathcal{L}_{PAL}$ it follows that $N,u' \models \varphi$, i.e., $u'$ is also in the domain of $N|\varphi$. From $Zuu'$, $M,u \models \varphi$, and the fact the $u'$ is in the domain of $M|\varphi$ it follows that $Z'uu'$, as required. This proves **forth**. The step **back** is shown similarly. Note that in particular $Z'st$.

This therefore establishes that $Z' : (M|\varphi,s) \unfrown (N|\varphi,t)$,

$(N|\varphi,t)$, so that by definition $(M|\varphi,s) \unfrown (N|\varphi,t)$.

By induction for $\psi$ it now follows that $M|\varphi,s \models \psi$ iff $N|\varphi,t \models \psi$, as desired.

**Case public announcement**

The case public announcement, wherein we show that $M,s \models [\varphi]\psi$ iff $N,t \models [\varphi]\psi$, is shown fairly similarly to the case quantifier, except that in step (*) we do not use bisimulation invariance for $\varphi \in \mathcal{L}_{PAL}$ but we use the inductive hypothesis for $\varphi \in \mathcal{L}_{SAPAL}$, and similarly on two occasions in step (**). $\square$

**COROLLARY 2.7**

Let $\varphi \in \mathcal{L}_L$ and $M,s \models \varphi$. Then $(M,s) \unfrown (N,t)$ implies $(M|\varphi,s) \unfrown (N|\varphi,t)$.
EL is also invariant under bounded bisimulation, with bound equal to the formula's modal depth. As every PAL formula is equivalent to an EL formula with equal modal depth (this is a special case of the translation introduced in [10]), it follows that PAL is similarly invariant. As we use a virtually identical result in subsequent proofs, we give a full proof here.

**LEMMA 2.8**

Let $n \in \mathbb{N}$ and $\varphi \in \mathcal{L}_{PAL}$ with $d(\varphi) = k \le n$, models $(M,s)$ and $(N,t)$, and $M,s \models \varphi$ be given. If $(M,s) \unfrown^n(N,t)$, then $(M|\varphi,s) \unfrown^{n-k}(N|\varphi,t)$.

**PROOF.** Let $Z^0 \supseteq \dots \supseteq Z^n$ be such that $Z^0 : (M,s) \unfrown^0(N,t)$, ..., $Z^n : (M,s) \unfrown^n(N,t)$. For all $i=0, \dots, n-k$, let $Z_\varphi^i : \mathcal{D}(M) \to \mathcal{D}(N)$ be defined as: $Z_\varphi^i \text{st}$ iff $Z^{i+k} \text{st}$ and $M,s \models \varphi$. As $d(\varphi) \le n$, from $n$-bisimulation invariance for PAL and $M,s \models \varphi$ also follows that $N,t \models \varphi$.

By natural induction on $n-k$ we show that $Z^n : (M,s) \unfrown^n(N,t)$ implies $Z_\varphi^{n-k}$ : $(M|\varphi,s) \unfrown^{n-k}(N|\varphi,t)$, from which the required follows.

Case $n-k=0$. We show **atoms**. We have that $Z_\varphi^0 \text{st}$ iff $Z^k \text{st}$, where the latter follows from $Z^k \supseteq Z^n$ and $Z^n \text{st}$. Therefore, $Z_\varphi^0 : (M|\varphi,s) \unfrown^0(N|\varphi,t)$.

Case $n-k > 0$. We show $(n-k)$-**forth**. Let $s \sim_a s'$ and $M,s' \models \varphi$, i.e., $s \sim_a s'$ in $M|\varphi$. From $Z^n : (M,s) \unfrown^n(N,t)$ and $s \sim_a s'$ follows that there is a $t' \sim_a t$ such that $Z^{n-1} : (M,s') \unfrown^{n-1}(N,t')$. As $n-k = n-d(\varphi) > 0$, $d(\varphi) < n$, so $d(\varphi) \le n-1$. From $Z^{n-1} : (M,s') \unfrown^{n-1}(N,t')$, $M,s' \models \varphi$ and $d(\varphi) \le n-1$ it follows by bisimulation invariance that $N,t' \models \varphi$. Therefore $t'$ is in the domain of $N|\varphi$. By induction, from $Z^{n-1} : (M,s') \unfrown^{n-1}(N,t')$ it follows that $Z_\varphi^{n-k-1} : (M|\varphi,s') \unfrown^{n-k-1}(N|\varphi,t')$. Therefore, $t'$ satisfies the requirement for $(n-k)$-**forth** for relation $Z_\varphi^{n-k}$.

The clause $(n-k)$-**back** is shown similarly. $\square$

<figure><img src="image_3.png" /></figure>

**PROPOSITION 2.9**

$(M,s) \unfrown^Q(N,t)$ implies $(M,s) \equiv_{SAPAL}^Q (N,t)$ and $(M,s) \equiv_{SCAPAL}^Q (N,t)$.

**PROOF.** The proof is by induction on formulas true in $(M,s)$. The crucial case quantifier is satisfied because (let $R \subseteq Q$): $M,s \models [R]\varphi$, iff $M,s \models [\psi]\varphi$ for all $\psi \in \mathcal{L}_{PAL}|R$, iff for all $\psi \in \mathcal{L}_{PAL}|R$, $M,s \models \psi$ implies $M|\psi,s \models \varphi$, iff (induction, Cor. 2.7) for all $\psi \in \mathcal{L}_{PAL}|R$, $N,s \models \psi$ implies $N|\psi,s \models \varphi$, iff (...) $N,s \models [R]\varphi$.

The proof for SCAPAL is similar. $\square$

<figure><img src="image_4.png" /></figure>

# 3 Modal properties of the quantifiers

We continue by discussing some peculiarities of the semantics, where we focus on modal properties of the quantifiers. We recall that APAL satisfies: $[!]\varphi \rightarrow \varphi$ (T), $[!]\varphi \rightarrow [!]![]\varphi$ (4), $\langle!\rangle[!]\varphi \rightarrow [!]\langle!\rangle\varphi$ (CR), and $[!]\langle!\rangle\varphi \rightarrow \langle!\rangle[!]\varphi$ (MK) [8, 47].

It may be useful to briefly consider the intuition behind these validities. The principle (T) is valid in APAL because if $\varphi$ is true after every announcement, then in particular it is true after the uninformative announcement $[\top]$. So $[!]\varphi$ implies $[\top]\varphi$, which is in turn equivalent to $\varphi$. Validity of (4) is most easily seen in its dual form $\langle!\rangle\langle!\rangle\varphi \rightarrow \langle!\rangle\varphi$; if $\langle!\rangle\langle!\rangle\varphi$ holds, then there are two announcements $\psi$ and $\chi$ that, if announced after each other, will make $\varphi$ true. The single announcement $\psi \wedge \langle\psi\rangle\chi$ (informally: ' $\psi$ is true, and now $\chi$ is true as well') has the same effect as announcing $\psi$ and $\chi$ sequentially, so $\langle!\rangle\varphi$ holds as well.

The properties (CR) and (MK) can be thought of as describing winning strategies when two players make one announcement each, with player one trying to make $\varphi$ true and player two trying to make it false. Then (CR) states that if player one has a winning strategy when they make the first
announcement, then they also have a winning strategy when they make the second announcement. Conversely, (MK) states that if player one can win when moving second, they can also win when they go first. The validity of these properties in APAL follows from the existence of a 'most informative announcement' with respect to a given formula $\varphi$, that is available to either player. So player one has a winning strategy if and only if this specific announcement makes $\varphi$ true.

### 3.1 SAPAL and FSAPAL

The logic SAPAL generalizes APAL, as $[P]\varphi$ is equivalent to $[!]\varphi$. We also considered FSAPAL where $Q \subseteq P$ in $[Q]\varphi$ is required to be finite.

**PROPOSITION 3.1**

SAPAL-valid are $[Q]\varphi \to \varphi$ (T) and $[Q \cup R]\varphi \to [Q][R]\varphi$ (4)

**PROOF.** The validity of $[Q]\varphi \to \varphi$ follows from the validity of $[\top]\varphi \leftrightarrow \varphi$. Just as for APAL, $[Q \cup R]\varphi \to [Q][R]\varphi$ is valid because two announcements can be made into one announcement, as in the PAL validity $[\psi][\chi]\varphi \leftrightarrow [\psi \wedge [\psi]\chi]\varphi$, and because $P(\psi \wedge [\psi]\chi) \subseteq Q \cup R$ if $P(\psi) \subseteq Q$ and $P(\chi) \subseteq R$. $\square$

The SAPAL versions of CR and MK, $\langle Q \rangle[R]\varphi \to [Q]\langle R \rangle\varphi$ (CR) and $[Q]\langle R \rangle\varphi \to \langle Q \rangle[R]\varphi$ (MK) are not valid in SAPAL, however.

**PROPOSITION 3.2**

Neither $\langle Q \rangle[R]\varphi \to [Q]\langle R \rangle\varphi$ nor $[Q]\langle R \rangle\varphi \to \langle Q \rangle[R]\varphi$ is valid in SAPAL.

**PROOF.** Let $(M, 0)$ be the two state pointed model shown below.

$$ \underline{0}(\overline{pq}) \xrightarrow{a} 1(p\bar{q}) $$

Since $q$ is false in both states, they are $\{q\}$-bisimilar. As such, no informative $\{q\}$-announcements are possible in this model or any of its submodels, in the sense that any such announcement holds either on all states or on no states.

As a result, we have $M, 0 \models \langle \neg p \rangle[\{q\}]K_a \neg p$ but $M, 0 \not\models [\top]\{q\}K_a \neg p$, and hence $M, 0 \not\models \langle \{p\} \rangle[\{q\}]K_a \neg p \to [\{p\}]\langle \{q\} \rangle K_a \neg p$. Similarly, we have $M, 0 \not\models [\{q\}]\langle \{p\} \rangle K_a \neg p \to \langle \{q\} \rangle[\{p\}]K_a \neg \bar{p}$

Also note that all sets of variables in the above proof are finite, so CR and MK are not valid in FSAPAL either.

### 3.2 SCAPAL

The SCAPAL quantifier does not distribute over conjunction: $[\subseteq]\varphi \wedge [\subseteq]\psi$ is not equivalent to $[\subseteq](\varphi \wedge \psi)$. This is easily demonstrated by an example.

**EXAMPLE 3.3**

Consider model $(M, 10)$ in Figure 2 ($p\bar{q}$: $p$ is true and $q$ is false). Then:

$$ M, 10 \models [\subseteq]((K_a p \rightarrow K_b K_a p) \wedge \neg q) $$

$$ M, 10 \models [\subseteq](K_a p \rightarrow K_b K_a p) $$

$$ M, 10 \models [\subseteq] \neg q $$
<figure><img src="image_5.png" /><figcaption>FIGURE 2. Model (N, 1) on the left, (M, 10) in the middle, (M|(p ∨ q), 10) on the right.</figcaption></figure>

The first is false, because, as depicted:

$M, 10 \models (p \lor q) (K_a p \land \neg K_b K_a p)$, so

$M, 10 \models (p \lor q) ((K_a p \land \neg K_b K_a p) \lor q)$, and therefore

$M, 10 \models \langle \subseteq \rangle ((K_a p \land \neg K_b K_a p) \lor q)$, which is equivalent to

$M, 10 \models [\subseteq]((K_a p \rightarrow K_b K_a p) \land \neg q).$

The second is true because the only model restrictions containing 10 that we can obtain with formulas involving $p$ are $\{10, 11\}$ and $\{10, 11, 00, 01\}$. The third is true because $q$ is false in state 10.

Therefore, $[\subseteq]\varphi \land [\subseteq]\psi$ is not equivalent to $[\subseteq](\varphi \land \psi)$.

### PROPOSITION 3.4

Valid in SCAPAL are $[\subseteq]\varphi \rightarrow \varphi$ (T), $[\subseteq]\varphi \rightarrow [\subseteq][\subseteq]\varphi$ (F), $[\subseteq]\langle\subseteq\rangle\varphi \rightarrow \langle\subseteq\rangle[\subseteq]\varphi$ (MK) and $\langle\subseteq\rangle[\subseteq]\varphi \rightarrow [\subseteq]\langle\subseteq\rangle\varphi$ (CR).

PROOF. T and 4 are valid for the same reason as in SAPAL. For CR and MK we can now (unlike for SAPAL) use the same method as in APAL, as in any state of a model we can announce the value of all variables occurring in $\varphi$. A proof of CR is found in [47, Prop. 3.10] (for the similar logic APAL$^+$), which corrects the incorrect proof of CR for APAL in [8]). A proof of MK is found in [8]. □

## 3.3 QIPAL and IPAL

We recall that in APAL the quantification is over $\varphi \in \mathcal{L}_{PAL}$. Fairly complex counterexamples demonstrate that $[!]\varphi \rightarrow [\psi]\varphi$ is invalid for certain $\psi \in \mathcal{L}_{APAL}$ containing quantifiers [30]. Now in $[\psi^\downarrow]\varphi$, $\psi \in \mathcal{L}_{QIPAL}$ may also contain quantifiers. This makes the relation to $[!]$ unclear. In $\mathcal{L}_{IPAL}$, that $\psi$ must be in $\mathcal{L}_{PAL}$ and the relation is clearer.

### PROPOSITION 3.5

Let $\psi \in \mathcal{L}_{PAL}$, $\chi \in \mathcal{L}_{IPAL}$ and pointed model $(M, s)$ be given. The following are equivalent:

1. $M, s \models \langle \psi^\downarrow \rangle \chi$

2. there is a $\varphi \in \mathcal{L}_{PAL}$ such that $\models \varphi \rightarrow \psi$ and $M, s \models \langle \varphi \rangle \chi$,

3. there is a $\varphi \in \mathcal{L}_{PAL}$ such that $M \models \varphi \rightarrow \psi$ and $M, s \models \langle \varphi \rangle \chi$,

4. there is a $\varphi \in \mathcal{L}_{PAL}$ such that $M, s \models \langle \varphi \land \psi \rangle \chi$.

### PROOF.

1 $\Leftrightarrow$ 2 This is the semantics of the $\langle \psi^\downarrow \rangle$ quantifier (in dual form).

2 $\Rightarrow$ 3 From $\models \varphi \rightarrow \psi$ it trivially follows that $M \models \varphi \rightarrow \psi$.

3 $\Rightarrow$ 4 Suppose that there is a $\varphi \in \mathcal{L}_{PAL}$ such that $M \models \varphi \rightarrow \psi$ and $M, s \models \langle \varphi \rangle \chi$. Because $M \models \varphi \rightarrow \psi$, we have $M \models \varphi \leftrightarrow (\varphi \land \psi)$, and therefore $M|\varphi = M|(\varphi \land \psi)$. From $M, s \models \langle \varphi \rangle \chi$ then follows that $M, s \models \langle \varphi \land \psi \rangle \chi$.
4 $\Rightarrow$ 2 Suppose that there is a $\varphi \in \mathcal{L}_{PAL}$ such that $M, s \models \langle\varphi \wedge \psi\rangle\chi$. Let $\varphi' = \varphi \wedge \psi$, and note that $\varphi' \in \mathcal{L}_{PAL}$. We have $\models \varphi' \rightarrow \psi$ and $M, s \models \langle\varphi'\rangle\chi$. $\square$

So we can think of $\langle\psi^{\downarrow}\rangle$ as announcing $\varphi \wedge \psi$ for some $\varphi$. It is important, however, that the announcements of $\varphi$ and $\psi$ happen simultaneously. We cannot simply split $\langle\psi^{\downarrow}\rangle$ into an arbitrary announcement $\langle!\rangle$ and the announcement $\langle\psi\rangle$, because the truth of $\psi$ may be affected by the announcement of $\varphi$, and vice versa. Only under an additional constraint on $\psi$ is such separation possible.

The positive formulas $\mathcal{L}_{PAL}^{+}$ are the PAL-fragment $p | \neg p | \varphi \wedge \varphi | \varphi \vee \varphi | K_a\varphi | [\neg\varphi]\varphi$. The truth of positive formulas (corresponding to the universal fragment in first-order logic) is preserved after update [48].

### COROLLARY 3.6

Let $\psi \in \mathcal{L}_{PAL}^{+}$. Then $\langle\psi^{\downarrow}\rangle\chi$ implies $\langle!\rangle\langle\psi\rangle\chi$.

*PROOF.* Let $M, s \models \langle\psi^{\downarrow}\rangle\chi$. From Prop. 3.5.4 we obtain that there is $\varphi \in \mathcal{L}_{PAL}$ such that $M, s \models \langle\varphi \wedge \psi\rangle\chi$. As $\psi$ is positive, in any states where $\psi$ is true it remains true after the update $\langle\varphi \wedge \psi\rangle$. An additional announcement of $\langle\psi\rangle$ therefore does not remove further states. So $M, s \models \langle\varphi \wedge \psi\rangle\chi$ implies $M, s \models \langle\varphi \wedge \psi\rangle\langle\psi\rangle\chi$.

By the definition of the APAL quantifier, it follows that $M, s \models \langle!\rangle\langle\psi\rangle\chi$. $\square$

Since every formula implies $\top$ and is implied by $\bot$, both $[\top\downarrow]$ and $[\bot\uparrow]$ quantify over every formula in $\mathcal{L}_{PAL}$. We therefore have the following proposition.

### PROPOSITION 3.7

Let $\varphi \in \mathcal{L}_{IPAL}$. Then $[\top\downarrow]\varphi$ and $[\bot\uparrow]\varphi$ are equivalent to $[!]\varphi$.

*PROOF.* Let model $(M, s)$ and $\varphi \in \mathcal{L}_{QIPAL}$ be given. Then: $M, s \models [\top\downarrow]\varphi$, iff $M, s \models [\psi]\varphi$ for all $\psi \in \mathcal{L}_{PAL}$ with $\models \psi \rightarrow \top$, iff $M, s \models [\psi]\varphi$ for all $\psi \in \mathcal{L}_{PAL}$, iff $M, s \models [!]\varphi$.

Similarly, $M, s \models [\bot\uparrow]\varphi$, iff $M, s \models [\psi]\varphi$ for all $\psi \in \mathcal{L}_{PAL}$ with $\models \bot \rightarrow \psi$, iff $M, s \models [\psi]\varphi$ for all $\psi \in \mathcal{L}_{PAL}$, iff $M, s \models [!]\varphi$. $\square$

### PROPOSITION 3.8

Valid in QIPAL are $[\psi^{\uparrow}]\varphi \rightarrow \varphi$ (T) and also $[\psi^{\uparrow}]\varphi \rightarrow [\psi^{\uparrow}][\chi^{\uparrow}]\varphi$ and $[\psi^{\downarrow}]\varphi \rightarrow [\psi^{\downarrow}][\chi^{\downarrow}]\varphi$ (4)

*PROOF.* All proofs are as in Prop. 3.1 and 3.4. $\square$

However, $[\psi^{\downarrow}]\varphi \rightarrow \varphi$ (T) is invalid. This is because whenever $M|\psi$ is a proper submodel of a given model $M$, the trivial announcement is not allowed. For example, in any model where $p$ is true but $a$ does not know this, we have $[p^{\downarrow}]K_a p$ but not $K_a p$. Also, $[\psi^{\uparrow}]\varphi \rightarrow [\chi^{\uparrow}][\psi^{\uparrow}]\varphi$ and $[\psi^{\downarrow}]\varphi \rightarrow [\chi^{\downarrow}][\psi^{\downarrow}]\varphi$ are invalid, as the following example shows for the latter.

### EXAMPLE 3.9

Given is model $M$ with two states $s, t$ indistinguishable for $a$, and with $p$ only true in $s$.

$$t(\bar{p}) \xrightarrow{a} s(p)$$

We have $M, s \models [(p \wedge K_a p)^{\downarrow}]\bot$, since $p \wedge K_a p$ holds on neither state, so any announcement implying $p \wedge K_a p$ cannot hold on any state either. Yet we also have $M, s_1 \not\models [\top\downarrow][(p \wedge K_a p)^{\downarrow}]\bot$, with witnesses $p$ for the first announcement and $p \wedge K_a p$ for the second.
# 4 Expressivity

We now address the relative expressivity of APAL, FSAPAL and SCAPAL and IPAL, where the proof that APAL is less expressive than IPAL is considerably more involved than the other proofs. Given logics *L* and *L'* with languages *L* and *L'*-*L'*, *L* is at least as expressive as *L'*, notation *L'* ≲ *L*, iff for $\varphi \in L$ there is a $\varphi' \in L'$ such that $\varphi$ is equivalent to $\varphi'$. Logics *L* and *L'* are equally expressive iff *L* ≲ *L'* and *L'* ≲ *L*, *L* is less expressive than *L'*, notation *L* ≺ *L'*, iff *L* ≲ *L'* but *L'* ≲ *L*; *L* and *L'* are incomparable (in expressivity), notation *L* ≍ *L'*, iff *L* ≲ *L'* and *L'* ≲ *L*.

## 4.1 APAL ≲ FSAPAL and APAL ≲ SCAPAL

We show that there is an APAL-formula that can distinguish two pointed models that cannot be distinguished by any FSAPAL-formula. We use that APAL, unlike FSAPAL, quantifies over arbitrarily many atoms. The proof is similar to the proof that APAL ≲ PAL in [8].

**PROPOSITION 4.1**

APAL ≲ FSAPAL and APAL ≲ SCAPAL.

**PROOF.** Consider APAL formula $\langle ! \rangle (K_{ap} \wedge \neg K_b K_{ap})$, and assume towards a contradiction that $\psi$ is an equivalent FSAPAL formula. Let $q \notin P(\psi)$. Now consider models $(M, 10)$ and $(N, 1)$ in Figure 2, where the value of $q$ in states 0 and 1 of $N$ is irrelevant. These models are $P(\psi)$-bisimilar. We now have that:

1. $M, 10 \models \langle ! \rangle (K_{ap} \wedge \neg K_b K_{ap})$

2. Observe that $M|(p \lor q) \models K_{ap} \wedge \neg K_b K_{ap}$. This model is shown in Figure 2.

3. $N, 1 \not\models \langle ! \rangle (K_{ap} \wedge \neg K_b K_{ap})$

4. $M, 10 \models \psi$ iff $N, 1 \models \psi$

5. By Prop. 2.9, $(M, 10) \stackrel{P(\psi)}{\rightleftharpoons} (N, 1)$ implies $(M, 10) \stackrel{P(\psi)}{=} \text{FSAPAL} (N, 1)$.

The third item contradicts the first two items. Therefore APAL ≲ FSAPAL.

As Prop. 2.9 also applies to SCAPAL, this also proves that APAL ≲ SCAPAL. $\square$

<figure><img src="image_6.png" /></figure>

## 4.2 SCAPAL ≲ APAL and FSAPAL ≲ APAL

The proof is similar to that of the previous section, but more involved. We now show that the assumption that there is an APAL formula $\psi$ equivalent to SCAPAL formula $\langle \subseteq \rangle (\neg q \wedge K_{ap} \wedge \neg K_b K_{ap})$ leads to a contradiction. Prior to that we present models and lemmas used in the proof.

Consider models $M_n$ and $N_n$ as follows, where $n \in \mathbb{N}$ is odd. Model $M_n = (S, \sim, V)$ is such that (i) $S = [0, 2n-1]$, (ii) for any $i < n$, $2i \sim_b (2i+1)$ and, except for $i=0$, $(2i-1) \sim_a 2i$ and also $(2n-1) \sim_a 0$, and (iii) for any $i < n$, variable $p$ is true in states $2i$, variable $q$ is only true in state $n$ and variable $r$ is always false. Model $N_n$ is like model $M_n$ except that variable $r$ is only true in $n$ and variable $q$ is always false. Figure 3 depicts $M_3$ and $N_3$.

**LEMMA 4.2**

Let $M \subseteq M_n$, $N \subseteq N_n$, $i,j,k \in \mathbb{N}$, with $i \in \mathcal{D}(M)$ and $j \in \mathcal{D}(N)$ be such that $(M, i) \stackrel{\leftrightarrow k}{=} (N, j)$. Then for all $\chi \in \mathcal{L}_{PAL}$ such that $M, i \models \chi$ there is a $\chi' \in \mathcal{L}_{PAL}$ such that $N, j \models \chi'$ and $(M|\chi, i) \stackrel{\leftrightarrow k}{=} (N|\chi', j)$. Furthermore, for all $\chi' \in \mathcal{L}_{PAL}$ such that $N, j \models \chi'$ there is a $\chi \in \mathcal{L}_{PAL}$ such that $M, i \models \chi$ and $(M|\chi, i) \stackrel{\leftrightarrow k}{=} (N|\chi', j)$.

**PROOF.** Without loss of generality, we can assume that $M$ and $N$ are connected. We begin by showing that every state $s$ of $M$ is uniquely identifiable by some formula $\varphi_s \in \mathcal{L}_{PAL}$. If the $q$-state is reachable
<figure><img src="image_7.png" /><figcaption>FIGURE 3. The models $M_3$ and $N_3$.</figcaption></figure>

from $s$, then the identifying formula is based on the shortest path to the $q$-state, and the agents along that path. For example, in $M_3$, state 5 is the only state from which the $q$-state, state 3, is reachable by taking a $b$-edge followed by an $a$-edge, but not by only following an $a$-edge or only a $b$-edge. Hence, state 5 in $M_3$ is uniquely identified by the formula $\hat{K}_b\hat{K}_a q \wedge \neg\hat{K}_a q \wedge \neg\hat{K}_b q$. If the $q$-state is not reachable from $s$ and $M$ contains at least two states, then there is a ‘leftmost’ state in $M$, which can be uniquely identified by the formula $\varphi_{left} = K_a p \lor K_b \neg p$. The state $s$ can then be uniquely identified by its distance to this leftmost state. If $M$ contains only one state, it can be identified trivially by $\top$.

Because $M$ is a finite model and each state can be uniquely identified by a formula, each submodel of $M$ is the extension of a disjunction of such formulas. Every state of $N$ is similarly uniquely identifiable, so each submodel of $N$ is also the extension of some formula.

In order for $(M, i)$ and $(N, j)$ to be $k$-bisimilar it is necessary and sufficient that (i) the $q$ and $r$ state are not reachable in $k$ steps from $(M, i)$ and $(N, j)$, respectively, (ii) there is a leftmost (resp. rightmost) state reachable from $(M, i)$ in less than $k$ steps if and only if there is a leftmost (resp. rightmost) state reachable from $(N, j)$ in less than $k$ steps. Condition (i) is always preserved in submodels. In order to guarantee that $(M|\chi, i) \stackrel{\leftrightarrow}{\kern-\nulldelimiterspace}^k (N|\chi', j)$ it therefore suffices to preserve (ii), which can be done by taking $\chi$ or $\chi'$ to be the formula such that $\chi$ holds on a state $l \le k$ steps to the left/right of $(M, i)$ if and only if $\chi'$ holds $l$ steps to the left/right of $(N, j)$. $\square$

In general, two $k$-bisimilar states need not be $k$-indistinguishable in APAL. This is because the $[!]$ operator quantifies over formulas of arbitrary depth. For submodels of $M_n$ and $N_n$, however, $k$-bisimilarity does imply $k$-indistinguishability.

LEMMA 4.3

Let $M \subseteq M_n$, $N \subseteq N_n$ and $i,j,k \in \mathbb{N}$, with $i \in \mathcal{D}(M)$ and $j \in \mathcal{D}(N)$. If $(M, i) \stackrel{\leftrightarrow}{\kern-\nulldelimiterspace}^k (N, j)$, then $(M, i) \stackrel{\equiv}{\kern-\nulldelimiterspace}^k \mathcal{APAL}(N, j)$.

PROOF. We show the equivalent formulation:

For all $\varphi \in \mathcal{L}_{\mathcal{APAL}}$, $M \subseteq M_n$, $N \subseteq N_n$ and $i,j,k \in \mathbb{N}$ with $i \in \mathcal{D}(M)$ and $j \in \mathcal{D}(N)$: if $(M, i) \stackrel{\leftrightarrow}{\kern-\nulldelimiterspace}^k (N, j)$ and $d(\varphi) \le k$, then $M, i \models \varphi$ iff $N, j \models \varphi$.

The proof is by induction on the structure of $\varphi$. The cases of interest are $K_b\varphi$, $[\psi]\varphi$, and $[!]\varphi$. As $k$-bisimilarity is a symmetric relation, it suffices to show only one direction of the equivalence.
**Case** $K_a\varphi$: Suppose $d(K_a\varphi) \le k$. We have $M, i \models K_a\varphi$ iff for all $i' \sim_a i$, $M, i' \models \varphi$. As $(M, i) \unfrown^k(N, j)$, for all $j' \sim_a j$ there is some $i' \sim_a i$ such that $(M, i') \unfrown^{k-1}(N, j')$. As $d(K_a\varphi) \le k$, $d(\varphi) \le k-1$. Therefore, by induction, $N, j' \models \varphi$. And therefore $N, j \models K_a\varphi$.

**Case** $[\psi]\varphi$: Suppose $d([\psi]\varphi) \le k$, and $M, i \models [\psi]\varphi$. Let $d(\psi) = x$ and $d(\varphi) = y$, then $x+y = d(\psi) + d(\varphi) = d([\psi]\varphi) \le k$. By definition, $M, i \models [\psi]\varphi$ iff $M, i \models \psi$ implies $M|\psi, i \models \varphi$. From $M, i \models \psi$, $(M, i) \unfrown^k(N, j)$ and $d(\psi) = x \le k$ and induction we obtain $N, j \models \psi$. From $(M, i) \unfrown^k(N, j)$, $M, i \models \psi$, $d(\psi) = x \le k-y$, a part identical to that of Lemma 2.8 except that where bisimulation invariance for PAL is used on $\psi \in \mathcal{L}_{PAL}$ we now use induction on $\psi \in \mathcal{L}_{APAL}$, we obtain that $(M|\psi, i) \unfrown^y(N|\psi, j)$. From that, $M|\psi, i \models \varphi$, $d(\varphi) = y$ and induction we obtain $N|\psi, j \models \varphi$. Then, $N, j \models \psi$ implies $N|\psi, j \models \varphi$ is by definition $N, j \models [\psi]\varphi$.

**Case** [!] $\varphi$: Suppose towards a contradiction that $N, j \not\models$ [!] $\varphi$. Then there is some $\chi' \in \mathcal{L}_{PAL}$ such that $N, j \models \chi'$ and $N|\chi', j \not\models \varphi$. By assumption $(M, i) \unfrown^k(N, j)$, so the conditions of Lemma 4.2 are satisfied. So there is a $\chi \in \mathcal{L}_{PAL}$ such that $M, i \models \chi$ and $(M|\chi, i) \unfrown^k(N|\chi, j)$. The induction hypothesis and the fact that $N|\chi', j \not\models \varphi$ then imply that $M|\chi, i \not\models \varphi$. We therefore have $M, i \not\models [\chi]\varphi$, contradicting $M, i \models$ [!] $\varphi$. From this contradiction, we conclude that $N, j \models$ [!] $\varphi$. $\square$

**PROPOSITION 4.4**

SCAPAL $\not\leq$ APAL.

**PROOF.** Consider $\mathcal{L}_{SCAPAL}$ formula $\varphi = (\subseteq)(\neg q \wedge K_{ap} \wedge \neg K_b K_{ap})$. Let $\psi$ be the supposedly equivalent $\mathcal{L}_{APAL}$ formula. Take $n > d(\psi)$. We now show that:

1. $M_n, 0 \models (\subseteq)(\neg q \wedge K_{ap} \wedge \neg K_b K_{ap})$

2. $N_n, 0 \not\models (\subseteq)(\neg q \wedge K_{ap} \wedge \neg K_b K_{ap})$

3. $M_n, 0 \models \psi$ iff $N_n, 0 \models \psi$

These items are proved by the following arguments:

1. The state $n$ is distinguished by formula $q$. This allows us to distinguish each finite subset of the domain, in the usual way, in $\mathcal{L}_{EL}$ (note that there is no mirror symmetry along the $0$— $n$ 'diameter' of the circular models $M_n$ and $N_n$). Thus there is a formula $\eta \in \mathcal{L}_{EL}|q$ that distinguishes the set of states $\{0, 1\}$. We now have that:

$$
\begin{align*}
M_n, 0 &\models \eta \\
M_n|\eta, 0 &\models \neg q \wedge K_{ap} \wedge \neg K_b K_{ap} \\
M_n, 0 &\models (\eta)(\neg q \wedge K_{ap} \wedge \neg K_b K_{ap}) \\
M_n, 0 &\models (\subseteq)(\neg q \wedge K_{ap} \wedge \neg K_b K_{ap})
\end{align*}
$$

2. On the other hand, $N_n, 0 \not\models (\subseteq)(\neg q \wedge K_{ap} \wedge \neg K_b K_{ap})$. This is because we cannot use that $r$ is only true in $n$, as $r \notin P(\neg q \wedge K_{ap} \wedge \neg K_b K_{ap})$, and because $(N_n, 0) \unfrown^{pq}(O, 0)$. Clearly $O, 0 \not\models (\subseteq)(\neg q \wedge K_{ap} \wedge \neg K_b K_{ap})$.

3. However, $M_n, 0 \models \psi$ iff $N_n, 0 \models \psi$. This follows from Lemma 4.3, as $n > d(\psi)$ and $(M_n, 0) \unfrown^{d(\psi)}(N_n, 0)$. $\square$

**PROPOSITION 4.5**

FSAPAL $\not\leq$ APAL.

**PROOF.** As Prop. 4.4, but we now take FSAPAL formula $\langle q \rangle (\neg q \wedge K_{ap} \wedge \neg K_b K_{ap})$ instead of SCAPAL formula $\langle \subseteq \rangle (\neg q \wedge K_{ap} \wedge \neg K_b K_{ap})$. $\square$

As [!] $\varphi$ is equivalent to [P]$\varphi$ we rather trivially have that APAL $\leq$ SAPAL, so that with Prop. 4.5 and its consequence SAPAL $\not\leq$ APAL we immediately obtain:
$$ M_{-3,3}: \quad -3(q) \frac{a}{-2(p)} \frac{b}{-1} \frac{a}{0(p)} \frac{b}{1} \frac{a}{2(p)} \frac{b}{3(q)} $$

$$ N_{-3,3}: \quad -3 \frac{a}{-2(p)} \frac{b}{-1} \frac{a}{0(p)} \frac{b}{1} \frac{a}{2(p)} \frac{b}{3} $$

FIGURE 4. The models $M_{-3,3}$ and $N_{-3,3}$.

COROLLARY 4.6
APAL $\prec$ SAPAL.

## 4.3 SCAPAL $\prec$ FSAPAL

We first show that SCAPAL $\leq$ FSAPAL, and then show that SCAPAL $\prec$ FSAPAL.

PROPOSITION 4.7
SCAPAL $\leq$ FSAPAL.

PROOF. It is trivial that SCAPAL $\leq$ FSAPAL, since $\models [\subseteq]\varphi \leftrightarrow [P(\varphi)]\varphi$. Formally, we inductively define a translation function $f$ from SCAPAL to FSAPAL by

$$ \begin{array}{lclcl} f(p) & = & p & f(\varphi \lor \psi) & = & f(\varphi) \lor f(\psi) \\ f(\neg\varphi) & = & \neg f(\varphi) & f(K_a\varphi) & = & K_a f(\varphi) \\ & & & f([\subseteq]\varphi) & = & [P(\varphi)]f(\varphi) \end{array} $$

In the final line we could equivalently have written $f([\subseteq]\varphi) = [P(f(\varphi))]f(\varphi)$, as $f$ does not affect the set of atoms that occur in a formula. We then have $\models \varphi \leftrightarrow f(\varphi)$ (which is shown by induction), and therefore SCAPAL $\leq$ FSAPAL. $\square$

We now show SCAPAL $\prec$ FSAPAL. In the proof we use models $M_{-n,n}$ and $N_{-n,n}$ similar to $M_n$ and $N_n$ used in the previous subsection. They are depicted in Figure 4 for $n=3$, compare to Figure 3. (Imagine ‘cutting open’ $M_3$ and $N_3$ at the $q$ resp. $r$ state, and remove $r$ as we can now use the distinguishing power of $p$ on the edges of the chain.) Similarly to Lemma 4.3, we first show a Lemma 4.8.

### LEMMA 4.8

Let $M \subseteq M_{-n,n}$, $N \subseteq N_{-n,n}$ and $i,j,k \in \mathbb{N}$, with $i \in \mathcal{D}(M)$ and $j \in \mathcal{D}(N)$. If $(M,i) \stackrel{\square k}{\equiv} (N,j)$, then $(M,i) \stackrel{k}{\equiv} \mathcal{SCAPAL}(N,j)$.

PROOF. We show by formula induction that $M, i \models \varphi$ iff $N, j \models \varphi$ for any $\varphi \in \mathcal{L}_{\mathcal{SCAPAL}}$ with $d(\varphi) \leq k$. Cases $K_a\psi$ and $[\chi]\psi$ are the same. The case quantifier $[\subseteq]\psi$ is different and shown as follows.

First, suppose that $q \notin P(\psi)$. Then from $(M, i) \stackrel{\square k}{\equiv} (N, j)$ and Lemma 2.9 it directly follows that $M, i \models [\subseteq]\psi$ iff $N, j \models [\subseteq]\psi$.

Next, suppose that $q \in P(\psi)$; w.l.o.g. we may also assume that $p \in P(\psi)$. By assumption, $(M, i) \stackrel{\square k}{\equiv} (N, j)$. Just as for Lemma 4.2, every $M' \subseteq M$ is definable in $M$ by a formula in $\mathcal{L}_{PAL}|pq$, and every $N' \subseteq N$ is definable in $N$ by a formula in $\mathcal{L}_{PAL}|pq$. It follows that for every $\chi \in \mathcal{L}_{PAL}|pq$ with $M, i \models \chi$ there is a $\xi \in \mathcal{L}_{PAL}|pq$ such that $(M|\chi, i) \stackrel{\square k}{\equiv} (N|\xi, j)$, and vice versa. Therefore, $M, i \models [\subseteq]\psi$ iff $N, j \models [\subseteq]\psi$. $\square$

PROPOSITION 4.9
SCAPAL $\prec$ FSAPAL.
PROOF. We proceed as usual, however, with distinguishing FSAPAL formula $⟨q⟩(K_a p ∧ ¬K_b K_a p)$. Let $\psi$ be the supposedly equivalent $\mathcal{L}_{\text{SCAPAL}}$ formula. Take $n > d(\psi)$. Then:

1. $M_{-n,n}, 0 \models ⟨q⟩(K_a p \wedge \neg K_b K_a p)$

2. $N_{-n,n}, 0 \not\models ⟨q⟩(K_a p \wedge \neg K_b K_a p)$ (obvious)

3. $M_{-n,n}, 0 \models \psi$ iff $N_{-n,n}, 0 \models \psi$ (use $(M_{-n,n}, 0) \unfrown^d ⟨\psi⟩(N_{-n,n}, 0)$ & Lemma 4.8)

☐

## 4.4 Results for IPAL

Let us first present all our results for IPAL in relation to the other logics in the contribution, with the exception of the proof that APAL $\prec$ IPAL, our main result.

### PROPOSITION 4.10

APAL $\preceq$ IPAL.

PROOF. This follows from Prop. 3.7 that $[\uparrow\downarrow]\varphi$ is equivalent to $[!]\varphi$. ☐

We can also obtain strictness.

### PROPOSITION 4.11

APAL $\prec$ IPAL.

PROOF. The proof of this result is rather involved and presented in the next subsection. ☐

The relative expressivity between IPAL and FSAPAL/SCAPAL mirrors the results already obtained between APAL and FSAPAL/SCAPAL.

### PROPOSITION 4.12

IPAL $\asymp$ FSAPAL and IPAL $\asymp$ SCAPAL.

PROOF. FSAPAL $\not\preceq$ IPAL and SCAPAL $\not\preceq$ IPAL are shown as FSAPAL $\not\preceq$ APAL (Prop. 4.5) and SCAPAL $\not\preceq$ APAL (Prop. 4.4), except that in the inductive case for the quantifier of the proof of Lemma 4.3 we do not consider all witnesses $\psi$ for the quantifier $⟨!⟩$ but only those that imply the given $\chi$ in $⟨\chi\downarrow⟩$ or that are implied by the given $\chi$ in $⟨\chi\downarrow⟩$.

From APAL $\prec$ IPAL, APAL $\not\preceq$ FSAPAL and APAL $\not\preceq$ SCAPAL (Prop. 4.1), we immediately obtain IPAL $\not\preceq$ FSAPAL and IPAL $\not\preceq$ SCAPAL. ☐

## 4.5 APAL $\prec$ IPAL

This section contains the proof of Proposition 4.11.

Let us start this proof by defining the sets of models that we will use. These models consist of a base part

$$ \begin{array}{c} s_1(p) \xrightarrow{b} s_2(p, q) \\ a \\ \hline t_1(p) \xrightarrow{b} t_2(p, q) \end{array} $$

plus a number of *branches* of the form, for some $l \in \mathbb{N}$

$$ u_0 \underline{b} u_1(p) \underline{a} u_2(p) \dots \underline{a/b} u_{l-2}(p) \underline{u_{l-1}(p)} $$
<figure><img src="image_8.png" /><figcaption>FIGURE 5. Typical model used in the proof that APAL < IPAL.</figcaption></figure>

The atom $p$ holds in every state except $u_1$, and the accessibility alternates between $a$ and $b$, so the final agent may be $a$ or $b$ depending on whether $l$ is even. We refer to the state $u_0$ as the *root* of the branch.

The models that we will consider consist of a base part, where both $s_2$ and $t_2$ are $a$-attached to any finite number of branches, possibly of different lengths. An example of such a model, where $s_2$ is attached to two branches of lengths 2 and 5, while $t_2$ is attached to three branches of length 2, 3 and 4, is shown in Figure 5.

We say that two states in the model are *on the same side* if one can be reached from the other without using the $a$-edge between $s_1$ and $t_1$, and *on the other side* otherwise.

We then divide these types of models into two sets: a set $\mathfrak{N}$ where there is at least one length $l$ such that both $s_2$ and $t_2$ are attached to at least one branch of length $l$, and a set $\mathfrak{M}$ where there is no such shared length $l$. We will first show that IPAL can uniformly distinguish between these sets.

LEMMA 4.13

Let $M \in \mathfrak{M}$ and $N \in \mathfrak{N}$. Furthermore, let $\varphi = [p^{\uparrow}](\psi_1 \rightarrow \langle T^{\downarrow} \rangle \psi_2)$, where $\psi_1 = \hat{K}_b \hat{K}_a \neg p$ and $\psi_2 = K_b \neg q \wedge \hat{K}_a \hat{K}_b q$. Then $M, s_1 \models \varphi$ and $N, s_1 \not\models \varphi$.

PROOF. The key observation is that announcing any epistemic formula $\chi$ implied by $p$ can remove access to a branch by removing the state $u_0^i$ for that branch, but it cannot change the length of a branch, or remove any of the states $s_1, s_2, t_1$ and $t_2$, since all other states satisfy $p$, and therefore also $\chi$.

Let $\chi$ then be any epistemic formula implied by $p$ such that $M|\chi, s_1 \models \hat{K}_b \hat{K}_a \neg p$. Then at least one branch on the top side of the model is retained. Because $M \in \mathfrak{M}$, there is no branch on the bottom side of the model that has the same length. This implies that $M|\chi, s_2$ and $M|\chi, t_2$ are distinguishable.
by a modal formula. As such, there is an epistemic announcement $\xi$ that removes $s_2$ while retaining $s_1$, $t_1$ and $t_2$, so we have $(M|\chi)|\xi, s_1 \models \psi_2$.

This suffices to show that $M, s_1 \models [p^\uparrow](\psi_1 \rightarrow \langle\uparrow\downarrow\rangle\psi_2)$.

Regarding $N$, since it is a member of $\mathfrak{N}$ there is some $l$ such that the top and bottom sides of $N$ both have a branch of length $l$. Let $\chi$ be the epistemic formula that retains a $\neg p$ state only if it is the root of a branch of length exactly $l$. Then we have $N|\chi, s_1 \models \psi_1$. Yet in $N|\chi$, the top and bottom side of the model are bisimilar, so there is no announcement that would retain $t_2$ while removing $s_2$. Hence $N|\chi, s_1 \not\models \langle\uparrow\downarrow\rangle\psi_2$.

This suffices to show that $N, s_1 \models [p^\uparrow](\psi_1 \rightarrow \langle\uparrow\downarrow\rangle\psi_2)$.

☐

Left to show is that there is no APAL formula that similarly distinguishes between $\mathfrak{N}$ and $\mathfrak{N}$. Unfortunately, this proof is significantly more complex than the other expressivity proofs in this paper. It is therefore useful to first introduce a few auxiliary definitions and lemmas.

### DEFINITION 4.14

Let $(X, x)$ be a submodel of a model of type $\mathfrak{M}$ or $\mathfrak{N}$. We classify $(X, x)$ based on which worlds are retained, in the following way:

* If $x = u_i^j$ and $u_0^j$ is not reachable from $x$ in $X$, then $(X, x)$ is a *dead branch*.

* If at least one state $u_0^j$ is reachable from $x$ in $X$ and on the same side, then this side of $(X, x)$ is a *bouquet*. If furthermore $s_2$ or $t_2$ is reachable on the same side, then the bouquet has a *stem* of length 1. If $s_1$ or $s_2$ is also reachable on the same side, then the bouquet has a *stem* of length 2.

* If $s_1, s_2, t_1$ or $t_2$ is same-side reachable from $(X, x)$ but no state $u_0^j$ is, then this side of $(X, x)$ is a *dead stem*. Two dead steams have the same form if they both retain their $q$ world or both remove it, and both retain their $\neg q$ world or both remove it.

### DEFINITION 4.15

Let $(X, x)$ and $(Y, y)$ be pointed submodels of models of type $\mathfrak{M}$ or $\mathfrak{N}$ and let $k \in \mathbb{N}$. We say that $(X, x)$ and $(Y, y)$ are $k$-akin if one of the following three conditions holds for both this side of the models and, if reachable, the other side:

* they are both dead branches,

* they are both bouquets with the same stem length and

- for every $l \le k$, if the bouquet in $X$ has a branch of length $l$ then so does the one in $Y$, and vice versa,

- if the bouquet in $X$ has exactly $m \le (k+1)^2$ branches of different lengths greater than $k$ then so does the one in $Y$, and vice versa,

- if the top and bottom sides of $X$ and $Y$ are each bouquets with stem 2, then the top and bottom side of $X$ are bisimilar if and only if the top and bottom side of $Y$ are bisimilar,

* $(X, x)$ and $(Y, y)$ are both dead stems of the same form.

### DEFINITION 4.16

Let $k \in \mathbb{N}$, and let $(X, x)$ and $(Y, y)$ be $k$-akin. The relation $\approx^k$ is the restriction of the following relation to the connected parts of the two models:

* $(X, s_i) \approx^k (Y, s_i)$ and $(X, t_i) \approx^k (Y, t_i)$ for $i \in \{1, 2\}$,
* for every $0 \le i \le k-1$, if $(X, u_i')$ lies in a branch of length at most $k$, then $(X, u_i'') \approx^k (Y, u_i'')$,
  where $(Y, u_i'')$ lies in the branch of $Y$ at the same length at the same side,<fnref n="1" /> and vice versa,

* for every $0 \le i \le k-1$, if $(X, u_i')$ lies in a branch of length greater than $k$, then $(X, u_i'') \approx^k (Y, u_i'')$ for every $u_i'$ that lies in a branch of the same side of length greater than $k$, and vice versa,

* for every $i, i' \ge k$, if $(X, u_i')$ and $(Y, u_{i'}')$ are on the same side, then $(X, u_i'') \approx^k (Y, u_{i'}')$.

We will use $\approx^k$ as the invariant in our inductive proof. One important property of $\approx^k$ is that it is a $k$-bisimulation.

**LEMMA 4.17**

If $(X, x) \approx^k (Y, y)$ then for every $a$- or $b$-successor $x'$ of $x$ there is an $a$- or $b$-successor $y'$ of $y$ such that $(X, x') \approx^{k-1} (Y, y')$, and vice versa.

**LEMMA 4.18**

The relation $\approx^k$ is a $k$-bisimulation.

The proofs are conceptually very simple, but still requires a lot of notation and different cases, so we omit them.

We have now completed all the preliminary work and can prove the result that we are after.

**LEMMA 4.19**

Let $k \in \mathbb{N}$, and let $(X, x) \approx^k (Y, y)$. Then for every $\varphi$ of depth at most $k$, we have $X, x \models \varphi$ iff $Y, y \models \varphi$.

**PROOF.** By induction on formula construction. If $\varphi$ is Boolean, then the lemma follows immediately from the fact that $\approx^k$ is a $k$-bisimulation.

Suppose then as induction hypothesis that the lemma holds for all $\varphi'$ that are strict subformulas of $\varphi$. Assume towards a contradiction that $\varphi$ distinguishes between $(X, x)$ and $(Y, y)$. Since the conditions of the lemma are symmetric we can assume without loss of generality that $X, x \models \varphi$ and $Y, y \not\models \varphi$.

A Boolean combination of formulas distinguishes between two states only if one of the combined formulas does. If the main connective of $\varphi$ is Boolean it therefore follows immediately from the induction hypothesis that $\varphi$ does not distinguish between $(X, x)$ and $(Y, y)$. This leaves three cases for the main connective of $\varphi$: $K_a$, $[\psi]$ and $[!]$.

Suppose that $\varphi = K_a\psi$. Then $Y, y \not\models K_a\psi$, so there is an $a$-successor $y'$ of $y$ such that $Y, y \not\models \psi$. By $(X, x) \approx^k (Y, y)$ there is an $a$-successor $x'$ of $x$ such that $(X, x') \approx^{k-1} (Y, y')$. By the induction hypothesis, together with the fact that $d(\psi) \le k-1$, we then have $X, x' \not\models \psi$, and therefore $X, x \not\models K_a\psi$, contradicting our assumption that $K_a\psi$ distinguishes between $(X, x)$ and $(Y, y)$.

Suppose that $\varphi = [\psi]\chi$. Then $X, x \models [\psi]\chi$, and therefore either $X, x \not\models \psi$ or $X \models \psi, x \models \chi$. In the first case, by the induction hypothesis we also have $Y, y \not\models \psi$, which implies that $Y, y \models [\psi]\chi$ contradicting the assumption that $[\psi]\chi$ distinguishes between the two pointed models.

<footnote n="1">¹Which must exist because $(X, x)$ and $(Y, y)$ are $k$-akin.</footnote>
In the second case, compare the models $X|\psi$ and $Y|\psi$. Because $\psi$ is, by the induction hypothesis, invariant under $\approx^k$, for every branch in $X|\psi$ that is cut off at a length at most $k$, its counterpart in $Y|\psi$ is cut off at the same length. The states $s_1, s_2, t_1$ and $t_2$ are similarly retained in one model if and only if they are retained in the other. It follows that $(X|\psi, x) \approx^k (Y|\psi, y)$. By the induction hypothesis the two models are therefore indistinguishable by $\chi$. This contradicts the assumption that $X, x \models [\psi]\chi$ and $Y, y \not\models [\psi]\chi$.

Finally, suppose that $\varphi = [!]\chi$. We assumed $X, x \models \varphi$ and $Y, y \not\models \varphi$, so there is some epistemic formula $\psi$ such that $Y, y \not\models [\psi]\chi$. We will create an epistemic formula $\psi'$ such that $(X|\psi', x) \approx^k (Y|\psi, y)$.

First, note that the top and bottom side of $X$ are bisimilar if and only if the top and bottom side of $Y$ are. If top and bottom are bisimilar, we can perform a bisimilarity contraction on both models, obtaining a model where one side has been removed entirely. As such, we can assume without loss of generality that if both sides of the model still exist, then they are non-bisimilar. Because all models under consideration are finite this also implies that the top and bottom sides are distinguishable by a modal formula.

As a result, every state can be uniquely identified by (1) whether it is on the top or bottom side, (2) if it is in a branch, the length of that branch and (3) its position in the branch or in the stem. By using a disjunction of characterizing formulas we can create a formula that retains an arbitrary set of identifiable states.

We now create $\psi'$ as follows:

1. For each side, $\psi'$ holds on the stem states iff $\psi$ does.

2. For each side, if $\psi$ removes a branch of length $l \le k$, or trims it to a length $l' < l$, then so does $\psi'$.

3. For each side, if $\psi$ cuts down a branch of length $l > k$ to $l' \le k-1$, then $\psi'$ cuts down a branch of length $l'' > k$ to $l'$.

4. For each side, if $\psi$ retains $m \le k^2$ branches of length at least $k-1$, then $\psi'$ retains exactly $m$ such branches as well.

5. For each side, if $\psi$ retains $m > k^2$ branches of length at least $k-1$ then $\psi'$ retains $m' > k^2$ such branches.

6. If $y$ ends up in a short branch in $Y$ then $x$'s branch in $X$ is cut to the same length.

Note that items 3–5 can be done because of the condition that $X$ and $Y$ contained either the same number of (different length) long branches, or more than $(k+1)^2$ of them. Some long branches may be ‘consumed’ to provide the branches of length $l \le k-1$. But $\psi$ and $\psi'$ consume the same number of branches, and at most $k-1$ of them. So $X$ has enough long branches to provide either the same number of long branches in $X|\psi'$ and $Y|\psi$ or at least $k^2$ of them.

By construction, the models $X|\psi'$ and $Y|\psi$ satisfy the conditions for being $(k-1)$-akin. Furthermore, $x$ and $y$ are in the same relative position, so $(X|\psi', x) \approx^{k-1} (Y|\psi, y)$. By the induction hypothesis we therefore have $X|\psi', x \models \chi$ iff $Y|\psi, y \models \chi$. This contradicts our assumption that $X, x \models [!]\chi$ and $Y, y \not\models [!]\chi$.

In each case, we arrived at a contradiction. So $\varphi$ does not distinguish between $(X, x)$ and $(Y, y)$, completing the induction step and thereby the proof. $\square$

We have now shown that there is an IPAL formula that distinguishes between $\mathfrak{M}$ and $\mathfrak{N}$ (Lemma 4.13) and that there is no APAL formula that similarly distinguishes the two sets (Lemma 4.19). This implies that there is no APAL formula that is equivalent to the distinguishing IPAL formula. So we have $\mathfrak{IPAL} \not\subseteq \mathfrak{APAL}$. Together with APAL $\le \mathfrak{IPAL}$ (Proposition 4.10), this yields the result that that we were after, namely that $\mathfrak{APAL} < \mathfrak{IPAL}$ (Proposition 4.11).
**5 Decidability and undecidability of satisfiability**

The satisfiability problem of APAL is decidable when there is only one agent, whereas it is
undecidable when there are at least two agents [2, 20]. The approach is by encoding/formalizing
an undecidable tiling problem into APAL [13]. There are some decidable logics with quantification
over information change, e.g. Boolean arbitrary public announcement logic [46]. It is therefore a
relevant question whether the APAL versions considered in this paper are decidable. It turns out that
they are all *undecidable* (for more than one agent). We prove this by referring to the undecidability
proof in [2] and listing, for each of SAPAL, SCAPAL and IPAL, the exact changes needed in that
proof in order to show undecidability. For all proof details and proof structure we refer to [2].

PROPOSITION 5.1

The satisfiability problem for SAPAL, FSAPAL, SCAPAL and IPAL is undecidable.

PROOF. In [2] it is shown that, given a finite set $C$ of colours, there is an APAL formula $\varphi$ that formalizes an undecidable tiling problem of tiles coloured with $C$. We cannot determine whether $\varphi$ is satisfiable as this would solve the tiling problem. Therefore the satisfiability problem of APAL is undecidable. This formula $\varphi$ has many constituents that describe properties that need to be satisfied by the tiling, and APAL quantifiers occur in the formulas describing such properties (see Example 5.2 below). For each of SAPAL, SCAPAL and IPAL there is a very simple way to translate these $\mathcal{L}_{APAL}$ formulas into equivalent $\mathcal{L}_{SAPAL}$, $\mathcal{L}_{SCAPAL}$, respectively $\mathcal{L}_{IPAL}$ formulas. Furthermore, for SAPAL the translation only uses finite sets of variables, so it is a translation to FSAPAL as well.

First, we note that the APAL undecidability proof in [2] only uses two agents and a *finite set* $C \cup \Lambda$ of atoms that is the union of a finite set $C$ of colours plus a set $\Lambda = \{u, d, l, r, \heartsuit, \clubsuit, \diamondsuit, \spadesuit\}$. Let us at least explain the intuitive meaning of these different atoms. The properties formalized in the proof describe the requirements to tile an infinite grid where a square in the grid has four sides $u, d, l, r$ (for ‘up’, ‘down’, ‘left’ and ‘right’) and where each square is labeled with one of $\heartsuit, \clubsuit, \diamondsuit, \spadesuit$. The four sides of the tiles have colours from $C$ and the colours of adjoining tiles positioned on the grid have to match. No other atoms are required.

The required truth (value) preserving translations from $\mathcal{L}_{APAL}$ to $\mathcal{L}_X$, where $X$ is one of SAPAL, SCAPAL and IPAL, are now as follows. We recall the above $\varphi \in \mathcal{L}_{APAL}$ encoding the tiling. Then:

• For SAPAL, replace each occurrence of [!] in $\varphi$ by $[C \cup \Lambda]$.

• For SCAPAL, let $\top_{C \cup \Lambda} := \bigwedge_{p \in C \cup \Lambda} (p \lor \neg p)$. Now replace each subformula of $\varphi$ of shape [!] $\psi$ by $[\subseteq](\psi \land \top_{C \cup \Lambda})^2$.

• For IPAL, replace each occurrence of [!] in $\varphi$ by $[\top^\downarrow]$.

These translations are indeed adequate. For SAPAL it is sufficient to observe that the set of atoms
$P$ considered is $C \cup \Lambda$ and that [!]$\varphi$ is equivalent to [P]$\varphi$ for the entire (finite) set of atoms. The
case SCAPAL is slightly more complex, as the witnesses of a constituent of shape [!] $\psi$ of the tiling
formula $\varphi$ may need more atoms than are occurring in the formula $\psi$ (as demonstrated below in
Example 5.2). The translation simply forces any formula bound by a quantifier to employ all atoms
in the language by adding another conjunct that does not affect the truth value as it is always true.
Finally, Prop. 3.7 showed that $[\top^\downarrow]\varphi$ is equivalent to [!]$\varphi$.

Apart from these translations, no other adjustments to the proof in [2] are needed. $\square$

<footnote n="2">²More properly, we should see this as an inductively defined translation $t : \mathcal{L}_{APAL} \to \mathcal{L}_{SCAPAL}$ with only non-trivial clause $t([!]\varphi) := [\subseteq](t(\varphi) \land \top_{C \cup \Lambda})$.</footnote>
### EXAMPLE 5.2

A constituent of the formula $\varphi$ encoding the tiling of the plain is as follows, where $\mathfrak{s}$ and $\mathfrak{e}$ are the two agents used in the proof. It says that for any square of the infinite grid labelled with a $\heartsuit$, there is some square below some square to the left of some square above some square to the right of that square, that is $n$-bisimilar (i.e. a square that is also labelled with $\heartsuit$, but now the occurrence on the right-hand side of the formula below). See [2, page 617].

$$ c_{\mathit{apal}}(\heartsuit) := \heartsuit \to [!] (K_{\mathfrak{s}}(r \to (K_{\mathfrak{e}}(l \to (K_{\mathfrak{s}}(u \to K_{\mathfrak{e}}(d \to K_{\mathfrak{s}}(l \to K_{\mathfrak{e}}(r \to K_{\mathfrak{s}}(d \to K_{\mathfrak{e}}(u \to \hat{K}_{\mathfrak{s}}(\heartsuit))))))))))$$

For SAPAL this $c_{\mathit{apal}}(\heartsuit)$ is translated into

$$ c_{\mathit{fsapal}}(\heartsuit) := \heartsuit \to [\Lambda_C](K_{\mathfrak{s}}(r \to (K_{\mathfrak{e}}(l \to (K_{\mathfrak{s}}(u \to K_{\mathfrak{e}}(d \to K_{\mathfrak{s}}(l \to K_{\mathfrak{e}}(r \to K_{\mathfrak{s}}(d \to K_{\mathfrak{e}}(u \to \hat{K}_{\mathfrak{s}}(\heartsuit))))))))))$$

For SCAPAL, this $c_{\mathit{apal}}(\heartsuit)$ is translated into the following. Here, it is relevant to observe that in the proof in [2] the witness formula for this occurrence of $[!]$ contains the atoms $\spadesuit, \diamond$ and $\spadesuit$ that do not occur in $c_{\mathit{apal}}(\heartsuit)$. Therefore, without the trivially true conjunct $\supset_{C \cup \Lambda}$ used in the translation, this witness would not have been available. Merely replacing $[!]$ by $[\subseteq]$ in $c_{\mathit{apal}}(\heartsuit)$ would have resulted a formula with a different meaning.

$$ c_{\mathit{scapal}}(\heartsuit) := \heartsuit \to [\subseteq](K_{\mathfrak{s}}(r \to (K_{\mathfrak{e}}(l \to (K_{\mathfrak{s}}(u \to K_{\mathfrak{e}}(d \to K_{\mathfrak{s}}(l \to K_{\mathfrak{e}}(r \to K_{\mathfrak{s}}(d \to K_{\mathfrak{e}}(u \to \hat{K}_{\mathfrak{s}}(\heartsuit)))))))))) \land \supset_{C \cup \Lambda}) $$

For IPAL, $c_{\mathit{apal}}(\heartsuit)$ is translated into:

$$ c_{\mathit{ipal}}(\heartsuit) = \heartsuit \to [\supset\downarrow](K_{\mathfrak{s}}(r \to (K_{\mathfrak{e}}(l \to (K_{\mathfrak{s}}(u \to K_{\mathfrak{e}}(d \to K_{\mathfrak{s}}(l \to K_{\mathfrak{e}}(r \to K_{\mathfrak{s}}(d \to K_{\mathfrak{e}}(u \to \hat{K}_{\mathfrak{s}}(\heartsuit))))))))))$$

## 6 Axiomatization

In this section we report on axiomatizations of the logics under consideration. The known axiomatization of APAL is infinitary (non-RE) [8, 9]. The infinitary axiomatizations of SAPAL (and also of FSAPAL, as a special case) and SCAPAL are straightforward variations of the axiomatization of APAL, and can similarly be proved sound and complete. It requires merely checking very few and very local changes of the completeness proof, as we will see. These axiomatizations we can confidently present as results. It seems the axiomatization of QIPAL (and of IPAL, as a special case) is similarly a variation of that of APAL, but the adjustments there are larger and require checking details in various parts of the completeness proof. It seems then advisable to redo the entire proof, so that the concerned reader can check the correctness of the argument. This is beyond the scope of our current investigation and therefore, as they say, referred to further research. However, the value of such further research may be limited, if the conjectured axiomatization is the only outcome. More adventurous pursuits, such as the reported search for finitary (RE) axiomatizations for APAL variations, may then be worthier.

Let us first present the axiomatization of APAL. The derivation rule involving the quantifier is formulated in terms of so-called necessity forms [24]. Consider a new symbol $\dot{\heartsuit}$. The necessity forms
are defined inductively as follows, where $\varphi$ is a formula in some logical language $\mathcal{L}$ and $a \in A$.

$$ \psi(\sharp) ::= \sharp \mid (\varphi \rightarrow \psi(\sharp)) \mid K_a \psi(\sharp) \mid [\varphi] \psi(\sharp) $$

A necessity form contains a unique occurrence of the symbol $\sharp$. If $\psi(\sharp)$ is a necessity form and $\varphi \in \mathcal{L}$, then $\psi(\varphi) \in \mathcal{L}$ is the substitution of $\sharp$ by $\varphi$ in $\psi(\sharp)$.

## DEFINITION 6.1

([8, 9]).

The axiomatization **APAL** of APAL consists of the following axioms and rules. In the rule **R[!]**, the expressions $\chi$ ($[\psi]\varphi$) and $\chi$ ($[!]\varphi$) are instantiations of a necessity form $\chi$ ($\sharp$).

<table><tr><td><b>P</b></td><td>All propositional tautologies</td><td><b>K</b></td><td>$K_a(\varphi \rightarrow \psi) \rightarrow (K_a\varphi \rightarrow K_a\psi)$</td></tr><tr><td><b>T</b></td><td>$K_a\varphi \rightarrow \varphi$</td><td><b>4</b></td><td>$K_a\varphi \rightarrow K_a K_a\varphi$</td></tr><tr><td><b>5</b></td><td>$\neg K_a\varphi \rightarrow K_a \neg K_a\varphi$</td><td><b>AP</b></td><td>$[\varphi]p \leftrightarrow (\varphi \rightarrow p)$</td></tr><tr><td><b>AN</b></td><td>$[\varphi]\neg\psi \leftrightarrow (\varphi \rightarrow \neg[\varphi]\psi)$</td><td><b>AC</b></td><td>$[\varphi](\psi \land \chi) \leftrightarrow ([\varphi]\psi \land [\varphi]\chi)$</td></tr><tr><td><b>AK</b></td><td>$[\varphi]K_a\psi \leftrightarrow (\varphi \rightarrow K_a[\varphi]\psi)$</td><td><b>AA</b></td><td>$[\varphi][\psi]\chi \leftrightarrow [\varphi \land [\varphi]\psi]\chi$</td></tr><tr><td><b>A[!]</b></td><td>$[!]\varphi \rightarrow [\psi]\varphi$ where $\psi \in \mathcal{L}_{EL}$</td><td><b>MP</b></td><td>From $\varphi$ and $\varphi \rightarrow \psi$ infer $\psi$</td></tr><tr><td><b>NecK</b></td><td>From $\varphi$ infer $K_a\varphi$</td><td><b>NecA</b></td><td>From $\varphi$ infer $[\psi]\varphi$</td></tr><tr><td></td><td></td><td><b>R[!]</b></td><td>From $\chi$ ($[\psi]\varphi$) for all $\psi \in \mathcal{L}_{EL}$ infer $\chi$ ($[!]\varphi$)</td></tr></table>

The soundness and completeness of **APAL** was shown in [8]. An error in that completeness proof was later corrected in [7]. Even later a simplified completeness proof was given in [9]: that will be our further reference. Note that the system in [9] contains an additional derivation rule 'From $\varphi$ infer $[!]\varphi$, that however is derivable in **APAL**.

## DEFINITION 6.2

(Axiomatizations SAPAL and SCAPAL).

The axiomatization **SAPAL** of SAPAL is as **APAL** but where the axiom and rule involving the quantifier are replaced by (where $Q \subseteq P$):

$$ \begin{array}{l} \textbf{A}[\mathcal{Q}] \quad [\mathcal{Q}]\varphi \rightarrow [\psi]\varphi \text{ where } \psi \in \mathcal{L}_{\text{EL}}|\mathcal{Q} \\ \textbf{R}[\mathcal{Q}] \quad \text{From } \chi([\psi]\varphi) \text{ for all } \psi \in \mathcal{L}_{\text{EL}}|\mathcal{Q} \text{ infer } \chi([\mathcal{Q}]\varphi) \end{array} $$

The axiomatization **SCAPAL** of SCAPAL is as **APAL** but where the axiom and rule involving the quantifier are replaced by:

$$ \begin{array}{l} \textbf{A}[\sqsubseteq] \quad [\sqsubseteq]\varphi \rightarrow [\psi]\varphi \text{ where } \psi \in \mathcal{L}_{\text{EL}}|P(\varphi) \\ \textbf{R}[\sqsubseteq] \quad \text{From } \chi([\psi]\varphi) \text{ for all } \psi \in \mathcal{L}_{\text{EL}}|P(\varphi) \text{ infer } \chi([\sqsubseteq]\varphi) \end{array} $$

## PROPOSITION 6.3

The axiomatizations **SAPAL** and **SCAPAL** are sound and complete.

**PROOF.** It suffices to sketch the proof. The soundness of the axiomatizations **SAPAL** and **SCAPAL** is evident as the axiom and the rule follow the semantics of, respectively, the $[\mathcal{Q}]$ and $[\sqsubseteq]$ quantifier. All remaining axioms and rules are standard from PAL. The completeness proof proceeds exactly as in [9], with very minimal changes: the quantifier $[!]$ only features in the subinductive case $[\psi][!]\chi$ and in the inductive case $[!]\psi$ of the proof of the Truth Lemma [9, pages 75–76]. Apart from changing the notation of the quantifier, it suffices to replace four occurrences of the word 'epistemic formulas', i.e. $\psi \in \mathcal{L}_{EL}$, by 'epistemic formulas in $\mathcal{L}_{EL}|\mathcal{Q}$' respectively 'epistemic formulas in
$\mathcal{L}_{EL}|P(\varphi)'$. This minimal change is sufficient because the Truth Lemma for **APAL** is proved by a lexicographic complexity measure wherein $[\psi]\varphi$ is less complex than $[!]\varphi$ for any $\psi \in \mathcal{L}_{EL}$, for the simple reason that $[\psi]\varphi$ contains one less quantifier than $[!]\varphi$. Similarly, $[\psi]\varphi$ is less complex than $[Q]\varphi$ and than $[P(\varphi)]\varphi$ for any $\psi \in \mathcal{L}_{EL}$. No other changes are required in the completeness proof. $\square$

Let us now consider IPAL$^↓$. Given the semantics of the quantifier and Proposition 3.5.4 the candidate axiom and rule are as follows:

$$A[↓↓] [\eta^↓]\varphi \rightarrow [\psi \wedge \eta]\varphi \text{ where } \psi \in \mathcal{L}_{EL}$$

$$R[↓↓] \text{ From } \chi([\psi \wedge \eta]\varphi) \text{ for all } \psi \in \mathcal{L}_{EL} \text{ infer } \chi([\eta^↓]\varphi)$$

This still seems to be sufficient to demonstrate completeness, with, given the presence of an additional formula $\eta$, minor further adjustments of the proof for APAL.

We have not considered the case IPAL$^↑$.

Now consider QIPAL. Instead of the changed axiom and rule above we would now need two rules (and two similar rules for the other quantifier):

$$RA[↓↓] \text{ From } \psi \rightarrow \eta \text{ infer } [\eta^↓]\varphi \rightarrow [\psi]\varphi \text{ where } \psi \in \mathcal{L}_{EL}$$

$$RR[↓↓] \text{ From } \chi([\psi]\varphi) \text{ for all } \psi \in \mathcal{L}_{EL} \text{ such that } \psi \rightarrow \eta, \text{ infer } \chi([\eta^↓]\varphi)$$

It may be that completeness can still be obtained for this system, but this would require more checks, e.g. we appear to need a slightly changed complexity measure in the completeness proof, such that $\psi \rightarrow \eta <_{d\square}^{Size} \chi([\eta^↓]\varphi)$ [9, page 68]. At this stage it therefore seems best to relegate all this to conjectures.

# 7 IPAL, substructural logics and dynamic consequence

## 7.1 Introduction

In this section we discuss the motivation for the (Q)IPAL $↓$-quantifier, connecting it with the implication connective of *substructural logics* [21, 35, 38, 42]. This connection is explored also via a brief study of a *dynamic consequence relation* [44, 45] arising from the notion of IPAL validity.

In a nutshell, our semantics of $[\varphi^↓]\psi$ is loosely inspired by the satisfaction clause for implication in the relational semantics for substructural logic, according to which ‘$\varphi$ implies $\psi$’ is satisfied in a state iff combining that state with any state satisfying $\varphi$ will result in a state satisfying $\psi$. Information update is one natural reading of ‘combining states’ and ‘any state satisfying $\varphi$’ translates in the information update setting into looking at updates with any formula implying $\varphi$. The dynamic consequence relation arising from the notion of IPAL validity is not closed under most of the usual structural rules, nor under substitution, although it satisfies a form of weakening even stronger than that satisfied by van Benthem’s dynamic consequence arising from PAL. Details follow.

## 7.2 Substructural logics and implication

Substructural logics are logics weaker than classical Boolean logic. The name reflects the fact that their Gentzen-style formulations are obtained, roughly speaking, by omitting some (or all) *structural rules* of Gentzen’s sequent calculus for intuitionistic logic, most prominently *weakening* (i), *contraction* (c) and *commutativity* or ‘exchange’ (e)

$$\frac{\Gamma, \Delta \Rightarrow \psi}{\Gamma, \varphi, \Delta \Rightarrow \psi} \quad (i)$$

$$\frac{\Gamma, \varphi, \varphi, \Delta \Rightarrow \psi}{\Gamma, \varphi, \Delta \Rightarrow \psi} \quad (c)$$

$$\frac{\Gamma, \varphi, \chi, \Delta \Rightarrow \psi}{\Gamma, \chi, \varphi, \Delta \Rightarrow \psi} \quad (e).$$
Other structural rules featuring in this contribution are *strong weakening* (si), *left monotonicity* (lm), *cautious monotonicity* (cm) and *reflexivity* (r).

$$ \frac{\Gamma, \Delta \Rightarrow \varphi}{\Gamma, \Sigma, \Delta \Rightarrow \varphi} \text{ (si)} $$

$$ \frac{\Gamma \Rightarrow \varphi}{\psi, \Gamma \Rightarrow \varphi} \text{ (lm)} $$

$$ \frac{\Gamma \Rightarrow \varphi \quad \Gamma, \Delta \Rightarrow \psi}{\Gamma, \varphi, \Delta \Rightarrow \psi} \text{ (cm)} $$

$$ \overline{\Gamma, \varphi \Rightarrow \varphi} \text{ (r)} $$

Substructural logics have general algebraic semantics [21] but—similarly as in modal logic—models of a more concrete kind are better at facilitating fruitful interpretations. Substructural logics also have general *relational semantics* [40, 41], directly inspired by Kripke semantics for modal logic. In order to understand the key aspects of this semantics, one needs to take into account the role played by *implication*, namely, that implication *internalizes consequence* in the sense that

$$ \Gamma, \varphi \Rightarrow \psi \quad \text{iff} \quad \Gamma \Rightarrow \varphi \rightarrow \psi. $$

Relational semantics for substructural logics treat implication as a *binary modal operator*, i.e. the relational models contain a *ternary accessibility relation R* between states (pieces of information) *x, y, z* that is referred to in the satisfaction (denoted $|=$) condition for formulas of the form $\varphi \rightarrow \psi$:

$$ x \models \varphi \rightarrow \psi \quad \text{iff} \quad \text{for all } y \text{ and } z, Rxyz \text{ and } y \models \varphi \text{ imply } z \models \psi. $$

This is an obvious generalization of the standard Kripke satisfaction condition for formulas of the form $\Box \psi$. General readings indicating the relation of the ternary semantics to various notions of conditionality have been proposed in [12]. Another approach (i.e. however, not completely orthogonal to the former one) is to read *R* in terms of *combining pieces of information*. Dunn and Restall point out that:

‘perhaps the best reading [of *Rxyz*] is to say that the combination of the pieces of information *x* and *y* (not necessarily the union) is a piece of information in *z*’ [19, p. 67].

Restall adds that:

‘a body of information warrants $\varphi \rightarrow \psi$ if and only if whenever you *update* that information with new information which warrants $\varphi$, the resulting (perhaps new) body of information warrants $\psi$’ [39, p. 362] (notation adjusted).

On the informational reading, substructural implication clearly resembles an information update operator; see also [3, 4] where it is observed that dynamic epistemic logic can be seen as a two-sorted substructural logic, and that the product update is a special case of the ternary accessibility relation. The question is, what kind of update operator does substructural implication represent? Our semantics of $[\varphi^{\downarrow}]\psi$ modify PAL announcements so that the result reflects the ‘non-determinism’ of substructural implication—in evaluating $\varphi \rightarrow \psi$ at a given state, there is no one ‘canonical’ piece of information representing $\varphi$ that is combined with the given state (think of the truth set of $\varphi$ in the PAL satisfaction clause), but usually a number of them is considered. In the semantics of $[\varphi^{\downarrow}]\psi$ the role of these various pieces of information is played by formulas implying $\varphi$ (or, rather, by truth sets of formulas implying $\varphi$).

The question is, how does this notion compare to substructural implication on the one hand and to PAL announcements on the other. A study of dynamic consequence relations is a particularly useful way of comparison.

## 7.3 *Dynamic consequence*

We now define a novel dynamic consequence relation $\Rightarrow^{\downarrow}$.
### DEFINITION 7.1

(Dynamic consequence).

Let $\Sigma$ be a finite (possibly empty) sequence of EL-formulas and $\varphi$ a EL-formula.

IPAL dynamic consequence $\Sigma \Rightarrow \downarrow \varphi$ iff $\models [\Sigma \downarrow] \varphi$

PAL dynamic consequence $\Sigma \Rightarrow \uparrow \varphi$ iff $\models [\Sigma \uparrow] \varphi$

Relation $\Rightarrow \downarrow$ can be seen as a variant of $\Rightarrow \uparrow$ which is van Benthem's dynamic consequence relation in its 'local' version [44, 45].

We can see that, trivially, the (Q)IPAL $\downarrow$-quantifier internalizes $\Rightarrow \downarrow$ similarly as substructural implication internalizes $\Rightarrow$: we have $\Gamma, \varphi \Rightarrow \downarrow \psi$ iff $\Gamma \Rightarrow \downarrow [\varphi \downarrow] \psi$. As shown below, $\Rightarrow \downarrow$ differs from $\Rightarrow \uparrow$ by satisfying a stronger version of weakening, and it shares with $\Rightarrow \uparrow$ a number of other properties usually not present in substructural consequence relations (such as not being closed under substitution). This shows that, despite certain resemblances, one would need to further modify the (Q)IPAL $\downarrow$-quantifier to mimic substructural implication in a PAL-like setting, and vice versa.

### LEMMA 7.2

$\models [\psi \downarrow] \varphi$ implies $\models [\psi \downarrow \downarrow] [\chi \downarrow] \varphi$.

PROOF. This follows from Proposition 3.8 that $[\psi \downarrow] \varphi \rightarrow [\psi \downarrow \downarrow] [\chi \downarrow] \varphi$. $\square$

We recall from Example 3.9 that $\not\models [\psi \downarrow] \varphi \rightarrow [\chi \downarrow \downarrow] [\psi \downarrow] \varphi$. Despite that, we still have that:

### LEMMA 7.3

$\models [\psi \downarrow] \varphi$ implies $\models [\chi \downarrow \downarrow] [\psi \downarrow] \varphi$.

PROOF. Assume $\models [\psi \downarrow] \varphi$. Now suppose towards a contradiction that $\not\models [\chi \downarrow \downarrow] [\psi \downarrow] \varphi$. Let $(M, s)$ be such that $M, s \not\models [\chi \downarrow \downarrow] [\psi \downarrow] \varphi$. Then there is $\eta$ implying $\chi$ such that $M|\eta, s \not\models [\psi \downarrow] \varphi$. This contradicts assumption $\models [\psi \downarrow] \varphi$. $\square$

### PROPOSITION 7.4

IPAL dynamic consequence is closed under strong weakening (si).

PROOF. Lemma 7.2 says in other words that $\psi \Rightarrow \downarrow \varphi$ implies $\psi \chi \Rightarrow \downarrow \varphi$, whereas Lemma 7.3 says in other words that $\psi \Rightarrow \downarrow \varphi$ implies $\chi \psi \Rightarrow \downarrow \varphi$. We can show that, for arbitrary sequences, $\Gamma, \Delta \Rightarrow \downarrow \varphi$ implies $\Gamma, \Sigma, \Delta \Rightarrow \downarrow \varphi$, by an induction on the length of the sequences involved, using the above sequent representations of Lemma 7.2 and Lemma 7.3. $\square$

As observed by van Benthem, $\Rightarrow \uparrow$ does not satisfy (si). For example, $[\neg K_a p] \neg K_a p$ is valid, but $[\neg K_a p][p] \neg K_a p$ is not valid. This is therefore a difference between $\Rightarrow \downarrow$ and $\Rightarrow \uparrow$.

As a corollary to Proposition 7.4, $\Rightarrow \downarrow$ also satisfies the structural rules *left monotonicity* (lm) and *cautious monotonicity* (cm). These are also satisfied by $\Rightarrow \uparrow$ [45].

Finally note that $\Rightarrow \downarrow$ (as well as $\Rightarrow \uparrow$ or any other conceivable dynamic consequence relation involving public announcements) does not satisfy reflexivity (r). For example, it is elementary that $\models [p \downarrow] p$ (i.e. $p \Rightarrow \downarrow p$), whereas on the other hand, just as elementary, $\not\models [(p \wedge \neg K_a p) \downarrow] (p \wedge \neg K_a p)$. Just as PAL is not closed under substitution, also IPAL is not closed under substitution. Hence, $\Rightarrow \downarrow$ is not a consequence relation in the Tarskian sense.

## 8 Conclusions

We investigated some logics that are almost APAL but not quite: the logics FSAPAL, SCAPAL and IPAL. They distinguish themselves by their widely varying relative expressivity. On the other
hand, their axiomatizations are very similar to that of APAL, and they also have undecidable satisfiability problems. We have shown that the IPAL quantifier, motivated by the satisfaction clause for substurstructural implication, yields a substructural dynamic consequence relation differing from van Benthem's dynamic consequence based on PAL.

**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, H. van Ditmarsch and T. French. The undecidability of quantified announcements. *Studia Logica*, **104**, 597–640, 2016.

[3] G. Aucher. Dynamic epistemic logic as a substructural logic. In *Johan van Benthem on Logic and Information Dynamics*, A. Baltag and S. Smets., eds, pp. 855–880. Springer, 2014.

[4] G. Aucher. Dynamic epistemic logic in update logic. *Journal of Logic and Computation*, **26**, 1913–1960, 2016.

[5] G. Aucher and T. Bolander. Undecidability in epistemic planning. In *Proc. of 23rd IJCAI*, F. Rossi., ed., pp. 27–33, 2013.

[6] R.J. Aumann. Agreeing to disagree. *Annals of Statistics*, **4**, 1236–1239, 1976.

[7] P. Balbiani. Putting right the wording and the proof of the Truth Lemma for APAL. *Journal of Applied Non-Classical Logics*, **25**, 2–19, 2015.

[8] P. Balbiani, A. Baltag, H. van Ditmarsch, A. Herzig, T. Hoshi and T. De Lima. ‘Knowable’ as ‘known after an announcement’. *The Review of Symbolic Logic*, **1**, 305–334, 2008.

[9] P. Balbiani and H. van Ditmarsch. A simple proof of the completeness of APAL. *Studies in Logic*, **8**, 65–78, 2015.

[10] A. Baltag, L. S. Moss and S. Solecki. The logic of public announcements, common knowledge, and private suspicions. In *Proc. of 7th TARK*, pp. 43–56. Morgan Kaufmann, 1998.

[11] A. Baltag, A. Özgün and A. L. Vargas Sandoval. APAL with memory is better. In *Logic, Language, Information, and Computation*, vol. 10944, pp. 106–129, 2018.

[12] Jc. Beall, R. Brady, J. M. Dunn, A. P. Hazen, E. Mares, R. K. Meyer, G. Priest, G. Restall, D. Ripley, J. Slaney and R. Sylvan. On the ternary relation and conditionality. *Journal of Philosophical Logic*, **41**, 595–612, 2012.

[13] R. Berger. *Memoirs of the AMS*. American Mathematical Society, 1966.

[14] P. Blackburn, M. de Rijke and Y. Venema. *Modal Logic*. Cambridge University Press, Cambridge, 2001.

[15] T. Bolander and M.B. Andersen. Epistemic planning for single and multi-agent systems. *Journal of Applied Non-Classical Logics*, **21**, 9–34, 2011.

[16] T. Bolander, T. Charrier, S. Pinchinat and F. Schwarzentruber. Del-based epistemic planning: Decidability and complexity. *Artificial Intelligence*, **287**, 103304, 2020.

[17] T. Charrier and F. Schwarzentruber. Arbitrary public announcement logic with mental programs. In *Proc. of AAMAS*, pp. 1471–1479. ACM, 2015.

[18] M.C. Cooper, A. Herzig, F. Maffre, F. Maris and P. Régnier. The epistemic gossip problem. *Discrete Mathematics*, **342**, 654–663, 2019.

[19] J. M. Dunn and G. Restall. Relevance logic. In *Handbook of Philosophical Logic*, D. M. Gabbay and F. Guenthner., eds, vol. 6, 2nd edn., pp. 1–128. Springer Netherlands, 2002.

[20] T. French and H. van Ditmarsch. Undecidability for arbitrary public announcement logic. In *Advances in Modal Logic* 7, pp. 23–42. College Publications, 2008.
[21] N. Galatos, P. Jipsen, T. Kowalski and H. Ono. *Residuated Lattices: An Algebraic Glimpse at Substructural Logics*. Elsevier, 2007.

[22] R. Galimullin. *Coalition Announcements*. PhD Thesis. University of Nottingham, UK, 2019.

[23] J. D. Gerbrandy and W. Groeneveld. Reasoning about information change. *Journal of Logic, Language, and Information*, **6**, 147–169, 1997.

[24] R. Goldblatt. *Axiomatising the Logic of Computer Programming*. Springer, 1982.

[25] A. Herzig and F. Maffre. How to share knowledge by gossiping. *AI Communications*, **30**, 1–17, 2017.

[26] R. Hilpinen. Remarks on personal and impersonal knowledge. *Canadian Journal of Philosophy*, **7**, 1–9, 1977.

[27] J. Hintikka. *Knowledge and Belief*. Cornell University Press, 1962.

[28] A.-M. Kermarrec and M. van Steen. Gossiping in distributed systems. *SIGOPS Operating Systems Review*, **41**, 2–7, 2007.

[29] A. D. Kshemkalyani and M. Singhal. *Distributed Computing: Principles, Algorithms, and Systems*. Cambridge University Press, New York, NY, USA, 2008.

[30] L. B. Kuijer. How arbitrary are arbitrary public announcements? In *Pristine Perspectives on Logic, Language and Computation*, M. Colinet, S. Katrenko and R. K. Rendsvig., eds, pp. 109–123, 2014.

[31] U. Maurer. Information-theoretic cryptography. In *Advances in Cryptology—CRYPTO '99, LNCS 1666*, M. Wiener., ed., pp. 47–64. Springer, 1999.

[32] J. McCarthy. Formalization of two puzzles involving knowledge. In *Formalizing Common Sense: Papers by John McCarthy*, V. Lifschitz., ed. Ablex Publishing Corporation, Norwood, NJ, 1990.

[33] G. E. Moore. A reply to my critics. In *The Philosophy of G.E. Moore*, pp. 535–677, P. A. Schilpp., ed. Northwestern University, Evanston, 1942.

[34] Y. O. Moses, D. Dolev and J.Y. Halpern. Cheating husbands and other stories: a case study of knowledge, action, and communication. *Distributed Computing*, **1**, 167–176, 1986.

[35] F. Paoli. *Substructural Logics: A Primer*. Springer Netherlands, Dordrecht, 2002.

[36] J. A. Plaza. Logics of public communications. In *Proc. of the 4th ISMIS*, pp. 201–216. Oak Ridge National Laboratory, 1989.

[37] R. Ramanujam and S. P. Suresh. Information based reasoning about security protocols. *Electronic Notes in Theoretical Computer Science*, **55**, 2001.

[38] G. Restall. *An Introduction to Substructural Logics*. Routledge, London, 2000.

[39] G. Restall. Relevant and substructural logics. In *Logic and the Modalities in the Twentieth Century*, D. Gabbay and J. Woods., eds, vol. 7, pp. 289–398. Elsevier, 2006.

[40] R. Routley and R. K. Meyer. Semantics of entailment. In *Truth, Syntax and Modality*, H. Leblanc., ed., pp. 194–243. North Holland, Amsterdam, 1973.

[41] R. Routley, V. Plumwood, R. K. Meyer and R. T. Brady. *Relevant Logics and Their Rivals*, **1**. Ridgeview, 1982.

[42] P. Schröder-Heister and K. Došen., eds. *Substructural Logics*. Clarendon Press, Oxford, 1993.

[43] J. van Benthem. Semantic parallels in natural language and computation. In *Logic Colloquium '87, Proceedings of the Colloquium held in Granada*. Amsterdam, North-Holland, 1989.

[44] J. van Benthem. Structural properties of dynamic reasoning. In *Meaning: The Dynamic Turn*, J. Peregrin., ed., pp. 15–31. Elsevier, Amsterdam, 2003.

[45] J. van Benthem. Logical dynamics meets logical pluralism? *Australasian Journal of Logic*, **6**, 182–209, 2008.
[46] H. van Ditmarsch and T. French. Quantifying over Boolean announcements. *Logical Methods in Computer Science*, **18**, 20, 2022.

[47] H. van Ditmarsch, T. French and J. Hales. Positive announcements. *Studia Logica*, **109**, 639–681, 2021.

[48] H. van Ditmarsch and B. Kooi. The secret of my success. *Synthese*, **151**, 201–232, 2006.

[49] H. van Ditmarsch, M. Liu, L.B. Kuijer and I. Sedlár. Expressivity of some versions of APAL. In M.A. Martins and I. Sedlár., eds, *Dynamic Logic. New Trends and Applications*, pp. 120–136. Springer, 2020. LNCS 12569. https://doi.org/10.1007/978-3-030-65840-3_8

[50] P. van Emde Boas, J. Groenendijk and M. Stokhof. The Conway paradox: its solution in an epistemic framework. In *Truth, Interpretation and Information: Selected Papers From the Third Amsterdam Colloquium*, pp. 159–182. Foris Publications, Dordrecht, 1984.