Asynchronous Announcements

TL;DR

This paper introduces a novel multi-agent epistemic logic for asynchronous announcements, capturing how agents receive and believe announcements over time, with a complete axiomatization and applications to distributed computing.

Contribution

It develops the first complete axiomatization of asynchronous announcement logic, modeling asynchronous message reception and belief updates in multi-agent systems.

Findings

Provides a reduction system for formulas in AA

Models message exchange processes in distributed computing

Demonstrates the logic's completeness and applicability

Abstract

We propose a multi-agent epistemic logic of asynchronous announcements, where truthful announcements are publicly sent but individually received by agents, and in the order in which they were sent. Additional to epistemic modalities the logic contains dynamic modalities for making announcements and for receiving them. What an agent believes is a function of her initial uncertainty and of the announcements she has received. Beliefs need not be truthful, because announcements already made may not yet have been received. As announcements are true when sent, certain message sequences can be ruled out, just like inconsistent cuts in distributed computing. We provide a complete axiomatization for this \emph{asynchronous announcement logic} (AA). It is a reduction system that also demonstrates that any formula in $AA$ is equivalent to one without dynamic modalities, just as for public announcement logic. A detailed example modelling message exchanging processes in distributed computing in $AA$ closes our investigation.

Tables

Table 1. Table 1: Comparing public announcement logic and asynchronous announcement logic

Equations

$$\phi ,\psi :=p\mid \perp \mid \neg \phi \mid (\phi \vee \psi )\mid B_a\phi \mid [\phi ]\psi \mid [a]\phi$$

$$\phi ,\psi :=p\mid \neg p\mid \perp \mid \top \mid (\phi \vee \psi )\mid (\phi \wedge \psi )\mid B_a\phi$$

$$\begin{array}[]{lllllllll}{\parallel}{p}{\parallel}&:=&2&{\parallel}{\varphi\vee\psi}{\parallel}&:=&{\parallel}{\varphi}{\parallel}+{\parallel}{\psi}{\parallel}&{\parallel}{[\varphi]\psi}{\parallel}&:=&2{\parallel}{\varphi}{\parallel}+{\parallel}{\psi}{\parallel}\\ {\parallel}{\bot}{\parallel}&:=&1&{\parallel}{B_{a}\varphi}{\parallel}&:=&{\parallel}{\varphi}{\parallel}+1&{\parallel}{[a]\varphi}{\parallel}&:=&{\parallel}{\varphi}{\parallel}+2\\ {\parallel}{\neg\varphi}{\parallel}&:=&{\parallel}{\varphi}{\parallel}+1\end{array}$$

$$\begin{array}[]{lllllllll}{\parallel}{\epsilon}{\parallel}&:=&0&{\parallel}{\alpha a}{\parallel}&:=&{\parallel}{\alpha}{\parallel}+1&{\parallel}{\alpha\psi}{\parallel}&:=&{\parallel}{\alpha}{\parallel}+{\parallel}{\psi}{\parallel}\end{array}$$

$$\begin{array}[]{llllll}\deg(p)&=&0&\deg(B_{a}\varphi)&=&\deg(\varphi)+1\\ \deg(\bot)&=&0&\deg([\varphi]\psi)&=&\deg(\varphi)+\deg(\psi)\\ \deg(\neg\varphi)&=&\deg(\varphi)&\deg([a]\varphi)&=&\deg(\varphi)\\ \deg(\varphi\vee\psi)&=&\max\{\deg(\varphi),\deg(\psi)\}\end{array}$$

$$\begin{array}[]{lll}\deg(\alpha,\varphi)&=&\deg([\alpha]\varphi)\end{array}$$

$$\begin{array}[]{lllll}(\alpha,\varphi)\ll(\beta,\psi)&\text{iff}&\text{either}&\deg(\alpha,\varphi)<\deg(\beta,\psi),\\ &&\text{or}&\deg(\alpha,\varphi)=\deg(\beta,\psi)\text{ and }{\parallel}{\alpha}{\parallel}+{\parallel}{\varphi}{\parallel}<{\parallel}{\beta}{\parallel}+{\parallel}{\psi}{\parallel}.\end{array}$$

$$\begin{array}[]{lcl}s\bowtie\epsilon\\ s\bowtie\alpha a&\text{iff}&s\bowtie\alpha\text{ and }{\mid}{\alpha}{\mid}_{a}<{\mid}{\alpha}{\mid}_{!}\\ s\bowtie\alpha\psi&\text{iff}&s\bowtie\alpha\text{ and }s,\alpha\models\psi\\ \\ s,\alpha\models p&\text{iff}&s\in V(p)\\ s,\alpha\not\models\bot\\ s,\alpha\models\neg\varphi&\text{iff}&s,\alpha\not\models\varphi\\ s,\alpha\models\varphi\vee\psi&\text{iff}&s,\alpha\models\varphi\text{ or }s,\alpha\models\psi\\ s,\alpha\models B_{a}\varphi&\text{iff}&t,\beta\models\varphi\text{ for all }t\in W\ \text{and for all histories}\ \beta\\ &&\text{such that }sR_{a}t,\alpha\triangleright_{a}\beta,\text{ and }t\bowtie\beta\\ s,\alpha\models[\varphi]\psi&\text{iff}&s,\alpha\models\varphi\text{ implies }s,\alpha\varphi\models\psi\\ s,\alpha\models[a]\varphi&\text{iff}&{\mid}{\alpha}{\mid}_{a}<{\mid}{\alpha}{\mid}_{!}\text{ implies }s,\alpha a\models\varphi\end{array}$$

$$\begin{array}[]{lcl}W^{s\alpha}&:=&\{(t,\beta)\mid t\in W\ \text{and}\ \alpha\triangleright\beta\ \text{and}\ t\bowtie\beta\},\\ (t,\beta)R^{s\alpha}_{a}(t^{\prime},\beta^{\prime})&\text{:iff}&tR_{a}t^{\prime}\text{ and }\beta\triangleright_{a}\beta^{\prime},\\ (t,\beta)\in V^{s\alpha}(p)&\text{:iff}&t\in V(p).\end{array}$$

$$(A7)[\alpha ]B_a\phi \leftrightarrow [\alpha ]\perp \vee \bigwedge \{B_a[\beta ]\phi \mid \alpha {▹}_a\beta \}$$

$$[\phi a]B_a\psi \leftrightarrow [\phi a]\perp \vee \bigwedge \{B_a[\beta ]\psi \mid \phi a{▹}_a\beta \},$$

$$[\phi a]B_a\psi \leftrightarrow [\phi a]\perp \vee \bigwedge \{B_a[\phi aB]\psi \mid B\subseteq A\setminus a\},$$

$$[\phi ][a]B_a\psi \leftrightarrow (\phi \to B_a[\phi ][a]\psi ).$$

$$(s,\alpha ){\mathbf{R}}_a(t,\beta )\text{ iff }s{R}_{a}t,\alpha {▹}_a\beta ,\text{ and }t\bowtie \beta$$

$$\begin{array}[]{llll}\text{if}&sR_{a}t,&\alpha\triangleright_{a}\beta,&t\bowtie\beta,\\ \text{and}&tR_{a}u,&\beta\triangleright_{a}\gamma,&u\bowtie\gamma,\\ \text{then}&sR_{a}u,&\alpha\triangleright_{a}\gamma,&u\bowtie\gamma\end{array}$$

$$\begin{array}[]{llll}\text{if}&sR_{a}t,&\alpha\triangleright_{a}\beta,&t\bowtie\beta,\\ \text{and}&sR_{a}u,&\alpha\triangleright_{a}\gamma,&u\bowtie\gamma,\\ \text{then}&tR_{a}u,&\beta\triangleright_{a}\gamma,&u\bowtie\gamma\end{array}$$

$$\neg {Kw}_i{m}_i\wedge K_i(m_a\vee m_b\vee m_c)$$

$$\begin{array}[]{lll}\neg\mathit{Kw}_{i}m_{i}&\wedge&K_{i}(\neg\mathit{Kw}_{a}\wedge K_{a}(m_{a}\vee m_{b}\vee m_{c})\wedge\\ &&K_{i}(\neg\mathit{Kw}_{b}\wedge K_{b}(m_{a}\vee m_{b}\vee m_{c})\wedge\\ &&K_{i}(\neg\mathit{Kw}_{c}\wedge K_{c}(m_{a}\vee m_{b}\vee m_{c})\end{array}$$

$$\begin{array}[]{lll}W^{\prime}&=&\{(s,\beta)\mid s\in W,\beta\text{ a history such that }\beta{\upharpoonright}_{!}\subseteq\alpha{\upharpoonright}_{!},\text{and}\ s\bowtie\beta\}\\ (s,\beta)R^{\prime}_{a}(t,\gamma)&\text{iff}&sR_{a}t\ \text{and}\ \beta=\gamma\\ (s,\beta)R^{\prime}_{\varphi}(t,\gamma)&\text{iff}&s=t\ \text{and}\ \beta\varphi=\gamma\\ (s,\beta)R^{\prime}_{[a]}(t,\gamma)&\text{iff}&s=t\ \text{and}\ \beta{a}=\gamma\\ (s,\beta)R^{\prime}_{\triangleright_{a}}(t,\gamma)&\text{iff}&s=t\ \text{and}\ \beta\triangleright_{a}\gamma\\ V^{\prime}(p)&=&\{(s,\beta)\in W^{\prime}\mid s\in V(p)\}\end{array}$$

$$\begin{array}[]{lll}M^{\alpha{\upharpoonright}_{!}},s,\beta\models[\varphi]\psi&\text{iff}&\text{if}\ \beta\varphi{\upharpoonright}_{!}\subseteq\alpha{\upharpoonright}_{!}\ \text{then}\\ &&M^{\alpha{\upharpoonright}_{!}},t,\gamma\models\psi\text{ for all }(t,\gamma)\text{ such that }(s,\beta)R^{\prime}_{\varphi}(t,\gamma),\\ &&\text{else}\\ &&M^{\beta\varphi{\upharpoonright}_{!}},s,\beta\models[\varphi]\psi\\ M^{\alpha{\upharpoonright}_{!}},s,\beta\models B_{a}\psi&\text{iff}&M^{\alpha{\upharpoonright}_{!}},t,\gamma\models\psi\text{ for all }(t,\gamma)\ \text{such that}\ (s,\beta)R^{\prime}_{a}(t,\gamma)\ \text{and}\ (s,\beta)R^{\prime}_{\triangleright_{a}}(t,\gamma)\\ M^{\alpha{\upharpoonright}_{!}},s,\beta\models[a]\psi&\text{iff}&M^{\alpha{\upharpoonright}_{!}},t,\gamma\models\psi\text{ for all }(t,\gamma)\ \text{such that}\ (s,\beta)R^{\prime}_{[a]}(t,\gamma)\end{array}$$

$$\alpha a\beta {▹}_b\delta \text{ iff }\delta {\upharpoonright }_{!b}=\delta {\upharpoonright }_{!}=\alpha a\beta {\upharpoonright }_{!b}\text{ iff }\delta {\upharpoonright }_{!b}=\delta {\upharpoonright }_{!}=\alpha \beta {\upharpoonright }_{!b}\text{ iff }\alpha \beta {▹}_b\delta .\text{vspace}-.9cm$$

Full text

We provide a complete axiomatization for this asynchronous announcement logic ($AA$). It is a reduction system that also demonstrates that any formula in $AA$ is equivalent to one without dynamic modalities, just as for public announcement logic. A detailed example modelling message exchanging processes in distributed computing in $AA$ closes our investigation.

1 Introduction

What does an agent know and how does its knowledge change in a distributed system consisting of multiple agents that act independently from one another and wherein each agent may keep its own time? Agents’ knowledge may change while they send and receive messages to each other and they may also receive messages from the environment, under conditions of temporal uncertainty. Such notions of asynchronous knowledge and of asynchronous common knowledge have been investigated in depth in distributed computing [5, 10, 15, 16, 19] and in temporal epistemic logics to describe their behaviour [6, 12, 20, 23]. Dynamic Epistemic Logic ($DEL$) [3, 33, 4, 26, 30] (or online references such as https://en.wikipedia.org/wiki/Dynamic_epistemic_logic and https://plato.stanford.edu/entries/dynamic-epistemic/) is a modal logic of knowledge and change of knowledge that models observation, i.e., receiving messages, and that has no notion of time, i.e., no temporal modalities. $DEL$ was thought to enforce synchrony [29, 27]. However, more recent studies revealed different ways for $DEL$ to accommodate asynchrony.

In the first place, agents may be uncertain about the number of actions that have already taken place: this is asynchrony due to partial observation, causing indistinguishable histories (sequences of messages) of different length. A framework for such asynchrony was convincingly presented in [7], wherein they demonstrated that the supposed synchronicity of $DEL$ was a mere artifact of the [29] embedding of $DEL$ into synchronous temporal epistemic logics, namely caused by a non-standard interpretation of the Pnueli perfect recall axiom. Asynchrony of that kind is implicit in many $DEL$ scenarios. For example, in gossip protocols agents communicate by calling each other, so that $a$ may have called $b$ without another agent $c$ noticing that the call took place. Such fully distributed gossip is modelled in [1]. For another example, in the ‘One hundred prisoners and a light bulb’ riddle agents communicate asynchronously by individually toggling a light bulb out of sight and hearing of other agents [34]. As a final example, the immediate snapshot algorithm, wherein agents are unaware of other agents possibly simultaneously accessing a shared memory location, has been modelled in $DEL$ by [11].

A different kind of asynchrony results when the sending and receiving of messages are separate, so that the receiver is uncertain about the moment a received message was sent. To our knowledge, the asynchronous reception of messages broadcast by the environment has only been modelled in $DEL$ by [13, 14, 25] — from here on we refer to the reference journal version [14] only. Our proposal further develops a preliminary version, see https://arxiv.org/abs/1705.03392v2, presented at the workshop Strategic Reasoning (SR 2017) in Liverpool. It builds on the protocol-generated forest of [29, 32] and the history-based structures of [21], as well as the asynchronous knowledge and concurrent common knowledge of [6, 12, 18, 20]. Like [14] we assume that announcements are still broadcast to all agents, but individually received. Unlike [14] our epistemic notion is interpreted over past messages only, and we provide an axiomatization by way of a reduction to the modal fragment, just as for public announcement logic [22]. Before we delve further into technical particulars, let us first continue with a detailed example illustrating our approach.

Consider two agents Anne ($a$) and Bill ($b$), and two propositional variables ${p}$ and ${q}$. Anne knows the truth about ${p}$ and Bill knows the truth about ${q}$, and this is common knowledge between them. We can encode this uncertainty in a Kripke model (Figure 1(i)). In public announcement logic ($PAL$) [22] we can formalize that after the announcement of $p\vee q$, Bill does not know that ${p}$ is true but Anne considers it possible that he knows, namely as $[p\vee{q}](\neg B_{b}{p}\wedge\hat{B}_{a}B_{b}{p})$. (The formula $\neg B_{b}{p}\wedge\hat{B}_{a}B_{b}{p}$ would be true if $p$ and $q$ were initially both true.) Operator $[{p}\vee{q}]$ is a dynamic modality interpreted by model restriction. The (knowledge or belief) modalities bound by it are interpreted in the restriction (Figure 1(pal)), not in the original model.

Let us now assume that announcements are still publicly sent, but individually received. Then, after the announcement $p\vee q$ is made (Figure 1(ii)), Anne may have received that information ${p}\vee{q}$ but Bill not yet (Figure 1(iii)), after which Bill receives it too (Figure 1(iv)). Unlike in Figure 1(pal), in (iv) they do not know that the other knows; there is no common knowledge between them of $p\vee q$.

Separating sending from receiving messages permits a notion of asynchronous knowledge in $DEL$, that is a function of the usual modal accessibility but also of uncertainty over the announcements received by other agents. In (iii), after receiving announcement $p\vee q$, Anne considers it possible that Bill knows $p$, namely if the state is $p\overline{q}$ and if Bill has also received the announcement, as in (iv). For different reasons she also considers it possible that Bill does not know $p$. Firstly, if the state is $pq$ (or $\overline{p}q$) and the announcement has been received by Bill (iv)). But, secondly, also if the actual state is $p\overline{q}$ and the announcement has not yet been received by Bill (iii), in which case Bill still considers it possible that the state is $\overline{p}\overline{q}$. And what Anne knows in (iii) should be the same as what she knows in (iv).

What does Bill know? According to usage in distributed computing [12], even when Bill has not received the announcement $p\vee q$, he can imagine that such a message has been sent and that Anne has received it. Therefore, although he is uncertain about $p$ (i), he should consider it possible that announcement $p\vee q$ was made (ii), and that Anne has received it (iii), that she therefore considers it possible that he has received it too (iv), and that he therefore now knows that $p$. This notion of knowledge does not seem to fit well a setting wherein the messages are announcements, whose role is to reduce uncertainty of the value of unchanging facts. It well fits the setting of distributed computing wherein messages that are broadcast, i.e., announcements, contain novel facts. In $PAL$ the future is predictable: all facts may become known. In our setting, this only allows for weak forms of higher-order knowledge: an agent cannot know that another agent remains ignorant.

We therefore focus on what agents know based on the announcements they have received so far, ignoring possible future announcements. That means that in situations (i), (ii), (iii) above, Bill ‘knows’ that Anne knows that he is uncertain about $p$, as he has not received the announcement $p\vee q$. In (i) and (ii) this is true, but in (iii) this is no longer true. Bill’s knowledge is then incorrect belief. Indeed, the asychronous epistemic notion that we propose is one of asynchronous belief (however, as we will see, of the special kind that many such beliefs will eventually become knowledge). Other defining assumptions of our asynchronous semantics are that agents receive the announcements in the order in which they are made, as is not uncommon in distributed computing [12, 20]; and that announcements are true when sent, as in $PAL$.

The assumption that announcements are true when sent, results in partial synchronization. Let us suppose that Anne and Bill are both uncertain about $p$. Then, announcement $p$ is followed by announcement $\neg B_{b}p$. If Anne received $p$ and $\neg B_{b}p$, she should not consider it possible that Bill has received $p$ before the second announcement was made. In other words, the histories of sending and receiving events that she considers possible include $pa(\neg B_{b}p)ba$ and $p(\neg B_{b}p)aab$, but exclude $pb(\neg B_{b}p)aa$ and $pab(\neg B_{b}p)ba$ where the first $a$ in the sequence stands for Anne receiving the first announcement $p$, the second $a$ stands for her receiving the second announcement $\neg B_{b}p$, and similarly for $b$. In terms of [20], $pb(\neg B_{b}p)aa$ and $pab(\neg B_{b}p)ba$ would be called inconsistent cuts. In order for second announcement $\neg B_{b}p$ to be truthful, Bill must still be uncertain about $p$, and for Bill to remain uncertain about $p$ he must not yet have received the first announcement $p$. We will introduce a so-called ‘agreement’ relation between states and histories, and we then say that a state $s$ in the model does not agree with history $pb(\neg B_{b}p)aa$. Agents only consider histories possible that agree with the states they consider possible. This requires to define a satisfaction relation and such an agreement relation by simultaneous induction.

Intuitively, summing up, in our approach an agent knows/believes $\varphi$ iff $\varphi$ is true: (1) in all states that it considers possible, (2) for all prefixes of announcement sequences that other agents may have received, (3) taking into account that the announcements it received were true when sent, (4) while ignoring that other agents may have received more announcements than itself.

We now present an outline of our contribution. Section 2 defines the syntax and Section 3 defines the semantics of asynchronous announcement logic $AA$. In particular, Section 3.5 relates $AA$ to basic modal logic. Section 4 discusses the axiomatization: Section 4.1 provides an axiomatization of $AA$ on the class of models with empty histories, and Section 4.2 provides rewrite rules on the class of models with arbitrary histories. Section 5 obtains results for the model class $\mathcal{S}5$, elaborates on the difference between knowledge and belief, and compares our proposal with various dynamic and temporal epistemic logics and with distributed computing. Section 6 models a typical scenario of message sending agents in distributed computing.

2 Syntax

2.1 Language of asynchronous announcement logic

Definition 1** (Language of AA)**

Let $P$ be a countable set of atoms (denoted $p$, $q$, etc.) and $A$ be a finite set of agents (denoted $a$, $b$, etc.). The language ${\mathcal{L}}_{aa}$ of asynchronous announcement logic is defined as follows:

[TABLE]

We will follow the standard rules for omission of the parentheses. Without the constructs $[a]\cdot$ we get the language ${\mathcal{L}}_{pal}$ of public announcement logic and without the construct $[\varphi]\cdot$ as well we get the language ${\mathcal{L}}_{ml}$ of multi-agent modal logic. The positive fragment ${\mathcal{L}}_{ml}^{+}$ of ${\mathcal{L}}_{ml}$ is defined as follows:

[TABLE]

We will use the standard abbreviations for the Boolean constructs. We will also use the following constructs: $\langle a\rangle\varphi:=\neg[a]\neg\varphi$, $\langle\varphi\rangle\psi:=\neg[\varphi]\neg\psi$ and $\hat{B}_{a}\varphi:=\neg B_{a}\neg\varphi$. For $B_{a}\varphi$ read “agent $a$ believes/knows $\varphi$,” for $[\varphi]\psi$ read “after public announcement $\varphi$ has been sent/made, $\psi$,” and for $[a]\varphi$ read “after agent $a$ receives/reads the next announcement, $\varphi$.” For all formulas $\eta,\psi$ and for all atoms $p$, we denote by $\eta(p/\psi)$ the uniform substitution of the occurrences of $p$ in $\eta$ by $\psi$.

Consider $A\cup{\mathcal{L}}_{aa}$ as an alphabet, with agents and formulas as letters. Variables for words in this language are $\alpha,\beta,\dots$. The empty word is denoted $\epsilon$. Given a word $\alpha$ over $A\cup{\mathcal{L}}_{aa}$, ${\mid}{\alpha}{\mid}$ is its length, ${\mid}{\alpha}{\mid}_{a}$ is the number of its $a$’s for each $a\in A$, ${\mid}{\alpha}{\mid}_{!}$ is the number of its formula occurrences, $\alpha{\upharpoonright}_{!}$ is the projection of $\alpha$ to ${\mathcal{L}}_{aa}$, and $\alpha{\upharpoonright}_{!a}$ is the restriction of $\alpha{\upharpoonright}_{!}$ to the first $|\alpha|_{a}$ formulas. (We use the symbol ‘!’ here because in $PAL$ expression $!\varphi$ often represents “the announcement is $\varphi$”.) These notions have obvious inductive definitions. We say that a word $\beta$ is a prefix of a word $\alpha$ (in symbols $\alpha\subseteq\beta$) if $\beta$ is an initial sequence of $\alpha$. Obviously, for all words $\alpha,\beta$, $\alpha\subseteq\alpha$ and if $\beta\subseteq\alpha$, then for all $a\in A$ and $\psi\in{\mathcal{L}}_{aa}$, $\beta\subseteq\alpha{a}$ and $\beta\subseteq\alpha\psi$. Given a word $\alpha$ and $n\in\mathbb{N}$, $\alpha^{n}$ denotes a concatenation of $n$ copies of $\alpha$.

Let $\alpha$ be a word over $A\cup{\mathcal{L}}_{aa}$. In the single-agent case, when $A=\{a\}$, it is clear that ${\mid}{\alpha}{\mid}={\mid}{\alpha}{\mid}_{a}+{\mid}{\alpha}{\mid}_{!}$. Otherwise, in the multi-agent case, when $|A|\geq 2$, considering an enumeration $(a_{1},\ldots,a_{n})$ of $A$ without repetition, ${\mid}{\alpha}{\mid}={\mid}{\alpha}{\mid}_{a_{1}}+\ldots+{\mid}{\alpha}{\mid}_{a_{n}}+{\mid}{\alpha}{\mid}_{!}$.

Definition 2** (History)**

A word $\alpha$ in the language $A\cup{\mathcal{L}}_{aa}$ is a history if for all prefixes $\beta\subseteq\alpha$ and for all $a\in A$, ${\mid}\beta{\mid}_{!}\geq{\mid}\beta{\mid}_{a}$.

Obviously, if $\beta$ is a prefix of a history $\alpha$, then $\beta$ is a history too. In the definition of histories, the requirement “for all $a\in A$, ${\mid}\beta{\mid}_{!}\geq{\mid}\beta{\mid}_{a}$” means that, for all $n\in\mathbb{N}$, if there is an $n$-th occurrence of agent $a$ in $\alpha$, then there is a prior $n$-th formula in $\alpha$ that will be the announcement then received by agent $a$. This match will be used in the semantics.

Definition 3** (View relation)**

Let $\alpha,\beta$ be histories and $a\in A$. We define: $\alpha\triangleright_{a}\beta$ iff $\beta{\upharpoonright}_{!}=\beta{\upharpoonright}_{!a}=\alpha{\upharpoonright}_{!a}$.  The set $\mathsf{view}_{a}(\alpha):=\{\beta\mid\alpha\triangleright_{a}\beta\}$ is the view of $a$ given $\alpha$.

Observe that, for all $a\in A$, if $\alpha\triangleright_{a}\beta$ then ${\beta}{\upharpoonright}_{!}$ is a prefix of ${\alpha}{\upharpoonright}_{!}$. Informally, the view of agent $a$ given history $\alpha$ consists of all the different ways in which $a$ can receive the announcements in $\alpha$. In other words, the view of $a$ given $\alpha$ consists of the histories $a$ considers possible but without taking the meaning of the announcements in the history into account, which, as we will see, results in a further restriction. In Section 5 we will present an alternative for the view relation, without the requirement that ${\mid}{\beta}{\mid}_{!}={\mid}{\alpha}{\mid}_{a}$.

Example 4

Let us have two agents, $A=\{a,b\}$, and let the history be $\alpha=(p\vee q)a$. Then $\mathsf{view}_{a}(\alpha)$, the set of all histories $\beta$ such that $\alpha\triangleright_{a}\beta$, is $\{(p\vee q)ab,(p\vee q)ba,(p\vee q)a\}$, whereas $\mathsf{view}_{b}(\alpha)=\{\epsilon\}$. Let now $\alpha^{\prime}=(p\vee q)ab$. Then $\mathsf{view}_{a}(\alpha^{\prime})=\{(p\vee q)ab,(p\vee q)ba,(p\vee q)a\}$ and $\mathsf{view}_{b}(\alpha^{\prime})=\{(p\vee q)ab,(p\vee q)ba,(p\vee q)b\}$.

The following alternative characterizations of the $\triangleright_{a}$ relation will be useful. The proof is left to the reader.

Lemma 5

Let $\alpha,\beta$ be histories and $a\in A$. The following conditions are equivalent:

${\mid}{\beta}{\mid}_{a}={\mid}{\alpha}{\mid}_{a}$, ${\beta}{\upharpoonright}_{!a}={\alpha}{\upharpoonright}_{!a}$ and ${\mid}{\beta}{\mid}_{!}={\mid}{\alpha}{\mid}_{a}$; 2. 2.

${\mid}\beta{\mid}_{a}={\mid}\alpha{\mid}_{a}$* and $\beta{\upharpoonright}_{!}=\alpha{\upharpoonright}_{!a}$;* 3. 3.

$\beta{\upharpoonright}_{!}=\beta{\upharpoonright}_{!a}=\alpha{\upharpoonright}_{!a}$.

We can introduce modalities for histories by abbreviation, using reception and announcement modalities of the form $[a]$ and $[\psi]$. For all words $\alpha$ over $A\cup{\mathcal{L}}_{aa}$, the modality $[\alpha]$ is inductively defined as: $[\epsilon]\varphi:=\varphi$, $[\alpha a]\varphi:=[\alpha][a]\varphi$, and $[\alpha\psi]\varphi:=[\alpha][\psi]\varphi$; whereas its dual $\langle\alpha\rangle\varphi$ is defined by abbreviation as $\neg[\alpha]\neg\varphi$. We will read $[\alpha]\varphi$ as “if the sequence $\alpha$ of events can be executed then $\varphi$ holds after its execution,” whereas we will read $\langle\alpha\rangle\varphi$ as “the sequence $\alpha$ of events can be executed and $\varphi$ holds after its execution”. Clearly, for all words $\alpha$ over $A\cup{\mathcal{L}}_{aa}$, for all $a\in A$ and for all $\varphi,\psi\in{\mathcal{L}}_{aa}$, $[a\alpha]\varphi$ is an abbreviation of $[a][\alpha]\varphi$, $\langle a\alpha\rangle\varphi$ of $\langle a\rangle\langle\alpha\rangle\varphi$, $[\psi\alpha]\varphi$ to $[\psi][\alpha]\varphi$, and $\langle\psi\alpha\rangle\varphi$ of $\langle\psi\rangle\langle\alpha\rangle\varphi$.

2.2 Results for histories

We continue with some basic results for histories that will be used later.

Lemma 6

Let $\alpha,\beta$ be histories. For all $a,b\in A$, if $\alpha\triangleright_{a}\beta$ then ${\mid}\beta{\mid}_{b}\leq{\mid}\alpha{\mid}_{a}$.

{proof}

Let $a,b\in A$ be such that ${\alpha}{\triangleright_{a}}{\beta}$. Hence, ${\mid}\beta{\mid}_{!}={\mid}\alpha{\mid}_{a}$. Since $\beta$ is a history, ${\mid}\beta{\mid}_{!}\geq{\mid}\beta{\mid}_{b}$. Since ${\mid}\beta{\mid}_{!}={\mid}\alpha{\mid}_{a}$, ${\mid}\beta{\mid}_{b}\leq{\mid}\alpha{\mid}_{a}$.

Lemma 7

Let $\alpha,\beta$ be histories, and $a\in A$.

If $\epsilon\triangleright_{a}\alpha$ then $\alpha=\epsilon$, 2. 2.

if $\alpha\triangleright_{a}\beta$ then $\beta\triangleright_{a}\beta$.

{proof}

Suppose $\epsilon\triangleright_{a}\alpha$. Hence, ${\mid}\alpha{\mid}_{!}={\mid}\epsilon{\mid}_{a}=0$. Since $\alpha$ is a history, for all $b\in A$, ${\mid}\alpha{\mid}_{!}\geq{\mid}\alpha{\mid}_{b}$, and thus $|\alpha|_{b}=0$. Consequently, $\alpha=\epsilon$. 2. 2.

Suppose $\alpha\triangleright_{a}\beta$. Hence, ${\mid}\beta{\mid}_{a}={\mid}\alpha{\mid}_{a}$ and ${\mid}\beta{\mid}_{!}={\mid}\alpha{\mid}_{a}$. Thus, ${\mid}\beta{\mid}_{!}={\mid}\beta{\mid}_{a}$. Consequently, $\beta\triangleright_{a}\beta$.

Given history $\alpha$ and agent $a$, we recursively define a word $\alpha_{a}$ as follows:

• •

$\epsilon_{a}=\epsilon$;

• •

$(\alpha\varphi)_{a}=\alpha_{a}$;

• •

$(\alpha b)_{a}=\alpha_{a}$ for each $b\in A\setminus\{a\}$;

• •

for all $n>0$, $(\alpha ba^{n})_{a}=(\alpha a^{n})_{a}$ for each $b\in A\setminus\{a\}$;

• •

for all $n>0$, if $|\alpha\varphi a^{n}|_{!}=|\alpha\varphi a^{n}|_{a}$ then $(\alpha\varphi a^{n})_{a}=\alpha\varphi a^{n}$ else $(\alpha\varphi a^{n})_{a}=(\alpha a^{n})_{a}$.

Informally, $\alpha_{a}$ is the concatenation of the prefix $\gamma$ of $\alpha$ until the $|\alpha|_{a}$-th occurrence of a formula in $\alpha$ with $|\alpha|_{a}-|\gamma|_{a}$ times the letter $a$.

Lemma 8

For all histories $\alpha$ and for all agents $a$, $\alpha_{a}$ is a history such that $\alpha\triangleright_{a}\alpha_{a}$

{proof}

The proof is by $<$-induction on ${\mid}\alpha{\mid}$.

Proposition 9** (The view relation is serial, transitive, and Euclidean)**

Let $\alpha$, $\beta$ and $\gamma$ be histories. For all agents $a$,

there is a history $\delta$ such that $\alpha\triangleright_{a}\delta$, namely $\alpha_{a}$, 2. 2.

if $\alpha\triangleright_{a}\beta$ and $\beta\triangleright_{a}\gamma$ then $\alpha\triangleright_{a}\gamma$, 3. 3.

if $\alpha\triangleright_{a}\beta$ and $\alpha\triangleright_{a}\gamma$ then $\beta\triangleright_{a}\gamma$.

{proof}

By Lemma 8. 2. 2.

Suppose $\alpha\triangleright_{a}\beta$ and $\beta\triangleright_{a}\gamma$. Hence, ${\mid}\beta{\mid}_{a}={\mid}\alpha{\mid}_{a}$, $\beta{\upharpoonright}_{!a}=\alpha{\upharpoonright}_{!a}$, ${\mid}\gamma{\mid}_{a}={\mid}\beta{\mid}_{a}$, $\gamma{\upharpoonright}_{!a}=\beta{\upharpoonright}_{!a}$ and ${\mid}\gamma{\mid}_{!}={\mid}\beta{\mid}_{a}$. Thus, ${\mid}\gamma{\mid}_{a}={\mid}\alpha{\mid}_{a}$, $\gamma{\upharpoonright}_{!a}=\alpha{\upharpoonright}_{!a}$ and ${\mid}\gamma{\mid}_{!}={\mid}\alpha{\mid}_{a}$. Consequently, $\alpha\triangleright_{a}\gamma$. 3. 3.

Suppose $\alpha\triangleright_{a}\beta$ and $\alpha\triangleright_{a}\gamma$. Hence, ${\mid}\beta{\mid}_{a}={\mid}\alpha{\mid}_{a}$, $\beta{\upharpoonright}_{!a}=\alpha{\upharpoonright}_{!a}$, ${\mid}\gamma{\mid}_{a}={\mid}\alpha{\mid}_{a}$, $\gamma{\upharpoonright}_{!a}=\alpha{\upharpoonright}_{!a}$ and ${\mid}\gamma{\mid}_{!}={\mid}\alpha{\mid}_{a}$. Thus, ${\mid}\gamma{\mid}_{a}={\mid}\beta{\mid}_{a}$, $\gamma{\upharpoonright}_{!a}=\beta{\upharpoonright}_{!a}$ and ${\mid}\gamma{\mid}_{!}={\mid}\beta{\mid}_{a}$. Consequently, $\beta\triangleright_{a}\gamma$.

From Proposition 9, we obtain:

Corollary 10

For all histories $\alpha,\beta$ and for all agents $a$, if $\alpha\triangleright_{a}\beta$ then $\alpha_{a}\triangleright_{a}\beta$ and $\beta\triangleright_{a}\alpha_{a}$.

Lemma 11

*Let $\alpha,\beta$ be histories. In the single-agent case, if ${\alpha}{\triangleright_{a}}{\beta}$ then ${\mid}{\beta}{\mid}=2{\mid}{\alpha}{\mid}_{a}$. Otherwise, in the multi-agent case, if ${\alpha}{\triangleright_{a}}{\beta}$ then $2{\mid}{\alpha}{\mid}_{a}\leq{\mid}{\beta}{\mid}\leq(|A|+1){\mid}{\alpha}{\mid}_{a}$. *

{proof}

In the single-agent case, suppose $\alpha\triangleright_{a}\beta$. Hence, ${\mid}{\beta}{\mid}_{a}={\mid}{\alpha}{\mid}_{a}$ and ${\mid}{\beta}{\mid}_{!}={\mid}{\alpha}{\mid}_{a}$. Thus, ${\mid}{\beta}{\mid}=2{\mid}{\alpha}{\mid}_{a}$. In the multi-agent case, suppose ${\alpha}{\triangleright_{a}}{\beta}$. Hence, by Lemma 6, for all $b\in A\setminus\{a\}$, ${\mid}\beta{\mid}_{b}\leq{\mid}\alpha{\mid}_{a}$. Moreover, ${\mid}\beta{\mid}_{a}={\mid}\alpha{\mid}_{a}$ and ${\mid}\beta{\mid}_{!}={\mid}\alpha{\mid}_{a}$. Thus, $2\cdot{\mid}\alpha{\mid}_{a}\leq{\mid}\beta{\mid}\leq(|A|+1)\cdot{\mid}\alpha{\mid}_{a}$.

Since $A$ is finite, by Lemma 11, the relation ${\triangleright_{a}}$ is image-finite. But we can do better. Let $X$ and $Y$ be distinct symbols. A Dyck word is a string consisting, for some $n\in\mathbb{N}$, of $n$ $X$’s and $n$ $Y$’s such that no prefix of the string has more $Y$’s than $X$’s. This matches exactly our histories of announcements ($X$) and read actions ($Y$). The number of Dyck words of length $2n$ is $C_{n}$ where $C_{n}$ is the $n$-th Catalan number, defined as $C_{n}:=\frac{1}{n+1}\binom{2n}{n}$. This generates the sequence $1,1,2,5,14,42,\dots$, see https://oeis.org/A000108.

Proposition 12

In the single-agent case, for all histories $\alpha$, $|\mathsf{view}_{a}(\alpha)|=C_{{\mid}\alpha{\mid}_{a}}$.

{proof}

If there is a single agent, then histories can be transformed into Dyck words over the symbols $X$ and $Y$ when one replaces announcements by the symbol $X$ and read actions by the symbol $Y$. Moreover, $\mathsf{view}_{a}(\alpha)$ is the set of all histories $\beta$ such that $\beta{\upharpoonright}_{!}=\alpha{\upharpoonright}_{!a}$ and $\beta{\upharpoonright}_{!a}=\alpha{\upharpoonright}_{!a}$. Hence, ${\mid}\mathsf{view}_{a}(\alpha){\mid}=C_{{\mid}\alpha{\mid}_{a}}$.

However, in the multi-agent case, an agent can receive $n$ announcements in many more than $C_{n}$ ways. Example 4 showed that if there are two agents, an agent can receive one announcement in three different ways instead of one way for one agent.

3 Semantics

3.1 A well-founded order for the semantics

A well-founded order $\ll$ between (history, formula) pairs will be the basis of our semantics. It uses an auxiliary function ${\parallel}\cdot{\parallel}$ on formulas and on histories, and an auxiliary function $deg(\cdot)$ on (history, formula) pairs.

For all $\varphi\in{\mathcal{L}}_{aa}$, let ${\parallel}{\varphi}{\parallel}$ be the positive integer inductively defined as follows:

[TABLE]

and for all words $\alpha$ over $A\cup{\mathcal{L}}_{aa}$, let ${\parallel}{\alpha}{\parallel}$ be the nonnegative integer inductively defined as:

[TABLE]

Then, for all formulas $\varphi$, let $\deg(\varphi)$ be the nonnegative integer inductively defined as follows (this is often known as the modal depth of a formula, the maximum stack of epistemic modalities potentially occurring in it):

[TABLE]

Also, given a pair of the form $(\alpha,\varphi)$ where $\alpha$ is a history and $\varphi\in{\mathcal{L}}_{aa}$,

[TABLE]

Finally, let $\ll$ be the well-founded order between (history, formula) pairs defined as follows:

[TABLE]

Various results for these orders are found in the Appendix on page Appendix: results for the well-founded order $\ll$.

3.2 Semantics of asynchronous announcement logic

A model is a triple $(W,R,V)$, where $W$ is a nonempty set of states, $R:A\rightarrow\mathcal{P}(W\times W)$ maps each $a\in A$ to a binary accessibility relation $R_{a}$ on $W$, and $V:P\rightarrow\mathcal{P}(W)$ maps each atom $p$ to the set $V(p)$ of states in $W$ where $p$ is true.

Definition 13** (Semantics)**

Given a model $(W,R,V)$, we simultaneously define the agreement relation $\bowtie$ between states and histories and the satisfaction relation $\models$ between pairs of states and histories, and formulas. The model is left implicit in these relations.

[TABLE]

A formula $\varphi$ is $\epsilon$-valid (or valid), notation $\models^{\epsilon}\varphi$ (or $\models\varphi$), iff for all models $(W,R,V)$ and for all $s\in W$, $s,\epsilon\models\varphi$. The set of validities is called $AA^{\epsilon}$ (or $AA$), for asynchronous announcement logic. A formula $\varphi$ is $*$-valid (or always valid), notation $\models^{*}\varphi$, iff for all histories $\alpha$, $\models[\alpha]\varphi$; further, $\varphi$ is $\epsilon$-satisfiable (or satisfiable) iff there are $(W,R,V)$ and $s\in S$ such that $s,\epsilon\models\varphi$, and $\varphi$ is $*$-satisfiable (or sometimes satisfiable) if there is a history $\alpha$ such that $\langle\alpha\rangle\varphi$ is $\epsilon$-satisfiable. The set of $*$-validities is called $AA^{*}$.

Thanks to the items $1$–$7$ of Lemma 73 in the Appendix, the reader may verify that the definitions of the relations “agrees with” and “satisfies” are well-founded.

Importantly, the meaning of $[\varphi]\psi$ in $AA$ is different from the meaning of $[\varphi]\psi$ in $PAL$.

As dynamic epistemic logics go, $AA$ is unusual because dynamic modalities do not result in model transformations. Such transformations are implicit in the history. Given a model $M=(W,R,V)$, we can easily see the clause for announcement as a model transformer: as the truth of $[\varphi]\psi$ is conditional on the truth of $\varphi$, the states in the domain $W$ that survive this operation are exactly the $\varphi$-restriction, as in $PAL$. However, to interpret the $\psi$ bound by announcement $\varphi$, we may have to access the model prior to that announcement. In that respect our models are rather like the protocol-generated forests of [29], however with the additional complication of uncertainty of reception of announcements by other agents, which is made precise in the $[a]\varphi$ and $B_{a}\varphi$ semantics. The relation of $AA$ to history-based semantics is addressed in Section 5.4.

3.3 Examples

We continue with examples of validities and non-validities.

Example 14

We have $\models[p][a]B_{a}p$. The formula $[p][a]B_{a}p$ stands for ‘after announcement of factual information $p$, and subsequent reception by agent $a$, agent $a$ knows that $p$’. To show that it is valid, is elementary. Take any $(W,R,V)$, $s\in W$. Then the following conditions are equivalent:

• •

$s,\epsilon\models[p][a]B_{a}p$,

• •

if $s,\epsilon\models p\text{ then }s,p\models[a]B_{a}p$,

• •

if $s,\epsilon\models p\text{ then }s,pa\models B_{a}p$,

• •

if $s,\epsilon\models p\text{ then }t,\beta\models p\text{ for all }t\in W\ \text{and for all histories}\ \beta\text{ such that }sR_{a}t,t\bowtie\beta\text{ and }pa\triangleright_{a}\beta$.

If $b$ is the only other agent, the possible histories $\beta$ such that $pa\triangleright_{a}\beta$ are: $pa,pba,pab$. As they all contain the announcement $p$, the above conditions are true.

Example 15

On the other hand, $\not\models[p]B_{a}p$. Let $p$ be true but not known to agent $a$, as in the model $p(s)$—$a$—$\overline{p}(t)$. Then $s,\epsilon\models p$, and therefore $s\bowtie p$. But we do not have $s,p\models B_{a}p$: from $p\triangleright_{a}\epsilon$, $R_{a}st$, $t\bowtie\epsilon$, and $t,\epsilon\models\neg p$ it follows that $s,p\models\hat{B}_{a}\neg p$. In fact, because $p\triangleright_{a}\beta$ iff $\epsilon\triangleright_{a}\beta$, we have that $[p]B_{a}p$ is equivalent to $p\rightarrow B_{a}p$.

Example 16

Next, $\not\models^{*}[p][a]B_{a}p$. Consider a model wherein agent $a$ initially is uncertain about the truth of $p$ and wherein in actual state $s$ variables $p$ and $q$ are true with $p\not=q$, e.g. $pq$—$a$—$\overline{p}q$. The left state is $s$, let the right state be $t$. Then $s,q\models\langle p\rangle\langle a\rangle\hat{B}_{a}\neg p$, seeing that $s,\epsilon\models q$, $s,q\models p$, $|qp|_{a}<|qp|_{!}$ and $s,qpa\models\hat{B}_{a}\neg p$. Differently said, given the history $qpa$, in the event wherein $a$ receives “the next announcement,” it receives the information that $q$ contained in the first announcement, not the information that $p$ contained in the second announcement which agent $a$ will receive next if she reads again.

Example 17

We also have $\models^{*}[a]\bot\rightarrow[p][a]B_{a}p$. For any state $s$ and history $\alpha$, $[a]\bot$ is only true in $(s,\alpha)$ if agent $a$ has received all announcements in the history $\alpha$ (i.e., $|\alpha|_{!}=|\alpha|_{a}$). This means that if a further announcement is made, such as $p$, and $a$ then receives ‘the next announcement’, that must be the annoucement of $p$ just made. After that, $B_{a}p$ is true. Similarly, $\models^{*}[p][a]([a]\bot\rightarrow B_{a}p)$. It will also be clear that $\models[a]\bot$, but $\not\models^{*}[a]\bot$.

Example 18

In Figure 1(iv), after Anne and Bill have both received the announcement $p\vee q$, they both know $p\vee q$: $B_{a}(p\vee q)\wedge B_{b}(p\vee q)$ is now true. For this we can, as usual, write $E_{ab}(p\vee q)$ (everybody knows $p\vee q$). But they do not know that the other knows $p\vee q$. However, after the announcement of $E_{ab}(p\vee q)$ and both receiving it we obtain $E^{2}_{ab}(p\vee q)$: everybody knows that everybody knows $p\vee q$. And so on. Anne and Bill can achieve any finite approximation of common knowledge, but they cannot get common knowledge of $p\vee q$.

With individually received messages no growth of common knowledge will ever occur, unlike in $PAL$ where reception is synchronous [12, 18]. But we can gradually construct so-called concurrent common knowledge [12, 20], as above.

Section 6 contains an extended example relating the semantics of $AA$ to modelling processes sending and receiving events in distributed computing.

3.4 Validities and other results for the semantics

We continue with results relating the satisfaction relation and the agreement relation, and with some fairly general always-validities. In the following result, $p$ being a propositional variable and $\varphi$ being a formula, for all formulas $\chi$ possibly containing a specific occurrence of $p$, the expression $\chi[p/\varphi]$ will denote the formula obtained from $\chi$ by replacing this specific occurrence by $\varphi$ and for all histories $\gamma$ possibly containing a specific occurrence of $p$, the expression $\gamma[p/\varphi]$ will denote the history obtained from $\gamma$ by replacing this specific occurrence by $\varphi$.

Lemma 19

Let $(W,R,V)$ be a model. Let $p$ be a propositional variable. Let $\varphi,\psi$ be formulas such that for all $s\in W$ and for all histories $\alpha$, $s,\alpha\models\varphi$ iff $s,\alpha\models\psi$. Let $\chi$ be a formula possibly containing a specific occurrence of $p$ and $\gamma$ be a history possibly containing a specific occurrence of $p$. For all $s\in W$, the following conditions hold:

• •

$s\bowtie\gamma[p/\varphi]$* iff $s\bowtie\gamma[p/\psi]$,*

• •

$s,\gamma[p/\varphi]\models\chi$* iff $s,\gamma[p/\psi]\models\chi$,*

• •

$s,\gamma\models\chi[p/\varphi]$* iff $s,\gamma\models\chi[p/\psi]$.*

{proof}

The proof is by $\ll$-induction on $(\gamma,\chi)$.

Lemma 20

Let $(W,R,V)$ be a model. Let $s$ be a state and let $\alpha$ be a history. If $s\bowtie\alpha$ and $\beta\subseteq\alpha$, then $s\bowtie\beta$.

{proof}

The proof is by induction on ${\mid}\alpha{\mid}$.

Lemma 21

Let $(W,R,V)$ be a model. Let $\alpha$ be a history and $\beta$ be a word. For every formula $\chi$ and for every world $s$ such that $s\bowtie\alpha$, $s,\alpha\models\langle\beta\rangle\chi$ if and only if (i) the concatenation $\alpha\beta$ is a history, (ii) $s\bowtie\alpha\beta$, and (iii) $s,\alpha\beta\models\chi$.

{proof}

The proof is by induction on ${\mid}\beta{\mid}$.

Case “$\beta=\epsilon$”. Left to the reader.

Case “$\beta=a\beta^{\prime}$”. Suppose $s,\alpha\models\langle a\rangle\langle\beta^{\prime}\rangle\chi$. Hence, $|\alpha|_{a}<|\alpha|_{!}$. Thus, $\alpha a$ is a history and $s\bowtie\alpha a$. Moreover, $s,\alpha a\models\langle\beta^{\prime}\rangle\chi$. Consequently, by induction hypothesis, $\alpha a\beta^{\prime}$ is a history, $s\bowtie\alpha a\beta^{\prime}$ and $s,\alpha a\beta^{\prime}\models\chi$. Conversely, suppose $\alpha a\beta^{\prime}$ is a history, $s\bowtie\alpha a\beta^{\prime}$ and $s,\alpha a\beta^{\prime}\models\chi$. Hence, by induction hypothesiss $s,\alpha a\models\langle\beta^{\prime}\rangle\chi$. Thus $s,\alpha\models\langle a\rangle\langle\beta^{\prime}\rangle\chi$.

Case “$\beta=\psi\beta^{\prime}$”. Suppose $s,\alpha\models\langle\psi\rangle\langle\beta^{\prime}\rangle\chi$. Hence, $s,\alpha\models\psi$ and $s,\alpha\psi\models\langle\beta^{\prime}\rangle\chi$. Thus, by induction hypothesis, $\alpha\psi\beta^{\prime}$ is a history, $s\bowtie\alpha\psi\beta^{\prime}$ and $s,\alpha\psi\beta^{\prime}\models\chi$. Conversely, suppose $\alpha\psi\beta^{\prime}$ is a history, $s\bowtie\alpha\psi\beta^{\prime}$ and $s,\alpha\psi\beta^{\prime}\models\chi$. Consequently, $s\bowtie\alpha\psi$ and $s,\alpha\models\psi$. Moreover, by induction hypothesis, $s,\alpha\psi\models\langle\beta^{\prime}\rangle\chi$. Hence, $s,\alpha\models\langle\psi\rangle\langle\beta^{\prime}\rangle\chi$.

Lemma 22

Let $(W,R,V)$ be a model, $\alpha$ be a history, $\beta$ be a word over $A\cup{\mathcal{L}}_{aa}$ and $\varphi$ be a formula. For all $s\in W$,

• •

$s,\alpha\models\langle\beta\rangle\varphi$* iff $s,\alpha\not\models[\beta]\neg\varphi$,*

• •

$s,\alpha\models[\beta]\varphi$* iff $s,\alpha\not\models\langle\beta\rangle\neg\varphi$.*

{proof}

The proof is by $<$-induction on ${\mid}\beta{\mid}$.

Lemma 23

Let $\beta$ be a word over $A\cup{\mathcal{L}}_{aa}$. For all models $(W,R,V)$, for all $s\in W$ and for all formulas $\varphi$,

$s,\epsilon\models\langle\beta\rangle\varphi$* iff $\beta$ is a history, $s\bowtie\beta$ and $s,\beta\models\varphi$,* 2. 2.

$s,\epsilon\models[\beta]\varphi$* iff, if $\beta$ is a history and $s\bowtie\beta$, then $s,\beta\models\varphi$.*

{proof}

By Lemma 21 and Lemma 22.

Corollary 24

For all $\varphi\in{\mathcal{L}}_{aa}$, $\models^{*}\varphi$ iff for all models $(W,R,V)$, for all $s\in W$ and for all histories $\alpha$, if $s\bowtie\alpha$ then $s,\alpha\models\varphi$.

{proof}

By Lemma 23.

We note that the formulation of Corollary 24 could well have served as an alternative definition of $*$-validity, instead of “for all histories $\alpha$, $\models[\alpha]\varphi$.”

Lemma 25

Let $(W,R,V)$ be a model. For all histories $\alpha$ and for all states $s$, the following conditions are equivalent:

$s\bowtie\alpha$, 2. 2.

for all histories $\beta$, for all words $\gamma$ and for all formulas $\varphi$, if $\alpha=\beta\varphi\gamma$ then $s,\beta\models\varphi$.

{proof}

Let $\alpha$ be a history and $s$ be a state.

$(1\Rightarrow 2).$ Suppose $s\bowtie\alpha$. Let $\beta$ be a history, $\gamma$ be a word and $\varphi$ be a formula such that $\alpha=\beta\varphi\gamma$. Since $s\bowtie\alpha$, $s\bowtie\beta\varphi$. Hence, $s\bowtie\beta$ and $s,\beta\models\varphi$.

$(2\Rightarrow 1).$ Suppose for all histories $\beta$, for all words $\gamma$ and for all formulas $\varphi$, if $\alpha=\beta\varphi\gamma$ then $s,\beta\models\varphi$. We prove that $s\bowtie\alpha$ by $<$-induction on ${\mid}\alpha{\mid}$.

Case “$\alpha=\epsilon$”. Then $s\bowtie\alpha$.

Case “$\alpha=\alpha^{\prime}a$”. Since $\alpha$ is a history, $\alpha^{\prime}$ is a history such that ${\mid}\alpha^{\prime}{\mid}_{!}\geq{\mid}\alpha^{\prime}{\mid}_{a}$. Moreover, for all histories $\beta$, for all words $\gamma$ and for all formulas $\varphi$, if $\alpha^{\prime}=\beta\varphi\gamma$ then $\alpha=\beta\varphi\gamma a$ and, by our hypothesis, $s,\beta\models\varphi$. Thus, by induction hypothesis, $s\bowtie\alpha^{\prime}$. Since ${\mid}\alpha^{\prime}{\mid}_{!}\geq{\mid}\alpha^{\prime}{\mid}_{a}$, $s\bowtie\alpha$.

Case “$\alpha=\alpha^{\prime}\psi$”. Since $\alpha$ is a history, $\alpha^{\prime}$ is a history. Moreover, by our hypothesis, $s,\alpha^{\prime}\models\psi$. Consequently, $s\bowtie\alpha$.

We continue with some results for always-validity $\models^{*}$.

Proposition 26

Let $\varphi\in{\mathcal{L}}_{aa}$. If $\models^{*}\varphi$ then $\models\varphi$.

{proof}

Suppose $\models^{*}\varphi$. Hence, $\models[\epsilon]\varphi$. Thus, $\models\varphi$.

Proposition 27

Let $\varphi,\psi\in{\mathcal{L}}_{aa}$ and $a\in A$. Then:

$\models^{*}\varphi$* implies $\models^{*}B_{a}\varphi$,* 2. 2.

$\models^{*}B_{a}(\varphi\rightarrow\psi)\rightarrow(B_{a}\varphi\rightarrow B_{a}\psi)$.

{proof}

Suppose $\not\models^{*}B_{a}\varphi$. Hence, by Corollary 24, let $(W,R,V)$ be a model, $\alpha$ be a history and $s\in W$ be such that $s\bowtie\alpha$ and $s,\alpha\not\models B_{a}\varphi$. Let $t\in W$ and $\beta$ be a history such that $sR_{a}t$, $\alpha\triangleright_{a}\beta$, $t\bowtie\beta$ and $t,\beta\not\models\varphi$. Thus, by Lemma 23, $t,\epsilon\not\models[\beta]\varphi$. Consequently, $\not\models^{*}\varphi$. 2. 2.

Suppose $\not\models^{*}B_{a}(\varphi\rightarrow\psi)\rightarrow(B_{a}\varphi\rightarrow B_{a}\psi)$. Hence, by Corollary 24, let $(W,R,V)$ be a model, $\alpha$ be a history and $s\in W$ be such that $s\bowtie\alpha$ and $s,\epsilon\not\models B_{a}(\varphi\rightarrow\psi)\rightarrow(B_{a}\varphi\rightarrow B_{a}\psi)$. Thus, $s,\alpha\models B_{a}(\varphi\rightarrow\psi)$, $s,\alpha\models B_{a}\varphi$ and $s,\alpha\not\models B_{a}\psi$. Let $t\in W$ and $\beta$ be a history such that $sR_{a}t$, $\alpha\triangleright_{a}\beta$, $t\bowtie\beta$ and $t,\beta\not\models\psi$. Since $s,\alpha\models B_{a}(\varphi\rightarrow\psi)$ and $s,\alpha\models B_{a}\varphi$, we obtain that $t,\beta\models\varphi\rightarrow\psi$ and $t,\beta\models\varphi$. Thus, $t,\beta\models\psi$: a contradiction.

Lemma 28

Let $\varphi,\psi$ be formulas such that $\models^{*}\varphi\leftrightarrow\psi$. Let $M=(W,R,V)$ be a model. Let $\alpha$ be a history. Let $\beta$ be a word such that $\alpha\varphi\beta$ and $\alpha\psi\beta$ are histories and let $\chi$ be a formula. For all states $s\in W$, $s\bowtie\alpha\varphi\beta$ iff $s\bowtie\alpha\psi\beta$, and $s,\alpha\varphi\beta\models\chi$ iff $s,\alpha\psi\beta\models\chi$.

The proof of this lemma is found in the Appendix.

Proposition 29** (Substitution of equivalents)**

Let $\varphi,\psi$ be formulas such that $\models^{*}\varphi\leftrightarrow\psi$. For all formulas $\chi$ and for all atoms $p$, $\models^{*}\chi(p/\varphi)\leftrightarrow\chi(p/\psi)$.

{proof}

The proof is by induction on $\chi$.

Cases “$\chi$ is an atom”, “$\chi=\bot$”, “$\chi=\neg\chi^{\prime}$” and “$\chi=\chi_{1}\vee\chi_{2}$”. Left to the reader.

Case “$\chi=[\eta]\chi^{\prime}$”. Let $(W,R,V)$ be a model, $s$ be a state and $\alpha$ be a history such that $s\bowtie\alpha$. We have: $s,\alpha\models[\eta(p/\varphi)]\chi^{\prime}(p/\varphi)$ iff $s,\alpha\models\eta(p/\varphi)$ implies $s,\alpha\eta(p/\varphi)\models\chi^{\prime}(p/\varphi)$ iff, by induction hypothesis and using Lemma 28, $s,\alpha\models\eta(p/\psi)$ implies $s,\alpha\eta(p/\psi)\models\chi^{\prime}(p/\psi)$ iff $s,\alpha\models[\eta(p/\psi)]\chi^{\prime}(p/\psi)$. Since $(W,R,V)$, $s$ and $\alpha$ were arbitrary, $\models^{*}\chi(p/\varphi)\leftrightarrow\chi(p/\psi)$.

Case “$\chi=B_{a}\chi^{\prime}$”. Let $(W,R,V)$ be a model, $s$ be a state and $\alpha$ be a history such that $s\bowtie\alpha$. We have: $s,\alpha\models B_{a}\chi^{\prime}(p/\varphi)$ iff for all states $t$ and for all histories $\beta$, if $sR_{a}t$, $\alpha\triangleright_{a}\beta$ and $t\bowtie\beta$ then $t,\beta\models\chi^{\prime}(p/\varphi)$ iff, by induction hypothesis, for all states $t$ and for all histories $\beta$, if $sR_{a}t$, $\alpha\triangleright_{a}\beta$ and $t\bowtie\beta$ then $t,\beta\models\chi^{\prime}(p/\psi)$ iff $s,\alpha\models B_{a}\chi^{\prime}(p/\psi)$. Since $(W,R,V)$, $s$ and $\alpha$ were arbitrary, $\models^{*}\chi(p/\varphi)\leftrightarrow\chi(p/\psi)$.

Lemma 30

Let $(W,R,V)$ be a model, $s$ be a state and $a$ be an agent. For all histories $\alpha,\beta$, if ${\alpha}\triangleright_{a}{\beta}$, $s\bowtie\alpha$ and $s\bowtie\beta$ then $s,\alpha\models B_{a}\varphi$ iff $s,\beta\models B_{a}\varphi$.

{proof}

By Proposition 9.

In particular, it follows that $s,\alpha\models B_{a}\varphi$ iff $s,\alpha_{a}\models B_{a}\varphi$. Let us now see some results concerning the positive fragment ${\mathcal{L}}_{ml}^{+}$. For this we will define a preorder on histories as follows: $\alpha\preceq\beta$ if and only if:

• •

$\alpha{\upharpoonright}_{!}\subseteq\beta{\upharpoonright}_{!}$;

• •

for all $a\in A$, $|\alpha|_{a}\leq|\beta|_{a}$;

• •

for every model $(W,R,V)$ and every state $s$, $s\bowtie\beta$ implies $s\bowtie\alpha$.

It is easy to see that $\preceq$ is a reflexive and transitive relation between histories.

Lemma 31

Let histories $\alpha,\beta$ and $a\in A$ be given.

$\alpha\subseteq\beta$* implies $\alpha\preceq\beta$,* 2. 2.

$\alpha_{a}\preceq\alpha$.

{proof}

$(1).$ Suppose $\alpha\subseteq\beta$. Hence, $\alpha{\upharpoonright}_{!}\subseteq\beta{\upharpoonright}_{!}$ and for all $a\in A$, $|\alpha|_{a}\leq|\beta|_{a}$. Now, let $(W,R,V)$ be a model and $s$ be a state such that $s\bowtie\beta$. Thus, by Lemma 20, $s\bowtie\alpha$. Since $(W,R,V)$ and $s$ were arbitrary, $\alpha\preceq\beta$.

$(2).$ From the construction of $\alpha_{a}$ (see Section 2.2) it follows that $\alpha_{a}=\gamma a^{n}$ for some history $\gamma$ such that $\gamma\subseteq\alpha$ and $n=|\gamma|_{!}-|\gamma|_{a}$. Moreover, $\alpha{\upharpoonright}_{!}=\alpha_{a}{\upharpoonright}_{!}$, $|\alpha|_{a}=|\alpha_{a}|_{a}$. Now, let $(W,R,V)$ be a model and $s$ be a state such that $s\bowtie\alpha$. Thus, by Lemma 20, $s\bowtie\gamma$. Since $\alpha_{a}=\gamma a^{n}$ and $n=|\gamma|_{!}-|\gamma|_{a}$, $s\bowtie\alpha_{a}$. Since $\alpha{\upharpoonright}_{!}=\alpha_{a}{\upharpoonright}_{!}$ and $|\alpha|_{a}=|\alpha_{a}|_{a}$, $\alpha_{a}\preceq\alpha$.

Lemma 32

Let $\alpha$, $\beta$ and $\gamma$ be histories. If $\gamma\preceq\alpha$ and $\alpha\triangleright_{a}\beta$ then there exists a history $\delta$ such that $\gamma\triangleright_{a}\delta$ and $\delta\preceq\beta$.

{proof}

Suppose $\gamma\preceq\alpha$ and $\alpha\triangleright_{a}\beta$. Hence, $\gamma{\upharpoonright}_{!}\subseteq\alpha{\upharpoonright}_{!}$ and $|\gamma|_{a}\leq|\alpha|_{a}$. Moreover, ${\mid}{\beta}{\mid}_{a}={\mid}{\alpha}{\mid}_{a}$, ${\beta}{\upharpoonright}_{!a}={\alpha}{\upharpoonright}_{!a}$ and ${\mid}{\beta}{\mid}_{!}={\mid}{\alpha}{\mid}_{a}$. Thus, $|\gamma|_{a}\leq|\beta|_{a}$. Let $\beta^{\prime}$ be the initial segment of $\beta$ up until the $|\gamma|_{a}$-th occurrence of $a$. Consequently, ${\mid}{\beta^{\prime}}{\mid}_{a}={\mid}{\gamma}{\mid}_{a}$. Moreover, $\beta^{\prime}\subseteq\beta$. Hence, by Lemma 31, $\beta^{\prime}\preceq\beta$. Let $\delta=\beta^{\prime}_{a}$. Thus, by Lemma 8, $\beta^{\prime}{\upharpoonright_{!a}}=\delta{\upharpoonright_{!a}}=\delta{\upharpoonright_{!}}$ and ${\mid}{\delta}{\mid}_{a}={\mid}{\beta^{\prime}}{\mid}_{a}$. Moreover, by Lemma 31, $\delta\preceq\beta^{\prime}$. Since $\beta^{\prime}\preceq\beta$, $\delta\preceq\beta$. Since ${\mid}{\beta^{\prime}}{\mid}_{a}={\mid}{\gamma}{\mid}_{a}$ and ${\mid}{\delta}{\mid}_{a}={\mid}{\beta^{\prime}}{\mid}_{a}$, we obtain that ${\mid}{\delta}{\mid}_{a}={\mid}{\gamma}{\mid}_{a}$. From all this, it follows that $\gamma\triangleright_{a}\delta$ and $\delta\preceq\beta$.

Lemma 33

Let $(W,R,V)$ be a model. Let $\varphi\in{\mathcal{L}}_{ml}^{+}$. For all states $s$ and for all histories $\alpha^{\prime},\alpha$, if $\alpha^{\prime}\preceq\alpha$, $s\bowtie\alpha$ and $s,\alpha^{\prime}\models\varphi$ then $s,\alpha\models\varphi$.

{proof}

The proof is by induction on $\varphi$.

Cases “$\varphi=p$”, “$\varphi=\neg p$”, “$\varphi=\bot$”, “$\varphi=\top$”, “$\varphi=\psi\vee\chi$” and “$\varphi=\psi\wedge\chi$”. Left to the reader.

Case “$\varphi=B_{a}\psi$”. Let $s$ be a state and $\alpha^{\prime},\alpha$ be histories such that $\alpha^{\prime}\preceq\alpha$, $s\bowtie\alpha$, $s,\alpha^{\prime}\models B_{a}\psi$ and $s,\alpha\not\models B_{a}\psi$. Let $t$ be a state and $\beta$ be a history such that $sR_{a}t$, $\alpha\triangleright_{a}\beta$, $t\bowtie\beta$ and $t,\beta\not\models\psi$. Since $\alpha^{\prime}\preceq\alpha$, by Lemma 32, let $\beta^{\prime}$ be a history such that $\alpha^{\prime}\triangleright_{a}\beta^{\prime}$ and $\beta^{\prime}\preceq\beta$. Since $t\bowtie\beta$, $t\bowtie\beta^{\prime}$. Since $s,\alpha^{\prime}\models B_{a}\psi$, $sR_{a}t$ and $\alpha^{\prime}\triangleright_{a}\beta^{\prime}$, we obtain that $t,\beta^{\prime}\models\psi$. Since $\beta^{\prime}\preceq\beta$ and $t\bowtie\beta$, by induction hypothesis, $t,\beta\models\psi$: a contradiction.

With this lemma in hand, we can now easily demonstrate that:

Proposition 34** (Positive is preserved)**

For all $\varphi\in{\mathcal{L}}_{ml}^{+}$ and words $\alpha$, $\models^{*}\varphi\rightarrow[\alpha]\varphi$.

{proof}

Let $\varphi\in{\mathcal{L}}_{ml}^{+}$ and $\alpha$ be a word such that $\not\models^{*}\varphi\rightarrow[\alpha]\varphi$. Hence, by Corollary 24, let $(W,R,V)$ be a model, $s$ be a state and $\beta$ be a history such that $s\bowtie\beta$ and $s,\beta\not\models\varphi\rightarrow[\alpha]\varphi$. Thus, $s,\beta\models\varphi$ and $s,\beta\not\models[\alpha]\varphi$. Consequently, by Lemma 21 and Lemma 22, the concatenation $\beta\alpha$ is a history, $s\bowtie\beta\alpha$, and $s,\beta\alpha\not\models\varphi$. Hence, $\beta\subseteq\beta\alpha$. Thus, by Lemma 31, $\beta\preceq\beta\alpha$. Since $s\bowtie\beta\alpha$ and $s,\beta\models\varphi$, by Lemma 33, $s,\beta\alpha\models\varphi$: a contradiction.

3.5 Relation to standard modal logic

If we restrict the language ${\mathcal{L}}_{aa}$ to ${\mathcal{L}}_{ml}$, the fragment without dynamic modalities, there is an interesting relation between ‘valid’ and ‘always valid’, and the standard modal logic K. Let $\models^{K}$ be the standard satisfaction relation (‘Kripke semantics’) for the language ${\mathcal{L}}_{ml}$ on models $(W,R,V)$; so that, in particular, $M,s\models^{K}B_{a}\varphi$ iff $M,t\models^{K}\varphi$ for all $t$ such that $sR_{a}t$. To properly describe the relation between $\models^{K}$ and (asynchronous announcement semantics) $\models$ we introduce the notion of a flat model.

Definition 35** (Flat model)**

Given a model $M=(W,R,V)$, a state $s\in W$, and a history $\alpha$ such that $s\bowtie\alpha$. Let $\triangleright$ be the reflexive transitive closure of the union of all $\triangleright_{a}$. The flat model $\overline{M^{s\alpha}}=(W^{s\alpha},R^{s\alpha},V^{s\alpha})$ is defined as follows.111The ‘overline’ in $\overline{M^{s\alpha}}$ is used to suggest weight ‘flattening’ the epistemic and temporal aspects of $M$ and $(s,\alpha)$ into a model with merely epistemic aspects. In the old days of manual proof correction similar notation was used to ‘push down’ an upper case letter into the lower case correction.

[TABLE]

Proposition 36

For all $\varphi\in{\mathcal{L}}_{ml}$, (i) $\models^{K}\varphi$ iff $\models\varphi$, and (ii) $\models\varphi$ iff $\models^{*}\varphi$.

{proof}

The first item follows from the fact that for all histories $\beta$, if $\epsilon\triangleright_{a}\beta$ then $\beta=\epsilon$. As for the second item, remark that if $\models^{*}\varphi$ then $\models[\epsilon]\varphi$ and, therefore, $\models\varphi$. (We also recall Proposition 26, for arbitrary $\varphi\in{\mathcal{L}}_{aa}$, of which the previous is a special case.) Reciprocally, to prove that $\models\varphi$ implies $\models^{*}\varphi$, we now first prove that $\models^{K}\varphi$ implies $\models^{*}\varphi$, by way of proving the contrapositive: if $\varphi$ is sometimes satisfiable ($*$-satisfiable), then $\varphi$ is satisfiable in ordinary Kripke semantics.

Let $M=(W,R,V)$, $s\in W$, and history $\alpha$ with $s\bowtie\alpha$ be given. Consider the flat model $\overline{M^{s\alpha}}$ for $M$, $s$, and $\alpha$ (Def. 35). We now prove by induction on $\varphi\in{\mathcal{L}}_{ml}$ that for all $(t,\beta)\in W^{s\alpha}$, $M,t,\beta\models\varphi$ iff $\overline{M^{s\alpha}},(t,\beta)\models^{K}\varphi$ (where for clarity we write $M$ explicitly in expressions like $M,t,\beta\models\varphi$). The only case of interest is that for the modality $B_{a}$.

$M,t,\beta\models B_{a}\varphi\\ \Leftrightarrow\\ M,t^{\prime},\beta^{\prime}\models\varphi\text{ for all }t^{\prime},\beta^{\prime}\text{ such that }tR_{a}t^{\prime},\beta\triangleright_{a}\beta^{\prime}\text{ and }t^{\prime}\bowtie\beta^{\prime}\\ \Leftrightarrow\quad\quad\text{induction}\\ \overline{M^{s\alpha}},(t^{\prime},\beta^{\prime})\models^{K}\varphi\text{ for all }t^{\prime},\beta^{\prime}\text{ such that }tR_{a}t^{\prime},\beta\triangleright_{a}\beta^{\prime}\text{ and }t^{\prime}\bowtie\beta^{\prime}\\ \Leftrightarrow\\ \overline{M^{s\alpha}},(t^{\prime},\beta^{\prime})\models^{K}\varphi\text{ for all }(t^{\prime},\beta^{\prime})\text{ such that }(t,\beta)R^{s\alpha}_{a}(t^{\prime},\beta^{\prime})\\ \Leftrightarrow\\ \overline{M^{s\alpha}},(t,\beta)\models^{K}B_{a}\varphi$

Having shown this, in particular it holds that $M,s,\alpha\models\varphi$ iff $\overline{M^{s\alpha}},(s,\alpha)\models^{K}\varphi$. As $s$ and $\alpha$ were arbitrary, it follows that $\models^{K}\varphi$ implies $\models^{*}\varphi$, as required. From $\models\varphi$ iff $\models^{K}\varphi$, and $\models^{K}\varphi$ implies $\models^{*}\varphi$, it now follows that $\models\varphi$ implies $\models^{*}\varphi$.

From Lemma 36 it follows that for all three semantics the logic (with respect to the language ${\mathcal{L}}_{ml}$ only) is the minimal modal logic K.

In particular, this means that the standard axiom $B_{a}(\varphi\rightarrow\psi)\rightarrow(B_{a}\varphi\rightarrow B_{a}\psi)$ (K axiom), and the standard rules ‘$\varphi$ implies $B_{a}\varphi$’ (Necessitation) and ‘$\varphi$ iff $\varphi(p/\psi)$’ (Uniform Substition) of the modal logic K are valid, resp., validity preserving. For example, for $\varphi,\psi\in{\mathcal{L}}_{ml}$ we have that $\models^{*}\varphi$ iff (Prop. 36) $\models^{K}\varphi$ iff (in K) $\models^{K}\varphi(p/\psi)$ iff (Prop. 36) $\models^{*}\varphi(p/\psi)$.

The axiom $K$ and the rule Necessitation for $B_{a}$ were already established in Proposition 27, for all formulas $\varphi\in{\mathcal{L}}_{aa}$. It is therefore relevant to observe that Uniform Substitution is not conservative for this extension ${\mathcal{L}}_{aa}$.

Example 37

There exist $\varphi,\psi\in{\mathcal{L}}_{aa}$ such that $\models^{*}\varphi$ and $\not\models^{*}\varphi(p/\psi)$, for instance $\varphi=[p][a]([a]\bot\rightarrow B_{a}p)$ and $\psi=p\wedge\neg B_{a}p$. The thing is that $\models^{*}[p][a]([a]\bot\rightarrow B_{a}p)$, but $s,\epsilon\not\models[p\wedge\neg B_{a}p][a]([a]\bot\rightarrow B_{a}(p\wedge\neg B_{a}p))$ where $s$ is a state in the model $(W,R,V)$ defined by $W=\{s,t\}$, $R_{a}=W\times W$ and $V(p)=\{s\}$.

4 Axiomatization

In Section 4.1 we axiomatize $AA^{\epsilon}$, the $\epsilon$-validities. This is a reduction system eliminating reception and announcement modalities. In Section 4.2 we determine $*$-validities that are reduction axioms. However, we do not axiomatize $AA^{*}$. Section 4.3 compares $PAL$ reductions, $AA^{\epsilon}$ reductions, and $AA^{*}$ reductions.

4.1 Axiomatization of AA

In this section, we present an axiomatization of $AA$ on the class of all models with empty histories. We prove its completeness by showing that for all formulas $\varphi\in{\mathcal{L}}_{aa}$, there exists a formula $\psi\in{\mathcal{L}}_{ml}$ such that $\varphi\leftrightarrow\psi$ is valid in the class of all models with empty histories. In other words, the dynamic modalities $[a]$ and $[\varphi]$ can be eliminated from the language, as far as one is concerned with $\epsilon$-validity. We will do this by using an truth preserving transformation $tr$. The completeness proof therefore consists in showing that ${\mathcal{L}}_{aa}$ is equally expressive as ${\mathcal{L}}_{ml}$ on the class of all models with empty histories. Similar results are well-known for $PAL$, but we consider them remarkable for its asynchronous version.

Definition 38

For all words $\alpha$ over $A\cup{\mathcal{L}}_{aa}$ and for all ${\mathcal{L}}_{aa}$-formulas $\varphi$, we inductively define the ${\mathcal{L}}_{ml}$-formula $tr(\alpha,\varphi)$ as follows:

• •

$tr(\epsilon,\bot)=\bot$,

• •

$tr(\alpha a,\bot)=tr(\alpha,\bot)$* if ${\mid}\alpha{\mid}_{a}<{\mid}\alpha{\mid}_{!}$,*

• •

$tr(\alpha a,\bot)=\top$* if ${\mid}\alpha{\mid}_{a}\geq{\mid}\alpha{\mid}_{!}$,*

• •

$tr(\alpha\varphi,\bot)=tr(\alpha,\varphi)\rightarrow tr(\alpha,\bot)$,

• •

$tr(\alpha,p)=tr(\alpha,\bot)\vee p$,

• •

$tr(\alpha,\neg\varphi)=tr(\alpha,\varphi)\rightarrow tr(\alpha,\bot)$,

• •

$tr(\alpha,\varphi\vee\psi)=tr(\alpha,\varphi)\vee tr(\alpha,\psi)$,

• •

$tr(\alpha,B_{a}\varphi)=tr(\alpha,\bot)\vee\bigwedge\{B_{a}tr(\beta,\varphi)\mid\alpha\triangleright_{a}\beta\}$,

• •

$tr(\alpha,[a]\varphi)=tr(\alpha a,\varphi)$,

• •

$tr(\alpha,[\varphi]\psi)=tr(\alpha\varphi,\psi)$.

Let us remark that the above definition of the truth preserving translation $tr$ is indeed inductive, namely with respect to the well-founded order $\ll$ between (history, formula) pairs defined in Section 3.1 (Lemma 73 in the Appendix).

Lemma 39

Let $(W,R,V)$ be a model and $s\in W$. For all words $\alpha$ over $A\cup{\mathcal{L}}_{aa}$ and for all formulas $\varphi$, $s,\epsilon\models tr(\alpha,\varphi)$ iff $s,\epsilon\models[\alpha]\varphi$.

The proof is found in the Appendix. In particular, for $\alpha=\epsilon$ and given that $[\epsilon]\varphi=\varphi$, we obtain that for all models, states and formulas: $s,\epsilon\models tr(\epsilon,\varphi)$ iff $s,\epsilon\models\varphi$, so that $\varphi\mapsto tr(\epsilon,\varphi)$ therefore defines a truth (value) preserving translation from ${\mathcal{L}}_{aa}$ to ${\mathcal{L}}_{ml}$.

Corollary 40** (Elimination of dynamic modalities)**

For all $\varphi\in{\mathcal{L}}_{aa}$ there is a $\psi\in{\mathcal{L}}_{ml}$ (namely $\psi=tr(\epsilon,\varphi)$) such that $\models\varphi\leftrightarrow\psi$.

With these results in hand we will now present the axiomatization $\mathbf{AA}$. The axioms of $\mathbf{AA}$ exactly follow the pattern of the translation function $tr$ of Def. 38.

Definition 41** (Axiomatization $\mathbf{AA}$)**

Let $\mathbf{AA}$ be the axiomatization given by the following axioms and inference rules:

• •

the tautologies in the language ${\mathcal{L}}_{aa}$,

• •

the theorems of the least normal modal logic in the language ${\mathcal{L}}_{ml}$,

• •

the following axioms:

$(A1)$:

$[\alpha]p\leftrightarrow[\alpha]\bot\vee p$,

$(A2)$:

$[\alpha a]\bot\leftrightarrow[\alpha]\bot$*  if ${\mid}\alpha{\mid}_{a}<{\mid}\alpha{\mid}_{!}$,*

$(A3)$:

$[\alpha a]\bot$*  if ${\mid}\alpha{\mid}_{a}\geq{\mid}\alpha{\mid}_{!}$,*

$(A4)$:

$[\alpha\varphi]\bot\leftrightarrow[\alpha]\bot\vee\neg[\alpha]\varphi$,

$(A5)$:

$[\alpha]\neg\varphi\leftrightarrow[\alpha]\bot\vee\neg[\alpha]\varphi$,

$(A6)$:

$[\alpha](\varphi\vee\psi)\leftrightarrow[\alpha]\varphi\vee[\alpha]\psi$,

$(A7)$:

$[\alpha]B_{a}\varphi\leftrightarrow[\alpha]\bot\vee\bigwedge\{B_{a}[\beta]\varphi\mid\alpha\triangleright_{a}\beta\}$.

• •

the following inference rules:

$(MP)$:

from $\varphi$ and $\varphi\rightarrow\psi$ infer $\psi$,

$(R2)$:

from $\varphi\leftrightarrow\psi$ infer $B_{a}\varphi\leftrightarrow B_{a}\psi$,

The notion of $\mathbf{AA}$-proof being defined as usual, we will say that a formula $\varphi$ is $\mathbf{AA}$-derivable (denoted $\vdash\varphi$) iff there exists a proof of $\varphi$ from the above axiomatization.

Lemma 42

For all words $\alpha$ over $A\cup{\mathcal{L}}_{aa}$ and for all formulas $\varphi$, $\vdash[\alpha]\varphi\leftrightarrow tr(\alpha,\varphi)$.

{proof}

The proof is by $\ll$-induction on $(\alpha,\varphi)$.

Theorem 43** (Axiomatization AA is sound and complete)**

*For all $\varphi\in{\mathcal{L}}_{aa}$, $\vdash\varphi$ iff $\models\varphi$. *

{proof}

The soundness of AA ($\vdash\varphi$ implies $\models\varphi$) follows from Lemma 39, wherein it is shown that the translation $tr$ is truth preserving, and thus that all the axioms are sound.

We now show the completeness ($\models\varphi$ implies $\vdash\varphi$). Suppose $\not\vdash\varphi$. Let $\psi=tr(\epsilon,\varphi)$. Since $\not\vdash\varphi$, by Lemma 42, $\not\vdash\psi$. Since $\psi$ is a formula in ${\mathcal{L}}_{ml}$, by the standard completeness of the least normal modal logic in the language ${\mathcal{L}}_{ml}$, $\not\models^{K}\psi$. Hence, by Lemma 36, $\not\models\psi$. Thus, by Lemma 39, $\not\models\varphi$.

Let us remark that, as for ${\mathcal{L}}_{pal}$, we now have for ${\mathcal{L}}_{aa}$ an effective way to determine whether a given $\varphi$ is $\epsilon$-valid (for the class of models with arbitrary relations): if $tr(\epsilon,\varphi)$ is a theorem in the minimal modal logic K, $\varphi$ is $\epsilon$-valid; otherwise, $\varphi$ is not $\epsilon$-valid. This makes it fairly easy to prove the decidability of $AA$.

Proposition 44

$AA$* has the finite model property.*

{proof}

Suppose $\varphi$ is satisfiable. Let $M=(W,R,V)$ and state $s\in W$ be such that $s,\epsilon\models\varphi$. By Lemma 42, this means that $s,\epsilon\models tr(\epsilon,\varphi)$. Since $tr(\epsilon,\varphi)\in\mathcal{L}_{ml}$, by Proposition 36 (stating that $\models\psi$ iff $\models^{K}\psi$ for $\psi\in{\mathcal{L}}_{ml}$), this gives $M,s\models^{K}tr(\epsilon,\varphi)$ in the usual Kripke semantics. As the minimal modal logic K has the finite model property, there exists a finite model $M^{f}$ and a world $v$ in $M^{f}$ such that $M^{f},v\models^{K}tr(\epsilon,\varphi)$. By the same reasoning, this means that in $M^{f}$ we have $v,\epsilon\models tr(\epsilon,\varphi)$ according to the $AA$ semantics, and thus, again by Lemma 42, $v,\epsilon\models\varphi$.

Since $AA$ has a finitary axiomatization and the finite model property we directly obtain decidability.

Corollary 45

$AA$* is decidable.*

4.2 Reduction axioms for AA∗

In this section we determine always-validities ($*$-validities) that have the shape of reduction axioms for announcement. This is instructive, because they resemble the reduction axioms of $PAL$. However, these reductions cannot provide an complete axiomatization as in the previous section. Although we can eliminate the dynamic modalities from $\epsilon$-validities, as formulated in Corollary 40, we cannot eliminate dynamic modalities from $*$-validities.

Proposition 46** (Failure of elimination of dynamic modalities)**

There are $\varphi\in{\mathcal{L}}_{aa}$ such that for all $\psi\in{\mathcal{L}}_{ml}$ $\not\models^{*}\varphi\leftrightarrow\psi$.

{proof}

Consider the formula $[a]\bot\in{\mathcal{L}}_{aa}$. Suppose towards a contradiction that there is a $\psi\in{\mathcal{L}}_{ml}$ such that $\models^{*}[a]\bot\leftrightarrow\psi$. Then in particular we have that $\models[a]\bot\leftrightarrow\psi$. As $\models[a]\bot$, it follows that $\models\psi$: $\psi$ is $\epsilon$-valid. As $\psi\in{\mathcal{L}}_{ml}$, with Proposition 36 (stating that $\models\psi$ iff $\models^{*}\psi$) we obtain $\models^{*}\psi$: $\psi$ is $*$-valid.

Now take any $M=(W,R,V)$ and $s\in W$. From $\models\psi$ then follows $s,\epsilon\models\psi$. Also, obviously, $s\bowtie\top$ and $s,\top\models\neg[a]\bot$. From that and $\models^{*}[a]\bot\leftrightarrow\psi$ then follows that $s,\top\models\neg\psi$. However, from $\models^{*}\psi$ we obtain $s,\top\models\psi$. We have the required contradiction.

We now continue by listing reductions for atoms, conjunction, and negation after announcements $[\varphi]$, and some other reductions for formulas occurring after read modalities $[a]$.

Proposition 47

Let $\varphi,\psi\in{\mathcal{L}}_{aa}$. Then

$\models^{*}[\varphi]\bot\leftrightarrow\neg\varphi$** 2. 2.

$\models^{*}[\varphi]p\leftrightarrow(\varphi\rightarrow p)$** 3. 3.

$\models^{*}[\varphi]\neg\psi\leftrightarrow(\varphi\rightarrow\neg[\varphi]\psi)$** 4. 4.

$\models^{*}[\varphi](\psi\vee\chi)\leftrightarrow([\varphi]\psi\vee[\varphi]\chi)$** 5. 5.

$\models^{*}[\varphi]B_{a}\psi\leftrightarrow(\varphi\rightarrow B_{a}\psi)$**

The proof is found in the Appendix.

The possibly better known reduction schema $[\varphi](\psi\wedge\chi)\leftrightarrow([\varphi]\psi\wedge[\varphi]\chi)$ is also $*$-valid. It can be obtained from $[\varphi]\neg\psi\leftrightarrow(\varphi\rightarrow\neg[\varphi]\psi)$ and $[\varphi](\psi\vee\chi)\leftrightarrow([\varphi]\psi\vee[\varphi]\chi)$, and some propositional manipulations.

We emphasize that $[\varphi]B_{a}\psi\leftrightarrow(\varphi\rightarrow B_{a}\psi)$ is invalid for $PAL$. This is obvious, as in $AA$ an agent does not observe the announcement (yet). Dually, the axiom $[\varphi]B_{a}\psi\leftrightarrow(\varphi\rightarrow B_{a}[\varphi]\psi)$ of $PAL$ is invalid for $AA$. That is equally obvious (take $\varphi=p$ and $\psi=p$), as in $PAL$ the sending and receiving of the announcement are instantaneous (synchronous).

Proposition 48

For all $\varphi\in{\mathcal{L}}_{pal}$ there is a $\varphi^{\prime}\in{\mathcal{L}}_{ml}$ such that $\models^{*}\varphi\leftrightarrow\varphi^{\prime}$.

{proof}

This is proved by truth preserving rewriting, as in $PAL$, where it makes no difference that the reduction for belief after announcement is different from the one in $PAL$: it is still an equivalence, with a lower complexity on the right.

This proof is by (natural) induction on the number of announcements occurring in $\varphi$. If $\varphi$ contains no announcements, we are done. Otherwise, take an innermost announcement, i.e., a subformula $[\psi]\eta$ of $\varphi$ such that $\eta$ does not contain an announcement modality. Then, show that $\models^{*}[\psi]\eta\leftrightarrow\psi^{\prime}$ for some $\psi^{\prime}\in{\mathcal{L}}_{ml}$ by repeated use of the cases distinguished in Proposition 47. Finally, using Proposition 29, apply induction on the formula $\varphi([\psi]\eta/\psi^{\prime})$, as that contains one less announcement modality than $\varphi$.

By the same rewriting procedure we obtain

Corollary 49

For all $\varphi,\psi\in{\mathcal{L}}_{pal}$, $\models^{*}[\varphi]\psi\leftrightarrow(\varphi\rightarrow\psi)$.

And the last may be used to prove the following proposition, that may be of interest as it is an axiom in a well-known axiomatization of $PAL$.

Proposition 50

For all $\varphi,\psi,\eta\in{\mathcal{L}}_{pal}$, $\models^{*}[\varphi][\psi]\eta\leftrightarrow[\varphi\wedge[\varphi]\psi]\eta$.

{proof}

Using the result in Corollary 49, observe that $\models^{*}[\varphi][\psi]\eta\leftrightarrow(\varphi\rightarrow[\psi]\eta)$ and $\models^{*}(\varphi\rightarrow[\psi]\eta)\leftrightarrow(\varphi\rightarrow(\psi\rightarrow\eta))$, so that $\models^{*}[\varphi][\psi]\eta\leftrightarrow(\varphi\wedge\psi\rightarrow\eta)$. Somewhat similarly, $\models^{*}[\varphi\wedge[\varphi]\psi]\eta\leftrightarrow(\varphi\wedge[\varphi]\psi\rightarrow\eta)$ and $\models^{*}(\varphi\wedge[\varphi]\psi\rightarrow\eta)\leftrightarrow(\varphi\wedge(\varphi\rightarrow\psi)\rightarrow\eta)$, i.e., $\models^{*}(\varphi\wedge[\varphi]\psi\rightarrow\eta)\leftrightarrow(\varphi\wedge\psi\rightarrow\eta)$. Therefore, $\models^{*}[\varphi][\psi]\eta\leftrightarrow[\varphi\wedge[\varphi]\psi]\eta$.

Clearly, $[\varphi][\psi]\eta\leftrightarrow[\varphi\wedge[\varphi]\psi]\eta$ is invalid for asynchronous announcement logic. Merging two announcements into one announcement upsets the order of their reception in formulas bound by such announcements. For a simple counterexample,

• •

$[a]\bot\rightarrow[p][q][a][a]\bot$ is not $*$-valid;

• •

whereas $[a]\bot\rightarrow[p\wedge[p]q][a][a]\bot$ is $*$-valid;

• •

therefore, $[p][q][a][a]\bot\leftrightarrow[p\wedge[p]q][a][a]\bot$ is not $*$-valid.

We continue with various $*$-validities involving reception modalities $[a]$. We first show that the order in which agents receive the announcements is irrelevant as long as no announcement is sent in between (similar to the validity $\bigcirc_{a}\bigcirc_{b}\varphi\leftrightarrow\bigcirc_{b}\bigcirc_{a}\varphi$ of [14]).

Proposition 51

$\models^{*}[a][b]\varphi\leftrightarrow[b][a]\varphi$**

The proof is found in the Appendix.

Proposition 52

Let $\varphi\in{\mathcal{L}}_{aa}$.

$\models^{*}[\varphi]\neg[a]\bot$, 2. 2.

$\models^{*}B_{a}[a]\bot$.

{proof}

Let $(W,R,V)$, $s\in W$, and $\alpha$ such that $s\bowtie\alpha$ be given.

Assume $s,\alpha\models\varphi$. From that and $s\bowtie\alpha$ follows $s\bowtie\alpha\varphi$. From $s\bowtie\alpha$ it follows that $|\alpha|_{a}\leq|\alpha|_{!}$, so that $|\alpha\varphi|_{a}<|\alpha\varphi|_{!}$. Therefore $s\bowtie\alpha\varphi{a}$, so that $s,\alpha\varphi\models\langle a\rangle\top$, in other words, $s,\alpha\varphi\models\neg[a]\bot$. By definition, $s,\alpha\models[\varphi]\neg[a]\bot$. 2. 2.

Suppose $s,\alpha\not\models B_{a}[a]\bot$. Let $t\in W$ and $\beta$ be a word over $A\cup{\mathcal{L}}_{aa}$ such that $sR_{a}t$, $\alpha\triangleright_{a}\beta$, $t\bowtie\beta$ and $t,\beta\not\models[a]\bot$. Hence, ${\mid}\beta{\mid}_{a}<{\mid}\beta{\mid}_{!}$. Since $\alpha\triangleright_{a}\beta$, ${\mid}\beta{\mid}_{a}={\mid}\beta{\mid}_{!}$: a contradiction.

The result that $B_{a}[a]\bot$ may puzzle the reader. It formalizes that agents reason about the past and not about the future. Even when more announcements have already been sent than have been received by agent $a$, the beliefs of agent $a$ are only based on the received announcements, not on all announcements. See also Section 5.2.

Proposition 53

Let $\varphi\in{\mathcal{L}}_{aa}$. Then $\models^{*}[a]\bot\rightarrow([a]\varphi\leftrightarrow\top)$.

{proof}

Let $(W,R,V)$, $s\in W$, and $\alpha$ such that $s\bowtie\alpha$ be given. $s,\alpha\models[a]\bot$ implies $|\alpha|_{a}\geq|\alpha|_{!}$. We now get that $s,\alpha\models[a]\varphi$, i.e., $s,\alpha\models[a]\varphi\leftrightarrow\top$.

The shape $[a]\bot\rightarrow([a]\varphi\leftrightarrow\top)$ of this validity is to emphasize the difference with the next validity $\neg[a]\bot\rightarrow([a]\varphi\leftrightarrow\varphi)$. Of course we also have that $\models^{*}[a]\bot\rightarrow[a]\varphi$.

Proposition 54

Let $\varphi\in{\mathcal{L}}_{aa}$ and such that $B_{a}$ and $[a]$ do not occur in $\varphi$. Then $\models^{*}\neg[a]\bot\rightarrow([a]\varphi\leftrightarrow\varphi)$.

The proof is found in the Appendix. We can contrast Proposition 54 and Proposition 53 as follows: if agent $a$ has not yet received all announcements ($\neg[a]\bot$ is true), that agent receiving the next announcement does not influence the beliefs of other agents or the truth of any proposition not involving $a$, so we can delete or add the reception modality while preserving truth ($[a]\varphi\leftrightarrow\varphi$ is true); whereas if the agent has received all announcements ($[a]\bot$ is true), anything goes after (the impossible event of) receiving the next announcement, i.e., any proposition is true after the reception modality for ($[a]\varphi$ is true).

However, if $a$ may occur in $\varphi$, then $\not\models^{*}\neg[a]\bot\rightarrow([a]\varphi\leftrightarrow\varphi)$. In particular, neither $\models^{*}\neg[a]\bot\rightarrow([a]B_{a}\varphi\leftrightarrow B_{a}\varphi)$ nor $\models^{*}\neg[a]\bot\rightarrow([a][a]\varphi\leftrightarrow[a]\varphi)$. For a counterexample of the former, consider a model wherein the agent initially does not believe $p$, where $p$ is true in state $s$, and after the announcement that $p$. Then $s,p\models\neg[a]\bot$ and $s,p\models[a]B_{a}p$ but $s,p\not\models B_{a}p$: the agent had to receive the announcement $p$ in order to believe that $p$. For a counterexample of the latter consider the same model. On the one hand, $s,p\models\neg[a]\bot$, i.e., $s,p\not\models[a]\bot$. But on the other hand, $s,p\models[a][a]\bot$. Therefore, $s,p\not\models[a]\bot\leftrightarrow[a][a]\bot$. For any pair $(s,\alpha)$, whenever $\alpha$ contains one unreceived announcement, then $(s,\alpha)$ satisfies $[a][a]\bot$ but falsifies $[a]\bot$.

Reduction of belief after receiving announcement?

We did not find a reduction axiom for belief after receiving announcement, that one could expect to have a shape $[\varphi][a]B_{a}\psi\leftrightarrow\eta$, where $\eta$ contains a subformula $B_{a}\eta^{\prime}$ such that $\eta^{\prime}$ contains a subformula $[\varphi]\eta^{\prime\prime}$ (or, more specifically, $[\varphi][a]\eta^{\prime\prime}$). Or else, some reduction that might have a slightly more general shape $[\alpha]B_{a}\psi\leftrightarrow\eta$, where $\alpha$ is a history containing $a$ after $\varphi$ and possibly satisfying even further constraints. The special case of axiom $(A7)$ of $AA^{\epsilon}$ for $\alpha=\varphi{a}$, that in the single-agent case has form $[\varphi][a]B_{a}\psi\leftrightarrow(\varphi\rightarrow B_{a}[\varphi][a]\psi)$ (see also the next subsection), is clearly not valid in $AA^{*}$, as the $a$ in question may read another announcement than $\varphi$, namely the next unread announcement in a history $\alpha$ of a pair $(s,\alpha)$ in which we interpret that form. We also have not proved that no reduction exists for belief after receiving announcement.

Example 55

Consider the model $p\overline{q}{r}(s)$—$a$—$pq\overline{r}(t)$. We will now evaluate a formula of shape $\langle\varphi\rangle\langle a\rangle\hat{B}_{a}\psi$ (the dual of shape $[\varphi][a]B_{a}\psi$) in state $s$ of this model, however, not for the empty history but assuming history $pa$. Let $\varphi$ be $\langle a\rangle\top\vee r$ and let $\psi$ be $q$. Then $s,pa\models\langle\varphi\rangle\langle a\rangle\hat{B}_{a}q$. Indeed $s,pa\models\langle a\rangle\top\vee r$ (because $s,pa\models r$), and also $s,pa\varphi{a}\models\hat{B}_{a}q$, because $R_{a}st$, $pa\varphi{a}\triangleright_{a}p\varphi{a}a$, $t\bowtie p\varphi{a}a$ (because $t,p\models\langle a\rangle\top$), and $t,p\varphi{a}a\models q$.

In order to interpret $\hat{B}_{a}$ in $\langle\varphi\rangle\langle a\rangle\hat{B}_{a}\psi$, we need to swap elements of the history $\alpha$ in which we interpret this formula, with elements of the history $\varphi{a}$ preceding $\hat{B}_{a}$ in the formula. It is unclear how to formalize this interaction in general.

The reductions for $AA^{*}$ given in this section do not constitute a system to rewrite formulas into some standard, simpler, form. We recall that not all dynamic modalities can be eliminated from the language in a $*$-valid equivalent way, as $[a]\bot$ is irreducible. It would be of interest to determine whether all public announcement modalities can be eliminated, i.e., whether for each $*$-validity there is an equivalent formula without public announcement modalities.

4.3 Public announcements versus asynchronous announcements

Table 1 compares the axioms of $PAL$, and the axioms of the two asynchronous announcement logics $AA^{\epsilon}$ and $AA^{*}$. Additional reductions only involving the interaction of read modalities $[a]$ have not been taken into account, as they are irrelevant for $PAL$.

To see the correspondence with the axioms of AA in Proposition 47, replace the arbitrary history in those formulations by the appropriate announcement. For example, in $(A1)\ [\alpha]p\leftrightarrow([\alpha]\bot\vee p)$ we take $\alpha=\varphi$ which results in $[\varphi]p\leftrightarrow([\varphi]\bot\vee p)$, in other words, $[\varphi]p\leftrightarrow(\neg\varphi\vee p)$, i.e., $[\varphi]p\leftrightarrow(\varphi\rightarrow p)$. For another example, in $(A4)\ [\alpha\varphi]\bot\leftrightarrow[\alpha]\bot\vee\neg[\alpha]\varphi$ we take $\alpha=\epsilon$ which results in $[\varphi]\bot\leftrightarrow[\epsilon]\bot\vee\neg[\epsilon]\varphi$, i.e., $[\varphi]\bot\leftrightarrow\neg\varphi$.

In particular it should be noted that if in

[TABLE]

we (simultaneously) take $\varphi=\psi$ and $\alpha=\varphi{a}$ then we get

[TABLE]

i.e., also using that $\models^{*}[ab]\psi\leftrightarrow[ba]\psi$ (Proposition 51),

[TABLE]

and therefore in the single-agent case, also using that $\models^{*}\neg[\varphi{a}]\bot\leftrightarrow\varphi$,

[TABLE]

5 Comparison to other semantics

In this section we give results for the class $\mathcal{S}5$ of models where all accessibility relations are equivalence relations, we consider an alternative for the ‘view’-relation resulting in asynchronous knowledge instead of asynchronous belief, we motivate the belief semantics by a detailed example involving belief as acknowledgement, we relate the $AA$ semantics to history-based semantics, we present the results of the related asynchronous broadcast logic, and we compare our histories containing announcements and receptions to the cuts of distributed computing.

5.1 Asynchronous announcement logic on the class S5

In this section we restrict the models $(W,R,V)$ to those where all accessibility relations $R_{a}$ are equivalence relations. Such models are known as $\mathcal{S}5$ models, and in that case $B_{a}\varphi$ stands for ‘the agent knows $\varphi$’, and, in standard Kripke semantics $\models^{K}$, the operator then satisfies the so-called properties of knowledge $B_{a}\varphi\rightarrow\varphi$ (T, factivity), $B_{a}\varphi\rightarrow B_{a}B_{a}\varphi$ (4, positive introspection), and $\neg B_{a}\varphi\rightarrow B_{a}\neg B_{a}\varphi$ (5, negative introspection). These properties correspond to, respectively, the facts that the accessibility relation $R_{a}$ is reflexive, transitive and Euclidean.

The properties of belief (also known as introspective belief) are as the properties of knowledge, except that $B_{a}\varphi\rightarrow\varphi$ is replaced by $B_{a}\varphi\rightarrow\hat{B}_{a}\varphi$ (D, consistency), which corresponds to seriality of underlying frames. The models with serial, transitive and Euclidean relations are known as $\mathcal{KD}45$ models.

We very straightforwardly have that $B_{a}$ satisfies the properties of knowledge:

Proposition 56

Let $\varphi\in{\mathcal{L}}_{aa}$. Then

• •

$\mathcal{S}5\models B_{a}\varphi\rightarrow\varphi$**

• •

$\mathcal{S}5\models B_{a}\varphi\rightarrow B_{a}B_{a}\varphi$**

• •

$\mathcal{S}5\models\neg B_{a}\varphi\rightarrow B_{a}\neg B_{a}\varphi$**

{proof}

Let $(W,R,V)$ and $s\in W$ be given. Then $s,\epsilon\models B_{a}\varphi$ iff $t,\beta\models\varphi$ for all $t,\beta$ such that $sR_{a}t$, $\epsilon\triangleright_{a}\beta$, and $t\bowtie\beta$. As $\mathsf{view}_{a}(\epsilon)=\{\epsilon\}$, and $t\bowtie\epsilon$ holds by definition, we get that: $s,\epsilon\models B_{a}\varphi$ iff $t,\epsilon\models\varphi$ for all $t$ such that $sR_{a}t$. As $R_{a}$ is an equivalence relation, $B_{a}$ therefore satisfies the three properties of knowledge.

In asynchronous announcement logic interpreted on $\mathcal{S}5$ models with history, the $B_{a}$ operator does not satisfy all the properties of knowledge (and therefore we write $B_{a}$ and not $K_{a}$ for this modality). For example, if agents $a,b$ are initially both uncertain about $p$ and this is common knowledge, as in the $\mathcal{S}5$ model $p$—$ab$—$\overline{p}$ (where the names of the states reflect the value of $p$ there), and the announcement of $p$ is made and received by $a$ but not yet by $b$, then $p,pa\models B_{a}p\wedge B_{b}\neg B_{a}p$: the beliefs of agent $b$ are incorrect. In general, whenever $|\alpha|_{!}>|\alpha|_{a}$, then agent $a$ has not yet received all announcements and may therefore hold incorrect beliefs. If $|\alpha|_{!}>|\alpha|_{a}$ then it is not the case that $\alpha\triangleright_{a}\alpha$: the view relation $\triangleright_{a}$ is not reflexive.

However, all the other properties of introspective belief hold for asynchronous announcement logic interpreted on $\mathcal{S}5$ models.

Proposition 57

Let $\varphi\in{\mathcal{L}}_{aa}$. Then:

• •

$\mathcal{S}5\models^{*}B_{a}\varphi\rightarrow\neg B_{a}\neg\varphi$**

• •

$\mathcal{S}5\models^{*}B_{a}\varphi\rightarrow B_{a}B_{a}\varphi$**

• •

$\mathcal{S}5\models^{*}\neg B_{a}\varphi\rightarrow B_{a}\neg B_{a}\varphi$**

{proof}

We recall that $s,\alpha\models B_{a}\varphi$ iff $t,\beta\models\varphi$ for all $t,\beta$ such that $sR_{a}t$, $\alpha\triangleright_{a}\beta$, and $t\bowtie\beta$, and that the view relation is defined as $\alpha\triangleright_{a}\beta$ iff $|\beta|_{a}=|\alpha|_{a}$, $\beta{\upharpoonright}_{!a}=\alpha{\upharpoonright}_{!a}$, and $|\beta|_{!}=|\alpha|_{a}$.

We show that the relation ${\mathbf{R}}_{a}$ defined on the set of pairs $(s,\alpha)$ with $s\bowtie\alpha$ as follows:

[TABLE]

is introspective (i.e., transitive, Euclidean, and serial), so that $B_{a}$ satisfies the three properties of belief. In the proof we will use that, as $R_{a}$ is an equivalence relation and $\triangleright_{a}$ is transitive and Euclidean, their product is also transitive and Euclidean.

Transitivity of ${\mathbf{R}}_{a}$ follows from the transitivity of $R_{a}$ and $\triangleright_{a}$ (the parts involving $\bowtie$ merely result in a restriction).

[TABLE]

Since $R_{a}$ and $\triangleright_{a}$ are Euclidean, ${\mathbf{R}}_{a}$ is Euclidean.

[TABLE]

Seriality of ${\mathbf{R}}_{a}$ follows from the reflexivity of $R_{a}$ and the seriality of $\triangleright_{a}$. For the latter, Proposition 9.1 showed that for any history $\alpha$, $\alpha\triangleright_{a}\alpha_{a}$. The proof of Lemma 31.2 that $\alpha_{a}\preceq\alpha$ demonstrated that for any state $s$ with $s\bowtie\alpha$ we also have $s\bowtie\alpha_{a}$. From $sR_{a}s$, $\alpha\triangleright_{a}\alpha_{a}$, and $s\bowtie\alpha_{a}$ we get that $(s,\alpha){\mathbf{R}}_{a}(s,\alpha_{a})$.

Let us now restrict the formulas $\varphi$ from the language ${\mathcal{L}}_{aa}$ to the language ${\mathcal{L}}_{ml}$, just as in Section 3.5. We there obtained in Lemma 36 that $\models^{K}\varphi$ iff $\models\varphi$, and that $\models\varphi$ iff $\models^{*}\varphi$. We are now in for a small surprise. Although we still have that

Corollary 58

$\mathcal{S}5\models^{K}\varphi$* iff $\mathcal{S}5\models\varphi$,*

we do not have in general that $\mathcal{S}5\models\varphi$ iff $\mathcal{S}5\models^{*}\varphi$. As a simple corollary of Proposition 26 we still have that $\mathcal{S}5\models^{*}\varphi$ implies $\mathcal{S}5\models\varphi$. However, recalling the proof of Lemma 36, we now do not have in general that $\mathcal{S}5\models^{K}\varphi$ implies $\mathcal{S}5\models^{*}\varphi$ (which by analogy we would need to prove that $\mathcal{S}5\models\varphi$ iff $\mathcal{S}5\models^{*}\varphi$). As $\mathcal{S}5\not\models^{*}B_{a}\varphi\rightarrow\varphi$, $*$-satisfiability in $\mathcal{S}5$ does not entail Kripke satisfiability in $\mathcal{S}5$. The typical counterexample is the one at the beginning of this section: $p,pa\models B_{a}p\wedge B_{b}\neg B_{a}p$. But $B_{a}p\wedge B_{b}\neg B_{a}p$ is not satisfiable in $\mathcal{S}5$. We note that, If $M$ is a $\mathcal{S}5$ model and $s$ a state in $M$, then the flat model $\overline{M^{s\alpha}}$ need not be a $\mathcal{S}5$ model.

Despite this disappointment, in the $\mathcal{S}5\models^{*}$ semantics some beliefs are, after all, correct, and thus knowledge. This may also come as a surprise, but in this case a pleasant one.

Proposition 59** (Positive beliefs are correct)**

Let $\varphi\in{\mathcal{L}}_{ml}^{+}$. Then $\mathcal{S}5\models^{*}B_{a}\varphi\rightarrow\varphi$.

{proof}

Let $s$ and $\alpha$ be a world and a history such that $s\bowtie\alpha$ and $s,\alpha\models B_{a}\varphi$. From that and Lemma 30 it follows that $s,\alpha_{a}\models B_{a}\varphi$. From $s\bowtie\alpha$ and Lemma 31.2 it follows $s\bowtie\alpha_{a}$. Then, from $s,\alpha_{a}\models B_{a}\varphi$, $sR_{a}s$, $\alpha_{a}\triangleright_{a}\alpha_{a}$, and $s\bowtie\alpha_{a}$ it follows that $s,\alpha_{a}\models\varphi$. As $\varphi\in{\mathcal{L}}_{ml}^{+}$ and $\alpha_{a}\preceq\alpha$, from Lemma 33 it follows that $s,\alpha\models\varphi$.

A different way of seeing this result is that eventually all beliefs become correct and therefore knowledge, because eventually all messages will be received (and, as we know, all messages were truthful when sent) and eventually all uncertainty may be resolved. In other words, initially or at some intermediate stage an agent may well incorrectly believe that another agent is ignorant, namely when the other agent has already received more announcements, but eventually the first agent will also receive those messages and then change his incorrect beliefs into correct and stable beliefs: knowledge of positive formulas. We consider this an important observation.

Let now AAS5 be the axiomatization formed by extending the axiomatization AA of $AA$ with the S5 axioms T, 4, and 5. Recalling the soundness and completeness of AA (Theorem 43), in view of Proposition 56 we immediately obtain:

Corollary 60** (Axiomatization AAS5 is sound and complete)**

For all $\varphi\in{\mathcal{L}}_{aa}$, AA${}_{\mathbf{S5}}\vdash\varphi$ iff $\mathcal{S}5\models\varphi$.

We conclude this section with yet another observation on the relation between knowledge and belief. Although $\mathcal{S}5\models^{*}$ satisfies the properties of belief, $\mathcal{KD}45\models^{*}$ does not satisfy the properties of belief. For a simple counterexample, consider the single-agent two-state $\mathcal{KD}45$ model with $R_{a}=\{(s,t),(t,t)\}$ and where $p$ is only true in $s$, visualized as $p\xrightarrow{a}\overline{p}$. Then $s,\epsilon\models B_{a}\neg p$. After the truthful announcement that $p$ and $a$ receiving it, the beliefs of agent $a$ are inconsistent, so that $s,pa\not\models B_{a}p\rightarrow\hat{B}_{a}p$. This is a well-known problem of $\mathcal{KD}45$ updates in $\mathcal{KD}45$ models [2].

5.2 Knowledge or belief?

We recall the definition of the view relation as

$\alpha\triangleright_{a}\beta$ iff ${\alpha}{\upharpoonright}_{!a}={\beta}{\upharpoonright}_{!a}={\beta}{\upharpoonright}_{!}$.

The restriction ${\beta}{\upharpoonright}_{!a}={\beta}{\upharpoonright}_{!}$ rules out that the agent considers other agents having received more announcements than herself. If we remove that constraint, we get

$\alpha\equiv_{a}\beta$ iff ${\alpha}{\upharpoonright}_{!a}={\beta}{\upharpoonright}_{!a}$.

The relation $\equiv_{a}$ is an equivalence relation.

The interpretation of $B_{a}$ is defined as $s,\alpha\models B_{a}\varphi$ iff $t,\beta\models\varphi$ for all $t,\beta$ such that $R_{a}st$, $\alpha\triangleright_{a}\beta$, $t\bowtie\beta$. If $R_{a}$ is an equivalence relation (the $\mathcal{S}5$ models), and if we replace $\alpha\triangleright_{a}\beta$ by $\alpha\equiv_{a}\beta$, it is no longer clear that the agreement relation $\bowtie$ is well-founded, for example one such $\beta$ would be $\alpha(B_{a}\varphi)$, as $\alpha\equiv_{a}\alpha(B_{a}\varphi)$. More precisely, in order to determine whether $s,\alpha\models B_{a}\varphi$, given that $R_{a}ss$ and $\alpha\equiv_{a}\alpha(B_{a}\varphi)$, we have to determine whether $s\bowtie\alpha(B_{a}\varphi)$, for which we have to determine whether $s,\alpha\models B_{a}\varphi$: a vicious circle. Or at least vicious on first sight, without alternative modelling solutions such as fixpoints.

We may need a novel way to give a semantics to the epistemic modality. However, any such modality will clearly be interpreted by an equivalence relation. Instead of $B_{a}$ having the properties of belief, it would then have the properties of knowledge; and one might as well write $K_{a}$ for it, as we will do from here on. In the temporal epistemic logics for interpreted systems the epistemic modality is indeed such a knowledge modality, and the view relation in such works always is an equivalence relation [12, 24, 19]. This is also the approach followed in [14].

Given the history of asychronous knowledge in distributed computing, one would by all means preferably have such a notion of knowledge also in a dynamic epistemic logic. This we cannot offer at this stage. Clearly, the generalization of our framework to epistemic notions that are closer to the common epistemic notions in distributed computing are obligatory further research, and we hope that our readers and those of [14] will be encouraged to develop such logics. However, we do not think that therefore the belief semantics is somehow a second choice. Both the knowledge and belief semantics have their advantages, and ideally one would have a logic wherein both knowledge and belief appear, and that can be tailored according to the need of the modeller. In the remainder of this subsection, let us more precisely focus on the differences between asynchronous knowledge and asynchronous belief, and on possible modelling advantages of asynchronous belief.

Knowledge of novel propositions

In dynamic epistemic logics, the messages sent do not contain novel relevant propositions but are updates on the uncertainty about the currently relevant propositions, that are a given and that have a fixed unchangeable value. The goal of such sequences of updates is to finally determine their value, and the interesting phenomena are those wherein some agents reveal their uncertainty about the beliefs of other agents and thus acquire hard information about such facts.

If facts also change value, for example if messages sent and received are recorded by making fresh variables (atoms) true, even knowledge of atoms can change and $K_{a}p$ may be true now but $K_{a}\neg p$ may be true later. This is the common scenario in distributed computing.

Belief in positive formulas is correct

As shown in Proposition 34, beliefs in positive formulas are stable. And, as shown in Proposition 59, for the class $\mathcal{S}5$ of initial models, such beliefs are correct, and thus knowledge. As explained there, this can be interpreted as all belief eventually becoming knowledge.

Decidability

The knowledge semantics reasons over all possible future updates of the current model, and therefore over all possible model restrictions. In other words, it quantifies over all announcements. Arbitrary public announcement logic is a logic with a modality for quantifying over announcements and this logic is known to be undecidable [9]. One might therefore expect a logic of announcements with asynchronous knowledge to be also undecidable (but we emphasize that we do not know this). However, the logic $AA$ with the belief semantics is decidable (Corollary 45).

Should knowledge of ignorance be unsatisfiable?

We now continue to explore somewhat informally the above knowledge semantics with $\equiv_{a}$. In this semantics, it seems that an agent can never know that another agent is ignorant.

Let us first see why $K_{a}\neg(K_{b}p\vee K_{b}\neg p)$ is unsatisfiable for an atom $p$. Let some model $M$ be given, as well as a state $s$ and a history $\alpha$ that is executable in $s$ (these assumptions of course remain somewhat informal, we would like to say that we assume a pair $(s,\alpha)$ such that $s\bowtie\alpha$). Atom $p$ is necessarily either true or false in $s$, and therefore in $(s,\alpha)$, such that either $p$ or $\neg p$ can be announced, and following this announcement $b$ may have received it but not (yet) $a$. In the first case, $b$ no longer considers any state possible wherein $p$ is false: $s,\alpha{p}{b}\not\models\hat{K}_{b}\neg p$, because there is no $t$ with $sR_{b}t$ and (for some unspecified $\beta$) $t,\beta\models\neg p$. In the second case, similarly, $b$ no longer considers any state possible wherein $p$ is true: $s,\alpha{\neg p}{b}\not\models\hat{K}_{b}\neg p$. (This is of course merely an intuitive argument explaining that $[pb]K_{b}p$ and $[\neg pb]K_{b}\neg p$ are also valid for the knowledge semantics.) From $s,\alpha{p}{b}\not\models\hat{K}_{b}p$ or $s,\alpha{\neg p}{b}\not\models\hat{K}_{b}\neg p$ and the semantics of knowledge we conclude that $s,\alpha\not\models K_{a}(\hat{K}_{b}p\wedge\hat{K}_{b}\neg p)$, i.e., that $s,\alpha\not\models K_{a}\neg(K_{b}p\vee K_{b}\neg p)$. As $M$, $s$ and $\alpha$ were arbitrary, it follows that $K_{a}\neg(K_{b}p\vee K_{b}\neg p)$ is unsatisfiable.

Similarly, this argument holds for any Boolean formula instead of an atom: for any Boolean formula $\varphi$, $K_{a}\neg(K_{b}\varphi\vee K_{b}\neg\varphi)$ is unsatisfiable.

We conjecture that it is also impossible to know that other agents are ignorant for arbitrary formulas $\varphi$, but this is even harder to make precise given that we have only informally considered the knowledge semantics. Given a finite model, an a priori argument is that we can always announce the characteristic formula of the current state and have this announcement be received by agent $b$, after which any formula $\varphi$ is either true or false, and, as we conjecture, even known by or knowable to $b$. From $K_{b}\varphi\vee K_{b}\neg\varphi$ we then obtain $\hat{K}_{a}(K_{b}\varphi\vee K_{b}\neg\varphi)$, negating the above.

Now consider the belief semantics. Here, it is obvious that formulas of shape $B_{a}\neg(B_{b}\varphi\vee B_{b}\neg\varphi)$ are satisfiable — and such beliefs may even be correct. For a very basic example, consider an initial model consisting of a $p$-state $s$ and a $\neg p$-state $t$ that are indistinguishable for two agents $a,b$. Obviously, $s,\epsilon\models B_{a}\neg(B_{b}p\vee B_{b}\neg p)$. Of course, also $s,pb\models B_{a}\neg(B_{b}p\vee B_{b}\neg p)$ even though $s,pb\models B_{b}p$. This is trivial. Let us proceed with the non-trivial: belief as acknowledgement.

Belief as acknowledgement

Continuing the analysis of this basic example, it is however non-trivial that $a$ may signal to $b$ that she has not yet received novel information, by announcing $B_{a}\neg(B_{b}p\vee B_{b}\neg p)$ — we recall that a truthful announcement by $a$ of $\varphi$ to $b$ is a truthful public announcement of $B_{a}\varphi$. Then, e.g., history $pb(B_{a}\neg(B_{b}p\vee B_{b}\neg p))b$ reveals to $b$ that he received the first announcement $p$ before $a$. Such announcements $B_{a}\neg(B_{b}p\vee B_{b}\neg p)$ are more acknowledgements by $a$ than beliefs of $a$. We can play this acknowledgement game to the full in the subsequent asynchronous analysis of the muddy children puzzle, wherein agents gain factual knowledge by acknowledging the ignorance of others, as usual. Such an analysis is evidently impossible in the $\equiv_{a}$ semantics wherein knowledge of ignorance of others is unsatisfiable.

5.3 Solving muddy children with asynchronous announcements

Consider the Muddy Children problem [18, 31] for the case of three children $a,b,c$ that are all muddy. We present the story as one about knowledge $K_{a}$, for sake of the exposition, but we always assume the $AA$ semantics of belief $B_{a}$ (possibly mistaken beliefs play no role in the analysis). Father first announces that at least one of the children is muddy. This is a public announcement of $m_{a}\vee m_{b}\vee m_{b}$. Father then repeatedly requests all children who know whether they are muddy to step forward. After the first two requests, no child steps forward, which corresponds to the public announcement of formula $\neg(\mathit{Kw}_{a}m_{a}\vee\mathit{Kw}_{b}m_{b}\vee\mathit{Kw}_{c}m_{c})$ — wherein we abbreviate $K_{i}\varphi\vee K_{i}\neg\varphi$ as $\mathit{Kw}_{i}\varphi$, for “‘agent $i$ knows whether $\varphi$.” This formalizes the statement “no child knows whether it is muddy.” Then, at the third request, all three children step forward. The second time they do not step forward is a typical example of an unsuccessful update (a formula that becomes false after being announced), because the final action can be seen as the public announcement of $\mathit{Kw}_{a}m_{a}\vee\mathit{Kw}_{b}m_{b}\vee\mathit{Kw}_{c}m_{c}$. Note that in the given model this (inclusive) disjunction has the same informative effect as the conjunction of the three knowing-whether terms.

This standard solution no longer works with asynchronous announcements, for different reasons. In the first place, the action of no child stepping forward can no longer be represented by a single formula, as this public announcement formula is implicitly a synchronization of the children’s individual decisions not to step forward. In the second place, if after receiving father’s announcement that $m_{a}\vee m_{b}\vee m_{c}$ a child $i$ merely announces $\neg\mathit{Kw}_{i}m_{i}$, it is unclear to the other children receiving both announcements in that order that child $i$ had received father’s announcement when it made its own announcement. Receiving this information is then no longer informative. The other children cannot rule out that child $i$ had announced $\neg\mathit{Kw}_{i}m_{i}$ before receiving father’s announcement (but still after father’s announcement was made), in which case it merely describes a commonly known property of the initial model. As the other children cannot distinguish this uninformative history from the informative history, they cannot draw an informative conclusion.

Our solution emphasizes the use of our epistemic belief/knowledge notion as one of acknowledgement. Following father’s initial announcement of $m_{a}\vee m_{b}\vee m_{c}$, let each child $i$ announce

[TABLE]

This means that $i$ still does not know whether she is muddy after having received father’s announcement that at least one child is muddy. She announces her ignorance while acknowledging the reception of father’s first announcement to the other children. Let all three children do this.

After receiving all these, each child $i$ now announces her continued ignorance while acknowledging reception of these three ignorance announcements including her own:

[TABLE]

This formalizes that even after having received the information that no child knows whether it is muddy, $i$ still does not know whether she is muddy.

After all three children have sent and subsequently received this information, they will all know that they are muddy. (And they may finally all three step forward, although slightly out of step as they do this asynchronously.) Problem solved!

It is straightforward to generalize this to any number of $n\geq 3$ children of which $k\leq n$ are muddy by further iterations of acknowledgement of ignorance in the previous round.

In the knowledge semantics with $\equiv_{i}$ instead of $\triangleright_{i}$, announcement $\neg\mathit{Kw}_{i}m_{i}\wedge K_{i}(m_{a}\vee m_{b}\vee m_{c})$ can still be made and received, but, crucially, not the other more complex announcements acknowledging ignorance (or subsequent iterations). We recall that knowledge of other agents’ ignorance of Booleans (such as $m_{i}$ and $\neg m_{i}$) is not satisfiable in that semantics.

5.4 History-based structures

In dynamic epistemic logic, the dynamic modalities induce model transformations and are then interpreted as relations between pointed models. They are not interpreted as relations between states in a given model. Various frameworks are known to enforce the interpretation of dynamic modalities by way of relations in a given model. This is typically in the setting of translating dynamic epistemic logics to temporal epistemic logics, in which case the dynamic transformations correspond to steps of a temporal next-time operator. If we wish to interpret dynamic modalities with an accessibility relation in some model, that model is then much larger than the ‘initial’ model used for model transformations. For example, if the dynamic modalities are for public announcements, the ‘supermodel’ should somehow contain all modally definable submodels of that initial model. To our knowledge, such constructions have first been proposed by Venema in [28]. Well-known are the protocol generated forests of [29], see also [32], and [7] for an asynchronous interpretation. A maybe less well-known, but equally elegant approach are the extended models of [35]. The asynchronous pre-models of [14] are also history-based structures.

In this section we define a history-based structure called asynchronous model that can be defined given a model and history, and show the obvious required correspondence.

Definition 61** (Asynchronous model)**

Let model $M=(W,R,V)$ and history $\alpha$ be given. The asynchronous model $M^{\alpha{\upharpoonright}_{!}}=(W^{\prime},R^{\prime},V^{\prime})$ is defined as:

[TABLE]

A member of the domain of an asynchronous model is an asynchronous state.

Definition 62

Let model $M=(W,R,V)$ and history $\alpha$ be given. The interpretation of formulas $\varphi\in{\mathcal{L}}_{aa}$ on asynchronous model $M^{\alpha{\upharpoonright}_{!}}=(W^{\prime},R^{\prime},V^{\prime})$ is defined by induction. We omit all the obvious clauses.

[TABLE]

As usual, in the clause for $[\varphi]\psi$, it need not be the case that $M^{\alpha{\upharpoonright}_{!}},s,\alpha\models\varphi$. Therefore, we do not assume that $s\bowtie\beta\varphi$. The two conditions of that clause are for the case where $\varphi$ is the next announcement in the asynchronous model for $\alpha$, and where $\varphi$ is ‘novel’, so to speak, in which case we have to construct another asynchronous model incorporating announcement $\varphi$, in order to proceed.

Proposition 63

Let $\varphi\in{\mathcal{L}}_{aa}$ be given. For all $M$, and $s$ and $\alpha$ with $s\bowtie\alpha$, $s,\alpha\models\varphi$ iff $M^{\alpha{\upharpoonright}_{!}},s,\alpha\models\varphi$.

The proof is found in the Appendix.

Example 64

We can now finally validate the depictions used for the introductory example involving Anne who knows about $p$ and Bill who knows about $q$, and the asynchronous announcement of $p\vee q$ followed by first Anne and then Bill receiving it.

Figure 2 depicts the asynchronous history model for this sequence of events. The relations $\triangleright_{a}$ and $\triangleright_{b}$ have only been visualized for some typical cases. Instead of naming the states we show their valuation of $p$ and $q$, as common in depictions of multi-agent models. For example, if in the initial model (i) the topleft state $\overline{p}{q}$ is called $s$ and the topright state $pq$ is called $t$, then these correspond to the asynchronous states $(s,\epsilon)$ and $(t,\epsilon)$ respectively, and the topright state $pq$ in the figure would then be $(t,(p\vee{q})ab)$, and so on.

The structures $i,ii,iii,iv$ of Figure 1 in the introduction should be seen as the, respectively $\epsilon$, $p\vee q$, $(p\vee q)a$, and $(p\vee q)ab$ projections of the asynchronous model.

5.5 Asynchronous broadcast logic

In [14] and the already cited related works the authors develop a logical semantics for sending and receiving messages that are announcements and where the epistemic notion is one of knowledge and not one of belief, unlike ours. The modelling justifications and consequences of these different semantics were discussed at length in Section 5.2. The logical language is the same as ours, except that they write $\bigcirc_{a}$ instead of (the diamond form) $\langle a\rangle$ for the reception modality, and $K_{a}$ instead of $B_{a}$ for the epistemic modality. They interpret their language on structures called asynchronous pre-models, with domain elements that are triples $(s,\sigma,c)$ where $s$ is an abstract state (from the domain of some initial Kripke model), $\sigma$ is a sequence of formulas taken from a protocol of allowed sequences of formulas, and $c$ is a cut, listing for each agent which announcements in the sequence $\sigma$ that agent has already received. The relation between such cuts and the histories in $AA$ will be explored in the next Section 5.6.

Announcements must be true when made and are individually received by the agents in the order in which they were sent. The knowledge modality $K_{a}$ is interpreted over histories of arbitrary length, thus guaranteeing that knowledge is correct: $K_{a}\varphi\rightarrow\varphi$ is valid. When interpreting knowledge on pre-models, not all triples $(s,\sigma,c)$ of the pre-model are taken into account but only those where all formulas of $\sigma$ could have been truthfully announced. They call this the requirement of consistency of $\sigma$ with $s$ (where we called this agreement, the relation $\bowtie$). Their semantics is then based on mutual recursion of ‘truth’ and ‘consistency’, similar to ours.

As their epistemic notion is one of knowledge, also taking into account announcements that have not yet been received, they face the already mentioned issue of circularity and of a well-founded semantics. They provide two well-founded solutions to this circularity problem. Their first solution is to restrict the structures to (initial) models that are finite point-generated trees, and where the model transformations are relative to the root of the model. This solution is reminiscent of [17]. Their second solution is to restrict the language to the so-called existential fragment wherein negations are only allowed of atoms, and wherein modalities are only allowed in ‘diamond’ form $\hat{K}_{a}\varphi$, $\bigcirc_{a}$, and $\langle\psi\rangle\varphi$. They present some validities for their logical semantics, such as $\bigcirc_{a}\bigcirc_{b}\varphi\leftrightarrow\bigcirc_{b}\bigcirc_{a}\varphi$: without intervening announcements, the order of reception does not matter. They do not provide an axiomatization. They obtain various complexity results. An interesting special case for complexity is when all announced formulas are Booleans. They show that the complexity of model checking for that case is PSPACE-complete, and that the complexity of satisfiability is NExptime-hard. They also show that the complexity of model checking on finite trees is in PSPACE and that the complexity of model checking for the existential fragment is in Exptime.

5.6 Cuts and distributed computing

In distributed computing, the activity of each agent $a\in A$ consists of events that are either messages sent to other agents or messages received from other agents. These events are temporally ordered. A cut is a selection of one of these events for each agent. For each agent we can then distinguish the events before and up to the cut (i.e., weakly before) from those that come after (i.e., strictly after) the cut. The cut is inconsistent if there are agents $a,b$ and a message $m$ such that the event of $a$ sending $m$ is after the cut for $a$, and the event of $b$ receiving $m$ is (weakly) before the cut for $b$. Otherwise the cut is consistent. An inconsistent cut violates that messages must have been sent (and therefore ‘happened’) before they are received. For the ‘happened before’ relation see the foundational [16] (that does not use the term ‘cut’), for ‘cuts’ see e.g. [20] and [15, p. 45].

In the logic $AA$, the agents only receive messages and the anonymous environment (the ‘announcer’) only sends messages. The requirement of consistency is satisfied by words $\alpha\in(A\cup{\mathcal{L}}_{aa})$ that are histories: a word $\alpha$ is a history if for all prefixes $\beta$ of $\alpha$ and for all agents $a$ we have that $|\beta|_{a}\leq|\beta|_{!}$, i.e., if at any stage an agent $a$ can only receive an announcement that has already been made. In that sense a word corresponds to an inconsistent cut if it is not a history. In this section we investigate the relation between histories and cuts. In another sense a history may be said to correspond to an inconsistent cut if we consider the announcement $\varphi$ as the message $B_{a}\varphi$ sent by agent $a$, as in distributed computing. That will be investigated in Section 6.

Given $n\in\mathbb{N}$, a $n$-cut is a function $f:A\rightarrow[0,n]$. A history $\alpha$ determines a pair $(\alpha{\upharpoonright}_{!},f^{\alpha})$, where $f^{\alpha}$ is the $|\alpha|_{!}$-cut $f$ such that for all $a\in A$, $f(a)=|\alpha|_{a}$. This notion of cut was proposed in [14] and in the prior SR 2017 version of this work, but it is merely another example of the standard notion of cut in distributed computing [15]. It will be clear that $f^{\alpha}=f^{\beta}$ iff $|\alpha|_{!}=|\beta|_{!}$ and for all $a\in A$, $|\alpha|_{a}=|\beta|_{a}$.

Different cuts always correspond to different histories, but different histories $\alpha,\beta$ may correspond to the same cut. If $\alpha{\upharpoonright}_{!}=\beta{\upharpoonright}_{!}$ and $|\alpha|_{a}=|\beta|_{a}$ for all $a\in A$, then obviously $(\alpha{\upharpoonright}_{!},f^{\alpha})=(\beta{\upharpoonright}_{!},f^{\beta})$: all agents have received the same announcements in the same order. However, it may be the case that $s\bowtie\alpha$ and $s\not\bowtie\beta$ for a certain state $s$ in some given model. As an example, consider the histories $\alpha=p(\neg B_{a}p)aa$ and $\beta=pa(\neg B_{a}p)a$. Given a model and a state $s$ where $p$ is true but unknown by $a$, $\alpha$ agrees with $s$ but $\beta$ does not agree with $s$. In fact, $\beta$ cannot agree with any state of any model, as after agent $a$ receives $p$ the announcement $\neg B_{a}p$ cannot be truthful. Histories are a more refined relation on message sending and receiving than cuts.

This suggests that histories have more ‘expressive power’ (in an informal sense) than cuts. However, to an important extent this is not the case: histories containing the same sequence of announcements and corresponding to the same cut are ‘indistinguishable’ in those states with which they both agree, in the sense that those states make the same formulas true, they have the same theory. A minor lemma precedes the proposition stating this result. Consequently, this more closely relates the cut-based semantics of [14] to our semantics, although the epistemic modalities are different.

Lemma 65

Let histories $\alpha,\beta$ be given such that $\alpha{\upharpoonright}_{!}=\beta{\upharpoonright}_{!}$ and $f^{\alpha}=f^{\beta}$.

For all $a\in A$ and histories $\gamma$, $\alpha\triangleright_{a}\gamma$ iff $\beta\triangleright_{a}\gamma$. 2. 2.

For all $a\in A$, if $|\alpha|_{!}<|\alpha|_{a}$ then $f^{\alpha{a}}=f^{\beta{a}}$. 3. 3.

For all $\varphi\in{\mathcal{L}}_{aa}$, $f^{\alpha\varphi}=f^{\beta\varphi}$.

{proof}

Recall that $f^{\alpha}=f^{\beta}$, iff $|\alpha|_{!}=|\beta|_{!}$ and for all $b\in A$, $|\alpha|_{b}=|\beta|_{b}$. (Note that assumption $\alpha{\upharpoonright}_{!}=\beta{\upharpoonright}_{!}$ already implies $|\alpha|_{!}=|\beta|_{!}$.)

From $\alpha{\upharpoonright}_{!}=\beta{\upharpoonright}_{!}$ and $|\alpha|_{a}=|\beta|_{a}$ we obtain $\alpha{\upharpoonright}_{!a}=\beta{\upharpoonright}_{!a}$. We now use Def. 3 of the view relation. 2. 2.

Given that $|\alpha|_{!}<|\alpha|_{a}$, $\alpha{a}$ and $\beta{a}$ are histories. From $\alpha{\upharpoonright}_{!}=\beta{\upharpoonright}_{!}$ we obtain that $\alpha{a}{\upharpoonright}_{!}=\beta{a}{\upharpoonright}_{!}$ ($=\alpha{\upharpoonright}_{!}$). Also, $|\alpha{a}|_{a}=|\alpha|_{a}+1=|\beta|_{a}+1=|\beta{a}|_{a}$, and for $b\neq a$, $|\alpha|_{b}=|\alpha{a}|_{b}=|\beta{a}|_{b}=|\beta|_{a}$. Therefore $f^{\alpha{a}}=f^{\beta{a}}$. 3. 3.

From $\alpha{\upharpoonright}_{!}=\beta{\upharpoonright}_{!}$ we obtain $\alpha\varphi{\upharpoonright}_{!}=\beta\varphi{\upharpoonright}_{!}$, as e.g. $\alpha\varphi{\upharpoonright}_{!}=(\alpha{\upharpoonright}_{!})\varphi$. Also, for all $b\in A$, $|\alpha\varphi|_{b}=|\alpha|_{b}=|\beta|_{b}=|\beta\varphi|_{b}$. Therefore $f^{\alpha\varphi}=f^{\beta\varphi}$.

Proposition 66

Let be given $\varphi\in{\mathcal{L}}_{aa}$, model $M=(W,R,V)$ with $s\in W$, histories $\alpha,\beta$ such that $f^{\alpha}=f^{\beta}$, and $s\bowtie\alpha$ and $s\bowtie\beta$. Then $s,\alpha\models\varphi$ iff $s,\beta\models\varphi$.

{proof}

The proof is by induction on $\varphi$. The trivial cases when $\varphi=p,\bot,\psi_{1}\vee\psi_{2},\neg\psi$ are left to the reader.

Case belief: $s,\alpha\models B_{a}\varphi$, iff $t,\gamma\models\varphi$ for all $(t,\gamma)$ such that $R_{a}st$, $\alpha\triangleright_{a}\gamma$, and $t\bowtie\gamma$, iff (by Lemma 65.1) $t,\gamma\models\varphi$ for all $(t,\gamma)$ such that $R_{a}st$, $\beta\triangleright_{a}\gamma$, and $t\bowtie\gamma$, iff $s,\beta\models B_{a}\varphi$.

Case reception: $s,\alpha\models[a]\psi$, iff $|\alpha|_{a}<|\alpha|_{!}$ implies $s,\alpha{a}\models\psi$, iff (Lemma 65.2 and induction) $|\beta|_{a}<|\beta|_{!}$ implies $s,\beta{a}\models\psi$.

Case announcement: $s,\alpha\models[\varphi]\psi$, iff $s,\alpha\models\varphi$ implies $s,\alpha\varphi\models\psi$, iff (Lemma 65.3 and twice induction) $s,\beta\models\varphi$ implies $s,\beta\varphi\models\psi$, iff $s,\beta\models[\varphi]\psi$.

6 Distributed computing and asynchronous announcements

In this section we give a detailed example of our logic and its semantics that is described in terms of distributed computing. Consider two agents $a$, $b$ each only knowing the (binary) value of their local state, respectively, $p$ and $q$. We can see this as an interpreted or distributed system in terms of [12, 8] for two processes/agents $a,b$ with possible global states $pq$ (i.e., $(p,q)$), $p\overline{q}$, $\overline{p}q$, $\overline{p}\overline{q}$, and with knowledge of the agents induced by their local state. We can alternatively see this as the model depicted in Figure 1(i). Let us assume that the actual values are $p$ for $a$ and $q$ for $b$.

In dynamic epistemic logics, an agent $a$ truthfully sending (broadcasting) a message $\varphi$ is simulated by the environment sending the (true) message $B_{a}\varphi$. These broadcast messages are the announcements. This is no different for asynchronous announcement logic.

Agent $a$ now sends her local value $p$ to $b$, and after receiving this message agent $b$ sends an acknowledgement to $a$, who then receives that. These are the two announcements $B_{a}p$ ($a$ announces $p$, for ‘the value of my local state is $p$’) and $B_{b}B_{a}p$ ($b$ announces $B_{a}p$, for ‘I now know that the value of your local state is $p$’). We can model this in asynchronous announcement logic in different ways: (i) we only model the asynchronous reception of the messages by $a$ and $b$, (ii) we introduce the environment as an agent $e$ sending the messages, or (iii) we let $a$ and $b$ send and receive messages.

Two processes a and b and implicit environment  Consider agents/processes $a,b$ and reception events $a_{1},a_{2},b_{1},b_{2}$ of the two announcements $B_{a}p$ and $B_{b}B_{a}p$ made by the environment, where a ‘before’ relation is a partial order between these events, along the familiar terms described in e.g. [16, 20, 15]. How to model the announcements is left implicit for now and deferred until later. We get:

a$$b$$b$$\bullet$$a_{1}$$\bullet$$a_{2}$$\bullet$$b_{1}$$\bullet$$b_{2}inconsistentconsistent

What is the partial order? Given the announcements, apart from the obviously enforced $a_{1}<a_{2}$ and $b_{1}<b_{2}$ the only other constraint is that $b_{1}<a_{2}$: agent $a$ cannot receive the message $B_{b}B_{a}p$ before agent $b$ has received message $B_{a}p$. A ‘cut’ determines how many messages each agent has received. The depicted consistent cut corresponds to the history $(B_{a}p)a$. The inconsistent cut does not respect that $b_{1}<a_{2}$. It corresponds to the history $(B_{a}p)a(B_{b}B_{a}p)a$ (or to $(B_{a}p)(B_{b}B_{a}p)aa$). In our terms we would say that the state $s$ where $p$ and $q$ are both true does not agree with that history, i.e., $s\not\bowtie(B_{a}p)a(B_{b}B_{a}p)a$.

Three processes a, b, and e  We now also model the environment explicitly as a process/agent $e$. We can also add this agent $e$ to the models in which we interpret asynchronous announcements, namely as an agent with the identity accessibility relation on such models, which implies that $B_{e}\varphi\leftrightarrow\varphi$: truthful messages — $B_{e}\varphi$ — are also true — $\varphi$. Therefore, announcements made by the environment need not be prefixed by the $B_{e}$ operator. Let us assume that $s_{1}$ is the announcement of $B_{a}p$ and $s_{2}$ is the announcement of $B_{b}B_{a}p$. In dynamic epistemic logics, an announcement made by an agent is also received by this agent (if you say something, you also hear it yourself). This is relevant because the message content may be modal and thus affect the knowledge or belief of the announcing agent (such as $a$ announcing to $b$: “$p$ is true but you don’t know this,” $K_{a}(p\wedge\neg K_{b}p)$). This is unlike a broadcast in distributed systems. But in the following depiction we therefore must also involve two reception events $e_{1}$ and $e_{2}$ for the environment.

e$$a$$b$$\bullet$$s_{1}$$\bullet$$s_{2}$$\bullet$$e_{1}$$\bullet$$e_{2}$$\bullet$$a_{1}$$\bullet$$a_{2}$$\bullet$$b_{1}$$\bullet$$b_{2}inconsistentinconsistentconsistent

The partial relation $a_{1}<a_{2}$, $b_{1}<b_{2}$, $b_{1}<a_{2}$ enforced so far is expanded with $s_{1}<a_{1},b_{1},e_{1}$ and $s_{2}<a_{2},b_{2},e_{2}$ (a message is sent before it is received) and the event ordering $s_{1}<s_{2}$ and $e_{1}<e_{2}$ for the environment.

However, the fact that messages sent by the environment are true when sent (the agreement relation of $AA$ again), enforces other logical/causal constraints that are of more interest. The environment announcing $B_{b}B_{a}p$ stands for the truth of that formula. This enforces that $b_{1}<s_{2}$ (but it is consistent with $a_{1}<s_{2}$ and with $s_{2}<a_{1}$). From $b_{1}<s_{2}$ now follows with the above constraint $s_{2}<a_{2}$ that $b_{1}<a_{2}$.

If we abstract from the reception of the environment, the leftmost cut in the figure corresponds to the histories $(B_{a}p)(B_{b}B_{a}p)aa$ and $(B_{a}p)a(B_{b}B_{a}p)a$. These are inconsistent because $s\not\bowtie(B_{a}p)(B_{b}B_{a}p)aa$ and $s\not\bowtie(B_{a}p)a(B_{b}B_{a}p)a$. The middle cut is also inconsistent (it does not obey that $b_{1}<s_{2}$) as it corresponds to histories $(B_{a}p)(B_{b}B_{a}p)a$ and $(B_{a}p)a(B_{b}B_{a}p)$. The right cut is consistent. It corresponds to history $(B_{a}p)a$.

Two processes a and b sending and receiving  We now let agents $a$ and $b$ send the messages themselves. The inconsistent cut corresponds to $(B_{a}p)aa$. In terms of $AA$ it is inconsistent not for lack of agreement (it contains messages that could not have been truthfully announced), but because it is not a history. Expression $(B_{a}p)aa$ is a word in the language $\{a,b\}\cup{\mathcal{L}}_{aa}$ but not a history, as $2=|(B_{a}p)aa|_{a}>|(B_{a}p)aa|_{!}=1$. The depicted consistent cut corresponds to history $(B_{a}p)a$.

a$$b$$b$$\bullet$$s_{1}$$\bullet$$a_{1}$$\bullet$$a_{2}$$\bullet$$s_{2}$$\bullet$$b_{1}$$\bullet$$b_{2}inconsistentconsistent

This modelling solution is stretching the use of asynchronous announcement logic. Agent $a$ sending a message $\varphi$ in $AA$ is simulated by the announcement $B_{a}\varphi$ by the environment, and therefore $a$ and $b$ both have to receive that. But no order is enforced for this reception: $a_{1}<b_{1}$ and $b_{1}<a_{1}$ are both causally permitted. In other words, the more intuitive history $(B_{a}p)ab(B_{b}B_{a}p)ab$ and the counterintuitive history $(B_{a}p)b(B_{b}B_{a}p)baa$ are both permitted. It seems quite possible to adjust the semantics of $AA$ to enforce only histories wherein the agent sending the message is always the first to receive it, and thus allowing to abstract from it. Such logics, deferred to future research, are more suitable for settings wherein agents both send and receive messages.

7 Conclusions and further research

We presented asynchronous announcement logic $AA$, a logic of epistemic change due to announcements, with separate modalities for sending and for receiving such messages. Our epistemic modality is one of belief, not one of knowledge. We provided an axiomatization for this logic $AA$ that is a reduction system: every formula is equivalent to a formula without announcement and reception modalities. The logic $AA$ is therefore also decidable. We determined results for special formulas and for special model classes: the positive formulas are preserved after update, and on the model class $\mathcal{S}5$, belief of positive formulas is correct and thus knowledge. The complexity of model checking and of satisfiability of AA is left for further research. We envisage numerous generalizations of our work, such as for subgroups synchronously receiving announcements, for non-public actions, and instead of belief for knowledge, wherein one also reasons about the future.

Acknowledgements

For their comments on or involvement in prior versions of this manuscript, or helpful interactions during seminars on this topic, we thank: Malvin Gattinger, Davide Grossi, Ramanujam, Armando Castañeda, Sergio Rajsbaum.

Hans van Ditmarsch is also affiliated to IMSc, Chennai, India. Since 2008, my IMSc host Ramanujam engaged me in discussions on modelling asynchronous messaging in dynamic epistemic logic. His support has always motivated and encouraged me. Sophia Knight introduced me to the work of Prakash Panangaden that inspired asynchronous announcements, and later Bastien Maubert and François Schwarzentruber became involved in this pursuit, all at the CELLO team in LORIA. Then, our ways parted and their work took the direction of [14]. Without this past collaboration the underlying work could not have resulted, and I thank them for all the interaction (and music) that we had together.

Appendix: results for the well-founded order $\ll$

The first part of the Appendix contains results for the order $\ll$, and the functions ${\parallel}\cdot{\parallel}$ and $deg(\cdot)$. First, concerning ${\parallel}\cdot{\parallel}$, note that, obviously, for all words $\alpha$ over $A\cup{\mathcal{L}}_{aa}$ and for all $a\in A$, ${\mid}\alpha{\mid}_{a}\leq{\parallel}\alpha{\parallel}$.

Lemma 67

For all words $\alpha$ over $A\cup{\mathcal{L}}_{aa}$, for all $a\in A$ and for all $\varphi\in{\mathcal{L}}_{aa}$, ${\parallel}a\alpha{\parallel}={\parallel}\alpha{\parallel}+1$ and ${\parallel}\varphi\alpha{\parallel}={\parallel}\alpha{\parallel}+{\parallel}\varphi{\parallel}$.

{proof}

The proof is by $<$-induction on ${\mid}\alpha{\mid}$.

Lemma 68

For all words $\alpha$ over $A\cup{\mathcal{L}}_{aa}$ and for all $\varphi\in{\mathcal{L}}_{aa}$, ${\parallel}[\alpha]\varphi{\parallel}=2{\parallel}\alpha{\parallel}+{\parallel}\varphi{\parallel}$.

{proof}

The proof is by $<$-induction on ${\mid}\alpha{\mid}$.

Lemma 69

For all words $\alpha$ over $A\cup{\mathcal{L}}_{aa}$, for all $k\in\mathbb{N}$, for all $\psi_{1},\ldots,\psi_{k}\in{\mathcal{L}}_{aa}$ and for all $\varphi\in{\mathcal{L}}_{aa}$, if $\alpha{\upharpoonright}_{!}=\psi_{1}\ldots\psi_{k}$ then $\deg([\alpha]\varphi)=\deg(\psi_{1})+\ldots+\deg(\psi_{k})+\deg(\varphi)$.

{proof}

The proof is by $<$-induction on ${\mid}\alpha{\mid}$.

Lemma 70

Let $\alpha$ be a history. Let $k$ be a nonnegative integer and $\varphi_{1},\ldots,\varphi_{k}\in{\mathcal{L}}_{aa}$. In the single-agent case, if ${\alpha}{\upharpoonright}_{!}=\varphi_{1}\ldots\varphi_{k}$ then ${\parallel}{\alpha}{\parallel}={\mid}{\alpha}{\mid}_{a}+{\parallel}{\varphi_{1}}{\parallel}+\ldots+{\parallel}{\varphi_{k}}{\parallel}$. Otherwise, in the multi-agent case, considering an enumeration $(a_{1},\ldots,a_{n})$ of $A$ without repetition, if ${\alpha}{\upharpoonright}_{!}=\varphi_{1}\ldots\varphi_{k}$ then ${\parallel}{\alpha}{\parallel}={\mid}{\alpha}{\mid}_{a_{1}}+\ldots+{\mid}{\alpha}{\mid}_{a_{n}}+{\parallel}{\varphi_{1}}{\parallel}+\ldots+{\parallel}{\varphi_{k}}{\parallel}$

{proof}

The proof is by $<$-induction on ${\mid}{\alpha}{\mid}$.

Lemma 71

Let $\alpha,\beta$ be histories and $a\in A$. If ${\alpha}{\triangleright_{a}}{\beta}$ then ${\parallel}{\beta}{\parallel}\leq|A|\cdot{\parallel}{\alpha}{\parallel}$.

{proof}

Suppose ${\alpha}{\triangleright_{a}}{\beta}$. Hence, ${\mid}{\beta}{\mid}_{a}={\mid}{\alpha}{\mid}_{a}$. Moreover, ${\beta}{\upharpoonright_{!}}$ is a prefix of ${\alpha}{\upharpoonright_{!}}$ and by Lemma 6, for all $b\in A\setminus\{a\}$, ${\mid}{\beta}{\mid}_{b}\leq{\mid}{\alpha}{\mid}_{a}$. Thus, by Lemma 70, ${\parallel}\beta{\parallel}\leq{\mid}A{\mid}\cdot{\mid}\alpha{\mid}_{a}+{\parallel}\alpha{\parallel}-{\mid}\alpha{\mid}_{a}$. Consequently, ${\parallel}\beta{\parallel}\leq({\mid}A{\mid}-1)\cdot{\mid}\alpha{\mid}_{a}+{\parallel}\alpha{\parallel}$. Hence, ${\parallel}\beta{\parallel}\leq{\mid}A{\mid}\cdot{\parallel}\alpha{\parallel}$.

Lemma 72

Let $\alpha,\beta$ be histories and $a\in A$. Let $k,l\in\mathbb{N}$ and $\varphi_{1},\ldots,\varphi_{k},\psi_{1},\ldots,\psi_{l}\in{\mathcal{L}}_{aa}$ be such that $\alpha{\upharpoonright}_{!}=\varphi_{1}\ldots\varphi_{k}$ and $\beta{\upharpoonright}_{!}=\psi_{1}\ldots\psi_{l}$. If ${\alpha}{\triangleright_{a}}{\beta}$ then $\deg(\varphi_{1})+\ldots+\deg(\varphi_{k})\geq\deg(\psi_{1})+\ldots+\deg(\psi_{l})$.

{proof}

Suppose $\alpha\triangleright_{a}\beta$. Since $\alpha{\upharpoonright}_{!}=\varphi_{1}\ldots\varphi_{k}$ and $\beta{\upharpoonright}_{!}=\psi_{1}\ldots\psi_{l}$, $\psi_{1}\ldots\psi_{l}$ is a prefix of $\varphi_{1}\ldots\varphi_{k}$. Thus, $\deg(\varphi_{1})+\ldots+\deg(\varphi_{k})\geq\deg(\psi_{1})+\ldots+\deg(\psi_{l})$.

Lemma 73

$(\alpha,\varphi)\ll(\alpha a,\varphi)$, 2. 2.

$(\alpha,\psi)\ll(\alpha\psi,\varphi)$* and $(\alpha,\bot)\ll(\alpha\varphi,\bot)$,* 3. 3.

$(\alpha,\varphi)\ll(\alpha,\neg\varphi)$* and $(\alpha,\varphi)\ll(\alpha\varphi,\bot)$,* 4. 4.

$(\alpha,\varphi)\ll(\alpha,\varphi\vee\psi)$* and $(\alpha,\psi)\ll(\alpha,\varphi\vee\psi)$,* 5. 5.

if ${\alpha}{\triangleright_{a}}{\beta}$ then $(\beta,\varphi)\ll(\alpha,B_{a}\varphi)$, 6. 6.

$(\alpha,\varphi)\ll(\alpha,[\varphi]\psi)$* and $(\alpha\varphi,\psi)\ll(\alpha,[\varphi]\psi)$,* 7. 7.

$(\alpha a,\varphi)\ll(\alpha,[a]\varphi)$, 8. 8.

$(\alpha,\bot)\ll(\alpha,p)$, 9. 9.

$(\alpha,\bot)\ll(\alpha,B_{a}\varphi)$, 10. 10.

$(\alpha,\bot)\ll(\alpha,\neg\varphi)$.

{proof}

Remark that $\deg(\alpha,\varphi)=\deg(\alpha a,\varphi)$. Moreover, since ${\parallel}{\alpha}{\parallel}+{\parallel}{\varphi}{\parallel}<{\parallel}{\alpha}{\parallel}+1+{\parallel}{\varphi}{\parallel}$, $(\alpha,\varphi)\ll(\alpha a,\varphi)$. 2. 2.

Remark that $\deg(\alpha,\psi)\leq\deg(\alpha\psi,\varphi)$. Moreover, since ${\parallel}{\alpha}{\parallel}+{\parallel}{\psi}{\parallel}<{\parallel}{\alpha}{\parallel}+{\parallel}{\psi}{\parallel}+{\parallel}{\varphi}{\parallel}$, $(\alpha,\psi)\ll(\alpha\psi,\varphi)$. In other respect, $\deg(\alpha,\bot)\leq\deg(\alpha\varphi,\bot)$. Moreover, since ${\parallel}{\alpha}{\parallel}+1<{\parallel}{\alpha}{\parallel}+{\parallel}{\varphi}{\parallel}+1$, $(\alpha,\bot)\ll(\alpha\varphi,\bot)$. 3. 3.

Remark that $\deg(\alpha,\varphi)=\deg(\alpha,\neg\varphi)$. Moreover, since ${\parallel}{\alpha}{\parallel}+{\parallel}{\varphi}{\parallel}<{\parallel}{\alpha}{\parallel}+{\parallel}{\varphi}{\parallel}+1$, $(\alpha,\varphi)\ll(\alpha,\neg\varphi)$. In other respect, remark that $\deg(\alpha,\varphi)=\deg(\alpha\varphi,\bot)$. Moreover, since ${\parallel}\alpha{\parallel}+{\parallel}\varphi{\parallel}<{\parallel}\alpha{\parallel}+{\parallel}\varphi{\parallel}+1$, we obtain that $(\alpha,\varphi)\ll(\alpha\varphi,\bot)$. 4. 4.

Remark that $\deg(\alpha,\varphi)\leq\deg(\alpha,\varphi\vee\psi)$ and $\deg(\alpha,\psi)\leq\deg(\alpha,\varphi\vee\psi)$. Moreover, since ${\parallel}{\alpha}{\parallel}+{\parallel}{\varphi}{\parallel}<{\parallel}{\alpha}{\parallel}+{\parallel}{\varphi}{\parallel}+{\parallel}{\psi}{\parallel}$ and ${\parallel}{\alpha}{\parallel}+{\parallel}{\psi}{\parallel}<{\parallel}{\alpha}{\parallel}+{\parallel}{\varphi}{\parallel}+{\parallel}{\psi}{\parallel}$, we obtain that $(\alpha,\varphi)\ll(\alpha,\varphi\vee\psi)$ and $(\alpha,\psi)\ll(\alpha,\varphi\vee\psi)$. 5. 5.

Suppose ${\alpha}{\triangleright_{a}}{\beta}$. Let $k,l\in\mathbb{N}$ and $\varphi_{1},\ldots,\varphi_{k},\psi_{1},\ldots,\psi_{l}$ be formulas such that $\alpha{\upharpoonright}_{!}=\varphi_{1}\ldots\varphi_{k}$ and $\beta{\upharpoonright}_{!}=\psi_{1}\ldots\psi_{l}$. Hence, by Lemma 72, $\deg(\varphi_{1})+\ldots+\deg(\varphi_{k})\geq\deg(\psi_{1})+\ldots+\deg(\psi_{l})$. Thus, $\deg(\beta,\varphi)<\deg(\alpha,B_{a}\varphi)$. Consequently, $(\beta,\varphi)\ll(\alpha,B_{a}\varphi)$. 6. 6.

Remark that $\deg(\alpha,\varphi)\leq\deg(\alpha,[\varphi]\psi)$ and $\deg(\alpha\varphi,\psi)=\deg(\alpha,[\varphi]\psi)$. Moreover, since ${\parallel}{\alpha}{\parallel}+{\parallel}{\varphi}{\parallel}<{\parallel}{\alpha}{\parallel}+2{\parallel}{\varphi}{\parallel}+{\parallel}{\psi}{\parallel}$ and ${\parallel}{\alpha}{\parallel}+{\parallel}{\varphi}{\parallel}+{\parallel}{\psi}{\parallel}<{\parallel}{\alpha}{\parallel}+2{\parallel}{\varphi}{\parallel}+{\parallel}{\psi}{\parallel}$, we obtain that $(\alpha,\varphi)\ll(\alpha,[\varphi]\psi)$ and $(\alpha\varphi,\psi)\ll(\alpha,[\varphi]\psi)$. 7. 7.

Remark that $\deg(\alpha a,\varphi)=\deg(\alpha,[a]\varphi)$. Moreover, since ${\parallel}{\alpha}{\parallel}+1+{\parallel}{\varphi}{\parallel}<{\parallel}{\alpha}{\parallel}+{\parallel}{\varphi}{\parallel}+2$, we obtain that $(\alpha a,\varphi)\ll(\alpha,[a]\varphi)$. 8. 8.

Remark that $\deg(\alpha,\bot)=\deg(\alpha,p)$. Moreover, since ${\parallel}{\alpha}{\parallel}+1<{\parallel}{\alpha}{\parallel}+2$, $(\alpha,\bot)\ll(\alpha,p)$. 9. 9.

Let $k\in\mathbb{N}$ and $\varphi_{1},\ldots,\varphi_{k}$ be formulas such that $\alpha{\upharpoonright}_{!}=\varphi_{1}\ldots\varphi_{k}$. Remark that $\deg(\alpha,\bot)=\deg(\varphi_{1})+\ldots+\deg(\varphi_{k})$ and $\deg(\alpha,B_{a}\varphi)=\deg(\varphi_{1})+\ldots+\deg(\varphi_{k})+\deg(\varphi)+1$. Hence, $\deg(\alpha,\bot)<\deg(\alpha,B_{a}\varphi)$ and $(\alpha,\bot)\ll(\alpha,B_{a}\varphi)$. 10. 10.

Remark that $\deg(\alpha,\bot)\leq\deg(\alpha,\neg\varphi)$. Moreover, since ${\parallel}{\alpha}{\parallel}+1<{\parallel}{\alpha}{\parallel}+1+{\parallel}{\varphi}{\parallel}$, we obtain that $(\alpha,\bot)\ll(\alpha,\neg\varphi)$.

Appendix: proof details

The second part of the Appendix contains longer proofs. We repeat the exact formulation of the lemmas and propositions in question.

Lemma 28 Let $\varphi,\psi$ be formulas such that $\models^{*}\varphi\leftrightarrow\psi$. Let $M=(W,R,V)$ be a model. Let $\alpha$ be a history. Let $\beta$ be a word such that $\alpha\varphi\beta$ and $\alpha\psi\beta$ are histories and let $\chi$ be a formula. For all states $s\in W$, $s\bowtie\alpha\varphi\beta$ iff $s\bowtie\alpha\psi\beta$, and $s,\alpha\varphi\beta\models\chi$ iff $s,\alpha\psi\beta\models\chi$.

{proof}

By $\ll$-induction on $(\beta,\chi)$.

Case “$(\beta,\chi)=(\epsilon,\bot)$”. Left to the reader.

Case “$(\beta,\chi)=(\beta^{\prime}a,\bot)$”. We have: $s\bowtie\alpha\varphi\beta^{\prime}a$ iff $s\bowtie\alpha\varphi\beta^{\prime}$ and $|\alpha\varphi\beta^{\prime}|_{a}<|\alpha\varphi\beta^{\prime}|_{!}$ iff, by induction hypothesis and using the fact that $(\beta^{\prime},\bot)\ll(\beta^{\prime}a,\bot)$, $s\bowtie\alpha\psi\beta^{\prime}$ and $|\alpha\psi\beta^{\prime}|_{a}<|\alpha\psi\beta^{\prime}|_{!}$, iff $s\bowtie\alpha\psi\beta^{\prime}a$. Moreover, neither $s,\alpha\varphi\beta^{\prime}a\models\bot$, nor $s,\alpha\psi\beta^{\prime}a\models\bot$.

Case “$(\beta,\chi)=(\beta^{\prime}\chi^{\prime},\bot)$”. We have: $s\bowtie\alpha\varphi\beta^{\prime}\chi^{\prime}$ iff $s\bowtie\alpha\varphi\beta^{\prime}$ and $s\alpha\varphi\beta^{\prime}\models\chi^{\prime}$ iff, by induction hypothesis and using the fact that $(\beta^{\prime},\bot)\ll(\beta^{\prime}\chi^{\prime},\bot)$, $s\bowtie\alpha\psi\beta^{\prime}$ and $s\alpha\psi\beta^{\prime}\models\chi^{\prime}$, iff $s\bowtie\alpha\psi\beta^{\prime}\chi^{\prime}$. Again, neither $s,\alpha\varphi\beta^{\prime}\chi\models\bot$, nor $s,\alpha\psi\beta^{\prime}\chi\models\bot$.

Case “$(\beta,\chi)=(\beta,p)$”. We have: $s\bowtie\alpha\varphi\beta$ iff, by induction hypothesis and using the fact that $(\beta,\bot)\ll(\beta,p)$, $s\bowtie\alpha\psi\beta$. Moreover, we have: $s,\alpha\varphi\beta\models p$ iff $s\in V(p)$ iff $s,\alpha\psi\beta\models p$.

Case “$(\beta,\chi)=(\beta,\neg\chi^{\prime})$”. We have: $s\bowtie\alpha\varphi\beta$ iff, by induction hypothesis and the fact that $(\beta,\chi^{\prime})\ll(\beta,\neg\chi^{\prime})$, $s\bowtie\alpha\psi\beta$. Morever, $s,\alpha\varphi\beta\models\neg\chi^{\prime}$ iff $s,\alpha\varphi\beta\not\models\chi^{\prime}$ iff, by induction hypothesis and the fact that $(\beta,\chi^{\prime})\ll(\beta,\neg\chi^{\prime})$, $s,\alpha\psi\beta\not\models\chi^{\prime}$ iff $s,\alpha\psi\beta\models\neg\chi^{\prime}$.

Case “$(\beta,\chi)=(\beta,\chi_{1}\vee\chi_{2})$”. We have: $s\bowtie\alpha\varphi\beta$ iff, by induction hypothesis and the facts that $(\beta,\chi_{1})\ll(\beta,\chi_{1}\vee\chi_{2})$ and $(\beta,\chi_{2})\ll(\beta,\chi_{1}\vee\chi_{2})$, $s\bowtie\alpha\psi\beta$. Moreover, $s,\alpha\varphi\beta\models\chi_{1}\vee\chi_{2}$ iff ($s,\alpha\varphi\beta\models\chi_{1}$ or $s,\alpha\varphi\beta\models\chi_{2}$) iff, by induction hypothesis and the facts that $(\beta,\chi_{1})\ll(\beta,\chi_{1}\vee\chi_{2})$ and $(\beta,\chi_{2})\ll(\beta,\chi_{1}\vee\chi_{2})$, $s,\alpha\psi\beta\models\chi_{1}$ or $s,\alpha\psi\beta\models\chi_{2}$ iff $s,\alpha\psi\beta\models\chi_{1}\vee\chi_{2}$.

Case “$(\beta,\chi)=(\beta,[a]\chi^{\prime})$”. We have: $s\bowtie\alpha\varphi\beta$ iff, by induction hypothesis and the fact that $(\beta,\chi^{\prime})\ll(\beta,[a]\chi^{\prime})$, $s\bowtie\alpha\psi\beta$. Morever, $s,\alpha\varphi\beta\models[a]\chi^{\prime}$ iff ${\mid}{\alpha\varphi\beta}{\mid}_{a}<{\mid}{\alpha\varphi\beta}{\mid}_{!}$ implies $s,\alpha\varphi\beta\models\chi^{\prime}$ iff, by induction hypothesis and the fact that $(\beta,\chi^{\prime})\ll(\beta,[a]\chi^{\prime})$, ${\mid}{\alpha\psi\beta}{\mid}_{a}<{\mid}{\alpha\psi\beta}{\mid}_{!}$ implies $s,\alpha\psi\beta\models\chi^{\prime}$ iff $s,\alpha\psi\beta\models[a]\chi^{\prime}$.

Case “$(\beta,\chi)=(\beta,[\eta]\chi)$”. We have: $s\bowtie\alpha\varphi\beta$ iff, by induction hypothesis and the fact that $(\beta,\chi^{\prime})\ll(\beta,[\eta]\chi^{\prime})$, $s\bowtie\alpha\psi\beta$. Morever, $s,\alpha\varphi\beta\models[\eta]\chi^{\prime}$ iff $s,\alpha\varphi\beta\models\eta$ implies $s,\alpha\varphi\beta\eta\models\chi^{\prime}$ iff, by induction hypothesis and the fact that $(\beta,\eta)\ll(\beta,[\eta]\chi^{\prime})$ and $(\beta\eta,\chi^{\prime})\ll(\beta,[\eta]\chi^{\prime})$, $s,\alpha\psi\beta\models\eta$ implies $s,\alpha\psi\beta\eta\models\chi^{\prime}$ iff $s,\alpha\psi\beta\models[\eta]\chi^{\prime}$.

Case “$(\beta,\chi)=(\beta,B_{a}\chi^{\prime})$”. We have: $s\bowtie\alpha\varphi\beta$ iff, by induction hypothesis and the fact that $(\beta,\chi^{\prime})\ll(\beta,B_{a}\chi^{\prime})$, $s\bowtie\alpha\psi\beta$. Moreover, suppose $s,\alpha\varphi\beta\not\models B_{a}\chi^{\prime}$. Let $t$ be a state and $\delta$ be a history such that $sR_{a}t$, $\alpha\varphi\beta\triangleright_{a}\delta$, $t\bowtie\delta$ and $t,\delta\not\models\chi^{\prime}$. Let $\delta[\varphi/\psi]$ be the history obtained from $\delta$ by eventually replacing an occurrence of $\varphi$ by $\psi$. Since $\alpha\varphi\beta\triangleright_{a}\delta$, $\alpha\psi\beta\triangleright_{a}\delta[\varphi/\psi]$. Now, since $t\bowtie\delta$ and $t,\delta\not\models\chi^{\prime}$, by induction hypothesis, $t\bowtie\delta[\varphi/\psi]$ and $t,\delta[\varphi/\psi]\not\models\chi^{\prime}$. Consequently, $s,\alpha\psi\beta\not\models B_{a}\chi^{\prime}$.

Lemma 39 Let $(W,R,V)$ be a model and $s\in W$. For all words $\alpha$ over $A\cup{\mathcal{L}}_{aa}$ and for all formulas $\varphi$, $s,\epsilon\models tr(\alpha,\varphi)$ iff $s,\epsilon\models[\alpha]\varphi$. {proof} The proof is done by $\ll$-induction on $(\alpha,\varphi)$. In all cases we only show the proof direction from left to right, as the other direction can be shown in a similar way.

Case $\alpha=\epsilon$ and $\varphi=\bot$. Obviously, $s,\epsilon\not\models tr(\epsilon,\bot)$ and $s,\epsilon\not\models[\epsilon]\bot$.

Case $\alpha=\beta a$ and $\varphi=\bot$. Suppose $s,\epsilon\models tr(\beta a,\bot)$. Hence, $s,\epsilon\models tr(\beta,\bot)$ and ${\mid}\beta{\mid}_{a}<{\mid}\beta{\mid}_{!}$, or ${\mid}\beta{\mid}_{a}\geq{\mid}\beta{\mid}_{!}$. In the former case, by induction hypothesis, $s,\epsilon\models[\beta]\bot$. Thus, by Lemma 23, $s\not\bowtie\beta$. Consequently, $s\not\bowtie\beta a$. Hence, by Lemma 23 again, $s,\epsilon\models[\beta a]\bot$. In the latter case, $s\not\bowtie\beta a$. Thus, by Lemma 23, $s,\epsilon\models[\beta a]\bot$.

Case $\alpha=\beta\psi$ and $\varphi=\bot$. Suppose $s,\epsilon\models tr(\beta\psi,\bot)$. Hence, $s,\epsilon\not\models tr(\beta,\psi)$ or $s,\epsilon\models tr(\beta,\bot)$. In the former case, by induction hypothesis, $s,\epsilon\not\models[\beta]\psi$. Thus, by Lemma 23, $s\bowtie\beta$ and $s,\beta\not\models\psi$. Consequently, $s\not\bowtie\beta\psi$. Hence, by Lemma 23 again, $s,\epsilon\models[\beta\psi]\bot$. In the latter case, by induction hypothesis, $s,\epsilon\models[\beta]\bot$. Thus, by Lemma 23, $s\not\bowtie\beta$. Consequently, $s\not\bowtie\beta\psi$. Hence, by Lemma 23 again, $s,\epsilon\models[\beta\psi]\bot$.

Case $\varphi=p$. Suppose $s,\epsilon\models tr(\alpha,p)$. Hence, $s,\epsilon\models tr(\alpha,\bot)$, or $s,\epsilon\not\models tr(\alpha,\bot)$ and $s,\epsilon\models p$. In the former case, by induction hypothesis, $s,\epsilon\models[\alpha]\bot$. Thus, by Lemma 23, $s\not\bowtie\alpha$. Consequently, by Lemma 23 again, $s,\epsilon\models[\alpha]p$. In the latter case, by induction hypothesis, $s,\epsilon\not\models[\alpha]\bot$. Moreover, $s\in V(p)$. Hence, by Lemma 23, $s\bowtie\alpha$. Moreover, $s,\alpha\models p$. Thus, by Lemma 23 again, $s,\epsilon\models[\alpha]p$.

Case $\varphi=\neg\psi$. Suppose $s,\epsilon\models tr(\alpha,\neg\psi)$. Hence, $s,\epsilon\not\models tr(\alpha,\psi)$ or $s,\epsilon\models tr(\alpha,\bot)$ In the former case, by induction hypothesis, $s,\epsilon\not\models[\alpha]\psi$. Thus, by Lemma 23, $s\bowtie\alpha$ and $s,\alpha\not\models\psi$. Consequently, by Lemma 23 again, $s,\epsilon\models[\alpha]\neg\psi$. In the latter case, by induction hypothesis, $s,\epsilon\models[\alpha]\bot$. Hence, by Lemma 23, $s\not\bowtie\alpha$. Thus, by Lemma 23 again, $s,\epsilon\models[\alpha]\neg\psi$.

Case $\varphi=\psi\vee\chi$. Suppose $s,\epsilon\models tr(\alpha,\psi\vee\chi)$. Hence, $s,\epsilon\models tr(\alpha,\psi)$ or $s,\epsilon\models tr(\alpha,\chi)$. In the former case, by induction hypothesis, $s,\epsilon\models[\alpha]\psi$. Thus, by Lemma 23, $s\not\bowtie\alpha$ or $s,\alpha\models\psi$. Consequently, $s\not\bowtie\alpha$ or $s,\alpha\models\psi\vee\chi$. Hence, by Lemma 23 again, $s,\epsilon\models[\alpha](\psi\vee\chi)$. The latter case is similarly treated.

Case $\varphi=B_{a}\psi$. Suppose $s,\epsilon\models tr(\alpha,B_{a}\psi)$. Hence, $s,\epsilon\models tr(\alpha,\bot)$ or $s,\epsilon\models\bigwedge\{B_{a}tr(\beta,\psi)\mid\alpha\triangleright_{a}\beta\}$. In the former case, by induction hypothesis, $s,\epsilon\models[\alpha]\bot$. Thus, by Lemma 23, $s\not\bowtie\alpha$. Consequently, by Lemma 23 again, $s,\epsilon\models[\alpha]B_{a}\psi$. In the latter case, for the sake of the contradiction, suppose $s,\epsilon\not\models[\alpha]B_{a}\psi$. Thus, by Lemma 23, $s\bowtie\alpha$ and $s,\alpha\not\models B_{a}\psi$. Let $t\in W$ and $\gamma$ be a history such that $sR_{a}t$, $\alpha\triangleright_{a}\gamma$, $t\bowtie\gamma$ and $t,\gamma\not\models\psi$. Since $s,\epsilon\models\bigwedge\{B_{a}tr(\beta,\psi)\mid\alpha\triangleright_{a}\beta\}$, we obtain that $s,\epsilon\models B_{a}tr(\gamma,\psi)$. We recall the reader that $sR_{a}t$. Moreover, obviously, $\epsilon\triangleright_{a}\epsilon$ and $t\bowtie\epsilon$. Consequently, $t,\epsilon\models tr(\gamma,\psi)$. Hence, by induction hypothesis, $t,\epsilon\models[\gamma]\psi$. Thus, by Lemma 23, $t\not\bowtie\gamma$ or $t,\gamma\models\psi$: a contradiction. Consequently, $s,\epsilon\models[\alpha]B_{a}\psi$.

Case $\varphi=[a]\psi$. Suppose $s,\epsilon\models tr(\alpha,[a]\psi)$. Hence, $s,\epsilon\models tr(\alpha a,\psi)$. Thus, by induction hypothesis, $s,\epsilon\models[\alpha a]\psi$. Consequently, $s,\epsilon\models[\alpha][a]\psi$.

Case $\varphi=[\psi]\chi$. Suppose $s,\epsilon\models tr(\alpha,[\psi]\chi)$. Hence, $s,\epsilon\models tr(\alpha\psi,\chi)$. Thus, by induction hypothesis, $s,\epsilon\models[\alpha\psi]\chi$. Consequently, $s,\epsilon\models[\alpha][\psi]\chi$.

Proposition 47 Let $\varphi,\psi\in{\mathcal{L}}_{aa}$. Then

$\models^{*}[\varphi]\bot\leftrightarrow\neg\varphi$ 2. 2.

$\models^{*}[\varphi]p\leftrightarrow(\varphi\rightarrow p)$ 3. 3.

$\models^{*}[\varphi]\neg\psi\leftrightarrow(\varphi\rightarrow\neg[\varphi]\psi)$ 4. 4.

$\models^{*}[\varphi](\psi\vee\chi)\leftrightarrow([\varphi]\psi\vee[\varphi]\chi)$ 5. 5.

$\models^{*}[\varphi]B_{a}\psi\leftrightarrow(\varphi\rightarrow B_{a}\psi)$

{proof}

Let $(W,R,V)$, $s\in W$, and $\alpha$ with $s\bowtie\alpha$ be given. We will implicitly use Corollary 24.

$s,\alpha\models[\varphi]\bot\\ \Leftrightarrow\\ s,\alpha\models\varphi$ implies $s,\alpha\varphi\models\bot\\ \Leftrightarrow\\ s,\alpha\not\models\varphi\\ \Leftrightarrow\\ s,\alpha\models\neg\varphi$. 2. 2.

$s,\alpha\models[\varphi]p\\ \Leftrightarrow\\ s,\alpha\models\varphi$ implies $s,\alpha\varphi\models p\\ \Leftrightarrow(\sharp)\\ s,\alpha\models\varphi$ implies $s,\alpha\models p\\ \Leftrightarrow\\ s,\alpha\models\varphi\rightarrow p$.

The equivalence $(\sharp)$ holds because the value of propositional variables is invariant for history shortening and history extension. 3. 3.

$s,\alpha\models[\varphi]\neg\psi\\ \Leftrightarrow\\ s,\alpha\models\varphi$ implies $s,\alpha\varphi\not\models\psi\\ \Leftrightarrow\\ s,\alpha\models\varphi\rightarrow\neg[\varphi]\psi$. 4. 4.

The proof is elementary. 5. 5.

$s,\alpha\models[\varphi]B_{a}\psi\\ \Leftrightarrow\\ s,\alpha\models\varphi\text{ implies }s,\alpha\varphi\models B_{a}\psi\\ \Leftrightarrow(*)\\ s,\alpha\models\varphi\text{ implies }s,\alpha\models B_{a}\psi\\ \Leftrightarrow\\ s,\alpha\models\varphi\rightarrow B_{a}\psi.\\$

$(*)$: This holds because $s,\alpha\models\varphi$ implies $s\bowtie\alpha\varphi$, and because $\alpha\varphi\triangleright_{a}\beta$ iff $\alpha\triangleright_{a}\beta$, which is true because $|\alpha\varphi|_{a}=|\alpha|_{a}$: the interpretation of knowledge is not affected by adding announcement $\varphi$ to the history $\alpha$.

Proposition 51 $\models^{*}[a][b]\varphi\leftrightarrow[b][a]\varphi$

{proof}

We first show the following, by induction on $\varphi$:

Let $\varphi\in{\mathcal{L}}_{aa}$, $\alpha,\gamma\in({\mathcal{L}}_{aa}\cup A)^{*}$, $s\bowtie\alpha$, and $\beta,\beta^{\prime}\in A^{*}$ such that for all $a\in A$, $|\beta|_{a}=|\beta^{\prime}|_{a}$. If $s\bowtie\alpha\beta\gamma$ and $s\bowtie\alpha\beta^{\prime}\gamma$, then $s,\alpha\beta\gamma\models\varphi$ iff $s,\alpha\beta^{\prime}\gamma\models\varphi$.

Note that $s\bowtie\alpha\beta$ iff $s\bowtie\alpha\beta^{\prime}$, as for each agent $a$ the number of occurrences in $\beta$ and $\beta^{\prime}$ is the same (their order with respect to other agents does not matter). The non-trivial cases of the induction are knowledge, announcement, and reception:

Case $B_{a}\varphi$: Suppose $s,\alpha\beta\gamma\models B_{a}\varphi$. Thus, $t,\delta\models\varphi$ for all $t,\delta$ such that $sR_{a}t$, $\alpha\beta\gamma\triangleright_{a}\delta$, and $t\bowtie\delta$. Observe that $\alpha\beta\gamma\triangleright_{a}\delta$ iff $\alpha\beta^{\prime}\gamma\triangleright_{a}\delta$, as from $|\beta|_{a}=|\beta^{\prime}|_{a}$ it follows that $|\alpha\beta\gamma|_{a}=|\alpha\beta^{\prime}\gamma|_{a}$, and we also have $\alpha\beta\gamma{\upharpoonright}_{!a}=\alpha\beta^{\prime}\gamma{\upharpoonright}_{!a}$, as $\beta$ and $\beta^{\prime}$ do not contain formulas. Therefore, $t,\delta\models\varphi$ for all $t,\delta$ such that $sR_{a}t$, $\alpha\beta^{\prime}\gamma\triangleright_{a}\delta$, and $t\bowtie\delta$, i.e., $s,\alpha\beta^{\prime}\gamma\models B_{a}\varphi$. (No inductive hypothesis is needed.)

Case $[a]\varphi$: Suppose $s,\alpha\beta\gamma\models[a]\varphi$. Thus, $|\alpha\beta\gamma|_{a}<|\alpha\beta\gamma|_{!}$ implies $s,\alpha\beta\gamma{a}\models\varphi$. We now use the inductive hypothesis for $\varphi$, applied to $\gamma^{\prime}=\gamma{a}$, to obtain that ${\mid}\alpha\beta^{\prime}\gamma{\mid}_{a}<{\mid}\alpha\beta\gamma{\mid}_{!}$ implies $s,\alpha\beta^{\prime}\gamma{a}\models\varphi$. Thus, $s,\alpha\beta^{\prime}\gamma\models[a]\varphi$.

Case $[\psi]\varphi$: Suppose $s,\alpha\beta\gamma\models[\psi]\varphi$. Thus, ($s,\alpha\beta\gamma\models\psi$ implies $s,\alpha\beta\gamma\psi\models\varphi$). The antecedent of the implication is equivalent to $s,\alpha\beta^{\prime}\gamma\models\psi$, by induction. The consequent of the implication is equivalent to $s,\alpha\beta^{\prime}\gamma\psi\models\varphi$, also by induction. Therefore, $s,\alpha\beta^{\prime}\gamma\models\psi$ implies $s,\alpha\beta^{\prime}\gamma\psi\models\varphi$. Hence, $s,\alpha\beta^{\prime}\gamma\models[\psi]\varphi$.

This completes the inductive proof. A corollary is:

Let $\beta,\beta^{\prime}\in A^{*}$ such that for all $a\in A$, $|\beta|_{a}=|\beta^{\prime}|_{a}$. Then $\models^{*}[\beta]\varphi\leftrightarrow[\beta^{\prime}]\varphi$.

The proposition to be proved is the special case for $\beta=ab$ and $\beta^{\prime}=ba$.

Proposition 54 Let $\varphi\in{\mathcal{L}}_{aa}$ and such that $B_{a}$ and $[a]$ do not occur in $\varphi$. Then $\models^{*}\neg[a]\bot\rightarrow([a]\varphi\leftrightarrow\varphi)$. {proof} This follows directly from the following slightly stronger proposition (namely from the case for $\beta=\epsilon$). By “$a$ does not occur in $\varphi$” we mean “$\varphi$ is a formula in the language ${\mathcal{L}}_{aa}$ with respect to the set of agents $A\setminus\{a\}$,” i.e., $B_{a}$ and $[a]$ do not occur in $\varphi$. By “$a$ does not occur in history $\alpha$” we mean “$a$ does not occur as an agent (as a letter) in $\alpha$ and $a$ does not occur in any formula $\psi$ that occurs (as a letter) in $\alpha$.”

Given are $\varphi\in{\mathcal{L}}_{aa}$, model $(W,R,V)$ with $s\in W$, and histories $\alpha$ and $\beta$, such that $a$ does not occur in $\beta$ or $\varphi$, and $|\alpha|_{!}>|\alpha|_{a}$. Then $s,\alpha{a}\beta\models\varphi$ iff $s,\alpha\beta\models\varphi$.

The proof is by induction on the structure of $\varphi$. The cases $\bot$, $p$, $\varphi\wedge\psi$, and $\neg\varphi$ are elementary. We note that the induction in the cases $[\varphi]\psi$ and $[b]\psi$ below is justified, as it applies to $\psi$ for any $\alpha$ and $\beta$ (where $a$ does not occur in $\beta$), therefore including the $\beta\varphi$ and $\beta{b}$, also in the proof below.

Case $[\varphi]\psi$:

$s,\alpha{a}\beta\models[\varphi]\psi\\ \Leftrightarrow\\ s,\alpha{a}\beta\models\varphi\text{ implies }s,\alpha{a}\beta\varphi\models\psi\\ \Leftrightarrow(\text{IH})\\ s,\alpha\beta\models\varphi\text{ implies }s,\alpha\beta\varphi\models\psi\\ \Leftrightarrow\\ s,\alpha\beta\models[\varphi]\psi$

Case $[b]\psi$ ($b\neq a$):

$s,\alpha{a}\beta\models[b]\psi\\ \Leftrightarrow\\ |\alpha{a}\beta|_{b}<|\alpha{a}\beta|_{!}$ implies $s,\alpha{a}\beta{b}\models\psi\\ \Leftrightarrow(\text{IH})\\ |\alpha{a}\beta|_{b}<|\alpha{a}\beta|_{!}$ implies $s,\alpha\beta{b}\models\psi\\ \Leftrightarrow\\ |\alpha\beta|_{b}<|\alpha\beta|_{!}$ implies $s,\alpha\beta{b}\models\psi\\ \Leftrightarrow\\ s,\alpha\beta\models[b]\psi$

Case $B_{b}\psi$:

By definition: $s,\alpha{a}\beta\models B_{b}\psi$ iff $t,\delta\models\psi\text{ for any }t,\delta\text{ such that }sR_{a}t,\alpha{a}\beta\triangleright_{b}\delta,\text{ and }t\bowtie\delta$. It then suffices to prove that $\alpha{a}\beta\triangleright_{b}\delta$ iff $\alpha\beta\triangleright_{b}\delta$. But this follows directly from the fact that $|\alpha a\beta|_{b}=|\alpha\beta|_{b}$ and $|\alpha a\beta|_{!}=|\alpha\beta|_{!}$, and thus $\alpha a\beta{\upharpoonright}_{!b}=\alpha\beta{\upharpoonright}_{!b}$, which entails that

[TABLE]

Proposition 63 Let $\varphi\in{\mathcal{L}}_{aa}$ be given. For all $M$, and $s$ and $\alpha$ with $s\bowtie\alpha$, $s,\alpha\models\varphi$ iff $M^{\alpha{\upharpoonright}_{!}},s,\alpha\models\varphi$.

{proof}

Instead of the above, we prove the slightly stronger proposition:

Let $\varphi\in{\mathcal{L}}_{aa}$ be given. For all $M$, and $s$ and $\alpha,\beta$ with $s\bowtie\alpha$ and $\alpha{\upharpoonright}_{!}\subseteq\beta{\upharpoonright}_{!}$, $s,\alpha\models\varphi$ iff $M^{\beta{\upharpoonright}_{!}},s,\alpha\models\varphi$.

From this, the required follows for $\alpha=\beta$.222As a matter of interest the stronger proposition also proves that truth in asynchronous models is preserved under history extension: let $\gamma{\upharpoonright}_{!}\subseteq\alpha{\upharpoonright}_{!}\subseteq\beta{\upharpoonright}_{!}$, then $M^{\alpha{\upharpoonright}_{!}},s,\gamma\models\varphi$ implies $M^{\beta{\upharpoonright}_{!}},s,\gamma\models\varphi$. The proof is by induction on $\varphi$. All cases are elementary except those involving modalities. Let $M$, and $s$ and $\alpha$ with $s\bowtie\alpha$ be given.

Case $B_{a}\varphi$:

$s,\alpha\models B_{a}\varphi\\ \Leftrightarrow\\ t,\gamma\models\varphi\ \text{for all}\ (t,\gamma)\ \text{such that}\ sR_{a}t,\alpha\triangleright_{a}\gamma,\text{and}\ t\bowtie\gamma\\ \Leftrightarrow\hfill\text{induction, use that}\ \gamma{\upharpoonright}_{!}=\alpha{\upharpoonright}_{!a}\subseteq\alpha{\upharpoonright}_{!}\subseteq\beta{\upharpoonright}_{!}\\ M^{\beta{\upharpoonright}_{!}},t,\gamma\models\varphi\ \text{for all}\ (t,\gamma)\ \text{such that}\ sR_{a}t,\alpha\triangleright_{a}\gamma,\text{and}\ t\bowtie\gamma\\ \Leftrightarrow\hfill\text{by definition,}\ (s,\alpha)R^{\prime}_{a}(t,\gamma)\ \text{iff}\ sR_{a}t\ \text{and}\ \alpha\triangleright_{a}\gamma,\text{and}\ t\bowtie\gamma\ \text{as}\ (t,\gamma)\in W^{\prime}\\ M^{\beta{\upharpoonright}_{!}},t,\gamma\models\varphi\text{ for all }(t,\gamma)\ \text{such that}\ (s,\alpha)R^{\prime}_{a}(t,\gamma)\ \text{and}\ (s,\alpha)R^{\prime}_{\triangleright_{a}}(t,\gamma)\\ \Leftrightarrow\\ M^{\beta{\upharpoonright}_{!}},s,\alpha\models B_{a}\varphi$

Case $[\varphi]\psi$:   In this case we need to distinguish subcase $\alpha\varphi{\upharpoonright}_{!}\subseteq\beta{\upharpoonright}_{!}$ from subcase $\alpha\varphi{\upharpoonright}_{!}\not\subseteq\beta{\upharpoonright}_{!}$. Below we show the second subcase, for the first subcase, replace below the occurrences of $M^{\alpha\varphi{\upharpoonright}_{!}}$ by $M^{\beta{\upharpoonright}_{!}}$ and remove the last equivalence.

s,\alpha\models[\varphi]\psi\\ \Leftrightarrow\\ s,\alpha\models\varphi\ \text{implies}\ s,\alpha\varphi\models\psi\\ \Leftrightarrow\hfill\text{induction}\\ M^{\alpha\varphi{\upharpoonright}_{!}},s,\alpha\models\varphi\ \text{implies}\ M^{\alpha\varphi{\upharpoonright}_{!}},s,\alpha\varphi\models\psi\\ \Leftrightarrow\hfill\text{either M^{\alpha\varphi{\upharpoonright}{!}},s,\alpha\not\models\varphi$, or the unique$R^{\prime}{\varphi}$-successor is$(t,\gamma)=(s,\alpha\varphi)}\\ M^{\alpha\varphi{\upharpoonright}_{!}},t,\gamma\models\psi\text{ for all }(t,\gamma)\text{ such that }(s,\alpha)R^{\prime}_{\varphi}(t,\gamma)\\ \Leftrightarrow\\ M^{\alpha\varphi{\upharpoonright}_{!}},s,\alpha\models[\varphi]\psi\\ \Leftrightarrow\hfill\text{case `else' of the semantics of [\varphi]\psi applies, as}\ \alpha\varphi{\upharpoonright}_{!}\not\subseteq\beta{\upharpoonright}_{!}\\ M^{\beta{\upharpoonright}_{!}},s,\alpha\models[\varphi]\psi

Case $[a]\varphi$:

s,\alpha\models[a]\varphi\\ \Leftrightarrow\\ |\alpha|_{a}<|\alpha|_{!}\ \text{implies}\ s,\alpha{a}\models\varphi\\ \Leftrightarrow\hfill\text{induction, also use that}\ \alpha{\upharpoonright}_{!}=\alpha{a}{\upharpoonright}_{!}\\ |\alpha|_{a}<|\alpha|_{!}\ \text{implies}\ M^{\beta{\upharpoonright}_{!}},s,\alpha{a}\models\varphi\\ \Leftrightarrow\hfill\text{either |\alpha|{a}=|\alpha|{!}$, or the unique$R^{\prime}_{[a]}$-successor is$(t,\gamma)=(s,\alpha{a})}\\ M^{\beta{\upharpoonright}_{!}},t,\gamma\models\varphi\text{ for all }(t,\gamma)\ \text{such that}\ (s,\alpha)R^{\prime}_{[a]}(t,\gamma)\\ \Leftrightarrow\\ M^{\beta{\upharpoonright}_{!}},s,\alpha\models[a]\varphi