Logics for Epistemic Actions: Completeness, Decidability, Expressivity ^†

Abstract

We build and study dynamic versions of epistemic logic. We study languages parameterized by an action signature that allows one to express epistemic actions such as (truthful) public announcements, completely private announcements to groups of agents, and more. The language $\mathcal{L}$(Σ) is modeled on dynamic logic. Its sentence-building operations include modalities for the execution of programs, and for knowledge and common knowledge. Its program-building operations include action execution, composition, repetition, and choice. We consider two fragments of $\mathcal{L}(\mathbf{\Sigma })$. In ${\mathcal{L}}_1(\mathbf{\Sigma })$, we drop action repetition; in ${\mathcal{L}}_0(\mathbf{\Sigma })$, we also drop common knowledge. We present the syntax and semantics of these languages and sound proof systems for the validities in them. We prove the strong completeness of a logical system for ${\mathcal{L}}_0(\mathbf{\Sigma })$ and the weak completeness of one for ${\mathcal{L}}_1(\mathbf{\Sigma })$. We show the finite model property and, hence, decidability of ${\mathcal{L}}_1(\mathbf{\Sigma })$. We translate ${\mathcal{L}}_1(\mathbf{\Sigma })$ into PDL, obtaining a second proof of decidability. We prove results on expressive power, comparing ${\mathcal{L}}_1(\mathbf{\Sigma })$ with modal logic together with transitive closure operators. We prove that a logical language with operators for private announcements is more expressive than one for public announcements.

1. Introduction

One of the goals of dynamic epistemic logic is to construct logical languages which allow one to represent a variety of possible types of changes affecting the information states of agents in a multi-agent setting. One wants (formal) logical systems with primitive operations corresponding to (informal) notions such as public announcement, completely private announcement, and private announcement to one agent with suspicion by another, etc. And then, after the logics are formulated, one would ideally want technical tools to use in their study and application.

The full formulation of such logics is somewhat of a complicated story. In the first place, one needs a reasonable syntax. On the semantic side, there is an unusual feature in that the truth of a sentence at a point in one model often depends on the truth of a related sentence in a different model. In effect, the kinds of actions we are interested in give rise to functions, or relations more generally, on the class of all possible models.

There have been some proposals on logical systems for dynamic epistemic logic beginning with the work of Plaza [1], Gerbrandy [2,3], and Gerbrandy and Groeneveld [4]. These papers formulated logical systems for the informal notions of public announcement and completely private announcement. They left open the matter of axiomatizing the logics in the presence of common-knowledge operators. (Without the common-knowledge operators, the systems are seen to be variants on standard multi-model logic.) And they also left open the question of the decidability of these systems. Our work began with complete axiomatizations for these systems and for more general systems. Our results were presented in [5]. As it happens, the logics which we constructed in [5] did not have the friendliest syntax. The first two authors pursued this matter for some time and eventually came to the proposals in [6]. The logical systems for the validities of the ultimate languages are certainly related to those in [5]. But due to the different formulation of the overall syntax and semantics, all of the work on soundness and completeness had to be completely reworked. The main purpose of the present paper is to present these results. Secondarily, we present some technical results on the systems such as results on expressive power.

1.1. Contents of This Paper: A High-Level View

This paper is a long technical development, and for this reason we did not include a full-scale motivation of the logical systems themselves. For a great deal of the motivational material, one should see [5]. Section 2 formulates all of the definitions needed in the paper. The presentation is based closely on the work in [6], so readers familiar with that paper may use Section 2 as a review. Other readers of this paper could take the logical systems here to simply be extensions of propositional dynamic logic which allow one to make “transitions from model to model” in addition to transitions “inside a given model”. In addition, Section 2.8 is new in this paper.

The logical languages studied in this paper are presented in Section 3. Section 3.2 presents some examples of the semantics, chosen to foreshadow work in Section 6 on expressive power. The logical system is presented in Section 4, along with a soundness result for most of the system. The completeness theorem for the logic comes in Section 5. The final section deals with questions of expressive power, and it may be read after Section 4.

Two aspects of our overall machinery are worth pointing out. The first is the use of the canonical action model. This is a semantic object built from syntactic objects (sequences of simple actions, terms in our language $\mathcal{L}(\mathbf{\Sigma })$). We would like to think that the use of the canonical model makes for a more elegant presentation than one would otherwise have.

The second feature is a term rewriting system for dealing with assertions in the language. The semantic equivalences in dynamic epistemic logic are sufficiently complicated that the ‘subsentence’ relation is not the most natural or useful one for many purposes. Instead, one needs to handcraft various ordering relations for use in inductive proofs, or in defining translations. For just one example, in the logic of public announcements one has an announcement–knowledge axiom in a form such as

$$[!\phi ]\square \psi \leftrightarrow (\phi \to \square [!\phi \left]\psi \right).$$

(1)

(Here, the notation $[!\phi ]\psi$ can be read: if $\phi$ is true, then after announcing it publicly, $\psi$ is true.) This is for a logic with just one agent, and in this discussion we are forgetting about common knowledge. To prove that the logic has a translation t back to ordinary modal logic, one wants to use the equivalence in (1), above, as the key step in the translation, defining ${(\left[\phi \right]\square \psi )}^t$ to be ${\phi }^t\to {(\square [!\phi ]\psi )}^t$. But then one needs to have some reason to say that both $\phi$ and (more critically) $\square [!\phi ]\psi$ are of lower complexity than the original formula $\left[\phi \right]\square \psi$. There are several ways to make this precise. One is to directly assign an element of some well-founded set to each formula and then use this as a measure of complexity. This is carried out in [7], and the well-founded set is the natural numbers. Our treatment is different, mainly because it goes via term rewriting. In effect, one takes the well-founded set to be the sentences themselves, with the order given by substitution using laws such as (1), but oriented in a specified direction (left to right, for example). Then the fact that we have a well-founded relation is a result one proves about oriented sets of laws (term rewriting systems). In our case, we use an interpretation constructed by hand.

Our term rewriting system is presented and studied in Section 5.2. It actually deals not with $\mathcal{L}(\mathbf{\Sigma })$ but with a different language called ${\mathcal{L}}_1(\mathbf{\Sigma })$. An important by-product of our completeness proof via rewriting is a Normal Form Theorem for ${\mathcal{L}}_1(\mathbf{\Sigma })$. This is an interesting result in itself, and it does not follow from other completeness proofs such as those in [7]. In order to use the rewriting system, one needs to know that substitution of “equivalent” objects preserves “equivalence” and that the proof system itself is strong enough to reduce sentences to normal form. Unfortunately, this “obvious” point takes a great deal of work. The details are all in this paper, and to our knowledge no other source presents complete proofs on these matters.

1.2. Comparison with Some Other Work

The first version of this paper is our 1998 conference publication [5]. We ourselves had several versions of this paper issued as technical reports or posted on web sites, and so in some sense the results here are public but not published. Since its inception, the subject of dynamic epistemic logic has taken off in a serious way. It sees dozens of papers a year. But it seems fair to say that the overall topics of investigation are not the logical systems presented in any of the original papers but rather are adaptations of the logics to settings involving probability, belief revision, quantum information, and the like. Still, the work reported here has been the subject of several existing publications. And so it makes sense for us to make the case that the results in this paper are still relevant and do not follow from previously published results.

Our 2016 paper [8] is also a follow-up version of [5]. But in [8], we did not have the space to include all of the material in this paper, and so the particular logic in that paper was a fragment of the one here, with a simpler technical treatment. In addition, the first part of [8] is from [6] and goes beyond what we do here.

The book Dynamic Epistemic Logic by Hans van Ditmarsch, Wiebe van der Hoek, and Barteld Kooi [7] is a textbook presentation containing some of the content of this paper and [6], with additional material on model checking, belief revision, and other topics. Section 6.4 presents the syntax of what it calls action model logic and writes as ${\mathcal{L}}_{KC\otimes }^{\mathrm{act}}(A,P)$. At first glance, the syntax of ${\mathcal{L}}_{KC\otimes }^{\mathrm{act}}(A,P)$ seems fairly close to the language $\mathcal{L}(\mathbf{\Sigma })$ presented in [6] and reviewed in Section 3 of this paper. A relatively small difference concerns the action models in ${\mathcal{L}}_{KC\otimes }^{\mathrm{act}}(A,P)$. (In general, action models are like Kripke models together with a “precondition” function mapping worlds to sentences.) These are required to have the property that each agent’s accessibility relation is an equivalence relation; our treatment is more general and, hence, can present logics for epistemic actions such as “cheating” in games. But the main difference is that our language $\mathcal{L}(\mathbf{\Sigma })$ uses what everyone would take to be a bona-fide syntax: sentences and program expressions are linearly ordered strings of symbols. In contrast, the syntax of ${\mathcal{L}}_{KC\otimes }^{\mathrm{act}}(A,P)$ employs action models directly. Structured but unordered objects occur inside of sentences. In a different context, it would be like studying formal language and their connection to automata by studying something that was like a regular expression but allowed finite automata to directly occur inside some syntactic object.

We have no objection ourselves to this move. In fact, this was the presentation we chose in our first version [5] of this paper. But over the years we have found quite a lot of resistance to this presentation on the grounds that one is “mixing syntax and semantics”. Again, we do not assert this objection, but we address it by employing the large technical machinery that we see in [6] and also Section 2 and Section 3. (We are keenly aware of the irony of our being criticized for “mixing syntax and semantics” in [5], and after we “un-mixed” them in [6], we find others making the same natural move.)

We would also like to mention the paper “Logics of Communication and Change”, van Benthem, van Eijck and Kooi [9]. This paper presents completeness theorem for a logical system in the same family as ours. But as it happens, the paper studies a different system. To see the differences, it is worthwhile to note that the source of much of the work in this area concerns assertions of common knowledge following an action of some sort. In our setting, these would be written $\left[\alpha \right]{\square }^{\ast }\phi$. It turns out that there is no equivalence of the form (1) for assertions such as this. This leads us to our action rule, an inference rule allowing the derivation of sentences of the kind under discussion. The idea in [9] is to start with a more expressive ’static’ language (than just epistemic logic with common knowledge), namely, an ‘epistemic’ version of propositional dynamic logic, called E-PDL in the paper (‘E’ for ‘epistemic’). Then one adds ‘action’ modalities corresponding to update models $[\mathsf{U},e]$; this modality would be like our $\left[\alpha \right]$, but in [9] as in [5,7], this U is an action model rather than a bona-fide syntactic object. One can then prove that the action modalities can be translated away into the static base, via reduction axioms. This very interesting and suggestive result is not available in our more restrictive setting, but that seems to be the price for sticking with a language that has a very clear epistemic interpretation. In fact, it is not known whether E-PDL is actually stronger than the logical systems in this paper 1, and if it is then it is not clear what is the epistemic use of this additional expressive power 2.

Finally, we would like to mention several articles quite related to our topic which appear in online sources or in handbooks: [10,11,12]. These sources should be useful to anyone wishing to obtain a wider perspective on the ideas in this paper or a slightly different presentation of them.

2. Definitions

This section provides all of our definitions. It is short on motivation, and we have situated the examples in Section 3.2, following all the definitions. See also Sections 1 and 2 of [6] for the motivation from epistemic logic and for a more leisurely presentation.

2.1. State Models and Propositions

We fix a set $\mathsf{AtSen}$ of atomic sentences and also a set $\mathcal{A}$ of agents. All of our definitions are relative to these sets.

A state model is a triple $\mathbf{S}=(S,{\stackrel{\mathcal{A}}{\to }}_{\mathbf{S}},\parallel ·{\parallel }_{\mathbf{S}})$ consisting of a non-empty set S of “states”; a family ${\stackrel{A}{⟶}}_{\mathbf{S}}$ of binary accessibility relations ${\stackrel{A}{⟶}}_{\mathbf{S}}\subseteq S\times S$, one for each agent $A\in \mathcal{A}$; and a “valuation” (or a “truth” map) ${\parallel .\parallel }_{\mathbf{S}}:\mathsf{AtSen}\to \mathcal{P}\left(S\right)$, assigning to each atomic sentence p a set ${\parallel p\parallel }_{\mathbf{S}}$ of states. These are exactly Kripke models generalized by having one accessibility relation for each agent. We use the terminology of state models because there are other kinds of models, action models and program models, in our study. When dealing with a single fixed-state model $\mathbf{S}$, we often drop the subscript $\mathbf{S}$ from all the notation.

Definition 2.1. 

Let $\mathsf{SMod}$ be the collection of all state models. An epistemic proposition is an operation $\mathit{\phi }$ defined on $\mathsf{SMod}$ such that for all $\mathbf{S}\in \mathsf{SMod}$, ${\mathit{\phi }}_{\mathbf{S}}\subseteq S$.

The collection of epistemic propositions is closed in various ways.

• For each atomic sentence p we have an atomic proposition p with ${\mathit{p}}_{\mathbf{S}}={\parallel p\parallel }_{\mathbf{S}}$.
• If $\mathit{\phi }$ is an epistemic proposition, then so is $\neg \mathit{\phi }$, where ${(\neg \mathit{\phi })}_{\mathbf{S}}=S\setminus {\mathit{\phi }}_{\mathbf{S}}$.
• If C is a set or class of epistemic propositions, then $\bigwedge C$ is an epistemic proposition, where

  $${(\bigwedge C)}_{\mathbf{S}}=\bigcap \{{\mathit{\phi }}_{\mathbf{S}}:\mathit{\phi }\in C\}.$$
• Taking C, above, to be empty, we have a “universally true” epistemic proposition $\mathbf{tr}$, with ${\mathbf{tr}}_{\mathbf{S}}=S$.
• We also may take C in part 3 to be a two-element set $\{\mathit{\phi },\mathit{\psi }\}$; here, we write $\mathit{\phi }\wedge \mathit{\psi }$ instead of $\bigwedge \{\mathit{\phi },\mathit{\psi }\}$. We see that if $\mathit{\phi }$ and $\mathit{\psi }$ are epistemic propositions, then so is $\mathit{\phi }\wedge \mathit{\psi }$, with ${(\mathit{\phi }\wedge \mathit{\psi })}_{\mathbf{S}}={\mathit{\phi }}_{\mathbf{S}}\cap {\mathit{\psi }}_{\mathbf{S}}$.
• If $\mathit{\phi }$ is an epistemic proposition and $A\in \mathcal{A}$, then ${\square }_A\mathit{\phi }$ is an epistemic proposition, with

  $${\left({\square }_A\mathit{\phi }\right)}_{\mathbf{S}}=\{s\in S:\mathrm{if} s\stackrel{A}{⟶}t, \mathrm{then} t\in {\mathit{\phi }}_{\mathbf{S}}\}.$$

  (2)
• If $\mathit{\phi }$ is an epistemic proposition and $\mathcal{B}\subseteq \mathcal{A}$, then ${\square }_{\mathcal{B}}^{\ast }\mathit{\phi }$ is an epistemic proposition, with

  $${\left({\square }_{\mathcal{B}}^{\ast }\mathit{\phi }\right)}_{\mathbf{S}}=\{s\in S:\mathrm{if} s\stackrel{{\mathcal{B}}^{\ast }}{⟶}t,\mathrm{then} t\in {\mathit{\phi }}_{\mathbf{S}}\}.$$
  Here $s\stackrel{{\mathcal{B}}^{\ast }}{⟶}t$ iff there is a sequence

  $$s=u_0\stackrel{A_1}{\to }{u}_1\stackrel{A_2}{\to }\cdots \stackrel{A_n}{\to }{u}_{n+1}=t$$

  where $A_1,\dots ,A_n\in \mathcal{B}$. In other words, there is a sequence of arrows labelled with agents from the set $\mathcal{B}$ taking s to t. We allow $n=0$ here, so $\stackrel{{\mathcal{B}}^{\ast }}{⟶}$ includes the identity relation on S.

Syntactic and Semantic Notions

It will be important for us to make a sharp distinction between syntactic and semantic notions. We have already begun to do this, speaking of atomic sentences and atomic propositions. The difference for us is that atomic sentences are entirely syntactic objects: we will not treat an atomic sentence p as anything except an unanalyzed mathematical object. On the other hand, this atomic sentence p also has associated with it the atomic proposition p. As defined in point 1, p will be a function whose domain is the (proper class of) state models, and it is defined by

$${\mathit{p}}_{\mathbf{S}}={\{s\in S:s\in \parallel p\parallel }_{\mathbf{S}}\}.$$

(3)

This difference may seem pedantic at first, and surely there are times when it is sensible to blur it. But for various reasons that will hopefully become clear, we need to insist on it.

Up until now, the only syntactic objects have been the atomic sentences $p\in \mathsf{AtSen}$. But we can build the collections of finitary and infinitary sentences by the same definitions that we have seen, and then the work of the past section is the semantics of our logical languages. For example, we have sentences $p\wedge q$, ${\square }_A\neg p$, and ${\square }_{\mathcal{B}}^{\ast }q$. These then have corresponding epistemic propositions as their semantics: $\mathit{p}\wedge \mathit{q}$, ${\square }_A\neg \mathit{p}$, and ${\square }_{\mathcal{B}}^{\ast }\mathit{q}$, respectively. Note that the latter is a properly infinitary proposition (and so ${\square }_{\mathcal{B}}^{\ast }q$ is a properly infinitary sentence); it abbreviates the infinite conjunction

$$p\wedge {\square }_{\mathcal{B}}p\wedge {\square }_{\mathcal{B}}{\square }_{\mathcal{B}}p\wedge \cdots$$

2.2. Updates

A transition relation between state models $\mathbf{S}$ and $\mathbf{T}$ is a relation between the sets S and T; i.e., a subset of $S\times T$. An update $\mathbf{r}$ is a pair of operations

$$\mathbf{r}=(\mathbf{S}\mapsto \mathbf{S}\left(\mathbf{r}\right),\mathbf{S}\mapsto {\mathbf{r}}_{\mathbf{S}}),$$

the first takes each $\mathbf{S}\in \mathsf{SMod}$ to a state model $\mathbf{S}\left(\mathbf{r}\right)$, and the second takes each $\mathbf{S}\in \mathsf{SMod}$ to a relation ${\mathbf{r}}_{\mathbf{S}}$ between $\mathbf{S}$ and $\mathbf{S}\left(\mathbf{r}\right)$. For the second map, we write ${\mathbf{r}}_{\mathbf{S}}:\mathbf{S}\to \mathbf{S}\left(\mathbf{r}\right)$. We call $\mathbf{S}\mapsto \mathbf{S}\left(\mathbf{r}\right)$ the update map, and $\mathbf{S}\mapsto {\mathbf{r}}_{\mathbf{S}}$ the update relation.

We continue our general discussion by noting that the collection of updates is closed in various ways.

• Skip and Crash: there exist updates called “Skip”, denoted by 1, and “Crash”, denoted by 0. Both keep the original state model unchanged $\mathbf{S}\left(\mathbf{1}\right)=\mathbf{S}\left(\mathbf{0}\right)=\mathbf{S}$, but they differ in the fact that ${\mathbf{1}}_{\mathbf{S}}$ is the identity relation on $\mathbf{S}$, while $0_{\mathbf{S}}$ is the empty relation.
• Sequential composition: if $\mathbf{r}$ and $\mathbf{s}$ are epistemic updates, then their composition $\mathbf{r};\mathbf{s}$ is again an epistemic update, where $\mathbf{S}(\mathbf{r};\mathbf{s})=\mathbf{S}\left(\mathbf{r}\right)\left(\mathbf{s}\right)$, and ${(\mathbf{r};\mathbf{s})}_{\mathbf{S}}={\mathbf{r}}_{\mathbf{S}};{\mathbf{s}}_{\mathbf{S}\left(\mathbf{r}\right)}$. Here, we use on the right side the usual composition ; of relations 3.
• Union (or non-deterministic choice): If X is any non-empty set of epistemic updates, then the union $⨆X$ is an epistemic update, defined as follows. For each $\mathbf{S}$, the set of states of the model $\mathbf{S}(⨆X)$ is the disjoint union of all the sets of states in each model $\mathbf{S}\left(\mathbf{r}\right)$ for $\mathbf{r}\in X$:

  $$\left\{\right(s,\mathbf{r}):\mathbf{r}\in X\mathrm{and}s\in \mathbf{S}(\mathbf{r}\left)\right\}.$$
  Similarly, each accessibility relation $\stackrel{A}{⟶}$ is defined as the disjoint union of the corresponding accessibility relations in each model:

  $$(t,\mathbf{r})\stackrel{A}{⟶}(u,\mathbf{s}) \mathrm{iff} \mathrm{if}\mathbf{r}=\mathbf{s} \mathrm{and} t\stackrel{A}{⟶}u\mathrm{in}\mathbf{S}\left(\mathbf{r}\right).$$
  The valuation ${\parallel p\parallel }_{\mathbf{S}(⨆X)}$ in $\mathbf{S}(⨆X)$ is the disjoint union of the valuations in each state model:

  $${\parallel p\parallel }_{\mathbf{S}(⨆X)}={\{(s,\mathbf{r}):\mathbf{r}\in X\mathrm{and}s\in \parallel p\parallel }_{\mathbf{S}\left(\mathbf{r}\right)}\}.$$
  Finally, the update relation ${(⨆X)}_{\mathbf{S}}$ between $\mathbf{S}$ and $\mathbf{S}(⨆X)$ is the union of all the update relations ${\mathbf{r}}_{\mathbf{S}}$:

  $$t{(⨆X)}_{\mathbf{S}}(u,\mathbf{r})\mathrm{iff}t{\mathbf{r}}_{\mathbf{S}}u.$$
  For the empty set of updates $X=\varnothing$, we conventionally put $⨆\varnothing :=0$ to be the above-defined “crash” update.
• Special case: binary union. The (disjoint) union of two epistemic updates $\mathbf{r}$ and $\mathbf{s}$ is an update $\mathbf{r}\bigsqcup \mathbf{s}$, given by $\mathbf{r}\bigsqcup \mathbf{s}=⨆\{\mathbf{r},\mathbf{s}\}$.
• Another special case: Kleene star (iteration). We have the operation of Kleene star on updates:

  $${\mathbf{r}}^{\ast }=⨆\{1,\mathbf{r},\mathbf{r}·\mathbf{r},\dots ,{\mathbf{r}}^n,\dots \}$$

  where ${\mathbf{r}}^n$ is recursively defined by ${\mathbf{r}}^0=1$, ${\mathbf{r}}^{n+1}={\mathbf{r}}^n;\mathbf{r}$.

The operations $\mathbf{r};\mathbf{s}$, $\mathbf{r}\bigsqcup \mathbf{s}$ and ${\mathbf{r}}^{\ast }$ are the natural analogues of the operations of union of relations, relational composition and iteration, and of the regular operations on programs in PDL. The intended meanings are: for $\mathbf{r};\mathbf{s}$, sequential composition (do $\mathbf{r}$, then do $\mathbf{s}$); for $\mathbf{r}\bigsqcup \mathbf{s}$, non-deterministic choice (do either $\mathbf{r}$ or $\mathbf{s}$); for ${\mathbf{r}}^{\ast }$, iteration (repeat $\mathbf{r}$ some finite number of times).

2.2.1. Standard Updates

An update $\mathbf{a}$ is standard if for all state models $\mathbf{S}$, ${\left({\mathbf{a}}_{\mathbf{S}}\right)}^{-1}$ is a partial function. (The relation ${\left({\mathbf{a}}_{\mathbf{S}}\right)}^{-1}$ is the inverse of the update relation; it is a subset of $\mathbf{S}\left(\mathbf{a}\right)\times \mathbf{S}$.)

Proposition 2.2. 

The update 1 is standard. The composition of standard updates is standard, as is any union of standard updates.

2.2.2. Updates Determine Dynamic Modalities

If $\mathit{\phi }$ is an epistemic proposition and $\mathbf{r}$ an update, then $\left[\mathbf{r}\right]\mathit{\phi }$ is an epistemic proposition defined by

$${\left(\left[\mathbf{r}\right]\mathit{\phi }\right)}_{\mathbf{S}}=\{s\in S:\mathrm{for}\mathrm{all}t\mathrm{such}\mathrm{that}s{\mathbf{r}}_{\mathbf{S}}t,t\in {\mathit{\phi }}_{\mathbf{S}\left(\mathbf{r}\right)}\}.$$

(4)

We should compare (4) and (2). The point is that we may treat updates in a similar manner to other box-like modalities; the structure given by an update allows us to do this.

We also define the dual proposition $\langle \mathbf{r}\rangle \mathit{\phi }$ by

$${\left(\langle \mathbf{r}\rangle \mathit{\phi }\right)}_{\mathbf{S}}=\{s\in S:\mathrm{for}\mathrm{some}t\mathrm{such}\mathrm{that}s{\mathbf{r}}_{\mathbf{S}}t,t\in {\mathit{\phi }}_{\mathbf{S}\left(\mathbf{r}\right)}\}.$$

2.3. Action Models and Program Models

Let $\mathsf{\Phi }$ be the collection of all epistemic propositions. An (epistemic) action model is a triple $\mathbf{\Sigma }=(\Sigma ,\stackrel{\mathcal{A}}{⟶},\mathrm{pre})$, where $\Sigma$ is a non-empty set of simple actions, $\stackrel{\mathcal{A}}{⟶}$ is an $\mathcal{A}$-indexed family of binary relations on $\Sigma$, and $\mathrm{pre}:\Sigma \to \mathsf{\Phi }$.

To model non-deterministic actions and non-simple actions (whose appearances to agents are not uniform on states), we define epistemic program models. In effect, this means that we decompose complex actions (‘programs’) into “simple” ones: they correspond to sets of simple, deterministic actions from a given action model.

A program model is defined as a pair $\pi =(\mathbf{\Sigma },\mathsf{\Gamma })$ consisting of an action model $\mathbf{\Sigma }$ and a set $\mathsf{\Gamma }\subseteq \Sigma$ of distinguished simple actions. Each of the simple actions $\gamma \in \mathsf{\Gamma }$ may be thought of as a possible “deterministic resolution” of the non-deterministic action $\pi$. As announced above, the intuition about the map called $\mathrm{pre}$ is that an action is executable in a given state only if all its preconditions hold at that state. We often spell out an epistemic program model as $(\Sigma ,\stackrel{\mathcal{A}}{⟶},\mathrm{pre},\mathsf{\Gamma })$ rather than $((\Sigma ,\stackrel{\mathcal{A}}{⟶},\mathrm{pre}),\mathsf{\Gamma })$. Also, we usually drop the word “epistemic” and just refer to these as program models.

2.4. The Update Product

Given a state model $\mathbf{S}=(S,{\stackrel{\mathcal{A}}{⟶}}_{\mathbf{S}},\parallel ·{\parallel }_{\mathbf{S}})$ and an action model $\mathbf{\Sigma }=(\Sigma ,\stackrel{\mathcal{A}}{⟶},\mathrm{pre})$, we define their update product to be the state model

$$\mathbf{S}\otimes \mathbf{\Sigma }=(S\otimes \Sigma ,\stackrel{\mathcal{A}}{⟶},\parallel .{\parallel }_{\mathbf{S}\otimes \mathbf{\Sigma }}),$$

given by the following: the new states are pairs of old states s and simple actions $\sigma$ which are “consistent”, in the sense that all preconditions of the action $\sigma$ “hold” at the state s

$$S\otimes \Sigma =\{(s,\sigma )\in S\times \Sigma :s\in \mathrm{pre}{\left(\sigma \right)}_{\mathbf{S}}\}.$$

(5)

The new accessibility relations are taken to be the “products” of the corresponding accessibility relations in the two frames; i.e., for $(s,\sigma ),(s^{\prime },{\sigma }^{\prime })\in \mathbf{S}\otimes \mathbf{\Sigma }$ we put

$$(s,\sigma )\stackrel{A}{⟶}(s^{\prime },{\sigma }^{\prime })\mathrm{iff}s\stackrel{A}{⟶}{s}^{\prime }\mathrm{and}\sigma \stackrel{A}{⟶}{\sigma }^{\prime },$$

(6)

and the new valuation map ${\parallel .\parallel }_{\mathbf{S}\otimes \mathbf{\Sigma }}:\mathsf{AtSen}\to \mathcal{P}(S\otimes \Sigma )$ is essentially given by the old valuation:

$${\parallel p\parallel }_{\mathbf{S}\otimes \mathbf{\Sigma }}={\{(s,\sigma )\in S\otimes \Sigma :s\in \parallel p\parallel }_{\mathbf{S}}\}.$$

(7)

2.5. Updates Induced by Program Models

Recall that we defined updates in Section 2.2. And above, in Section 2.3, we defined epistemic program models. Note that there is a big difference: the updates are pairs of operations on the class of all state models, and the program models are typically finite structures. We think of program models as capturing specific mechanisms, or algorithms, for inducing updates. This connection is made precise in the following definition.

Definition 2.3. 

Let $(\mathbf{\Sigma },\mathsf{\Gamma })$ be a program model. We define an update which we also denote $(\mathbf{\Sigma },\mathsf{\Gamma })$ as follows:

• $\mathbf{S}(\mathbf{\Sigma },\mathsf{\Gamma })=\mathbf{S}\otimes \mathbf{\Sigma }$.
• $s{(\mathbf{\Sigma },\mathsf{\Gamma })}_{\mathbf{S}}(t,\sigma )$ if $s=t$ and $\sigma \in \mathsf{\Gamma }$.

We call this the update induced by $(\mathbf{\Sigma },\mathsf{\Gamma })$.

Note that updates of the form $(\mathbf{\Sigma },\mathsf{\Gamma })$ have the property that for all state models $\mathbf{S}$, the inverse of the update relation ${(\mathbf{\Sigma },\mathsf{\Gamma })}_{\mathbf{S}}$ is a partial function. That is, these updates are standard.

2.6. Operations on Program Models

2.6.1. 1 and 0 

We define program models 1 and 0 as follows: for both of them we take our underlying action model to be given by any one-action set $\left\{\sigma \right\}$ with $\sigma \stackrel{A}{⟶}\sigma$ for all A, ${\mathrm{P}}_{\mathrm{RE}}\left(\sigma \right)=\mathbf{tr}$; the only difference is that for 1 we take the distinguished set ${\mathsf{\Gamma }}_{\mathbf{1}}=\left\{\sigma \right\}$, while for 0 we put ${\mathsf{\Gamma }}_{\mathbf{0}}=\varnothing$. The point here is that the update induced by the program model for 1 is equivalent to the update 1 from Section 2.2, and, similarly, the update induced by the program model for 0 is what we called 0 in Section 2.2. That explains why we purposely use the same notation for these program models as for the corresponding updates.

2.6.2. Sequential Composition

In all settings involving “actions” in some sense or other, sequential composition is a natural operation. In our setting, we would like to define a composition operation on program models, corresponding to the sequential composition of updates. Here is the relevant definition.

Let $\mathbf{\Sigma }=(\Sigma ,\stackrel{\mathcal{A}}{⟶},{\mathrm{pre}}_{\Sigma },{\mathsf{\Gamma }}_{\mathbf{\Sigma }})$ and $\mathbf{\Delta }=(\Delta ,\stackrel{\mathcal{A}}{⟶},{\mathrm{pre}}_{\Delta },{\mathsf{\Gamma }}_{\mathbf{\Delta }})$ be program models. We define the composition

$$\mathbf{\Sigma };\mathbf{\Delta }=(\Sigma \times \Delta ,\stackrel{\mathcal{A}}{⟶},{\mathrm{pre}}_{\Sigma ;\Delta },{\mathsf{\Gamma }}_{\Sigma ;\Delta })$$

to be the following program model:

• $\Sigma \times \Delta$ is the cartesian product of the sets $\Sigma$ and $\Delta$.
• $\stackrel{\mathcal{A}}{⟶}$ in the composition $\mathbf{\Sigma };\mathbf{\Delta }$ is the family of product relations, in the natural way:

  $$(\sigma ,\delta )\stackrel{A}{⟶}({\sigma }^{\prime },{\delta }^{\prime })iff\sigma \stackrel{A}{⟶}{\sigma }^{\prime }\mathrm{and}\delta \stackrel{A}{⟶}{\delta }^{\prime }.$$
• ${\mathrm{pre}}_{\Sigma ;\Delta }(\sigma ,\delta )=\langle (\mathbf{\Sigma },\sigma )\rangle {\mathrm{pre}}_{\Delta }\left(\delta \right)$.
• ${\mathsf{\Gamma }}_{\Sigma ;\Delta }={\mathsf{\Gamma }}_{\mathbf{\Sigma }}\times {\mathsf{\Gamma }}_{\mathbf{\Delta }}$.

In the definition of $\mathrm{pre}$, $(\mathbf{\Sigma },\sigma )$ is an abbreviation for the induced update $(\mathbf{\Sigma },\{\sigma \left\}\right)$, as defined in Section 2.5.

2.6.3. Unions

If $\mathbf{\Sigma }=(\Sigma ,\stackrel{\mathcal{A}}{⟶},{\mathrm{pre}}_{\mathbf{\Sigma }},{\mathsf{\Gamma }}_{\mathbf{\Sigma }})$ and $\mathbf{\Delta }=(\Delta ,\stackrel{\mathcal{A}}{⟶},{\mathrm{pre}}_{\Delta },{\mathsf{\Gamma }}_{\mathbf{\Delta }})$, we take $\mathbf{\Sigma }\bigsqcup \mathbf{\Delta }$ to be the disjoint union of the models, with the union of the distinguished actions. The intended meaning is the non-deterministic choice between the programs represented by $\mathbf{\Sigma }$ and $\mathbf{\Delta }$. Here is the definition in more detail, generalized to arbitrary (possibly infinite) disjoint unions: let ${\left\{{\mathbf{\Sigma }}_i\right\}}_{i\in I}$ be a family of program models, with ${\mathbf{\Sigma }}_i=({\Sigma }_i,{\stackrel{\mathcal{A}}{⟶}}_i,{\mathrm{pre}}_i,{\mathsf{\Gamma }}_i)$; we define their (disjoint) union

$$\underset{i\in I}{⨆}{\mathbf{\Sigma }}_i=\left(\underset{i\in I}{⨆}{\Sigma }_i,{\stackrel{\mathcal{A}}{⟶}}_i,{\mathrm{pre}}_i,{\mathsf{\Gamma }}_i\right)$$

to be the model given by:

• ${⨆}_{i\in I}{\Sigma }_i$ is ${\bigcup }_{i\in I}({\Sigma }_i\times \left\{i\right\})$, the disjoint union of the sets ${\Sigma }_i$.
• $(\sigma ,i)\stackrel{A}{⟶}(\tau ,j)$ if $i=j$ and $\sigma {\stackrel{A}{⟶}}_i\tau$.
• $\mathrm{pre}(\sigma ,i)={\mathrm{pre}}_i\left(\sigma \right)$.
• $\mathsf{\Gamma }={\bigcup }_{i\in I}({\mathsf{\Gamma }}_i\times \left\{i\right\})$.

2.6.4. Iteration

Finally, we define an iteration operation by ${\mathbf{\Sigma }}^{\ast }=⨆\{{\mathbf{\Sigma }}^n:n\in N\}$. Here, ${\mathbf{\Sigma }}^0=\mathbf{1}$ and ${\mathbf{\Sigma }}^{n+1}={\mathbf{\Sigma }}^n;\mathbf{\Sigma }$.

Our definition of the operations on program models are faithful to the corresponding operations on updates from Section 2.2.

Proposition 2.4 

([6]). The update induced by a composition of program models is isomorphic to the composition of the induced updates. Similarly, for sums and iteration, mutatis mutandis.

Since we shall not use this result, we omit the proof.

2.7. Action Signatures

Definition 2.5. 

An action signature is a structure

$$\mathbf{\Sigma }=(\Sigma ,\stackrel{\mathcal{A}}{⟶},({\sigma }_1,{\sigma }_2,\dots ,{\sigma }_n))$$

where $\mathbf{\Sigma }=(\Sigma ,\stackrel{\mathcal{A}}{⟶})$ is a finite Kripke frame, and ${\sigma }_1,{\sigma }_2,\dots ,{\sigma }_n$ is an enumeration of $\Sigma$ in a list without repetitions. We call the elements of $\Sigma$ action types. When we deal with an action signature, our notation for the action types usually includes a subscript (even though this is occasionally redundant); thus, the action types come with a number that indicates their position in the fixed enumeration of the action signature.

An action signature $\mathbf{\Sigma }$ together with an assignment of epistemic propositions to the action types in $\Sigma$ gives us a full-fledged action model. And this is the exact sense in which an action signature is an abstraction of the notion of action model. We shall use action signatures in constructing logical languages.

Example 2.6. 

Here is a very simple action signature which we call ${\mathbf{\Sigma }}_{\mathrm{skip}}$. Σ is a singleton $\left\{\mathrm{skip}\right\}$, $pre\left(\mathrm{skip}\right)=\mathbf{tr}$, and $\mathrm{skip}\stackrel{A}{⟶}\mathrm{skip}$ for all agents A. In a sense, which we shall make clear later, this is an action in which “nothing happens”, and, moreover, it is common knowledge that this is the case.

The next simplest action signature is the “test” signature ${\mathbf{\Sigma }}_{?}$. We take ${\mathbf{\Sigma }}_{?}=\{?,\mathrm{skip}\}$, with the enumeration $?,\mathrm{skip}$. We also take $?\stackrel{A}{⟶}\mathrm{skip}$, and $\mathrm{skip}\stackrel{A}{⟶}\mathrm{skip}$ for all A. This turns out to be a totally opaque form of test: φ is tested on the real world, but nobody knows this is happening. Its function will be to generate tests $?\phi$, which affect the states precisely in the way dynamic logic tests do.

For each set $\mathcal{B}\subseteq \mathcal{A}$ of agents, we define the action signature ${\mathrm{Pri}}^{\mathcal{B}}$ of completely private announcements to the group $\mathcal{B}$. It has $\Sigma =\{{\mathrm{Pri}}^{\mathcal{B}},\mathrm{skip}\}$; ${\mathrm{Pri}}^{\mathcal{B}}\stackrel{B}{⟶}{Pri}^{\mathcal{B}}$ for all $B\in \mathcal{B}$, ${\mathrm{Pri}}^{\mathcal{B}}\stackrel{C}{⟶}\mathrm{skip}$ for $C\notin \mathcal{B}$, and $\mathrm{skip}\stackrel{A}{⟶}\mathrm{skip}$ for all agents A.

The action signature $\mathrm{Pri}$ of all completely private announcements (to arbitrary subgroups) can be thought of as the disjoint union of all the action signatures ${Pri}^{\mathcal{B}}$ with $\mathcal{B}\subseteq \mathcal{A}$. However, we can avoid some redundancy by identifying all the $\mathrm{skip}$ actions regardless of which signature ${\mathrm{Pri}}^{\mathcal{B}}$ they come from: in other words, we set $\Sigma =\{{\mathrm{Pri}}^{\mathcal{B}}:\mathcal{B}\subseteq \mathcal{A}\}\cup \left\{\mathrm{skip}\right\}$, with ${\mathrm{Pri}}^{\mathcal{B}}\stackrel{B}{⟶}{\mathrm{Pri}}^{\mathcal{B}}$ for all $B\in \mathcal{B}\subseteq \mathcal{A}$, ${\mathrm{Pri}}^{\mathcal{B}}\stackrel{C}{⟶}\mathrm{skip}$ for $C\notin \mathcal{B}\subseteq \mathcal{A}$, and $\mathrm{skip}\stackrel{A}{⟶}\mathrm{skip}$ for all agents A.

Next, we consider the action signature ${\mathrm{Prss}}_k^{\mathcal{B}}$ of private announcements to the group $\mathcal{B}$ with secure suspicion of k possible announcements by the outsiders. It has the following components: $\Sigma =\{1,2,\dots ,k\}\cup \{1^{\prime },2^{\prime },\dots ,k^{\prime }\}\cup \left\{\mathrm{skip}\right\}$ (we assume these sets to be disjoint); $i\stackrel{B}{⟶}{i}^{\prime }$ for all $B\in \mathcal{B}$ and all $i\le k$; $i\stackrel{C}{⟶}j$ for all $i,j\le k$ and $C\notin \mathcal{B}$; $i^{\prime }\stackrel{B}{⟶}{i}^{\prime }$ for $i\le k$ and $B\in \mathcal{B}$; $i^{\prime }\stackrel{C}{⟶}\mathrm{skip}$ for all $i\le k$ and $C\notin \mathcal{B}$; and, finally, $\mathrm{skip}\stackrel{A}{⟶}\mathrm{skip}$ for all agents A.

The action signature ${Cka}_k^{\mathcal{B}}$ is given by: $\Sigma =\{1,\dots ,k\}$; $i\stackrel{B}{⟶}i$ for $i\le k$ and $B\in \mathcal{B}$; and, finally, $i\stackrel{C}{⟶}j$ for $i,j\le k$ and $C\notin \mathcal{B}$. This action signature is called the signature of common knowledge of alternatives for an announcement to the group $\mathcal{B}$.

2.7.1. Signature-Based Program Models

Let $\mathbf{\Sigma }$ be an action signature, let n be the number of action types in $\Sigma$, let $\mathsf{\Gamma }\subseteq \Sigma$, and let $\overrightarrow{\mathit{\psi }}={\mathit{\psi }}_1,\dots ,{\mathit{\psi }}_n$ be a list of epistemic propositions. We obtain a program model $(\mathbf{\Sigma },\mathsf{\Gamma },\overrightarrow{\mathit{\psi }})$ in the following way:

• The set of simple actions is $\Sigma$, and the accessibility relations are those given by the action signature.
• For $j=1,\dots ,n$, $\mathrm{pre}\left({\sigma }_j\right)={\mathit{\psi }}_j$.
• The set of distinguished actions is $\mathsf{\Gamma }$.

In the special case that $\mathsf{\Gamma }$ is the singleton set $\left\{{\sigma }_i\right\}$, we write the resulting signature-based program model as $(\mathbf{\Sigma },{\sigma }_i,\overrightarrow{\mathit{\psi }})$.

Finally, recall from Section 2.5 that every signature-based program model induces an update.

To summarize: every action signature, set of distinguished action types in it, and tuple of epistemic propositions gives a program model in a canonical way. Every program model induces a standard update.

As examples, note that both our program model 1 for “Skip” and our program model 0 for “Crash” (as defined above) are signature-based: indeed, the signature is ${\mathbf{\Sigma }}_{skip}$ as defined above (having only one action type $skip$, with loops for all agents and true precondition), while the designated sets of actions are ${\mathsf{\Gamma }}_{\mathbf{1}}=\left\{skip\right\}$ and, respectively, ${\mathsf{\Gamma }}_{\mathbf{0}}=\varnothing$.

2.8. Bisimulation-Based Notions of Equivalence

In this section, we discuss natural notions of equivalence for some of the definitions which we have already seen. We begin by recalling the most important notion of equivalence for state models, bisimulation.

Definition 2.7. 

Let $\mathbf{S}$ and $\mathbf{T}$ be state models. A bisimulation between $\mathbf{S}$ and $\mathbf{T}$ is a relation $R\subseteq S\times T$ such that whenever $sRt$, the following three properties hold:

• $s\in {\parallel p\parallel }_{\mathbf{S}}$ if $t\in {\parallel p\parallel }_{\mathbf{T}}$ for all atomic sentences p.
• For $A\in \mathcal{A}$ and $s^{\prime }$ such that $s\stackrel{A}{⟶}{s}^{\prime }$, there is some $t^{\prime }$ such that $t\stackrel{A}{⟶}{t}^{\prime }$ and $s^{\prime }R{t}^{\prime }$.
• For $A\in \mathcal{A}$ and $t^{\prime }$ such that $t\stackrel{A}{⟶}{t}^{\prime }$, there is some $s^{\prime }$ such that $s\stackrel{A}{⟶}{s}^{\prime }$ and $s^{\prime }R{t}^{\prime }$.

R is a total bisimulation if it is a bisimulation and, in addition: for all $s\in S$ there is some $t\in T$ such that $sRt$, and vice-versa.

Proposition 2.8. 

If there is a bisimulation R such that $sRt$, then s and t agree on all sentences φ in infinitary modal logic: $s\in {⟦\phi ⟧}_{\mathbf{S}}$ if $t\in {⟦\phi ⟧}_{\mathbf{T}}$.

Recall that $\mathsf{SMod}$ is the class of all state models. We have spoken of states as the elements of state models, but we also use the term states to refer to the pointed-model pairs $(\mathbf{S},s)$, with $\mathbf{S}\in \mathsf{SMod}$ and $s\in S$. The class of all states is itself a state model, except that its collection of states is a proper class rather than a set. Still, it makes sense to talk about bisimulation relations on the class of all states. The largest such is given by

$$(\mathbf{S},s)\equiv (\mathbf{T},t)\mathrm{iff}\mathrm{there}\mathrm{is}\mathrm{a}\mathrm{bisimulation}R\mathrm{between}\mathbf{S}\mathrm{and}\mathbf{T}\mathrm{such}\mathrm{that}sRt.$$

This relation ≡ is indeed an equivalence relation on ‘states’ (pointed models), called the bisimilarity relation. When $\mathbf{S}$ and $\mathbf{T}$ are clear from the context, we write $s\equiv t$ instead of $(\mathbf{S},s)\equiv (\mathbf{T},t)$.

2.8.1. Equivalence and Preservation by Bisimulation

Since we are discussing notions of equivalence here, it makes sense to also think about epistemic propositions. Two propositions $\mathit{\phi }$ and $\mathit{\psi }$ are equal if they are the same operation on $\mathsf{SMod}$. That is, for all $\mathbf{S}$, ${\mathit{\phi }}_{\mathbf{S}}={\mathit{\psi }}_{\mathbf{S}}$. Later, we shall introduce syntactically defined languages and also proof systems to go with them; in due course we shall see other interesting notions of equivalence.

Moving towards a connection of propositions with bisimulation, we say that a proposition $\mathit{\phi }$ is preserved by bisimulations if whenever $(\mathbf{S},s)\equiv (\mathbf{T},t)$, then $s\in {\mathit{\phi }}_{\mathbf{S}}$ iff $t\in {\mathit{\phi }}_{\mathbf{T}}$.

Proposition 2.9 

([6]). The propositions which are preserved by bisimulation include $\mathbf{tr}$ and the atomic propositions p, and they are closed under all of the (infinitary) operations on propositions from Section 2.1.

2.8.2. Equivalence of Bisimulation-Preserving Updates

From now we will focus on a special class of well-behaved updates: the ones that preserve bisimulation.

Definition 2.10. 

An update $\mathbf{r}$ preserves bisimulations if the following two conditions hold:

1. 

If $s{\mathbf{r}}_{\mathbf{S}}{s}^{\prime }$ and $(\mathbf{S},s)\equiv (\mathbf{T},t)$, then there is some $t^{\prime }$ such that $t{\mathbf{r}}_{\mathbf{T}}{t}^{\prime }$ and $(\mathbf{S}\left(\mathbf{r}\right),s^{\prime })\equiv (\mathbf{T}\left(\mathbf{r}\right),t^{\prime })$.

2. 

If $t{\mathbf{r}}_{\mathbf{T}}{t}^{\prime }$ and $(\mathbf{S},s)\equiv (\mathbf{T},t)$, then there is some $s^{\prime }$ such that $s{\mathbf{r}}_{\mathbf{S}}{s}^{\prime }$ and $(\mathbf{S}\left(\mathbf{r}\right),s^{\prime })\equiv (\mathbf{T}\left(\mathbf{r}\right),t^{\prime })$.

An action model $\mathbf{\Sigma }$ preserves bisimulations if the epistemic proposition $\mathrm{pre}\left(\sigma \right)$ is preserved under bisimulations for all $\sigma \in \Sigma$.

It is easy to see that the updates 1 and 0 are bisimulation-preserving, and, similarly, that the action models for the programs 1 and 0 preserve bisimulation. More examples can be produced using the following two results.

Proposition 2.11 

([6]). Concerning bisimulation preservation:

1. 

The bisimulation-preserving updates are closed under composition and (infinitary) unions.

2. 

If $\mathit{\phi }$ is preserved by bisimulations and $\mathbf{r}$ preserves bisimulations, then $\left[\mathbf{r}\right]\mathit{\phi }$ is preserved by bisimulations.

Proposition 2.12 

([6]). Let Σ be a bisimulation-preserving action model. Let $\mathsf{\Gamma }\subseteq \Sigma$ be arbitrary. Then, the update induced by $(\mathbf{\Sigma },\mathsf{\Gamma })$ preserves bisimulation.

We can now define an appropriate notion of equivalence between bisimulation-preserving updates.

Definition 2.13. 

Two bisimulation-preserving updates $\mathbf{a}$ and $\mathbf{b}$ are equivalent if the following two conditions hold:

• If $s{\mathbf{a}}_{\mathbf{S}}{s}^{\prime }$ then there is some $s^{″}$ such that $s{\mathbf{b}}_{\mathbf{S}}{s}^{″}$ and $(\mathbf{S}\left(\mathbf{a}\right),s^{\prime })\equiv (\mathbf{S}\left(\mathbf{b}\right),s^{″})$.
• If $s{\mathbf{b}}_{\mathbf{S}}{s}^{″}$, then there is some $s^{\prime }$ such that $s{\mathbf{a}}_{\mathbf{S}}{s}^{\prime }$ and $(\mathbf{S}\left(\mathbf{a}\right),s^{\prime })\equiv (\mathbf{S}\left(\mathbf{b}\right),s^{″})$.

We write $\mathbf{a}\cong \mathbf{b}$ for the update-equivalence relation.

Proposition 2.14. 

Update equivalence ≅ is an equivalence relation on the class of bisimulation-preserving updates.

Proof. 

For reflexivity, let $\mathbf{a}$ be a bisimulation-preserving update. We can check that $\mathbf{a}\cong \mathbf{a}$ by applying the definition of bisimulation preservation to $\mathbf{r}:=\mathbf{a}$ and to models $\mathbf{S}=\mathbf{T}$ and states $s=t$. Symmetry follows immediately from the definition of ≅ together with the symmetry of the bisimilarity relation ≡. For transitivity, assume that $\mathbf{a}\cong \mathbf{b}$ and $\mathbf{b}\cong \mathbf{c}$. To show that $\mathbf{a}\cong \mathbf{c}$, we check only condition 1 (since the proof of condition 2 is similar). For this, suppose that we have $s{\mathbf{a}}_{\mathbf{S}}{s}^{\prime }$. Since $\mathbf{a}\cong \mathbf{b}$, there must exist some $s^{″}$ such that $s{\mathbf{b}}_{\mathbf{S}}{s}^{″}$ and $(\mathbf{S}\left(\mathbf{a}\right),s^{\prime })\equiv (\mathbf{S}\left(\mathbf{b}\right),s^{″})$. The first of these, together with the fact that $\mathbf{b}\cong \mathbf{c}$, implies that there must exist some $s^{‴}$ such that $s{\mathbf{b}}_{\mathbf{S}}{s}^{‴}$ and $(\mathbf{S}\left(\mathbf{b}\right),s^{″})\equiv (\mathbf{S}\left(\mathbf{c}\right),s^{‴})$. By the transitivity of the bisimilarity relation, we also have $(\mathbf{S}\left(\mathbf{a}\right),s^{\prime })\equiv (\mathbf{S}\left(\mathbf{c}\right),s^{‴})$, as desired. □

Proposition 2.15. 

Let $\mathbf{S}$ and $\mathbf{T}$ be models and let $s,t$ be states. Assume that $(\mathbf{S},s)\equiv (\mathbf{T},t)$. Let $\mathbf{a}$ and $\mathbf{b}$ be bisimulation-preserving updates such that $\mathbf{a}\cong \mathbf{b}$. Then we have the following:

• If $s{\mathbf{a}}_{\mathbf{S}}{s}^{\prime }$, then there is some $t^{\prime }$ such that $t{\mathbf{b}}_{\mathbf{T}}{t}^{\prime }$ and $(\mathbf{S}\left(\mathbf{a}\right),s^{\prime })\equiv (\mathbf{T}\left(\mathbf{b}\right),t^{\prime })$.
• If $t{\mathbf{b}}_{\mathbf{T}}{t}^{\prime }$, then there is some $s^{\prime }$ such that $s{\mathbf{a}}_{\mathbf{S}}{s}^{\prime }$ and $(\mathbf{S}\left(\mathbf{a}\right),s^{\prime })\equiv (\mathbf{T}\left(\mathbf{b}\right),t^{\prime })$.

Proof. 

The second clause follows from the first, using the fact that the relations of update equivalence and bisimilarity are symmetric. So it is enough to check the first clause. From $s{\mathbf{a}}_{\mathbf{S}}{s}^{\prime }$, $(\mathbf{S},s)\equiv (\mathbf{T},t)$ and the fact that $\mathbf{a}$ preserves bisimulation, it follows that there exists some $t^{″}$ such that $t{\mathbf{a}}_{\mathbf{T}}{t}^{″}$ and $(\mathbf{S}\left(\mathbf{a}\right),s^{\prime })\equiv (\mathbf{T}\left(\mathbf{a}\right),t^{″})$. From $t{\mathbf{a}}_{\mathbf{T}}{t}^{″}$ and $\mathbf{a}\cong \mathbf{b}$, it follows that there exists some $t^{\prime }$ such that $t{\mathbf{b}}_{\mathbf{T}}{t}^{\prime }$ and $(\mathbf{T}\left(\mathbf{a}\right),t^{″})\equiv (\mathbf{T}\left(\mathbf{b}\right),t^{\prime })$. Putting these together and using the transitivity of the bisimilarity relation ≡, we conclude that $(\mathbf{S}\left(\mathbf{a}\right),s^{\prime })\equiv (\mathbf{T}\left(\mathbf{b}\right),t^{\prime })$, as desired. □

Proposition 2.16. 

Let $\mathbf{a}\cong \mathbf{b}$ and $\mathbf{c}\cong \mathbf{d}$. Then, $\mathbf{a};\mathbf{c}\cong \mathbf{b};\mathbf{d}$, and also $\mathbf{a}\bigsqcup \mathbf{c}\cong \mathbf{b}\bigsqcup \mathbf{d}$.

Proof. 

To prove $\mathbf{a};\mathbf{c}\cong \mathbf{b};\mathbf{d}$, we only check the first clause in the definition of update equivalence. Suppose that $s{(\mathbf{a};\mathbf{c})}_{\mathbf{S}}{s}^{\prime }$, i.e., there exists some $s^{″}$ such that $a{\mathbf{a}}_{\mathbf{S}}{s}^{″}$ and $s^{″}{\mathbf{c}}_{\mathbf{S}\left(\mathbf{a}\right)}{s}^{\prime }$. From $a{\mathbf{a}}_{\mathbf{S}}{s}^{″}$ and $\mathbf{a}\cong \mathbf{b}$, we infer that there is some $t^{″}$ with $s{\mathbf{b}}_{\mathbf{S}}{t}^{″}$ and $(\mathbf{S}\left(\mathbf{a}\right),s^{″})\equiv (\mathbf{S}\left(\mathbf{b}\right),t^{″})$. By using these together with the fact that $\mathbf{c}\cong \mathbf{d}$, and applying Proposition 2.15, we obtain some $t^{\prime }$ such that $t^{″}{\mathbf{c}}_{\mathbf{S}\left(\mathbf{b}\right)}{t}^{\prime }$ and $(\mathbf{S}\left(\mathbf{a}\right)\left(\mathbf{c}\right),s^{\prime })\equiv (\mathbf{S}\left(\mathbf{b}\right)\left(\mathbf{d}\right),t^{\prime })$, as desired.

For the second claim, we again only prove the first clause in the definition of $\mathbf{a}\bigsqcup \mathbf{c}\cong \mathbf{b}\bigsqcup \mathbf{d}$. Suppose that $s{(\mathbf{a}\bigsqcup \mathbf{c})}_{\mathbf{S}}{s}^{\prime }$. By the definition of $\mathbf{a}\bigsqcup \mathbf{c}$, this means that we either have $s^{\prime }=(t,\mathbf{a})$ for some t satisfying $s{\mathbf{a}}_{\mathbf{S}}t$, or else we have $s^{\prime }=(t,\mathbf{b})$ for some t satisfying $s{\mathbf{b}}_{\mathbf{S}}t$. We only treat the first case (the other case is similar), so we have $s^{\prime }=(t,\mathbf{b})$ and $s{\mathbf{a}}_{\mathbf{S}}t$. Using the fact that $\mathbf{a}\sim \mathbf{b}$, we infer that there exists some $t^{\prime }$ such that $s{\mathbf{b}}_{\mathbf{S}}{t}^{\prime }$ and $(\mathbf{S}\left(\mathbf{a}\right),t)\equiv (\mathbf{S}\left(\mathbf{b}\right),t^{\prime })$. Using these and taking the state $s^{″}:=(t^{\prime },\mathbf{b})$ in the model $\mathbf{S}(\mathbf{b}\bigsqcup \mathbf{d})$, we can easily check that we have $s{(\mathbf{b}\bigsqcup \mathbf{d})}_{\mathbf{S}}{s}^{″}$ and $(\mathbf{S}(\mathbf{a}\bigsqcup \mathbf{c}),s^{\prime })\equiv (\mathbf{S}(\mathbf{b}\bigsqcup \mathbf{d}),s^{″})$, as desired. □

Proposition 2.17. 

For all bisimulation-preserving $\mathbf{a}$, we have $\mathbf{a};1\cong 1;\mathbf{a}\cong \mathbf{a}$, as well as $\mathbf{a};0\cong 0;\mathbf{a}\cong 0$ and $\mathbf{a}\bigsqcup 0\cong 0\bigsqcup \mathbf{a}\cong \mathbf{a}$.

Proof. 

Easy verification. □

Proposition 2.18. 

Let $\mathbf{a}$ and $\mathbf{b}$ be standard bisimulation-preserving updates. If $\mathit{\phi }$ is preserved by bisimulations and $\mathbf{a}\cong \mathbf{b}$, then $\left[\mathbf{a}\right]\mathit{\phi }=\left[\mathbf{b}\right]\mathit{\phi }$, and also $\langle \mathbf{a}\rangle \mathit{\phi }=\langle \mathbf{b}\rangle \mathit{\phi }$.

Proof. 

We check the first assertion only. Fix $\mathbf{S}$, and let $s\in S$ be such that that $s\in {\left(\left[\mathbf{a}\right]\mathit{\phi }\right)}_{\mathbf{S}}$. Let $t\in \mathbf{S}\left(\mathbf{b}\right)$ be such that $s{\mathbf{b}}_{\mathbf{S}}t$. We must show that $t\in {\mathit{\phi }}_{\mathbf{S}\left(\mathbf{b}\right)}$.

For this, we use $s{\mathbf{b}}_{\mathbf{S}}t$ and $\mathbf{a}\cong \mathbf{b}$, and by the definition of update-equivalence we infer that there exists some $t^{\prime }$ such that $s{\mathbf{a}}_{\mathbf{S}}{t}^{\prime }$ and $(\mathbf{S}\left(\mathbf{a}\right),t^{\prime })\equiv (\mathbf{S}\left(\mathbf{b}\right),t)$. From $s\in {\left(\left[\mathbf{a}\right]\mathit{\phi }\right)}_{\mathbf{S}}$ and $s{\mathbf{a}}_{\mathbf{S}}{t}^{\prime }$, it follows that $t^{\prime }\in {\mathit{\phi }}_{\mathbf{S}\left(\mathbf{a}\right)}$. This, together with $(\mathbf{S}\left(\mathbf{a}\right),t^{\prime })\equiv (\mathbf{S}\left(\mathbf{b}\right),t)$ and the fact that $\mathit{\phi }$ is preserved by bisimulations, implies that $t\in {\mathit{\phi }}_{\mathbf{S}\left(\mathbf{b}\right)}$, as desired. □

Proposition 2.19. 

Let $\mathbf{a}$ and $\mathbf{b}$ be standard bisimulation-preserving updates. If $\mathbf{a}\cong \mathbf{b}$, then $\mathbf{a}$ and $\mathbf{b}$ have the same domain. That is, for all state models $\mathbf{S}$, $\mathit{dom}\left({\mathbf{a}}_{\mathbf{S}}\right)=\mathit{dom}\left({\mathbf{b}}_{\mathbf{S}}\right)$.

Proof. 

The domains are ${\left(\langle \mathbf{a}\rangle \mathbf{tr}\right)}_{\mathbf{S}}$ and ${\left(\langle \mathbf{b}\rangle \mathbf{tr}\right)}_{\mathbf{S}}$, where recall that $\mathbf{tr}$ is the “universally true” proposition. So the result follows from Proposition 2.18 and the fact that $\mathbf{tr}$ is preserved by bisimulations. □

Definition 2.20. 

Let $\mathbf{\Sigma }=(\Sigma ,\stackrel{\mathcal{A}}{⟶},\mathrm{pre})$ and ${\mathbf{\Sigma }}^{\prime }=({\Sigma }^{\prime },\stackrel{\mathcal{A}}{⟶},\mathrm{pre})$ be action models. As this notation indicates, we shall not introduce additional notation to differentiate the arrows and the $\mathrm{pre}$ functions on these action models. A bisimulation between $\mathbf{\Sigma }$ and ${\mathbf{\Sigma }}^{\prime }$ is a relation $R\subseteq \Sigma \times {\Sigma }^{\prime }$ such that whenever $\sigma R{\sigma }^{\prime }$, the following three properties hold:

1. 

$pre\left(\sigma \right)=pre\left({\sigma }^{\prime }\right)$.

2. 

For $A\in \mathcal{A}$ and $\rho$ such that $\sigma \stackrel{A}{⟶}\rho$, there is some ${\rho }^{\prime }$ such that ${\sigma }^{\prime }\stackrel{A}{⟶}{\rho }^{\prime }$ and $\rho R{\rho }^{\prime }$.

3. 

For $A\in \mathcal{A}$ and ${\rho }^{\prime }$ such that ${\sigma }^{\prime }\stackrel{A}{⟶}{\rho }^{\prime }$, there is some $\rho$ such that $\sigma \stackrel{A}{⟶}\rho$ and $\rho R{\rho }^{\prime }$.

We write $\sigma \sim {\sigma }^{\prime }$, and say that actions $\sigma$ and ${\sigma }^{\prime }$ are bisimilar, if there is a bisimulation R between $\mathbf{\Sigma }$ and ${\mathbf{\Sigma }}^{\prime }$ such that $\sigma R{\sigma }^{\prime }$ .

Let $\pi =(\mathbf{\Sigma },\mathsf{\Gamma })$ and $\rho =({\mathbf{\Sigma }}^{\prime },{\mathsf{\Gamma }}^{\prime })$ be program models. A bisimulation between $\pi$ and $\rho$ is a bisimulation R between $\mathbf{\Sigma }$ and $\mathbf{\Delta }$ such that the following hold:

1. 

If $\sigma \in \mathsf{\Gamma }$, then there is some ${\sigma }^{\prime }\in {\mathsf{\Gamma }}^{\prime }$ such that $\sigma R{\sigma }^{\prime }$.

2. 

If ${\sigma }^{\prime }\in {\mathsf{\Gamma }}^{\prime }$, then there is some $\sigma \in \mathsf{\Gamma }$ such that $\sigma R{\sigma }^{\prime }$.

If such a bisimulation exists, then we write $\pi \sim \rho$, and say that the program models $\pi$ and $\rho$ are bisimilar.

Proposition 2.21. 

If $\pi =(\mathbf{\Sigma },\mathsf{\Gamma })$ is any program model, 1 is the above-defined program model for “Skip” and 0 is the above-defined program model for “Crash”, then we have $\pi ;\mathbf{1}\sim \mathbf{1};\pi \sim \pi$, as well as $\pi ;\mathbf{0}\sim \mathbf{0};\pi \sim \mathbf{0}$ and $\pi \bigsqcup \mathbf{0}\sim \mathbf{0}\bigsqcup \pi \sim \pi$.

Proof. 

Easy verification. □

Proposition 2.22. 

If two bisimulation-preserving program models are bisimilar, then they induce equivalent updates.

Proof. 

Let $\pi =(\mathbf{\Sigma },\mathsf{\Gamma })$ and $\rho =({\mathbf{\Sigma }}^{\prime },{\mathsf{\Gamma }}^{\prime })$ be program models, and let R be a bisimulation between $\pi$ and $\rho$. To prove our claim, we first construct a bisimulation $\overline{R}$ between the update products $\mathbf{S}\otimes \mathbf{\Sigma }$ and $\mathbf{S}\otimes {\mathbf{\Sigma }}^{\prime }$, by putting for all states $(s,\sigma )\in S\otimes \Sigma ,(s^{\prime },{\sigma }^{\prime })\in S\otimes {\Sigma }^{\prime }$:

$$(s,\sigma )\overline{R}(s^{\prime },{\sigma }^{\prime })\mathrm{iff}s=s^{\prime }\mathrm{and}\sigma R{\sigma }^{\prime }.$$

It is easy to check that this is a bisimulation relation. The atomic preservation is obvious: $(s,\sigma \overline{R}(s^{\prime },{\sigma }^{\prime })$ implies that $s=s^{\prime }$, and so both $(s,\sigma )$ and $(s^{\prime },{\sigma }^{\prime })$ satisfy the same atomic sentences as $s=s^{\prime }$. For the forth clause, assume that we have $(s,\sigma )\stackrel{A}{⟶}(t,\rho )$ and $(s,\sigma )\overline{R}(s^{\prime },{\sigma }^{\prime })$. From these, we obtain $s\stackrel{A}{⟶}t$ and $\sigma \stackrel{A}{⟶}\rho$, as well as $s=s^{\prime }$ and $\sigma R{\sigma }^{\prime }$. Since R is a bisimulation between $\mathbf{\Sigma }$ and ${\mathbf{\Sigma }}^{\prime }$, there must exist some ${\rho }^{\prime }\in {\Sigma }^{\prime }$ such that ${\sigma }^{\prime }\stackrel{A}{⟶}{\rho }^{\prime }$ and $\rho R{\rho }^{\prime }$. This gives us that $\mathrm{pre}\left(\rho \right)=\mathrm{pre}\left({\rho }^{\prime }\right)$, and since $(t,\rho )\in S\otimes \Sigma$, we have that $t\in \mathrm{pre}\left(\rho \right)=\mathrm{pre}\left({\rho }^{\prime }\right)$, and so the state $(t,{\rho }^{\prime })\in S\otimes {\Sigma }^{\prime }$ exists. This state is our witness for the forth clause: it is easy now to check that we have $(s,{\sigma }^{\prime })\stackrel{A}{⟶}(t,{\rho }^{\prime })$ and $(t,\rho )\overline{R}(t,{\rho }^{\prime })$, as desired. The back condition is similar.

We can now prove that the updates $\pi$ and $\rho$ are equivalent. Let $\mathbf{a}$ be the update induced by $\pi$ (via the update product), and let $\mathbf{b}$ be the update induced by $\rho$. We need to prove that $\mathbf{a}\cong \mathbf{b}$. For this, we only check the first condition in the definition of update equivalence (the second condition is similar). Assume that $s{\mathbf{a}}_{\mathbf{S}}(s,\sigma )\in \Sigma$ with $\sigma \in \mathsf{\Gamma }$. Since R is a bisimulation between $(\mathbf{\Sigma },\mathsf{\Gamma })$ and $({\mathbf{\Sigma }}^{\prime },{\mathsf{\Gamma }}^{\prime })$, there exists some ${\sigma }^{\prime }\in {\mathsf{\Gamma }}^{\prime }$ such that $\sigma R{\sigma }^{\prime }$. This implies that $\mathrm{pre}\left(\sigma \right)=\mathrm{pre}\left({\sigma }^{\prime }\right)$, and so $(s,\sigma )\in \Sigma$ gives us $s\in \mathrm{pre}\left(\sigma \right)=\mathrm{pre}\left({\sigma }^{\prime }\right)$; hence, the state $(s,{\sigma }^{\prime })\in S\otimes {\Sigma }^{\prime }$ exists. This state is our witness for the first clause in the definition of update equivalence: it is easy now to check that we have $s{\mathbf{b}}_{\mathbf{S}}(s,{\sigma }^{\prime })$ and $(s,\sigma )\overline{R}(s,{\sigma }^{\prime })$, and so we also have $(\mathbf{S}\otimes \mathbf{\Sigma },(s,\sigma ))\equiv (\mathbf{S}\otimes {\mathbf{\Sigma }}^{\prime },(s,{\sigma }^{\prime }))$ (since $\overline{R}$ is a bisimulation between $\mathbf{S}\otimes \mathbf{\Sigma }$ and $\mathbf{S}\otimes {\mathbf{\Sigma }}^{\prime }$), as desired. □

Note Bisimilarity is not the weakest (most general) relation on program models that implies update equivalence. Cf. the work in [13], in which a weaker such relation is studied (‘action emulation’). So, in a sense, our notion of program bisimilarity is too strong for the job that it was designed for. However, it has the advantage of simplicity, and it will be sufficient for our purposes. It is also a very natural notion to study in the context of the other concepts of bisimulation equivalence considered in this section.

3. Signature-Based Languages $\mathcal{L}(\mathbf{\Sigma })$ and Their Fragments

At this point, we have enough general definitions to present the syntax and semantics of our signature-based languages $\mathcal{L}(\mathbf{\Sigma })$ and their important sublanguages ${\mathcal{L}}_0(\mathbf{\Sigma })$ and ${\mathcal{L}}_1(\mathbf{\Sigma })$. Most of the remaining parts of this paper study these languages.

3.1. Syntax and Semantics

Fix an action signature $\mathbf{\Sigma }$. See Figure 1 for the syntax of a logical language $\mathcal{L}(\mathbf{\Sigma })$, together with its sublanguages ${\mathcal{L}}_0(\mathbf{\Sigma })$ and ${\mathcal{L}}_1(\mathbf{\Sigma })$.

As in $PDL$, we have two sorts of syntactic objects: sentences and programs. The set of sentences and the set of programs are simultaneously defined by mutual recursions. We call programs of the form $\sigma {\psi }_1\cdots {\psi }_n$ basic actions, where $\sigma \in \Sigma$. Here, the number n is the number of action types in $\Sigma$, and basic actions are formed by postfixing any such action type $\sigma$ with an n-long string $\overrightarrow{\psi }$ of already-formed sentences ${\psi }_j$ in our language 4. Arbitrary programs are recursively formed from basic actions, as well as from the programs $skip$ and $crash$, by applying the standard regular program operations of $PDL$: non-deterministic choice $\pi \bigsqcup \rho$, sequential composition $\pi ;\rho$ and iteration ${\pi }^{\ast }$. In their turn, sentences are recursively built from atomic sentences $\pi$, by applying standard Boolean connectives, as well as modalities ${\square }_A\phi$ (for any agent A), ${\square }_{\mathcal{B}}^{\ast }\phi$ (for any set of agents $\mathcal{B}$) and $\left[\pi \right]\phi$ (for any program $\pi$).

The sublanguage ${\mathcal{L}}_1(\mathbf{\Sigma })$ is obtained by dropping iteration ${\pi }^{\ast }$ from the constructs of $\mathcal{L}(\mathbf{\Sigma })$, while the sublanguage ${\mathcal{L}}_0(\mathbf{\Sigma })$ is obtained by dropping both iteration ${\pi }^{\ast }$ and the common knowledge modalities ${\square }_{\mathcal{B}}^{\ast }\phi$.

We use the following standard abbreviations: $\mathsf{false}=\neg \mathsf{true}$, $\phi \vee \psi =\neg (\neg \phi \wedge \neg \psi )$, $\phi \to \psi =\neg (\phi \wedge \neg \psi )$, $\phi \leftrightarrow \psi =(\phi \to \psi )\wedge (\psi \to \phi )$, ${\diamond }_A\phi =\neg {\square }_A\neg \phi$, ${\diamond }_{\mathcal{B}}^{\ast }=\neg {\square }_{\mathcal{B}}^{\ast }\neg \phi$, and $\langle \pi \rangle \phi =\neg \left[\pi \right]\neg \phi$.

The semantics defines two operations by simultaneous recursion on $\mathcal{L}(\mathbf{\Sigma })$:

• $\phi \mapsto ⟦\phi ⟧$, taking the sentences of $\mathcal{L}(\mathbf{\Sigma })$ into epistemic propositions.
• $\pi \mapsto ⟦\pi ⟧$, taking the programs of $\mathcal{L}(\mathbf{\Sigma })$ into program models (and, hence, into induced updates).

The formal definition is given in Figure 1. The first map $\phi \mapsto ⟦\phi ⟧$ might be called the truth map for the language. When we began our study of state models, we started with a “valuation” (or a “truth” map) ${\parallel .\parallel }_{\mathbf{S}}:\mathsf{AtSen}\to \mathcal{P}\left(S\right)$, assigning to each atomic sentence p a set ${\parallel p\parallel }_{\mathbf{S}}$ of states. The truth map here extends this to sentences and actions of $\mathcal{L}(\mathbf{\Sigma })$. The overall definition is by simultaneous recursion on $\mathcal{L}(\mathbf{\Sigma })$. We employ the standard device of speaking of the definition in terms of a temporal metaphor. That is, we think of the definition of the semantics of a sentence or action as coming “after” the semantics of its subsentences and subactions.

With one key exception, the operations on the right-hand sides are immediate applications of our general definitions of the closure conditions on epistemic propositions from Section 2.1 and the operations on program models from Section 2.6. A good example to explain this is the clause for the semantics of sentences $\left[\pi \right]\phi$. Assuming that we have a program model $⟦\pi ⟧$, we obtain an induced update in Section 2.5 which we again denote $⟦\pi ⟧$. We also have an epistemic proposition $⟦\phi ⟧$. We can, therefore, form the epistemic proposition $[⟦\pi ⟧]⟦\phi ⟧$ (see Equation (4) in Section 2.2). Note that we have overloaded the square-bracket notation; this is intentional, and we have done the same with other notation as well.

Similarly, the semantics of $skip$ and $crash$ are the program models 1 and 0 of Section 2.6.

We also discuss the definition of the semantics for basic actions ${\sigma }_i\overrightarrow{\psi }$. For this, recall that we have a general definition of a signature-based program model $(\mathbf{\Sigma },\mathsf{\Gamma },{\mathit{\psi }}_1,\dots ,{\mathit{\psi }}_n)$, where $\mathsf{\Gamma }\subseteq \Sigma$ and the $\mathit{\psi }$’s are any epistemic propositions. What we have in the semantics of ${\sigma }_i\overrightarrow{\psi }$ is the special case of this where $\mathsf{\Gamma }$ is the singleton $\left\{{\sigma }_i\right\}$ and ${\mathit{\psi }}_i$ is $⟦{\psi }_i⟧$, a proposition which we have already defined when we come to define $⟦{\sigma }_i\overrightarrow{\psi }⟧$.

Logics Generated by Families of Signatures

Up until now, we have defined logics of the form $\mathcal{L}(\mathbf{\Sigma })$ for a single action signature $\mathbf{\Sigma }$. Recall also that each action signature is finite. It is also natural to think about the logic of all finite action signatures. That is, we want to combine all of the logics $\mathcal{L}(\mathbf{\Sigma })$ even though we cannot literally combine the action signatures.

More generally, given a family $\mathcal{S}$ of action signatures, we would like to combine all the logics ${\left\{\mathcal{L}(\mathbf{\Sigma })\right\}}_{\mathbf{\Sigma }\in \mathcal{S}}$ into a single logic. Let us assume the signatures $\mathbf{\Sigma }\in \mathcal{S}$ are mutually disjoint (otherwise, just choose mutually disjoint copies of these signatures). We define the logic $\mathcal{L}\left(\mathcal{S}\right)$ generated by the family $\mathcal{S}$ in the following way: the syntax is defined by taking the same definition we had in Figure 1 for the syntax of $\mathcal{L}(\mathbf{\Sigma })$, but in which on the side of the programs we take instead as basic actions all expressions of the form

$${\sigma }_i{\psi }_1\cdots {\psi }_n$$

where $\sigma \in \Sigma$, for some signature $\mathbf{\Sigma }\in \mathcal{S}$, and n is the length of the listing of non-trivial action types of $\mathbf{\Sigma }$. The semantics is again given by the same definition as in Figure 1, but in which the clause about $\sigma {\psi }_1\cdots {\psi }_n$ refers to the appropriate signature: for every $\mathbf{\Sigma }\in \mathcal{S}$, every $\sigma \in \Sigma$; if n is the length of the listing of $\mathbf{\Sigma }$, then

$$⟦{\sigma }_i{\psi }_1\cdots {\psi }_n⟧=(\mathbf{\Sigma },\sigma ,⟦{\psi }_1⟧,\dots ,⟦{\psi }_n⟧).$$

It is important to note that, in general, $\mathcal{L}\left(\mathcal{S}\right)$ is not a signature-based language of the form $\mathcal{L}(\mathbf{\Sigma })$ for any single (finite) signature $\mathbf{\Sigma }$. However, our definition of signature-based languages has a natural generalization to locally finite ’signatures’ 5, and then one can see the languages $\mathcal{L}\left(\mathcal{S}\right)$ as being based on such generalized signatures.

3.2. Examples

In this section, we provide examples of the concepts from Section 2.1, Section 2.2, Section 2.3, Section 2.4, Section 2.5, Section 2.6, Section 2.7, Section 2.8, Section 3.1. Our examples of state models are chosen with an eye towards one of the inexpressivity results in Section 6.2 and Section 6.3 near the end of the paper. So we know that they may appear artificial. Still, we trust that having a suitably detailed example may help the reader.

First, we need to introduce some concrete examples of signature-based languages. The language of public announcements $\mathcal{L}\left({\mathbf{\Sigma }}_{\mathrm{pub}}\right)$ is the special case of our general class of languages $\mathcal{L}(\mathbf{\Sigma })$ that is obtained by taking the action signature ${\mathbf{\Sigma }}_{\mathrm{pub}}$ of public announcements, as we defined it in Section 2.7: $\Sigma =\{Pub\}$, $Pub\stackrel{A}{⟶}Pub$, and $Pub\stackrel{B}{⟶}Pub$. We can similarly define the language of completely private announcements$\mathcal{L}\left({\mathbf{\Sigma }}_{pri}\right)$ by taking the signature $Pri$ of all private announcements, as defined in Section 2.7: $\Sigma =\{Pri\mathcal{B}:\mathcal{B}\subseteq \mathcal{A}\}\cup \left\{skip\right\}$, with ${Pri}^{\mathcal{B}}\stackrel{B}{⟶}{Pri}^{\mathcal{B}}$ for all $B\in \mathcal{B}\subseteq \mathcal{A}$, ${Pri}^{\mathcal{B}}\stackrel{C}{⟶}skip$ for $C\notin \mathcal{B}\subseteq \mathcal{A}$, and $skip\stackrel{A}{⟶}skip$ for all agents A. For both public and private announcements, we can consider sublanguages ${\mathcal{L}}_0\left({\mathbf{\Sigma }}_{\mathrm{pub}}\right)$, ${\mathcal{L}}_1\left({\mathbf{\Sigma }}_{\mathrm{pub}}\right)$, ${\mathcal{L}}_0\left({\mathbf{\Sigma }}_{\mathrm{pri}}\right)$, and ${\mathcal{L}}_1\left({\mathbf{\Sigma }}_{\mathrm{pri}}\right)$, as above, by applying the corresponding syntactic restrictions.

In our following examples, we will more specifically fix our set $\mathsf{AtSen}$ of atomic sentences to be a two-element set $\{p,q\}$, and fix the set $\mathcal{A}$ of agents to be the two-element set $\{A,B\}$.

As a first example, we consider a family of state models $C_n$, one for each even positive numbers n. $C_n$ is a cycle of $5n$ points $a_1,\dots ,a_{5n}$ arranged as follows:

$$a_1\stackrel{\hspace{1em}\hspace{1em}A\hspace{1em}\hspace{1em}}{⟷}{a}_2\stackrel{\hspace{1em}\hspace{1em}B\hspace{1em}\hspace{1em}}{⟷}{a}_3\hspace{1em}\cdots \hspace{1em}{a}_{5n-1}\stackrel{\hspace{1em}\hspace{1em}A\hspace{1em}\hspace{1em}}{⟷}{a}_{5n}\stackrel{\hspace{1em}\hspace{1em}B\hspace{1em}\hspace{1em}}{⟷}{a}_1$$

Since n is even, for $1\le i\le 5$, the connection is $a_{in-1}\stackrel{\hspace{1em}\hspace{1em}A\hspace{1em}\hspace{1em}}{⟷}{a}_{in}\stackrel{\hspace{1em}\hspace{1em}B\hspace{1em}\hspace{1em}}{⟷}{a}_{in+1}$ (We are taking subscripts modulo $5n$ here.) We also specify that p is true at all points except $a_1$ and $a_{2n+1}$, and q is true only at $a_{4n+1}$.

We will look at the sentence $\langle Pubp\rangle {\diamond }_{A,B}^{\ast }q$, belonging to the language ${\mathcal{L}}_1\left({\mathbf{\Sigma }}_{\mathrm{pub}}\right)$, and aim to evaluate in each of the models $C_n$. (Without abbreviations, this sentence would be $\neg \left[Pubp\right]{\square }_{A,B}^{\ast }\neg q$.) The point of this first example is to calculate ${⟦\langle Pubp\rangle {\diamond }_{A,B}^{\ast }q⟧}_{C_n}$. This takes a few steps.

The definitions tell us that $⟦p⟧=\mathit{p}$, and so

$${⟦p⟧}_{C_n}={\mathit{p}}_{C_n}={\parallel p\parallel }_{C_n}=\{a_i:i\ne 1,2n+1\}.$$

We have a signature-based program model $({\mathbf{\Sigma }}_{\mathrm{pub}},Pub,\mathit{p})$. (In more detail, ${\mathbf{\Sigma }}_{\mathrm{pub}}$ is an action signature, our distinguished set $\mathsf{\Gamma }\subseteq \Sigma$ is $\left\{Pub\right\}$, and ${\mathrm{P}}_{\mathrm{RE}}\left(Pub\right)$ is the the proposition p.) We can take the update product of this with $C_n$ to obtain the model $C_n\otimes ({\mathbf{\Sigma }}_{\mathrm{pub}},Pub,\mathit{p})$. The state set of this state model is

$$\{(a_i,Pub):1\le i\le 5n\&i\ne 1\&i\ne 2n+1\}.$$

The accessibilities are given by

$$\begin{gathered} (a_2,Pub)\stackrel{\hspace{1em}\hspace{1em}B\hspace{1em}\hspace{1em}}{⟷}(a_3,Pub)\stackrel{\hspace{1em}\hspace{1em}A\hspace{1em}\hspace{1em}}{⟷}\cdots \hspace{1em}\hspace{1em}\hspace{1em}\hspace{1em}(a_{2n-1},Pub)\stackrel{\hspace{1em}\hspace{1em}A\hspace{1em}\hspace{1em}}{⟷}(a_{2n},Pub) \\ (a_{2n+1},Pub)\stackrel{\hspace{1em}\hspace{1em}A\hspace{1em}\hspace{1em}}{⟷}(a_{2n+2},Pub)\stackrel{\hspace{1em}\hspace{1em}B\hspace{1em}\hspace{1em}}{⟷}\cdots \hspace{1em}\hspace{1em}\hspace{1em}\hspace{1em}(a_{5n-1},Pub)\stackrel{\hspace{1em}\hspace{1em}A\hspace{1em}\hspace{1em}}{⟷}(a_{5n},Pub) \end{gathered}$$

In this model p is true at all points, and q is true only at $(a_{4n+1},Pub)$. The update relation ${({\mathbf{\Sigma }}_{\mathrm{pub}},Pub,\mathit{p})}_{C_n}$ is

$$\{(a_i,(a_i,Pub)):1\le i\le 5n\&i\ne 1\&i\ne 2n+1\}.$$

The intuition is that when we relativize the model to p (that is, we update the model with a public announcement of p), $a_1$ and $a_{2n+1}$ disappear. The cycle breaks into two disconnected components.

To save on notation, let us write $D_n$ for the model $C_n\otimes ({\mathbf{\Sigma }}_{\mathrm{pub}},Pub,\mathit{p})$. It follows that

$${⟦q⟧}_{D_n}={\parallel \mathit{q}\parallel }_{D_n}=\left\{(a_{4n+1},Pub)\right\},$$

and, therefore, that

$${⟦{\diamond }_{A,B}^{\ast }q⟧}_{D_n}={\left({\diamond }_{A,B}^{\ast }\mathit{q}\right)}_{D_n}=\{(a_i,Pub):2n+1\le i\le 5n\}.$$

It now follows that

$$\begin{array}{ccc}{⟦\langle Pubp\rangle {\diamond }_{A,B}^{\ast }q⟧}_{C_n}\hfill & =& \{a_i:(a_i,Pub)\in D_n\&(a_i,Pub)\in {⟦{\diamond }_{A,B}^{\ast }q⟧}_{D_n}\}\hfill \\ & =& \{a_i:2n+2\le i\le 5n\}\hfill \end{array}$$

Later, we are going to be especially interested in the points $a_{n+1}$ and $a_{3n+1}$. The analysis above shows that $a_{n+1}$ does not belong to ${⟦\langle Pubp\rangle {\diamond }_{A,B}^{\ast }q⟧}_{C_n}$, but $a_{3n+1}$ does belong to it. The intuition is that after we relativize the original cycle to p by deleting $a_1$ and $a_{2n+1}$, there is no path from $a_{n+1}$ to $a_{4n+1}$. But even after we make the deletion, there is a path from $a_{3n+1}$ to $a_{4n+1}$, and this is why $a_{3n+1}$ satisfies the sentence $\langle Pubp\rangle {\diamond }_{A,B}^{\ast }q$.

A Second Example

We next consider a different example based on the signature $Pri$ of completely private announcements. ${\mathcal{L}}_1\left({\mathbf{\Sigma }}_{\mathrm{pri}}\right)$ contains the following sentence

$$\chi \equiv \langle {Pri}^{A}p,\mathsf{true}\rangle {\diamond }_A^{\ast }{\diamond }_B\neg p$$

(8)

We show in Section 6.3 that $\chi$ cannot be expressed by any sentence in ${\mathcal{L}}_1\left({\mathbf{\Sigma }}_{\mathrm{pub}}\right)$ and that ${\diamond }_A\chi$ is not expressible in ${\mathcal{L}}_1\left({\mathbf{\Sigma }}_{\mathrm{pub}}\right)$, even by a set of sentences. This means that there is no set T of sentences of ${\mathcal{L}}_1\left({\mathbf{\Sigma }}_{\mathrm{pub}}\right)$ such that for every state, $(\mathbf{S},s)$, $(\mathbf{S},s)\vDash \psi$ for each $\psi \in T$ iff $(\mathbf{S},s)\vDash \langle {Pri}^{A}p\mathsf{true}\rangle {\diamond }_A^{\ast }{\diamond }_B\neg p$. We take this inexpressibility result to be a formal confirmation that a logical system with private announcements is more powerful than a system with only public announcements.

Definition 3.1. 

For each non-zero natural number n we shall construct models ${\mathbf{S}}_n$ and ${\mathbf{T}}_n$. These two models have the same state set:

$$\{a,b\}\cup \{c_i:1\le i\le n\}.$$

The atomic proposition p is true at all points except b, and no other atomic propositions are true anywhere. The arrows in ${\mathbf{S}}_n$ are given by

1. 

$x\stackrel{A}{⟶}x$ for all x.

2. 

$a\stackrel{A}{⟶}b$.

3. 

$b\stackrel{A}{⟶}{c}_1$.

4. 

$c_i\stackrel{A}{⟶}b$ for all $1\le i\le n$.

5. 

$c_n\stackrel{B}{⟶}b$.

${\mathbf{T}}_n$ has all these arrows and exactly one more:

6. 

$a\stackrel{A}{⟶}{c}_1$.

The model ${\mathbf{S}}_n$ is shown in Figure 2. We did not show the reflexive $\stackrel{A}{⟶}$ arrows.

For all $x\ne a$, the submodels of ${\mathbf{S}}_n$ and ${\mathbf{T}}_n$ reachable from x are the same. Therefore, we have the following fact:

$$\mathrm{for} \mathrm{all}x\ne a,({\mathbf{S}}_n,x)\vDash \phi \mathrm{iff}({\mathbf{T}}_n,x)\vDash \phi$$

(9)

This holds for all $\phi$ in $\mathcal{L}\left({\mathbf{\Sigma }}_{\mathrm{pub}}\right)$.

Let us calculate ${\mathbf{S}}_n\otimes ({\mathbf{\Sigma }}_{\mathrm{pri}},{Pri}^A,\mathit{p},\mathbf{tr})$ and ${\mathbf{T}}_n\otimes ({\mathbf{\Sigma }}_{\mathrm{pri}},{Pri}^A,\mathit{p},\mathbf{tr})$. Intuitively, we are making a private announcement of p to A. To save on notation, we call the updated models ${\widehat{\mathbf{S}}}_n$ and ${\widehat{\mathbf{T}}}_n$.

Here are some facts about the structure of ${\widehat{\mathbf{S}}}_n$:

• $(a,{Pri}^A)\stackrel{A}{⟶}(a,{Pri}^A)$.
• The only $\stackrel{A}{⟶}$-successor of $(a,{Pri}^A)$ is itself. In particular, $(a,{Pri}^A)\stackrel{A}{⟶}(b,{Pri}^A)$ does not hold, since $(b,{Pri}^A)$ does not belong to the model.
• $(x,skip)\stackrel{A}{⟶}(y,skip)$ whenever $x\stackrel{A}{⟶}y$ in ${\mathbf{S}}_n$ and similarly for $(x,skip)\stackrel{B}{⟶}(y,skip)$.
• $(c_i,{Pri}^A)\stackrel{A}{⟶}(c_{i+1},{Pri}^A)$ for $1\le i<n$.

The structure of ${\widehat{\mathbf{T}}}_n$ differs from ${\widehat{\mathbf{S}}}_n$. Since $a\stackrel{A}{⟶}{c}_1$ in ${\mathbf{T}}_n$, we have a path in ${\widehat{\mathbf{T}}}_n$:

$$(a,{Pri}^A)\stackrel{A}{⟶}(c_1,{Pri}^A)\stackrel{A}{⟶}\cdots \stackrel{A}{⟶}(c_n,{Pri}^A)\stackrel{B}{⟶}(b,skip).$$

Once again, ${\widehat{\mathbf{S}}}_n$ contains no path from $(a,{Pri}^A)$ to any other point, in particular, no path to $(b,skip)$.

The update relation between ${\mathbf{S}}_n$ and ${\widehat{\mathbf{S}}}_n$ is $\{(x,(x,{Pri}^A)):x\ne b\}.$ And from this, we see that with $\chi$ from (8),

$$\begin{array}{ccccc}{⟦\chi ⟧}_{{\mathbf{S}}_n}\hfill & =& \{x:(x,{Pri}^A)\in {⟦{\diamond }_A^{\ast }{\diamond }_B\neg p⟧}_{{\widehat{\mathbf{S}}}_n}\}\hfill & =& \{c_i:1\le i\le n\}.\hfill \end{array}$$

In particular, $a\notin {⟦\chi ⟧}_{{\mathbf{S}}_n}$.

The update relation between ${\mathbf{T}}_n$ and ${\widehat{\mathbf{T}}}_n$ is the same, and we have

$$\begin{array}{ccccc}{⟦\chi ⟧}_{{\mathbf{T}}_n}\hfill & =& \{x:(x,{Pri}^A)\in {⟦{\diamond }_A^{\ast }{\diamond }_B\neg p⟧}_{{\widehat{\mathbf{T}}}_n}\}\hfill & =& \{x:x\ne b\}.\hfill \end{array}$$

And this time, $a\in {⟦\chi ⟧}_{{\mathbf{T}}_n}$.

In Section 6.3, we shall use these models to prove the result announced above: that our sentence ${\diamond }_A\chi$ is not expressible by any set of sentences using public announcements only. The intuition is that the models ${\mathbf{S}}_n$ and ${\mathbf{T}}_n$ differ on $\chi$ due to the private announcement in that sentence, but as far as public announcements go, the two models are “pretty close”. Of course, “pretty close” needs to be defined and studied, and this is what we do in our later section. The formal proof does not use any of our other results, and the reader may turn to it at this point.

3.3. Basic Properties

Proposition 3.2. 

Let φ be a sentence of $\mathcal{L}(\mathbf{\Sigma })$, and let α be an action of $\mathcal{L}(\mathbf{\Sigma })$. Then:

1. 

The epistemic proposition $⟦\phi ⟧$ is preserved by bisimulation.

2. 

The update $⟦\alpha ⟧$ is standard and preserves bisimulation.

Proof. 

By induction on $\mathcal{L}(\mathbf{\Sigma })$. For $\mathsf{true}$ and the atomic sentences $p_i$, we use Proposition 2.9. The same result takes care of the induction steps for all the sentential operators except $\left[\pi \right]\phi$. For this, we use Proposition 2.11 part 2, and also the induction hypothesis. Turning to the programs, the standardness comes from Proposition 2.2 and the observation that signature-based program models induce standard updates. The assertion that the interpretation of programs of $\mathcal{L}(\mathbf{\Sigma })$ preserve bisimulation comes from Proposition 2.11 part 1; for the programs ${\sigma }_i\overrightarrow{\psi }$, we use Proposition 2.12 and the induction hypothesis. □

In what follows, we shall use Proposition 3.2 without mentioning it.

3.4. The Canonical Action Model

We henceforth restrict ourselves to the language ${\mathcal{L}}_1(\mathbf{\Sigma })$, obtained by eliminating iteration ${\pi }^{\ast }$ from our repertoire. Moreover, in this section, we focus on the program expressions of ${\mathcal{L}}_1(\mathbf{\Sigma })$. We introduce some useful meta-syntactic terms and notations, that will allow us to structure (a subset of) our program expressions as a “syntactic program model”, called the canonical action model.

Definition 3.3. 

A simple action of ${\mathcal{L}}_1(\mathbf{\Sigma })$ is a program of ${\mathcal{L}}_1(\mathbf{\Sigma })$ that can be obtained from $skip$, $crash$ and basic actions of ${\mathcal{L}}_1(\mathbf{\Sigma })$ (of the form $\sigma \overrightarrow{\psi }$, but without the use of iteration ${\pi }^{\ast }$ within any precondition) by repeated applications of the sequential composition operation $\pi ;{\pi }^{\prime }$ (but no sum operation ⊔, and of course no iteration, since iteration is not present in ${\mathcal{L}}_1(\mathbf{\Sigma })$). So, in particular, simple actions include all the basic actions of ${\mathcal{L}}_1(\mathbf{\Sigma })$. We use letters such as $\alpha$ and $\beta$ to denote simple actions. We do so for the rest of this paper, without further notice.

3.4.1. The Canonical Action Model $\mathsf{\Omega }$

We define a program model $\mathsf{\Omega }$ in several steps. The actions of the model $\mathsf{\Omega }$ (that is, the elements of its carrier set) are the simple actions of the language ${\mathcal{L}}_1(\mathbf{\Sigma })$ (as defined just above). For all A, the accessibility relation $\stackrel{A}{⟶}$ is the smallest relation such that

• $skip\stackrel{A}{⟶}skip$.
• ${\sigma }_i\overrightarrow{\phi }\stackrel{A}{⟶}{\sigma }_j\overrightarrow{\psi }$ if ${\sigma }_i\stackrel{A}{⟶}{\sigma }_j$ in $\mathbf{\Sigma }$ and $\overrightarrow{\phi }=\overrightarrow{\psi }$.
• If $\alpha \stackrel{A}{⟶}{\alpha }^{\prime }$ and $\beta \stackrel{A}{⟶}{\beta }^{\prime }$, then $\alpha ;\beta \stackrel{A}{⟶}{\alpha }^{\prime };{\beta }^{\prime }$.

As before, we use the notation $\stackrel{{\mathcal{C}}^{\ast }}{⟶}$ for the reflexive-transitive closure of the union of all accessibility relations $\stackrel{A}{⟶}$ (on simple actions) labelled by agents $A\in \mathcal{C}$. In particular, the largest such relation ${\to }_{\mathcal{A}}^{\ast }$ is obtained by taking $\mathcal{C}=\mathcal{A}$ to be the set of all agents.

Proposition 3.4. 

As a frame, Ω is locally finite: for each simple α, there are only finitely many β such that $\alpha$.

Proof .

By induction on α; we use heavily the fact that the accessibility relations on Ω are the smallest family with their defining property. For the simple action expressions $\sigma \overrightarrow{\psi }$, we use the assumption that the action model Σ underlying all our definitions is finite. (Taking it to be locally finite would also be sufficient.) □

Next, we define ${\mathrm{P}}_{\mathrm{RE}}:\mathsf{\Omega }\to {\mathcal{L}}_1(\mathbf{\Sigma })$ by recursion so that

$$\begin{array}{ccc}{\mathrm{P}}_{\mathrm{RE}}\left(skip\right)\hfill & =& \mathsf{true}\hfill \\ {\mathrm{P}}_{\mathrm{RE}}\left(crash\right)\hfill & =& \mathsf{false}\hfill \\ {\mathrm{P}}_{\mathrm{RE}}\left({\sigma }_i\overrightarrow{\psi }\right)\hfill & =& {\psi }_i\hfill \\ {\mathrm{P}}_{\mathrm{RE}}(\alpha ;\beta )\hfill & =& \langle \alpha \rangle {\mathrm{P}}_{\mathrm{RE}}\left(\beta \right)\hfill \end{array}$$

This function ${\mathrm{P}}_{\mathrm{RE}}$ is not the function $\mathrm{pre}$ which is part of the structure of an epistemic action model. However, there is a connection: We are in the midst of defining the epistemic action model Ω, and its $\mathrm{pre}$ function is defined in terms of ${\mathrm{P}}_{\mathrm{RE}}$.

Another point: the last clause in the definition of ${\mathrm{P}}_{\mathrm{RE}}$ could read ${\mathrm{P}}_{\mathrm{RE}}(\alpha ;\beta )={\mathrm{P}}_{\mathrm{RE}}\left(\alpha \right)\wedge \left[\alpha \right]{\mathrm{P}}_{\mathrm{RE}}\left(\beta \right)$. This is equivalent to what we have above.

We set

$$\mathrm{pre}\left(\sigma \right)=⟦{\mathrm{P}}_{\mathrm{RE}}\left(\sigma \right)⟧.$$

This simple action model Ω is the canonical epistemic action model; it plays the same role in our work as the canonical model in modal logic.

Remark. 3.5.

The structure $(\mathsf{\Omega },\stackrel{\mathcal{A}}{⟶},{\mathrm{P}}_{\mathrm{RE}})$ is entirely syntactic. It is not an action model. This contrasts with the canonical action model $\mathsf{\Omega }=(\mathsf{\Omega },\stackrel{\mathcal{A}}{⟶},\mathrm{pre})$; the last component of this structure is semantic. The syntactic structure $(\mathsf{\Omega },\stackrel{\mathcal{A}}{⟶},{\mathrm{P}}_{\mathrm{RE}})$ is the one which is actually used in the statement of the action rule of the logical system. We emphasize this point to allay any suspicion that our logical system is formulated in terms of semantic concepts.

This is also perhaps a good place to remind the reader that neither $\mathrm{pre}$ nor $\mathrm{pre}$ is a first-class symbol in $\mathcal{L}(\mathbf{\Sigma })$; it is only a defined symbol. In Section 5, below, we shall introduce another language called ${\mathcal{L}}_1^{+}(\mathbf{\Sigma })$. In that language, $\mathrm{pre}$ will be a first-class function symbol.

We now proceed to study the main properties of the canonical action model.

Lemma 3.6. 

For any action type $\sigma \in \mathbf{\Sigma }$ and simple actions $\alpha ,\beta \in \mathsf{\Omega }$, we have the following bisimilarities between program models:

1. 

$(\mathbf{\Sigma },{\sigma }_i,⟦{\psi }_1⟧\cdots ⟦{\psi }_n⟧)\sim (\mathsf{\Omega },{\sigma }_i\overrightarrow{\psi })$

2. 

$(\mathsf{\Omega },\alpha ;\beta )\sim (\mathsf{\Omega },\alpha );(\mathsf{\Omega },\beta )$

where in the right-hand side of the second part we use the composition ; of program models.

Proof. 

For the first claim, the bisimulation is the relation $\{({\sigma }_j,{\sigma }_j\overrightarrow{\psi }):1\le j\le n\}$, where n is the number of elements in Σ.

For the second claim, the bisimulation relates any action of the form ${\alpha }^{\prime };{\beta }^{\prime }$ in Ω with the pair $({\alpha }^{\prime },{\beta }^{\prime })$ in $\mathsf{\Omega }\times \mathsf{\Omega }$. It is easy to check that this is a bisimulation betwen the action models Ω and $\mathsf{\Omega };\mathsf{\Omega }$, which obviously relates $\alpha ;\beta$ with $(\alpha ,\beta )$, as desired. □

Definition  3.7. 

For any $\alpha \in \mathsf{\Omega }$, let $\widehat{\alpha }$ be the program model $(\mathsf{\Omega },\{\alpha \left\}\right)$. As in Section 2.5, we use the same notation $\widehat{\alpha }$ to denote the induced update. (However, it will be important to distinguish the two uses, and so we speak of the program model $\widehat{\alpha }$ and also the update $\widehat{\alpha }$.)

We can now prove the main result on the canonical action model.

Theorem  3.8. 

Let $\alpha \in \mathsf{\Omega }$. Then, as updates, we have $⟦\alpha ⟧\cong \widehat{\alpha }$.

Proof. 

By induction on α. For $skip$ and $crash$, it is easy to check that, as updates, $\widehat{skip}$ is equivalent to the identity update 1, and $\widehat{crash}$ is equivalent to 0.

We next consider an action $\alpha :={\sigma }_i\overrightarrow{\psi }$. By the definition of the semantics, we have $⟦\alpha ⟧=(\mathbf{\Sigma },{\sigma }_i,⟦{\psi }_1⟧\cdots ⟦{\psi }_n⟧)$, while $\widehat{\alpha }=(\mathsf{\Omega },{\sigma }_i\overrightarrow{\psi })$. By the first claim in the previous Lemma, these program models are bisimilar; hence, they induce equivalent updates.

Finally, consider simple actions of the form $\alpha ;\beta$. By the semantics, $⟦\alpha ;\beta ⟧=⟦\alpha ⟧;⟦\beta ⟧$, and by the induction hypothesis, this is the same as $\widehat{\alpha };\widehat{\beta }$. By the second claim in the previous Lemma, this last program model is bisimilar with $\widehat{\alpha ;\beta }$; hence, the the induced updates are equivalent. □

4. The Logical System for Validity of ${\mathcal{L}}_1(\mathbf{\Sigma })$ Sentences

We write $\vDash \phi$ to mean that for all state models $\mathbf{S}$ and all $s\in S$, $s\in {⟦\phi ⟧}_{\mathbf{S}}$. In this case, we say that φ is valid.

In principle, we are of course interested in the validities of the full languages $\mathcal{L}(\mathbf{\Sigma })$. But as has already been mentioned, the satisfiability problems for these languages are, in general, not recursively axiomatizable. (See [14] for details on this.) This is one of the reasons we also consider sublanguages ${\mathcal{L}}_0(\mathbf{\Sigma })$ and ${\mathcal{L}}_1(\mathbf{\Sigma })$. It turns out that ${\mathcal{L}}_0(\mathbf{\Sigma })$ is the easiest to study: it is of the same expressive power as ordinary multi-modal logic. The main completeness result of the paper is a sound and complete proof system for the validities in ${\mathcal{L}}_1(\mathbf{\Sigma })$.

In Figure 3, below, we present the sound and complete logic for ${\mathcal{L}}_1(\mathbf{\Sigma })$. We write $⊢\phi$ if φ can be obtained from the axioms of the system using its inference rules. We often omit the turnstile ⊢ when it is clear from the context.

Most of the system will be quite standard from modal logic. The action axioms and the action rule are new, however. These include the in the atomic permanence axiom; note that, in this axiom, p is an atomic sentence. The axiom says that announcements do not change the brute fact of whether or not p holds. This axiom reflects the fact that our actions do not change any kind of local state.

The Action-Knowledge Axiom gives a criterion for knowledge after an action. It is perhaps easier to appreciate in dual form:

$$\langle {\sigma }_i\overrightarrow{\psi }\rangle {\diamond }_A\phi \leftrightarrow ({\psi }_i\wedge \bigvee \{{\diamond }_A\left[{\sigma }_j\overrightarrow{\psi }\right]\phi :{\sigma }_i\stackrel{A}{⟶}{\sigma }_{j}in\mathbf{\Sigma }\}).$$

In words, two sentences are equivalent: first, the assertion that the action ${\sigma }_i\overrightarrow{\psi }$ may be executed, and as a result of the execution, agent A will consider φ possible; and second, the precondition ${\psi }_i$ of the action holds, and A considers it possible (before the action) that the action is really ${\sigma }_j$ and that there is some possible world in which that action ${\sigma }_j$ may be executed and results in a state satisfying φ. This axiom should be compared with the Ramsey axiom in conditional logic.

The statement of our action rule uses the meta-syntactic terminology introduced in Section 3.4; in particular, the notion of simple actions, the syntactic accessibility relations $\stackrel{A}{⟶}$ and $\stackrel{{\mathcal{C}}^{\ast }}{⟶}$, and the syntactic precondition map ${\mathrm{P}}_{\mathrm{RE}}$ defined on simple actions in the (syntactic version of the) canonical action model. As for its meaning, the action rule gives a necessary criterion for common knowledge after a simple action. Since common knowledge is formalized by the ${\square }_{\mathcal{B}}^{\ast }$ construct, this rule is a kind of induction rule. (The sentences ${\chi }_{\beta }$ play the role of strong induction hypotheses.)

Remark 4.1.

Recall that $\stackrel{{\mathcal{C}}^{\ast }}{⟶}$ is an abbreviation for the reflexive and transitive closure of the relation ${\bigcup }_{A\in \mathcal{C}}\stackrel{A}{⟶}$. Recall also from Proposition 3.4 that there are only finitely many $\beta$ such that $\alpha \stackrel{{\mathcal{C}}^{\ast }}{⟶}\beta$. So even though the action rule might look like it takes infinitely many premises, it really only takes finitely many.

Remark 4.2. 

It is possible to drop the composition axiom in favor of a more involved version of the action rule. The point is we shall later introduce normal forms for sentences, and using the composition axiom will greatly simplify these normal forms. Moreover, adding the composition axiom leads to shorter proofs. The action rule here is geared towards those normal forms. So if we were to drop the composition axiom, we would need a stronger, more complicated, formulation of the action rule, one which involved sequences of actions. It is not terribly difficult to formulate such a rule, and completeness can be obtained by an elaboration of the work, which we shall do.

4.1. Soundness of the Axioms

In this section, we check the soundness of the axioms of the system (but not yet the soundness of the action rule). The basic axioms are all routine, and so we omit the details on them.

Proposition 4.3. 

The atomic permanence axiom $\left[{\sigma }_i\overrightarrow{\psi }\right]p\leftrightarrow ({\psi }_i\to p)$ is sound.

Proof. 

Recall from Section 2.7.1 how $⟦{\sigma }_i\overrightarrow{\psi }⟧$ works; call this update $\mathbf{r}$. Fix a state model $\mathbf{S}$. The following are equivalent:

• $s\in {⟦\left[{\sigma }_i\overrightarrow{\psi }\right]p⟧}_{\mathbf{S}}$.
• $s\in {\left(\left[\mathbf{r}\right]\mathit{p}\right)}_{\mathbf{S}}$.
• If $s{\mathbf{r}}_{\mathbf{S}}t$, then $t\in {\mathit{p}}_{\mathbf{S}\left(\mathbf{r}\right)}$.
• If $(s,{\sigma }_i)\in \mathbf{S}\left(\mathbf{r}\right)$, then $(s,{\sigma }_i)\in {\mathit{p}}_{\mathbf{S}\left(\mathbf{r}\right)}$.
• If $s\in {⟦{\psi }_i⟧}_{\mathbf{S}}$, then $s\in {\parallel p\parallel }_{\mathbf{S}}={\mathit{p}}_{\mathbf{S}}$.
• $s\in {⟦{\psi }_i\to p⟧}_{\mathbf{S}}$.

Most of the individual equivalences are easy, and we only comment on (3)⟺(4) and (4)⟺(5). The definition of the update $\mathbf{r}=(\mathbf{\Sigma },{\sigma }_i)$ implies that $\mathbf{S}\left(\mathbf{r}\right)=\mathbf{S}\otimes \mathbf{\Sigma }$. And ${\mathbf{r}}_{\mathbf{S}}$ has the property that everything which $s\in S$ is related to by ${\mathbf{r}}_{\mathbf{S}}$ is of the form $(s,{\sigma }_i)$, where ${\sigma }_i$ is from the statement of this axiom and $(s,{\sigma }_i)\in \mathbf{S}\left(\mathbf{r}\right)$. These points imply the equivalence (3)⟺(4). For (4)⟺(5), note that $(s,{\sigma }_i)\in \mathbf{S}\left(\mathbf{r}\right)$ if $s\in \mathrm{pre}{\left({\sigma }_i\right)}_{\mathbf{S}}={⟦{\psi }_i⟧}_{\mathbf{S}}$; also the definition of the update product in Equation (7) implies that $(s,{\sigma }_i)\in p_{\mathbf{S}\left(\mathbf{r}\right)}$ iff $s\in {\parallel p\parallel }_{\mathbf{S}}$. □

Proposition 4.4. 

The partial functionality axiom $\left[{\sigma }_i\overrightarrow{\psi }\right]\neg \chi \leftrightarrow ({\psi }_i\to \neg \left[{\sigma }_i\overrightarrow{\psi }\right]\chi )$ is sound.

Proof. 

Again, let $\mathbf{r}=⟦{\sigma }_i\overrightarrow{\psi }⟧$. Also, let $\mathbf{\chi }=⟦\chi ⟧$. Fix a state model $\mathbf{S}$. The following are equivalent:

• $s\in {⟦\left[{\sigma }_i\overrightarrow{\psi }\right]\neg \chi ⟧}_{\mathbf{S}}$.
• $s\in {\left(\left[\mathbf{r}\right]\neg \mathbf{\chi }\right)}_{\mathbf{S}}$.
• If $s{\mathbf{r}}_{\mathbf{S}}t$, then $t\in \neg {\mathbf{\chi }}_{\mathbf{S}\left(\mathbf{r}\right)}$.
• If $s{\mathbf{r}}_{\mathbf{S}}t$, then $t\notin {\mathbf{\chi }}_{\mathbf{S}\left(\mathbf{r}\right)}$.
• If $s\in {⟦{\psi }_i⟧}_{\mathbf{S}}$, then $(s,{\sigma }_i)\notin {\left(\left[\mathbf{r}\right]\mathbf{\chi }\right)}_{\mathbf{S}}$.
• If $s\in {⟦{\psi }_i⟧}_{\mathbf{S}}$, then $s\notin \neg {\mathbf{\chi }}_{\mathbf{S}\left(\mathbf{r}\right)}$.
• If $s\in {⟦{\psi }_i⟧}_{\mathbf{S}}$, then $s\in {(\neg \left[\mathbf{r}\right]\mathbf{\chi })}_{\mathbf{S}}$.
• $s\in {⟦{\psi }_i\to \neg \left[\mathbf{r}\right]\mathbf{\chi }⟧}_{\mathbf{S}}$.

The crucial equivalence here is (6)⟹(5). The reason this holds is that in the action model for ${\sigma }_i\overrightarrow{\psi }$, there is just one distinguished world. So for each fixed $s\in S$, there is at most one t such that $s{\mathbf{r}}_{\mathbf{S}}t$; i.e., $(s,{\sigma }_i)$. □

Proposition 4.5. 

The Action-Knowledge Axiom

$$\left[{\sigma }_i\overrightarrow{\psi }\right]{\square }_A\phi \leftrightarrow ({\psi }_i\to \bigwedge \{{\square }_A\left[{\sigma }_j\overrightarrow{\psi }\right]\phi :{\sigma }_i\stackrel{A}{⟶}{\sigma }_{j}in\mathbf{\Sigma }\})$$

is sound.

Proof. 

Again, let $\mathbf{r}=⟦{\sigma }_i\overrightarrow{\psi }⟧$. Fix a state model $\mathbf{S}$. The following are equivalent:

• $s\in {⟦\left[{\sigma }_i\overrightarrow{\psi }\right]{\square }_A\phi ⟧}_{\mathbf{S}}$.
• $s\in \left[\mathbf{r}\right]{⟦{\square }_A\phi ⟧}_{\mathbf{S}}$.
• If $s{\mathbf{r}}_{\mathbf{S}}u$, then $u\in {⟦{\square }_A\phi ⟧}_{\mathbf{S}\left(\mathbf{r}\right)}$.
• If $s\in {⟦{\psi }_i⟧}_{\mathbf{S}}$, then $(s,{\sigma }_i)\in {⟦{\square }_A\phi ⟧}_{\mathbf{S}\left(\mathbf{r}\right)}$.
• If $(s,{\sigma }_i)\in \mathbf{S}\left(\mathbf{r}\right)$, then for all $(t,{\sigma }_j)$ such that $(t,{\sigma }_j)\in \mathbf{S}\left(\mathbf{r}\right)$, $s\stackrel{A}{⟶}t$ and ${\sigma }_i\stackrel{A}{⟶}{\sigma }_j$, we have $(t,{\sigma }_j)\in {⟦\phi ⟧}_{\mathbf{S}\left(\mathbf{r}\right)}$.
• If $(s,{\sigma }_i)\in \mathbf{S}\left(\mathbf{r}\right)$, then for all t and all ${\sigma }_j$ such that $s\stackrel{A}{⟶}t$ and ${\sigma }_i\stackrel{A}{⟶}{\sigma }_j$: if $(t,{\sigma }_j)\in \mathbf{S}\left(\mathbf{r}\right)$, then $(t,{\sigma }_j)\in {⟦\phi ⟧}_{\mathbf{S}\left(\mathbf{r}\right)}$.
• If $(s,{\sigma }_i)\in \mathbf{S}\left(\mathbf{r}\right)$, then for all t and ${\sigma }_j$ such that $s\stackrel{A}{⟶}t$ and ${\sigma }_i\stackrel{A}{⟶}{\sigma }_j$: $t\in {⟦\left[{\sigma }_j\overrightarrow{\psi }\right]\phi ⟧}_{\mathbf{S}}$.
• If $s\in {⟦{\psi }_i⟧}_{\mathbf{S}}$, then for all ${\sigma }_j$ such that ${\sigma }_i\stackrel{A}{⟶}{\sigma }_j$, $s\in {⟦{\square }_A\left[{\sigma }_j\overrightarrow{\psi }\right]\phi ⟧}_{\mathbf{S}}$.
• $s\in {⟦{\psi }_i\to \bigwedge \{{\square }_A\left[{\sigma }_j\overrightarrow{\psi }\right]\phi :{\sigma }_i\stackrel{A}{⟶}{\sigma }_j\}⟧}_{\mathbf{S}}$

This completes the proof. □

Proposition 4.6. 

The action-mix axiom $\left[{\pi }^{\ast }\right]\phi \to \phi \wedge \left[\pi \right]\left[{\pi }^{\ast }\right]\phi$ is sound.

Proof. 

This is standard. □

Proposition 4.7. 

The skip axiom $\left[\mathit{skip}\right]\phi \leftrightarrow \phi$ is sound.

Proof. 

Fix a state model $\mathbf{S}$. Recall that the semantics of $skip$ is the update 1. So the following are equivalent:

• $s\in {⟦\left[skip\right]\phi ⟧}_{\mathbf{S}}$.
• If $s{\mathbf{1}}_{\mathbf{S}}t$, then $t\in {⟦\phi ⟧}_{\mathbf{S}\left(\mathbf{1}\right)}$.
• $s\in {⟦\phi ⟧}_{\mathbf{S}}$.

This completes the proof. □

Proposition 4.8. 

The crash axiom $\left[\mathit{crash}\right]\mathsf{false}$ is sound.

Proof. 

Recall that $⟦crash⟧=\mathbf{0}$, the update having an empty transition relation ${\mathbf{0}}_{\mathbf{S}}$. Working through the definitions, $\left[crash\right]\mathsf{false}$ is easily seen to hold vacuously. □

Proposition 4.9. 

The composition axiom $[\pi ;\rho ]\phi \leftrightarrow \left[\pi \right]\left[\rho \right]\phi$ is sound.

Proof. 

Write $\mathbf{r}$ for $⟦\pi ⟧$ and $\mathbf{b}$ for $⟦\rho ⟧$. Fix a state model $\mathbf{S}$. The following are equivalent:

• $s\in {⟦[\pi ;\rho ]\phi ⟧}_{\mathbf{S}}$.
• If $s{\left[\right[\pi ;\rho \left]\right]}_{\mathbf{S}}u$, then $u\in {⟦\phi ⟧}_{\mathbf{S}(\mathbf{r};\mathbf{b})}$.
• If $s{(\mathbf{r};\mathbf{b})}_{\mathbf{S}}u$, then $u\in {⟦\phi ⟧}_{\mathbf{S}(\mathbf{r};\mathbf{b})}$.
• If $s{\mathbf{r}}_{\mathbf{S}}t$ and $t{\mathbf{b}}_{\mathbf{S}\left(\mathbf{r}\right)}u$, then $u\in {⟦\phi ⟧}_{\mathbf{S}(\mathbf{r};\mathbf{b})}$.
• If $s{\mathbf{r}}_{\mathbf{S}}t$, then $t\in {⟦\left[\rho \right]\phi ⟧}_{\mathbf{S}\left(\mathbf{r}\right)}$.
• $s\in {⟦\left[\pi \right]\left[\rho \right]\phi ⟧}_{\mathbf{S}}$.

The equivalence of (3) and (4) is by the definition of relational composition. The remaining equivalences are from the semantic definitions. The equivalence of (4) and (5) is by the fact that $\mathbf{S}(\mathbf{r};\mathbf{b})=\mathbf{S}\left(\mathbf{r}\right)\left(\mathbf{b}\right)$. □

Proposition 4.10. 

The choice axiom $[\pi \bigsqcup \rho ]\phi \leftrightarrow \left[\pi \right]\phi \wedge \left[\rho \right]\phi$ is sound.

Proof. 

Fix a state model $\mathbf{S}$; we drop $\mathbf{S}$ from the notation in the rest of this proof. Write γ for $\pi \bigsqcup \rho$, $\mathbf{r}$ for $⟦\pi ⟧$, $\mathbf{b}$ for $⟦\rho ⟧$, and $\mathbf{c}$ for $⟦\gamma ⟧$. Then, the following are equivalent:

• $s\in {⟦[\pi \bigsqcup \rho ]\phi ⟧}_{\mathbf{S}}$.
• If $s\mathbf{c}u$, then $u\in {⟦\phi ⟧}_{\mathbf{S}\left(\mathbf{c}\right)}$.
• If $s\mathbf{r}t$, then $t\in {⟦\phi ⟧}_{\mathbf{S}\left(\mathbf{c}\right)}$; and if $s\mathbf{b}{t}^{\prime }$, then $t^{\prime }\in {⟦\phi ⟧}_{\mathbf{S}\left(\mathbf{c}\right)}$.
• If $s\mathbf{r}t$, then $t\in {⟦\phi ⟧}_{\mathbf{S}\left(\mathbf{r}\right)}$; and if $s\mathbf{b}{t}^{\prime }$, then $t^{\prime }\in {⟦\phi ⟧}_{\mathbf{S}\left(\mathbf{b}\right)}$.
• $s\in {⟦\left[\pi \right]\phi ⟧}_{\mathbf{S}}$ and $s\in {⟦\left[\rho \right]\phi ⟧}_{\mathbf{S}}$.
• $s\in {⟦\left[\pi \right]\phi \wedge \left[\rho \right]\phi ⟧}_{\mathbf{S}}$.

The equivalence (2)⟺(3) comes from the fact that each of the u such that $s\mathbf{c}u$ is either either (a) an element t of $\mathbf{S}\left(\mathbf{r}\right)$ related to s by $\mathbf{r}$, or else (b) an element $t^{\prime }$ of $\mathbf{S}\left(\mathbf{b}\right)$ related to s by $\mathbf{b}$. This is by the definition of $\mathbf{r}\bigsqcup \mathbf{b}$.

We show the equivalence (3)⟺(4) by considering the cases (a) and (b) noted just above. We use the fact that the natural injections of $\mathbf{S}\left(\mathbf{r}\right)$ and $\mathbf{S}\left(\mathbf{b}\right)$ in $\mathbf{S}\left(\mathbf{c}\right)$ are bisimulations, and also the fact that $⟦\phi ⟧$ is preserved by bisimulations (see Proposition 3.2). □

4.2. Soundness of the Action Rule

To show that the action rule is sound, we need the following preliminary result.

Lemma 4.11. 

$s\in {⟦\langle \alpha \rangle {\diamond }_{\mathcal{C}}^{\ast }\phi ⟧}_{\mathbf{S}}$ if there is a sequence of states from S

$$s=s_0{\to }_{A_1}{s}_1{\to }_{A_2}\cdots {\to }_{A_{k-1}}{s}_{k-1}{\to }_{A_k}{s}_k$$

where $k\ge 0$, and also a sequence of actions of the same length k,

$$\alpha ={\alpha }_0{\to }_{A_1}{\alpha }_1{\to }_{A_2}\cdots {\to }_{A_{k-1}}{\alpha }_{k-1}{\to }_{A_k}{\alpha }_k$$

such that $A_i\in \mathcal{C}$ and $s_i\in pre{\left({\alpha }_i\right)}_{\mathbf{S}}$ for all $0\le i<k$, and $s_k\in {⟦\langle {\alpha }_k\rangle \phi ⟧}_{\mathbf{S}}$.

Remark 4.12. 

The case $k=0$ just says that $s\in {⟦\langle \alpha \rangle {\diamond }_{\mathcal{C}}^{\ast }\phi ⟧}_{\mathbf{S}}$ is implied by $s\in {⟦\langle \alpha \rangle \phi ⟧}_{\mathbf{S}}$.

Proof. 

The following are equivalent:

• $s\in {⟦\langle \alpha \rangle {\diamond }_{\mathcal{C}}^{\ast }\phi ⟧}_{\mathbf{S}}$.
• $s\in {\left(\langle ⟦\alpha ⟧\rangle ⟦{\diamond }_{\mathcal{C}}^{\ast }\phi ⟧\right)}_{\mathbf{S}}$.
• $s\in {\left(\langle \widehat{\alpha }\rangle ⟦{\diamond }_{\mathcal{C}}^{\ast }\phi ⟧\right)}_{\mathbf{S}}$.
• $s\in \mathrm{pre}{\left(\alpha \right)}_{\mathbf{S}}$, and $(s,\alpha )\in {⟦{\diamond }_{\mathcal{C}}^{\ast }\phi ⟧}_{\mathbf{S}\otimes \mathsf{\Omega }}$.
• $s\in \mathrm{pre}{\left(\alpha \right)}_{\mathbf{S}}$, and for some $k\ge 0$ there is a sequence in $\mathbf{S}\otimes \mathsf{\Omega }$,

  $$(s,\alpha )=t_0{\to }_{A_1}{t}_1{\to }_{A_2}\cdots {\to }_{A_{k-1}}{t}_{k-1}{\to }_{A_k}{t}_k$$

  such that $A_i\in \mathcal{C}$ and $t_k\in {⟦\phi ⟧}_{\mathbf{S}\otimes \mathsf{\Omega }}$.
• There are sequences of states $s=s_0,\dots ,s_k$ and actions ${\alpha }_0,\dots ,{\alpha }_k$ as in the statement of this lemma.

The first equivalence is by the semantics of $\mathcal{L}(\mathbf{\Sigma })$. The equivalence (2)⟺(3) uses the equality $⟦\alpha ⟧=\widehat{\alpha }$ which we saw in the concluding statement of Theorem 3.8 in Section 3.4.1, and also Proposition 2.18. Equivalence (3)⟺(4) uses our overall definitions and the structure of Ω as an action model. (4)⟺(5) is just the semantics of ${\diamond }_{\mathcal{C}}^{\ast }$. Finally, the equivalence (5)⟺ (6) again uses the conclusion of Theorem 3.8. That is, for all i, $(s_i,\alpha )\in \mathbf{S}\otimes \mathsf{\Omega }$, if $s_i\in \mathrm{pre}{\left({\alpha }_i\right)}_{\mathbf{S}}$. □

Proposition 4.13. 

The action rule is sound.

Proof. 

Assume that $s\in {⟦{\chi }_{\alpha }⟧}_{\mathbf{S}}$ but also $s\in {⟦\langle \alpha \rangle {\diamond }_{\mathcal{C}}^{\ast }\neg \psi ⟧}_{\mathbf{S}}$. According to Lemma 4.11, there is a labeled sequence of states from S

$$s=s_0{\to }_{A_1}{s}_1{\to }_{A_2}\cdots {\to }_{A_{k-1}}{s}_{k-1}{\to }_{A_k}{s}_k$$

where $k\ge 0$ and each $A_i\in \mathcal{C}$, and also a sequence of actions of length k, with the same labels,

$$\alpha ={\alpha }_0{\to }_{A_1}{\alpha }_1{\to }_{A_2}\cdots {\to }_{A_{k-1}}{\alpha }_{k-1}{\to }_{A_k}{\alpha }_k$$

such that $s_i\in \mathrm{pre}{\left({\alpha }_i\right)}_{\mathbf{S}}$ for all $0\le i<k$, and $s_k\in {⟦\langle {\alpha }_k\rangle \neg \psi ⟧}_{\mathbf{S}}$. If $k=0$, we would have $s\in {⟦\langle \alpha \rangle \neg \psi ⟧}_{\mathbf{S}}$. But one of the assumptions in the statement of the action rule is that $⊢{\chi }_{\alpha }\to \left[\alpha \right]\psi$. So we would have $s\in {⟦\left[\alpha \right]\psi ⟧}_{\mathbf{S}}$. This would be a contradiction.

Now we argue the case $k>0$. We show by induction on $1\le i\le k$ that $s_i\in {⟦{\chi }_{{\alpha }_i}⟧}_{\mathbf{S}}$. The case $i=0$ is the opening assumption of this proof. Assume that $s_i\in {⟦{\chi }_{{\alpha }_i}⟧}_{\mathbf{S}}$. By hypothesis, $s_i\in \mathrm{pre}{\left({\alpha }_i\right)}_{\mathbf{S}}$. In view of the second assumption in the action rule, $s_i\in {⟦{\square }_{A_{i+1}}{\chi }_{{\alpha }_{i+1}}⟧}_{\mathbf{S}}$. Hence, $s_{i+1}\in {⟦{\chi }_{{\alpha }_{i+1}}⟧}_{\mathbf{S}}$. This completes our induction.

In particular, $s_k\in {⟦{\chi }_{{\alpha }_k}⟧}_{\mathbf{S}}$. Using again the first assumption in the action rule, we have $s_k\in {⟦\left[{\alpha }_k\right]\psi ⟧}_{\mathbf{S}}$. This is a contradiction. □

4.3. Syntactic Facts

At this point, we have presented the semantic facts which we need concerning ${\mathcal{L}}_1(\mathbf{\Sigma })$. These include the soundness of the logical system for validity. To prove completeness, we also need some syntactic facts. We could have presented this section earlier, but since it leans on the action rule, we have delayed it until establishing the soundness of that rule.

In this section, α, β, etc., denote simple actions in ${\mathcal{L}}_1(\mathbf{\Sigma })$.

4.3.1. A Stronger form of the Action-Knowledge Axiom

At this point, we establish a stronger form of the action-knowledge axiom. In Figure 3 in Section 4, this axiom was stated only for basic actions. The strengthenings here is to simple actions, that is, to compositions of basic actions, $skip$ and $crash$.

Lemma 4.14. 

The Action-Knowledge Axiom is provable for all simple actions α:

$$⊢\left[\alpha \right]{\square }_A\phi \leftrightarrow ({\mathrm{P}}_{\mathrm{RE}}\left(\alpha \right)\to \bigwedge \{{\square }_A\left[\beta \right]\phi :\alpha \stackrel{A}{⟶}\beta in\mathsf{\Omega }\})$$

(10)

Proof. 

By induction on α. If α is $skip$, ${\mathrm{P}}_{\mathrm{RE}}\left(\alpha \right)=\mathsf{true}$, the only β with $\alpha \stackrel{A}{⟶}\beta$ is $skip$, and equivalence (10) reads:

$$⊢\left[skip\right]{\square }_A\phi \leftrightarrow (\mathsf{true}\to {\square }_A\left[skip\right]\phi )$$

And this is an easy consequence of propositional reasoning, the skip axiom, and ${\square }_A$ necessitation. If α is $crash$, ${\mathrm{P}}_{\mathrm{RE}}\left(\alpha \right)=\mathsf{false}$, and there are no β such that $\alpha \stackrel{A}{⟶}\beta$. Equivalence (10) then reads:

$$⊢\left[crash\right]{\square }_A\phi \leftrightarrow (\mathsf{false}\to \mathsf{true}).$$

By the crash axiom and modal reasoning, $⊢\left[crash\right]{\square }_A\phi$; and so the assertion just above holds.

If α is of the form ${\sigma }_i\overrightarrow{\psi }$, then we simply have the Action-Knowledge Axiom in the form we know it.

So assume our lemma for ${\alpha }^{\prime }$ and α; we prove it for ${\alpha }^{\prime };\alpha$. We show that

$$⊢[{\alpha }^{\prime };\alpha ]{\square }_A\phi \leftrightarrow ({\mathrm{P}}_{\mathrm{RE}}({\alpha }^{\prime };\alpha )\to \bigwedge \{{\square }_A[{\beta }^{\prime };\beta ]\phi :{\alpha }^{\prime };\alpha \stackrel{A}{⟶}{\beta }^{\prime };\beta \mathrm{in}\mathsf{\Omega }\})$$

(11)

We start with the equivalence in (10), use $\left[{\alpha }^{\prime }\right]$ necessitation and normality, and obtain

$$⊢\left[{\alpha }^{\prime }\right]\left[\alpha \right]{\square }_A\phi \leftrightarrow (\left[{\alpha }^{\prime }\right]{\mathrm{P}}_{\mathrm{RE}}\left(\alpha \right)\to \bigwedge \{\left[{\alpha }^{\prime }\right]{\square }_A\left[\beta \right]\phi :\alpha \stackrel{A}{⟶}\beta \mathrm{in}\mathsf{\Omega }\})$$

(12)

By the induction hypothesis on ${\alpha }^{\prime }$ and several uses of the composition axiom, we have that for all β,

$$⊢\left[{\alpha }^{\prime }\right]{\square }_A\left[\beta \right]\phi \leftrightarrow ({\mathrm{P}}_{\mathrm{RE}}\left({\alpha }^{\prime }\right)\to \bigwedge \{{\square }_A[{\beta }^{\prime };\beta ]\phi :{\alpha }^{\prime }\stackrel{A}{⟶}{\beta }^{\prime }\mathrm{in}\mathsf{\Omega }\}).$$

The composition axiom and (12) lead to the provable equivalence of $[{\alpha }^{\prime };\alpha ]{\square }_A\phi$ and

$$\left[{\alpha }^{\prime }\right]{\mathrm{P}}_{\mathrm{RE}}\left(\alpha \right)\to ({\mathrm{P}}_{\mathrm{RE}}\left({\alpha }^{\prime }\right)\to \bigwedge \{{\square }_A[{\beta }^{\prime };\beta ]\phi :\alpha \stackrel{A}{⟶}\beta \mathrm{and}{\alpha }^{\prime }\stackrel{A}{⟶}{\beta }^{\prime }\mathrm{in}\mathsf{\Omega }\}).$$

But $⊢{\mathrm{P}}_{\mathrm{RE}}({\alpha }^{\prime };\alpha )\leftrightarrow {\mathrm{P}}_{\mathrm{RE}}\left({\alpha }^{\prime }\right)\wedge \left[{\alpha }^{\prime }\right]{\mathrm{P}}_{\mathrm{RE}}\left(\alpha \right)$. In addition, we have a general fact ${\alpha }^{\prime };\alpha \stackrel{A}{⟶}{\beta }^{\prime };\beta$ if ${\alpha }^{\prime }\stackrel{A}{⟶}{\beta }^{\prime }$ and $\alpha \stackrel{A}{⟶}\beta$. Using these observations and some propositional reasoning, we obtain (11), as desired. □

Remark 4.15. 

There are no sound versions of the Action-Knowledge Axiom for actions containing ⊔. For example, let $\mathcal{A}$ be a singleton, hence omitted from the notation. Consider $\mathbf{\Sigma }=\{\sigma ,\tau \}$ as an action signature with the enumeration $\sigma$, $\tau$, and with (say) the arrows $\sigma \to \tau$ and $\tau \to \sigma$. Note that by atomic permanence, $\left[\sigma pq\right]r$ is equivalent to $p\to r$; $\left[\tau pq\right]r$ is equivalent to $q\to r$; by action-knowledge and atomic permanence, $\left[\sigma pq\right]\square r$ is equivalent to $p\to \square (q\to r)$; and $\left[\tau pq\right]\square r$ is equivalent to $q\to \square (p\to r)$. Consider also the sentence $\left[\right(\sigma pq)\bigsqcup (\tau pq\left)\right]\square r$. By the choice axiom, it is equivalent to

$$(p\to \square (q\to r\left)\right)\wedge (q\to \square (p\to r\left)\right).$$

(13)

Now, we did not define ${\mathrm{P}}_{\mathrm{RE}}\left(\right(\sigma pq)\bigsqcup (\tau pq\left)\right)$, but the most reasonable choice is $p\vee q$. And we did not define the accessibility structure of actions containing ⊔, but in this case the most likely choice is to have $\left(\sigma pq\right)\bigsqcup \left(\tau pq\right)$ relate to itself and nothing else. But then when we write out the right-hand side of the equivalence (10), we obtain

$$(p\vee q)\to (\square (p\to r)\wedge \square (q\to r\left)\right).$$

Clearly, this is not equivalent to (13). Even if one were to change ${\mathrm{P}}_{\mathrm{RE}}\left(\right(\sigma pq)\bigsqcup (\tau pq\left)\right)$ to, say, $\mathsf{true}$, or to $p\wedge q$, we still would not have an equivalence: (13) is stronger.

4.3.2. A Stronger form of the Partial Functionality Axiom

We shall also need the following result, a version of the partial functionality axiom:

Lemma 4.16. 

$⊢\langle \alpha \rangle \phi \leftrightarrow {\mathrm{P}}_{\mathrm{RE}}\left(\alpha \right)\wedge \left[\alpha \right]\phi$.

Proof. 

This is an induction, much like the proof of Lemma 4.14, above. □

4.3.3. Syntactic Bisimulation

Our next set of results pertains to a syntactic notion of action equivalence, one with a bisimulation-like flavor.

Definition 4.17. 

A syntactic bisimulation is a relation R on the set $\mathsf{\Omega }$ of simple actions of $\mathcal{L}(\mathbf{\Sigma })$ with the following property: if $\alpha R\beta$, then

1. 

$⊢{\mathrm{P}}_{\mathrm{RE}}\left(\alpha \right)\leftrightarrow {\mathrm{P}}_{\mathrm{RE}}\left(\beta \right)$.

2. 

For all ${\alpha }^{\prime }$ and A such that $\alpha \stackrel{A}{⟶}{\alpha }^{\prime }$, there is some ${\beta }^{\prime }$ such that $\beta \stackrel{A}{⟶}{\beta }^{\prime }$ and ${\alpha }^{\prime }R{\beta }^{\prime }$.

3. 

For all ${\beta }^{\prime }$ and A such that $\beta \stackrel{A}{⟶}{\beta }^{\prime }$, there is some ${\alpha }^{\prime }$ such that $\alpha \stackrel{A}{⟶}{\alpha }^{\prime }$ and ${\alpha }^{\prime }R{\beta }^{\prime }$.

We say that $\alpha$ and $\beta$ are provably equivalent if there is some syntactic bisimulation relating them. We write $\alpha \equiv \beta$ in this case.

For sentences, we write $\phi \equiv \psi$ and say that $\phi$ and $\psi$ are equivalent if $⊢\phi \leftrightarrow \psi$.

Lemma 4.18. 

$⊢\langle \alpha \rangle \mathsf{true}\leftrightarrow {\mathrm{P}}_{\mathrm{RE}}\left(\alpha \right)$.

Proof. 

By induction on α. For $\alpha =skip$ and $\alpha =crash$, we use the skip axiom and the crash axiom, respectively. Here is the argument for α of the form ${\sigma }_i\overrightarrow{\psi }$. First, by necessitation we have $⊢\left[{\sigma }_i\overrightarrow{\psi }\right]\mathsf{true}$. And by this and partial functionality, $⊢\left[{\sigma }_i\overrightarrow{\psi }\right]\neg \mathsf{true}\leftrightarrow \neg {\psi }_i$. So $⊢\neg \left[{\sigma }_i\overrightarrow{\psi }\right]\neg \mathsf{true}\leftrightarrow {\psi }_i$. That is, $⊢\langle {\sigma }_i\overrightarrow{\psi }\rangle \mathsf{true}\leftrightarrow {\psi }_i$.

Finally, assume the result for β. Then, by normality and necessitation, $⊢\langle \alpha \rangle \langle \beta \rangle \mathsf{true}\leftrightarrow \langle \alpha \rangle {\mathrm{P}}_{\mathrm{RE}}\left(\beta \right)$. So $⊢\langle \alpha \rangle \langle \beta \rangle \mathsf{true}\leftrightarrow {\mathrm{P}}_{\mathrm{RE}}(\alpha ;\beta )$. We conclude by showing as a general fact that $⊢\langle \alpha \rangle \langle \beta \rangle \phi \leftrightarrow \langle \alpha ;\beta \rangle \phi$. For this, the composition axiom tells us that $⊢\left[\alpha \right]\left[\beta \right]\neg \phi \leftrightarrow [\alpha ;\beta ]\neg \phi$. So $⊢\neg \left[\alpha \right]\neg \neg \left[\beta \right]\neg \phi \leftrightarrow \neg [\alpha ;\beta ]\neg \phi$. Thus, $⊢\langle \alpha \rangle \langle \beta \rangle \phi \leftrightarrow \langle \alpha ;\beta \rangle \phi$, as desired. □

Lemma 4.19. 

The following monoid-type laws hold:

1. 

$⊢{\mathrm{P}}_{\mathrm{RE}}(\alpha ;\mathrm{skip})\leftrightarrow {\mathrm{P}}_{\mathrm{RE}}\left(\alpha \right)\leftrightarrow {\mathrm{P}}_{\mathrm{RE}}(\mathrm{skip};\alpha )$.

2. 

$⊢{\mathrm{P}}_{\mathrm{RE}}(\alpha ;(\beta ;\gamma \left)\right)\leftrightarrow {\mathrm{P}}_{\mathrm{RE}}\left(\right(\alpha ;\beta );\gamma )$.

Proof. 

We use the definitions to calculate

$$\begin{array}{ccc}{\mathrm{P}}_{\mathrm{RE}}(\alpha ;skip)\hfill & =& \langle \alpha \rangle \mathsf{true}\hfill \\ {\mathrm{P}}_{\mathrm{RE}}(skip;\alpha )\hfill & =& \langle skip\rangle {\mathrm{P}}_{\mathrm{RE}}\left(\alpha \right).\hfill \end{array}$$

We obtain a formal proof using Lemma 4.18 and the skip axiom. Turning to the second law,

$$\begin{array}{ccc}{\mathrm{P}}_{\mathrm{RE}}(\alpha ;(\beta ;\gamma \left)\right)\hfill & =& \langle \alpha \rangle {\mathrm{P}}_{\mathrm{RE}}(\beta ;\gamma )\hfill \\ & =& \langle \alpha \rangle \langle \beta \rangle {\mathrm{P}}_{\mathrm{RE}}\left(\gamma \right)\hfill \\ & \equiv & \langle \alpha ;\beta \rangle {\mathrm{P}}_{\mathrm{RE}}\left(\gamma \right)\hfill \\ & =& {\mathrm{P}}_{\mathrm{RE}}\left(\right(\alpha ;\beta );\gamma ).\hfill \end{array}$$

The equivalence above which mentions ≡ uses the composition axiom. □

Lemma 4.20. 

Concerning the syntactic equivalence ≡ on Ω:

1. 

The relation ≡ is an equivalence relation.

2. 

If ${\phi }_1\equiv {\psi }_1$, …, ${\phi }_n\equiv {\psi }_n$, then ${\sigma }_i\overrightarrow{\phi }\equiv {\sigma }_i\overrightarrow{\psi }$.

3. 

$\alpha ;skip\equiv \alpha \equiv skip;\alpha$.

4. 

$\alpha ;(\beta ;\gamma )\equiv (\alpha ;\beta );\gamma$.

5. 

If $\alpha \equiv {\alpha }^{\prime }$ and $\beta \equiv {\beta }^{\prime }$, then $\alpha ;\beta \equiv {\alpha }^{\prime };{\beta }^{\prime }$.

Proof. 

The first part is routine. Part (2) uses the bisimulation consisting of all pairs $({\sigma }_j\overrightarrow{\phi },{\sigma }_j\overrightarrow{\psi })$ such that $1\le j\le n$ and for all i, ${\phi }_i\equiv {\psi }_i$. Lemma 4.19 is used in parts (3) and (4). The rest of the argument for part (3) is easy and we omit it. For part (4), we take R to be the set of pairs

$$({\alpha }^{\prime };({\beta }^{\prime };{\gamma }^{\prime }),({\alpha }^{\prime };{\beta }^{\prime });{\gamma }^{\prime })$$

such that for some sequence w of ${\to }_A$ with $A\in {\mathcal{A}}^{\ast }$, ${\alpha }^{\prime }$ is reachable from α via w, and similarly for ${\beta }^{\prime }$ and ${\gamma }^{\prime }$ (via the same w). Part (5) is similar. □

Lemma 4.21. 

For all $A\in \mathcal{C}$ and all β such that $\alpha {\to }_A\beta$,

1. 

$⊢\left[\alpha \right]{\square }_{\mathcal{C}}^{\ast }\psi \to \left[\alpha \right]\psi$.

2. 

$⊢\left[\alpha \right]{\square }_{\mathcal{C}}^{\ast }\psi \wedge {\mathrm{P}}_{\mathrm{RE}}\left(\alpha \right)\to {\square }_A\left[\beta \right]{\square }_{\mathcal{C}}^{\ast }\psi$.

Proof. 

Part (1) follows from the epistemic-mix axiom and modal reasoning. For part (2), we start with a consequence of the epistemic-mix axiom: $⊢{\square }_{\mathcal{C}}^{\ast }\psi \to {\square }_A{\square }_{\mathcal{C}}^{\ast }\psi$. Then, by modal reasoning, $⊢\left[\alpha \right]{\square }_{\mathcal{C}}^{\ast }\psi \to \left[\alpha \right]{\square }_A{\square }_{\mathcal{C}}^{\ast }\psi$. By the Action-Knowledge Axiom in the generalized form of Lemma 4.14, we have $⊢\left[\alpha \right]{\square }_{\mathcal{C}}^{\ast }\psi \wedge {\mathrm{P}}_{\mathrm{RE}}\left(\alpha \right)\to {\square }_A\left[\beta \right]{\square }_{\mathcal{C}}^{\ast }\psi$. □

We present next our main result on the syntactic equivalence of actions. It is a syntactic version of Proposition 2.18.

Lemma 4.22. 

Let α and β be simple actions. If $\alpha \equiv \beta$, then for all φ, $⊢\left[\alpha \right]\phi \leftrightarrow \left[\beta \right]\phi$.

Proof. 

By induction on φ. Fix a syntactic bisimulation R relating α and β. For $\phi =\mathsf{true}$ or an atomic sentence $p_i$, our result is easy. The induction steps for ¬ and ∧ are trivial. The step for ${\square }_A$ is not hard, and so we omit it.

We next check the result for sentences $\left[\gamma \right]\phi$. We need to see that

$$⊢\left[\alpha \right]\left[\gamma \right]\phi \leftrightarrow \left[{\alpha }^{\prime }\right]\left[\gamma \right]\phi .$$

For this, it is sufficient by the composition axiom to show that $⊢[\alpha ;\gamma ]\phi \leftrightarrow [{\alpha }^{\prime };\gamma ]\phi$. By Lemma 4.20, parts (1) and (5), $\alpha ;\gamma \equiv {\alpha }^{\prime };\gamma$. So we have completed the induction hypothesis.

This leaves the step for sentences of the form ${\square }_{\mathcal{B}}^{\ast }\phi$, assuming the result for φ. We use the action rule to show that $⊢\left[\alpha \right]{\square }_{\mathcal{C}}^{\ast }\phi \to \left[\beta \right]{\square }_{\mathcal{C}}^{\ast }\phi$. We need a functional witness to R; that is, a map ${\beta }^{\prime }\mapsto {\alpha }^{\prime }$ for all ${\beta }^{\prime }$ such that $\beta \stackrel{\mathcal{A}\ast }{\mapsto }{\beta }^{″}$ such that, α′R β′ for all the actions. Further, let ${\chi }_{{\beta }^{\prime }}$ be $\left[{\alpha }^{\prime }\right]{\square }_{\mathcal{C}}^{\ast }\phi$ We need to show that for all A ∈ C and all ${\beta }^{\prime }\stackrel{A}{\mapsto }{\beta }^{″}$

a.

$⊢\left[\alpha \right]{\square }_{\mathcal{C}}^{\ast }\phi \to \left[{\beta }^{\prime }\right]\phi$

b.

If ${\beta }^{\prime }\stackrel{A}{\mapsto }{\beta }^{″}$ then $⊢\left[{\alpha }^{\prime }\right]{\square }_{\mathcal{C}}^{\ast }\phi \wedge {\mathrm{P}}_{\mathrm{RE}}\left({\beta }^{\prime }\right)\to {\square }_A\left[{\alpha }^{″}\right]{\square }_{\mathcal{C}}^{\ast }\phi .$

For (a), we know from Lemma 4.21 that $⊢\left[{\alpha }^{\prime }\right]{\square }_{\mathcal{C}}^{\ast }\phi \to \left[{\alpha }^{\prime }\right]\phi$ By induction hypothesis on φ, $⊢\left[{\alpha }^{\prime }\right]\phi \leftrightarrow \left[{\beta }^{\prime }\right]\phi$ And this implies (a). For (b), Lemma 4.21 tells us that under the assumptions,

$$⊢\left[{\alpha }^{\prime }\right]{\square }_{\mathcal{C}}^{\ast }\phi \wedge {\mathrm{P}}_{\mathrm{RE}}\left({\alpha }^{\prime }\right)\to {\square }_A\left[{\alpha }^{″}\right]{\square }_{\mathcal{C}}^{\ast }\phi .$$

The fact that R is a syntactic bisimulation tells us that $⊢{\mathrm{P}}_{\mathrm{RE}}\left({\alpha }^{\prime }\right)\leftrightarrow {\mathrm{P}}_{\mathrm{RE}}\left({\beta }^{\prime }\right)$ This implies (b).

This completes the induction on φ. □

Lemma 4.22 will be used in several places to come.

5. Completeness Theorems

In this section, we prove the completeness of our logical systems for ${\mathcal{L}}_0(\mathbf{\Sigma })$ and ${\mathcal{L}}_1(\mathbf{\Sigma })$. (See Figure 1 for these.) Recall that the difference between the two languages is that the second has the common-knowledge propositional operators ${\square }_{\mathcal{B}}^{\ast }$ while the first does not. This difference makes the bigger system much more expressive, and more difficult to study. As it happens, the extension of ${\mathcal{L}}_1(\mathbf{\Sigma })$ to the full logic $\mathcal{L}(\mathbf{\Sigma })$, the extension via the action iteration operation ${\pi }^{\ast }$, leads to a logical language whose validity problem is complete ${\mathsf{\Pi }}_1^1$. So there cannot be a recursively axiomatized logical system for the validities of $\mathcal{L}(\mathbf{\Sigma })$. Returning to the smaller ${\mathcal{L}}_1(\mathbf{\Sigma })$, even here the common-knowledge operators ${\square }_{\mathcal{B}}^{\ast }$ give a logical system which is not compact. So we cannot have a strongly complete logic for it; that is, we cannot axiomatize the notion of validity under hypotheses $T\vDash \phi$. The best one can hope for is weak completeness: $⊢\phi$ if and only if $\vDash \phi$. We prove this in Theorem 5.31. As a result of some preliminary results aimed toward that result, we establish the strong completeness of our axiomatization of the weaker logic ${\mathcal{L}}_0(\mathbf{\Sigma })$. The work there is easier because it relies on a translation into modal logic.

In a later section, we show that in contrast to our translation results for ${\mathcal{L}}_0(\mathbf{\Sigma })$, the larger language ${\mathcal{L}}_1(\mathbf{\Sigma })$ cannot be translated into $\mathcal{L}$ or even to $\mathcal{L}\left({\square }^{\ast }\right)$ (modal logic with extra modalities ${\square }_{\mathcal{B}}^{\ast }$). So completeness results for ${\mathcal{L}}_1(\mathbf{\Sigma })$ cannot simply be based on translation.

5.1. The Ideas

Our completeness proofs are somewhat involved, and it might help the reader to have a preview of some of the ideas before we get started. For ${\mathcal{L}}_0(\mathbf{\Sigma })$, the leading idea is that we can translate the logic back to ordinary modal logic. Then we obtain completeness by taking any logical system for modal logic and adding whatever principles are needed in order to make the translation. This idea is simple enough, and after looking at a few examples one can see how the translation of ${\mathcal{L}}_0(\mathbf{\Sigma })$ to modal logic should go. But the formal definition of the translation is complicated. Our definition goes via a term rewriting system related to the axioms of the logic. Part of our work in this section will be to prove the termination of our system. It would have been nice to use some off-the-shelf results of term rewriting theory to get the termination of our system, but this does not seem to be possible. In any case, we prove termination by establishing a decreasing interpretation of the system; that is, rewriting a sentence leads to a decrease in an order < that we study at length. Our interpretation is exponential rather than polynomial, and it was found by hand.

When we turn to ${\mathcal{L}}_1(\mathbf{\Sigma })$, our model is the filtration proof of the completeness of PDL due to Kozen and Parikh [15]. We need to use the action rule rather than an induction rule, but modulo this difference, the work is similar. We also need to use some of the details on the ordering < mentioned above. That is, even if one were interested in the completeness theorem of ${\mathcal{L}}_0(\mathbf{\Sigma })$ alone, our proof would still involve the general rewriting apparatus.

Definition 5.1. 

Let $\mathcal{NF}$ be the smallest set of ground sentences and actions in ${\mathcal{L}}_1(\mathbf{\Sigma })$ with the following properties:

1. 

Each atomic p belongs to $\mathcal{NF}$.

2. 

If $\phi ,\psi \in \mathcal{NF}$, then also $\neg \phi$, $\phi \wedge \psi$, ${\square }_A\phi$, and ${\square }_{\mathcal{C}}^{\ast }\phi$ belong to $\mathcal{NF}$.

3. 

If $\alpha \in \mathcal{NF}$, $\phi \in \mathcal{NF}$, and $\mathcal{C}\subseteq \mathcal{A}$, then $\left[\alpha \right]{\square }_{\mathcal{C}}^{\ast }\phi$ belongs to $\mathcal{NF}$.

4. 

If $k\ge 0$, if $\overrightarrow{{\psi }^1}$, …, $\overrightarrow{{\psi }^k}$ is a sequence of sequences of length $n(\mathbf{\Sigma })$ of elements of $\mathcal{NF}$, and if ${\sigma }_1,\dots ,{\sigma }_k\in \Sigma$,

$$(\cdots (({\sigma }_1\overrightarrow{{\psi }^1};{\sigma }_2\overrightarrow{{\psi }^2});\cdots ;{\sigma }_k\overrightarrow{{\psi }^k})$$

(14)

is an action term in $\mathcal{NF}$.

Lemma 5.2. 

There is a function $\mathit{nf}:{\mathcal{L}}_1(\mathbf{\Sigma })\to \mathcal{NF}$ such that for all φ, $⊢\phi \leftrightarrow \mathit{nf}\left(\phi \right)$. Moreover, if $\phi \in {\mathcal{L}}_0(\mathbf{\Sigma })$, then $\mathit{nf}\left(\phi \right)$ is a purely modal sentence (it contains no actions).

Lemma 5.3. 

There is a well-order < on ${\mathcal{L}}_1(\mathbf{\Sigma })$ such that for all φ and α:

1. 

$\mathit{nf}\left(\phi \right)\le \phi$.

2. 

${\mathrm{P}}_{\mathrm{RE}}\left(\alpha \right)<\left[\alpha \right]\phi$.

3. 

If $\alpha \stackrel{A}{⟶}\beta$, then $\left[\beta \right]\phi <\neg \left[\beta \right]\phi <\left[\alpha \right]{\square }_{\mathcal{C}}^{\ast }\phi$.

Lemma 5.4. 

For every φ there is a finite set $f\left(\phi \right)\subseteq \mathcal{NF}$ such that

1. 

$f\left(\phi \right)$ is closed under subsentences.

2. 

If $\left[\gamma \right]{\square }_{\mathcal{C}}^{\ast }\chi \in f\left(\phi \right)$, $\gamma \stackrel{{\mathcal{C}}^{\ast }}{⟶}\delta$, and $A\in \mathcal{C}$, then $f\left(\phi \right)$ also contains ${\square }_A\left[\delta \right]{\square }_{\mathcal{C}}^{\ast }\chi$, $\left[\delta \right]{\square }_{\mathcal{C}}^{\ast }\chi$, $\mathit{nf}\left({\mathrm{P}}_{\mathrm{RE}}\right(\delta \left)\right)$, and $\mathit{nf}\left(\right[\delta \left]\chi \right)$.

The proofs of these will appear in Section 5.2 just below. The proofs are technical, and so the reader not interested in those details might wish to omit the next section on a first reading of this paper. We shall use Lemmas 5.2–5.4 in the work on completeness below, but neither the details of the proofs nor the other results of Section 5.2 will be used in the rest of this paper.

5.2. Proofs of the Main Facts on Normal Forms and the Well-Order <

We turn to the proofs of Lemmas 5.2–5.4, just above. Our proofs are complicated and circuitous, so there might be shorter arguments. For example, we do not know of any proofs that avoid term rewriting theory. For the record, here are some of the reasons why we feel that the study of our system is complicated:

• The original statement of axioms such as the action-knowledge axiom is in terms of actions of the form $\left[{\sigma }_i\overrightarrow{\psi }\right]$.
• On the other hand, the action rule is best stated in terms of actions which are compositions of the actions $\left[{\sigma }_i\overrightarrow{\psi }\right]$. In a term-rewriting setting, this point and the previous one work against each other. Our work will be to work with the versions of the axioms that are generalized to the case of all simple actions.
• Again mentioning term rewriting, we will need to pick an orientation for the composition axiom. This will either be $\left[\alpha \right]\left[\beta \right]\phi ⇝[\alpha ;\beta ]\phi$, or $[\alpha ;\beta ]\phi ⇝\left[\alpha \right]\left[\beta \right]\phi$ 6. Both alternatives lead to difficulties at various points. We chose the first alternative, and for this reason, we will need a formulation of the Action-Knowledge Axiom as an infinite scheme.
• Our language has the program union operator ⊔, but because the axioms are not, in general, sound for sums, we need to reformulate things to avoid ⊔.

It is convenient to replace ${\mathcal{L}}_1(\mathbf{\Sigma })$ by a slightly different language which we call ${\mathcal{L}}_1^{+}(\mathbf{\Sigma })$. This new language is shown in Figure 4. For the purposes of this section, we stress the formulation of this as an algebra for a two-sorted signature. Starting with some fixed action signature Σ, we construct a two-sorted signature $\Delta =\Delta (\mathbf{\Sigma })$ of terms, obtained in the following way. Let n be the number of simple actions in Σ.

• Δ has two sorts: s (for sentences) and a (for actions).
• Each $p\in \mathsf{AtSen}$ is a constant symbol of sort s.
• ¬, ${\square }_A$, and ${\square }_{\mathcal{B}}^{\ast }$ are function symbols of type $s\to s$.
• ∧ and → are binary function symbols of type $s\times s\to s$.
• Each $\sigma \in \Sigma$ is a function symbol of sort $s^n\to a$.
• ; is function symbols of sort $a\times a\to a$.
• $app$ is a binary symbol of type $a\times s\to s$.
• ${\mathrm{P}}_{\mathrm{RE}}$ is a function symbol of sort $a\to s$.

The most important addition here is that we have ${\mathrm{P}}_{\mathrm{RE}}$ as a first-class part of the syntax; previously, it had been an abbreviation. We also add the implication symbol →, but this is only for convenience. Obviously, → may be dropped from the system. On the other hand, we dropped ⊔ (as we mentioned, some axioms are not sound as equations in general if we have ⊔). We might as well drop $skip$ as well since it, too, can be translated away.

Incidentally, the fact that $\mathrm{pre}$ is not a symbol of ${\mathcal{L}}_1(\mathbf{\Sigma })$ makes the issue of translating between ${\mathcal{L}}_1(\mathbf{\Sigma })$ and ${\mathcal{L}}_1^{+}(\mathbf{\Sigma })$ delicate. The reader might wish to formulate a careful translation in order to appreciate some of the features of our ordering < which we shall introduce in due course.

We adopt the usual notational conventions that ∧, ↔, and ;, are used as infix symbols. We continue our practice of writing ${\sigma }_i\overrightarrow{\psi }$ for what technically would be ${\sigma }_1({\psi }_1,\dots ,{\psi }_n)$. Also, we write $\left[\alpha \right]\psi$ instead of $app(\alpha ,\psi )$.

When dealing with ${\mathcal{L}}_1^{+}(\mathbf{\Sigma })$, we let α, β, etc., range over terms of sort a, and φ, ψ, χ, etc., range over terms of sort s. Finally, we use letters such as t and u for terms of either sort (so as to shorten many of our statements). We also will need to adjoin new variables to our signature in order to formulate the notion of substitution that leads to a term rewriting system. For this, we let $X_a$ and $X_s$ be sets of new symbols. In order to simplify our notation, we will use letters such as x, y, and z to range over both of these sets. That is, we will not notationally distinguish the two sorts of variables. The context will always make it clear what the sort of any given variable is.

Let ${\mathcal{L}}_1^{+}(\mathbf{\Sigma },X)$ be the terms built from our signature which now may contain the variables from X. Examples of such terms may be found in Figure 5.

Lemma 5.5. 

Let φ be a sentence of ${\mathcal{L}}_1(\mathbf{\Sigma })$. Then there is some ${\phi }^{†}\in {\mathcal{L}}_1(\mathbf{\Sigma })$ which does not contain ⊔, $\mathrm{crash}$ or $\mathrm{skip}$ such that $⊢\phi \leftrightarrow {\phi }^{†}$.

Proof. 

(J. Sack, personal communication) We define $\phi \mapsto {\phi }^{†}$ as follows:

$$\begin{array}{ccc}{\mathsf{true}}^{†}\hfill & =& \mathsf{true}\hfill \\ p_i^{†}\hfill & =& p_i\hfill \\ {(\neg \phi )}^{†}\hfill & =& \neg {\phi }^{†}\hfill \\ {(\phi \wedge \psi )}^{†}\hfill & =& {\phi }^{†}\wedge {\psi }^{†}\hfill \\ {\left({\square }_A\phi \right)}^{†}\hfill & =& {\square }_A{\phi }^{†}\hfill \\ {\left({\square }_{\mathcal{B}}^{\ast }\phi \right)}^{†}\hfill & =& {\square }_{\mathcal{B}}^{\ast }{\phi }^{†}\hfill \end{array}\begin{array}{ccc}{\left(\left[skip\right]\phi \right)}^{†}\hfill & =& {\phi }^{†}\hfill \\ {\left(\left[crash\right]\phi \right)}^{†}\hfill & =& \mathsf{true}\hfill \\ {\left([{\sigma }_i{\psi }_1\cdots {\psi }_n]\phi \right)}^{†}\hfill & =& [{\sigma }_i{\psi }_1^{†}\cdots {\psi }_n^{†}]{\phi }^{†}\hfill \\ {\left([\pi \bigsqcup \rho ]\phi \right)}^{†}\hfill & =& {\left(\left[\pi \right]\phi \right)}^{†}\wedge {\left(\left[\rho \right]\phi \right)}^{†}\hfill \\ {\left([\pi ;\rho ]\phi \right)}^{†}\hfill & =& {\left(\left[\pi \right]\left[\rho \right]\phi \right)}^{†}\hfill \\ \end{array}$$

The definition is by recursion on the number k of composition symbols (;) in φ. For a fixed k, we then use recursion on the total number of symbols. The overall recursion allows us to define ${\left([\pi ;\rho ]\phi \right)}^{†}$ to be ${\left(\left[\pi \right]\left[\rho \right]\phi \right)}^{†}$. And the ’inside’ recursion on the number of symbols allows us to define ${\left([\pi \bigsqcup \rho ]\phi \right)}^{†}$ in terms of ${\left(\left[\pi \right]\phi \right)}^{†}$ and ${\left(\left[\rho \right]\phi \right)}^{†}$.

We indicate two of the verifications that our definition works. Here are the details for the line involving ${\left([{\sigma }_i{\psi }_1\cdots {\psi }_n]\phi \right)}^{†}$. Assuming the relevant induction hypotheses, we see that ${\sigma }_i{\psi }_1\cdots {\psi }_n\equiv {\sigma }_i{\psi }_1^{†}\cdots {\psi }_n^{†}$ (see Lemma 4.20, part 2). And then by Lemma 4.22,

$$[{\sigma }_i{\psi }_1\cdots {\psi }_n]\phi \equiv [{\sigma }_i{\psi }_1^{†}\cdots {\psi }_n^{†}]\phi .$$

Using necessitation, we also have equivalence to $[{\sigma }_i{\psi }_1^{†}\cdots {\psi }_n^{†}]{\phi }^{†}$.

Some of the other cases use necessitation in this way also. In all cases, the verifications are similar. □

Remark 5.6. 

In the remainder of this paper, we shall assume that sentences and actions of ${\mathcal{L}}_1(\mathbf{\Sigma })$ do not contain ⊔, $crash$ or $skip$. We also regard them as ground terms of ${\mathcal{L}}_1^{+}(\mathbf{\Sigma })$: these are terms without variables.

Incidentally, the proof of Lemma 5.5 shows that ; is also eliminable. However, we shall not assume that ; is not found in our sentences. In fact, the rewriting system $\mathcal{R}$ that we present shortly will introduce compositions.

5.2.1. The Rewriting System $\mathcal{R}$ and Its Interpretation

We recall here the general notion of term rewriting as it applies to ${\mathcal{L}}_1^{+}(\mathbf{\Sigma },X)$. For more on this topic, especially on the notion of termination, see, e.g., Dershowitz [16]. Consider a rewrite rule (r) of the form $l⇝r$, where l and r are elements of ${\mathcal{L}}_1^{+}(\mathbf{\Sigma },X)$. This (r) generates a relation of immediate rewriting on ${\mathcal{L}}_1^{+}(\mathbf{\Sigma },X)$: we say that $t_1$ rewrites to $t_2$ via (r) if there is a term u with exactly one occurrence of a variable x (of either sort) and a substitution σ such that $u(x\leftarrow l^{\sigma })=t_1$ and $u(x\leftarrow r^{\sigma })=t_2$. That is, $t_1$ and $t_2$ result from u by substituting l and r in for x; however, we need not use l and r literally, but we could as well take a substitution instance of them. We would write $t_1\stackrel{r}{⟶}{t}_2$ for this.

Given a set $\mathcal{R}$ of rewrite rules, we write $t_1\stackrel{\mathcal{R}}{⟶}{t}_2$ if for some $r\in \mathcal{R}$, $t_1\stackrel{r}{⟶}{t}_2$. We naturally consider the transitive closure $\stackrel{{\mathcal{R}}^{\ast }}{⟶}$ of $\stackrel{\mathcal{R}}{⟶}$. We say that $t_1$ rewrites to $t_2$ via $\mathcal{R}$ if they stand in this relation $\stackrel{{\mathcal{R}}^{\ast }}{⟶}$.

We are mostly interested in the rewriting of ground terms. But we need the notion of variables to formulate this, and this is the only reason for introducing variables.

Now that we have made this preliminary discussion, we consider the term rewriting system $\mathcal{R}$ shown in Figure 5. We have numbered the rules, and we use this numbering in the sequel.

Remark 5.7. 

(r7${}_{\alpha }$) is an infinite scheme, and, in it, $\alpha$ is a term of sort a. But $\alpha$ need not be an action variable. (Indeed, the scheme is only interesting when $\alpha$ is a composition of actions of the form ${\sigma }_i\overrightarrow{\psi }$.) The right side of (r7${}_{\alpha }$) depends on $\alpha$, and this is why we use a scheme rather than a single rule. We need to explain what it means. First, the action terms of ${\mathcal{L}}_1^{+}(\mathbf{\Sigma },X)$ carry the structure of a frame by taking for each A the smallest relation $\stackrel{A}{⟶}$ such that the following two conditions hold:

1. 

If $i\stackrel{A}{⟶}j$ in $\mathbf{\Sigma }$, then ${\sigma }_i\overrightarrow{\psi }\stackrel{A}{⟶}{\sigma }_j\overrightarrow{\psi }$.

2. 

If $\alpha \stackrel{A}{⟶}{\alpha }^{\prime }$ and $\beta \stackrel{A}{⟶}{\beta }^{\prime }$, then $\alpha ;{\alpha }^{\prime }\stackrel{A}{⟶}\beta ;{\beta }^{\prime }$.

Moreover, we use the notation $\bigwedge \{{\square }_A\left[\beta \right]\phi :\alpha \stackrel{A}{⟶}\beta \}$ to stand for some fixed, but arbitrary, rendering of the conjunction as a nested list of binary conjuncts. The order will not matter, but we shall need an estimate of how many conjuncts there are.

We have a length function ℓ on action terms: $\mathcal{\ell }\left(x\right)=0$ for variables x, $\mathcal{\ell }\left({\sigma }_i\overrightarrow{\psi }\right)=1$, and $\mathcal{\ell }(\alpha ;\beta )=\mathcal{\ell }\left(\alpha \right)+\mathcal{\ell }\left(\beta \right)$. For each α, the number of β such that $\alpha \stackrel{A}{⟶}\beta$ is at most $n^{\mathcal{\ell }\left(\alpha \right)}$, where n is the size of Σ. This is easy to check by induction on $\mathcal{\ell }\left(\alpha \right)$.

Also on (r7${}_{\alpha }$): one is tempted to replace this infinite scheme by the finite one

$$\begin{array}{cccc}\left(r10\right)\hfill & \left[{\sigma }_i\overrightarrow{\psi }\right]{\square }_A\phi \hfill & ⇝& {\psi }_i\to \bigwedge \{{\square }_A\left[{\sigma }_j\overrightarrow{\psi }\right]\phi :i\stackrel{A}{⟶}j\}\hfill \end{array}$$

If one did this, one would have to reverse (r8) to read

$$\begin{array}{cccc}\left(r\mathit{11}\right)\hfill & [\alpha ;\beta ]\phi \hfill & ⇝& \left[\alpha \right]\left[\beta \right]\phi \hfill \end{array}$$

The reason is that (r10), above, only allows us to reduce expressions $\left[\alpha \right]{\square }_A\phi$ when α is of the form ${\sigma }_i\overrightarrow{\psi }$. The problem is that the normal forms of (r1)–(r6) + (r9) + (r10) + (r11) would include terms such as

$$\left[{\sigma }_1\overrightarrow{{\psi }^1}\right]\left[{\sigma }_2\overrightarrow{{\psi }^2}\right]\cdots \left[{\sigma }_k\overrightarrow{{\psi }^k}\right]{\square }_{\mathcal{C}}^{\ast }\phi ,$$

and these are not suitable for use in connection with the action rule. We will show about our system (r1)–(r9) that its normal forms includes terms such as

$$\left[(\cdots ({\sigma }_1\overrightarrow{{\psi }^1};{\sigma }_2\overrightarrow{{\psi }^2})\cdots {\sigma }_k\overrightarrow{{\psi }^k})\right]{\square }_{\mathcal{C}}^{\ast }\phi .$$

Again, this is mainly due to our choice in the direction of (r8).

5.2.2. Our Interpretation

An interpretation of a signature Δ is a $\Delta$ algebra. This is a carrier set for the sentences, a carrier set for the actions, and for each n-ary function symbol f of Δ a function of the appropriate sort. In our setting, both carrier sets will be $N_{\ge 3}$, the set of natural numbers which are at least 3. We shall use a, b, etc., to range over $N_{\ge 3}$ in this section. Our interpretation is shown in Figure 6. By recursion on terms $t(x_1,\dots ,x_k)$, we build an interpretation 7.

$$⟦t⟧(a_1,\dots ,a_k):{\left(N_{\ge 3}\right)}^k\to N_{\ge 3}.$$

The interpretation of each function symbol is strictly monotone in each argument. (For example, we check this for $⟦;⟧$. For fixed n and m, we consider the functions $\lambda a.n^{a+2}$ and $\lambda a.a^{m+2}$. Then, if $a<b$, $n^{a+2}<n^{b+2}$ and $a^{m+2}<b^{m+2}$.) So, by induction, each $⟦t⟧(a_1,\dots ,a_k)$ is strictly monotone as a function in each argument.

Lemma 5.8. 

Let $n=|\Sigma |$. For all action terms α, and all maps ι of variables to $N_{\ge 3}$,

$$⟦\alpha ⟧(\iota \left(x_1\right),\dots ,\iota \left(x_n\right))>n^{l\left(\alpha \right)}.$$

Proof. 

By induction on α. If α is a variable x, then $\mathcal{\ell }\left(\alpha \right)=0$. So $⟦\alpha ⟧\left(\iota \left(x\right)\right)=\iota \left(x\right)\ge 3>1=n^{\mathcal{\ell }\left(\alpha \right)}$. If α is a term of the form ${\sigma }_i\overrightarrow{\psi }$, then $\mathcal{\ell }\left(\alpha \right)=1$, and

$$\begin{array}{ccc}⟦{\sigma }_i{\psi }_1\cdots {\psi }_n⟧(\iota \left(x_1\right),\dots ,\iota \left(x_n\right))\hfill & =& ⟦{\psi }_1⟧(\iota \left(x_1\right),\dots ,\iota \left(x_n\right))+\cdots +⟦{\psi }_n⟧(\iota \left(x_1\right),\dots ,\iota \left(x_n\right))\hfill \\ & >& 3n\hfill \\ & >& n^{\mathcal{\ell }\left(\alpha \right)}\hfill \end{array}$$

Now assume our lemma for α and β.

$$\begin{array}{ccc}⟦\alpha ;\beta ⟧(\iota \left(x_1\right),\dots ,\iota \left(x_n\right))\hfill & =& {\left(⟦\alpha ⟧(\iota \left(x_1\right),\dots ,\iota \left(x_n\right))\right)}^{⟦\beta ⟧(\iota \left(x_1\right),\dots ,\iota \left(x_n\right))+1}\hfill \\ & >& n^{\mathcal{\ell }\left(\alpha \right);\left(n^{\mathcal{\ell }\left(\beta \right)+1}\right)}\hfill \\ & >& n^{\mathcal{\ell }\left(\alpha \right)+\mathcal{\ell }\left(\beta \right)}\mathrm{see}\mathrm{below}\hfill \\ & =& n^{\mathcal{\ell }(\alpha ;\beta )}\hfill \end{array}$$

In asserting that $\mathcal{\ell }\left(\alpha \right);n^{\mathcal{\ell }\left(\beta \right)}>\mathcal{\ell }\left(\alpha \right)+\mathcal{\ell }\left(\beta \right)$, we assume that $n>1$. If $n=1$, then our lemma is trivial. □

Proposition 5.9. 

If α is an action term of ${\mathcal{L}}_1^{+}(\mathbf{\Sigma })$ and $\alpha \stackrel{A}{⟶}\beta$, then $⟦\alpha ⟧$ and $⟦\beta ⟧$ are the same function. In particular, if α and β are ground action terms, then $⟦\alpha ⟧=⟦\beta ⟧$.

Proof. 

By induction on α. The point is that the interpretation of the actions ${\sigma }_i\overrightarrow{\psi }$ does not use the number i in any way. The rest follows by an easy induction. □

The following proposition is a technical but elementary result on exponentiation. It will be used in Lemma 5.11, below. One might notice that if we replace 3 by 2 in the statement, then some of the parts are no longer true. This is the reason why our overall interpretation uses $N_{\ge 3}$ rather than N or $N_{\ge 2}$.

Proposition 5.10. 

Let $a,b,c\ge 3$.

1. 

$2a^b>a+4$.

2. 

$a^{b+c}>a^b+a^c$.

3. 

$a^2>a+5$.

4. 

$a^{b+1}>3a+3$.

5. 

$a^b>(a+1)(b+1)$.

Lemma 5.11. 

For each of (r1)–(r9), the interpretation of the left side of the rule is strictly larger than the right side on all tuples of arguments in $N_{\ge 3}$.

Proof. 

We remind the reader that letters $a,b,c$, etc., denote elements of $N_{\ge 3}$. We use Proposition 5.10 without explicit mention.

(r1) $⟦x\to y⟧(a,b)=a+b+3>a+b+2=⟦\neg (x\wedge \neg y)⟧(a,b)$.

(r2) $⟦{\mathrm{P}}_{\mathrm{RE}}\left({\sigma }_i\overrightarrow{y}\right)⟧(a_1,\dots ,a_n)=⟦{\sigma }_i\overrightarrow{y}⟧(a_1,\dots ,a_n)\ge a_i+1>⟦y_i⟧(a_1,\dots ,a_n)$.

(r3)

$$\begin{array}{ccc}⟦{\mathrm{P}}_{\mathrm{RE}}(x;y)⟧(a,b)\hfill & =& a^{b+1}\hfill \\ & >& a+a^b\hfill \\ & =& ⟦{\mathrm{P}}_{\mathrm{RE}}\left(x\right)⟧(a,b)+⟦\left[x\right]{\mathrm{P}}_{\mathrm{RE}}\left(y\right)⟧(a,b)\hfill \\ & =& ⟦{\mathrm{P}}_{\mathrm{RE}}\left(x\right)\wedge \left[x\right]{\mathrm{P}}_{\mathrm{RE}}\left(y\right)⟧(a,b)\hfill \end{array}$$

(r4) $⟦\left[x\right]p⟧\left(a\right)=a^2>a+5=⟦{\mathrm{P}}_{\mathrm{RE}}\left(x\right)\to p⟧\left(a\right)$.

(r5)

$$\begin{array}{ccc}⟦\left[x\right]\neg y⟧(a,b)\hfill & =& a^{b+1}\hfill \\ & \ge & a^b+2a^b\hfill \\ & >& a+a^b+4\hfill \\ & =& a+⟦\left[x\right]y⟧(a,b)+4\hfill \\ & =& ⟦{\mathrm{P}}_{\mathrm{RE}}\left(x\right)\to \neg \left[x\right]y⟧(a,b)\hfill \end{array}$$

(r6) $⟦\left[x\right](y\wedge z)⟧(a,b,c)=a^{b+c}>a^b+a^c=⟦\left[x\right]y\wedge \left[x\right]z⟧(a,b,c)$.

(r7${}_{\alpha }$) Let $y_1,\dots ,y_n$ be the free variables of α. Fix $c_1,\dots ,c_n\in N_{\ge 3}$. Let $a=⟦\alpha ⟧(c_1,\dots ,c_n)$, and let $b\in N_{\ge 3}$ be arbitrary. Then

$$\begin{array}{ccc}⟦\left[\alpha \right]{\square }_{A}x⟧(c_1,\dots ,c_n,b)\hfill & =& a^{b+2}\hfill \\ & >& a^{b+1}+a^{b+1}\hfill \\ & >& a^{b+1}+3a+3\hfill \\ & =& a+a(2+a^b)+3\hfill \\ & >& a+n^{\mathcal{\ell }\left(a\right)}(2+a^b)+3\hfill \\ & \ge & ⟦{\mathrm{P}}_{\mathrm{RE}}\left(\alpha \right)\to \bigwedge \{{\square }_A\left[\beta \right]x:\alpha \stackrel{A}{⟶}\beta \}⟧(c_1,\dots ,c_n,b)\hfill \end{array}$$

Notice that we used Proposition 5.9 and our observation that the size of the conjunction on the right side of (r7${}_{\alpha }$) is at most $n^{\mathcal{\ell }\left(\alpha \right)}$.

(r8) $⟦\left[x\right]\left[y\right]z⟧(a,b,c)=a^{b^c}>a^{(b+1)c}={\left(a^{b+1}\right)}^c=⟦[x;y]z⟧(a,b,c)$.

(r9) $⟦x;(y;z)⟧(a,b,c)=a^{b^{c+1}+1}>a^{(b+1)(c+1)}={\left(a^{b+1}\right)}^{c+1}=⟦(x;y);z⟧(a,b,c)$. □

Definition 5.12. 

Let $\phi$ and $\psi$ be sentences in ${\mathcal{L}}_1(\mathbf{\Sigma })$. We regard these as ground terms in ${\mathcal{L}}_1^{+}(\mathbf{\Sigma })$. We write $\phi >\psi$ if $⟦\phi ⟧>⟦\psi ⟧$, where our interpretation is the one in Figure 6. We write $\phi <\psi$ if $\phi \le \psi$ to mean the obvious things.

Theorem 5.13. 

$\mathcal{R}$ is terminating: there are no infinite sequences

$$t_1\stackrel{\mathcal{R}}{⟶}{t}_2\stackrel{\mathcal{R}}{⟶}\cdots \stackrel{\mathcal{R}}{⟶}{t}_n\stackrel{\mathcal{R}}{⟶}{t}_{n+1}\cdots$$

Proof. 

We recall a standard argument. Assume we had a counter example, an infinite sequence of rewrites. We may assume without loss of generality that each $t_i$ is a ground term. Recall Lemma 5.11 and our observation that each $⟦t⟧(x_1,\dots ,x_k)$ is strictly monotone as a function in each argument. From this, it follows that $⟦t_1⟧>⟦t_2⟧>\cdots$, and these are all numbers. So we have a contradiction. □

5.2.3. Normal Forms

We remind the reader that we formulated the notions of equivalences of simple actions and also equivalence of sentences of ${\mathcal{L}}_1(\mathbf{\Sigma })$ in Section 4.3. We consider now a translation $\mathsf{trans}:{\mathcal{L}}_1^{+}(\mathbf{\Sigma })\to {\mathcal{L}}_1(\mathbf{\Sigma })$. The definition is by recursion on the well-order <. We take $\mathsf{trans}$ to be a homomorphism for all symbols except ${\mathrm{P}}_{\mathrm{RE}}$. For this, we require the following:

$$\begin{array}{ccc}\mathsf{trans}\left({\mathrm{P}}_{\mathrm{RE}}({\sigma }_i{\psi }_1,\dots ,{\psi }_n)\right)\hfill & =& \mathsf{trans}\left({\psi }_i\right)\hfill \\ \mathsf{trans}\left({\mathrm{P}}_{\mathrm{RE}}\right(\alpha ;\beta \left)\right)\hfill & =& \langle \mathsf{trans}\left(\alpha \right)\rangle \mathsf{trans}\left({\mathrm{P}}_{\mathrm{RE}}\right(\beta \left)\right)\hfill \\ & =& \neg \left[\mathsf{trans}\right(\alpha \left)\right]\neg \mathsf{trans}\left({\mathrm{P}}_{\mathrm{RE}}\right(\beta \left)\right)\hfill \end{array}$$

The reason we need recursion on < is that $\mathsf{trans}\left({\mathrm{P}}_{\mathrm{RE}}\right(\beta \left)\right)$ figures in $\mathsf{trans}\left({\mathrm{P}}_{\mathrm{RE}}\right(\alpha ;\beta \left)\right)$. So we need to know that ${\mathrm{P}}_{\mathrm{RE}}\left(\beta \right)<{\mathrm{P}}_{\mathrm{RE}}(\alpha ;\beta )$. Of course, we do not really need the specific < that we constructed for this; for this minor point, we might as well define $\phi <\psi$ if φ has fewer symbols than ψ.

Lemma 5.14. 

For all action terms α, $\mathsf{trans}\left({\mathrm{P}}_{\mathrm{RE}}\right(\alpha \left)\right)={\mathrm{P}}_{\mathrm{RE}}\left(\mathsf{trans}\right(\alpha \left)\right)$.

Proof. 

By induction on <. The important thing again is that when we write ${\mathrm{P}}_{\mathrm{RE}}\left(\mathsf{trans}\right(\alpha \left)\right)$ we are using ${\mathrm{P}}_{\mathrm{RE}}$ here as a defined symbol. Its recursion equations match the definition of $\mathsf{trans}$. □

Lemma 5.15. 

Let α be a ground action term of ${\mathcal{L}}_1^{+}(\mathbf{\Sigma })$. Then,

$$\{\mathsf{trans}\left(\beta \right):\alpha \stackrel{A}{⟶}\beta in{\mathcal{L}}_1^{+}(\Sigma )\}=\{\beta :\mathsf{trans}\left(\alpha \right)\stackrel{A}{⟶}\beta in{\mathcal{L}}_1(\Sigma )\}.$$

Proof. 

By induction on α. □

Lemma 5.16. 

If $t_1$ and $t_2$ are ground terms of ${\mathcal{L}}_1^{+}(\mathbf{\Sigma })$ such that $t_1\stackrel{\mathcal{R}}{⟶}{t}_2$, then $\mathsf{trans}\left(t_1\right)\equiv \mathsf{trans}\left(t_2\right)$.

Proof. 

Let u be a term with exactly one free variable x, and let σ be such that for some i, $t_1=u(x\leftarrow l^{\sigma })$ and $t_2=u(x\leftarrow r^{\sigma })$. We argue by induction on u. If u is just x, then we examine the rules of the system. All of them pertain to sentences except for (r9), and in the case of (r9) we use Lemma 4.20, part (4). The arguments for the other rules use Lemma 5.14, and we will give the details for two of them, (r3) and (r7).

For (r3),

$$\begin{array}{cccc}\mathsf{trans}\left({\mathrm{P}}_{\mathrm{RE}}\right(\alpha ;\beta \left)\right)\hfill & \equiv & \langle \mathsf{trans}\left(\alpha \right)\rangle \mathsf{trans}\left({\mathrm{P}}_{\mathrm{RE}}\right(\beta \left)\right)\hfill & \mathrm{definition} \mathrm{of} \mathsf{trans}\hfill \\ & \equiv & {\mathrm{P}}_{\mathrm{RE}}\left(\mathsf{trans}\right(\alpha \left)\right)\wedge \left[\mathsf{trans}\right(\alpha \left)\mathsf{trans}\right({\mathrm{P}}_{\mathrm{RE}}\left(\beta \right))\hfill & \mathrm{by} \mathrm{Lemma} 4.16\hfill \\ & \equiv & \mathsf{trans}\left({\mathrm{P}}_{\mathrm{RE}}\right(\alpha \left)\right)\wedge \left[\mathsf{trans}\right(\alpha \left)\right]\mathsf{trans}\left({\mathrm{P}}_{\mathrm{RE}}\right(\beta \left)\right)\hfill & \mathrm{using} \mathrm{Lemma} 5.14\hfill \\ & \equiv & \mathsf{trans}\left({\mathrm{P}}_{\mathrm{RE}}\right(\alpha )\wedge [\alpha \left]{\mathrm{P}}_{\mathrm{RE}}\right(\beta \left)\right)\hfill \end{array}$$

The infinite scheme (r7${}_{\alpha }$) is repeated below:

$$\left(\mathrm{r}{7}_{\alpha }\right)\left[\alpha \right]{\square }_{A}x⇝{\mathrm{P}}_{\mathrm{RE}}\left(\alpha \right)\to \bigwedge \{{\square }_A\left[\beta \right]x:\alpha \stackrel{A}{⟶}\beta \}.$$

Recall that α might have variables. What we need to check here is that ground instances of (r7${}_{\alpha }$) have equivalent translations. So take a ground sentence of the form $\left[\alpha \right]{\square }_A\phi$. Its translation is $\left[\mathsf{trans}\left(\alpha \right)\right]{\square }_A\left(\mathsf{trans}\left(\phi \right)\right)$. Using the Action-Knowledge Axiom and Lemmas 5.15 and 5.14:

$$\begin{array}{ccc}\left[\mathsf{trans}\left(\alpha \right)\right]{\square }_A\left(\mathsf{trans}\left(\phi \right)\right)\hfill & \equiv & {\mathrm{P}}_{\mathrm{RE}}\left(\mathsf{trans}\left(\alpha \right)\right)\to {\square }_A\bigwedge \{\left[\beta \right]\mathsf{trans}\left(\phi \right):\mathsf{trans}\left(\alpha \right)\stackrel{A}{⟶}\beta \}\hfill \\ & \equiv & \mathsf{trans}\left({\mathrm{P}}_{\mathrm{RE}}\left(\alpha \right)\right)\to \bigwedge \{{\square }_A\left[\mathsf{trans}\left(\beta \right)\right]\mathsf{trans}\left(\phi \right):\alpha \stackrel{A}{⟶}\beta \})\hfill \\ & \equiv & \mathsf{trans}\left({\mathrm{P}}_{\mathrm{RE}}\left(\alpha \right)\to \bigwedge \{{\square }_A\left[\beta \right]\phi :\alpha \stackrel{A}{⟶}\beta \}\right)\hfill \end{array}$$

This settles all of the cases in this lemma when u is a variable by itself. In the general case, we need a fact about substitutions. Let t be any term of ${\mathcal{L}}^{+}(\mathbf{\Sigma },X)$. Let σ and τ be two ground substitutions (these are substitutions all of whose values contain no variables) such that $\mathsf{trans}\left(\sigma \right(x\left)\right)$ and $\mathsf{trans}\left(\tau \right(x\left)\right)$ are equivalent (actions or sentences) for all variables x. Then, $\mathsf{trans}\left(t^{\sigma }\right)$ and $\mathsf{trans}\left(t^{\tau }\right)$ are again equivalent. The argument here is an easy induction on terms of ${\mathcal{L}}^{+}(\mathbf{\Sigma },X)$. It amounts to several facts which we have seen before: ≡ is a congruence for all of the syntactic operations on sentences, and also for those on programs (see Lemma 4.20); equivalent actions have equivalent preconditions (by definition); and if $\alpha \equiv \beta$, then $\left[\alpha \right]\phi \equiv \left[\beta \right]\phi$ (Lemma 4.22). □

A normal form in a rewriting system is a term which cannot be rewritten in the system. In a terminating system such as our $\mathcal{R}$, one may define a normal form for a term by rewriting as much as possible in some fixed way (for example, by always rewriting in the leftmost possible way). We shall need some information on the normal forms of $\mathcal{R}$, and we shall turn to this shortly.

Near the beginning of Section 5, we defined a set $\mathcal{NF}\subseteq {\mathcal{L}}_1(\mathbf{\Sigma })$. $\mathcal{NF}$ is the smallest set containing the atomic propositions and closed under all the boolean and modal operators; with the property that if α and φ belong to $\mathcal{NF}$, then so does $\left[\alpha \right]{\square }_{\mathcal{C}}^{\ast }\phi$ for all $\mathcal{C}\subseteq \mathcal{A}$; and, finally, that the programs built from sentences in $\mathcal{NF}$ are themselves in $\mathcal{NF}$ (see also (14) for a more complete description of this last closure condition.)

Lemma 5.17. 

A ground term $t\in {\mathcal{L}}_1^{+}(\mathbf{\Sigma })$ is a normal form of $\mathcal{R}$ if $t\in \mathcal{NF}$. In particular, ${\mathrm{P}}_{\mathrm{RE}}$ and → do not occur in normal forms.

Proof. 

An induction on $\mathcal{NF}\subseteq {\mathcal{L}}_1(\mathbf{\Sigma })$ shows that all sentences in $\mathcal{NF}$ are ground terms of ${\mathcal{L}}_1^{+}(\mathbf{\Sigma })$ and are, moreover, normal forms of the rewriting system $\mathcal{R}$: no rules of $\mathcal{R}$ can apply at any point. Going the other way, we show by induction on ${\mathcal{L}}_1^{+}(\mathbf{\Sigma })$ that if t is a (ground) normal form, then (regarding t as a sentence or action in ${\mathcal{L}}_1(\mathbf{\Sigma })$) $\phi \in \mathcal{NF}$. The base case and the induction steps for ¬, ∧, ${\square }_A$, and ${\square }_{\mathcal{B}}^{\ast }$ are all easy. Suppose our result holds for φ, and consider a normal form $\left[\alpha \right]\phi$. Then, α must be an action of the form $\left[{\sigma }_i\overrightarrow{\psi }\right]$ with all ${\psi }_j$ in normal form; if not, some rule would apply to α and, hence, to $\left[\alpha \right]\phi$. We are left to consider an action α. By induction hypothesis, the subsentences of α, too, are normal forms and, hence, belong to $\mathcal{NF}$. We claim that α must be of the right-branching form in Equation (14). This is because all of the other possibilities are reducible in the system using (r9). □

Lemma 5.18. 

A sentence $\phi \in {\mathcal{L}}_0(\mathbf{\Sigma })$ is a normal form of $\mathcal{R}$ if φ is a modal sentence (that is, if φ contains no actions).

Proof. 

By the easy part of Lemma 5.17, the modal sentences are normal forms. In the more significant direction, one first checks by induction on rewrite sequences that if $\phi \in {\mathcal{L}}_0(\mathbf{\Sigma })$ and ${\phi }^{\prime }$ is reachable from φ by a finite number of rewrites in $\mathcal{R}$, then ${\square }^{\ast }$ does not appear in ${\phi }^{\prime }$. So every normal form of φ is a purely modal sentence. It follows that if φ were a normal form to begin with, then φ would be a modal sentence. □

Corollary 5.19. 

For every $\phi \in {\mathcal{L}}_1(\mathbf{\Sigma })$, there is a normal form $\mathit{nf}\left(\phi \right)$ such that $⊢\phi \leftrightarrow \mathit{nf}\left(\phi \right)$. Moreover, $\mathit{nf}\left(\phi \right)\le \phi$.

Proof. 

Regard φ as a term in ${\mathcal{L}}_1^{+}(\mathbf{\Sigma })$. Let

$$\phi ={\phi }_1⇝{\phi }_2⇝\cdots ⇝{\phi }_n=\mathit{nf}\left(\phi \right)$$

be some sequence of rewrites which leads to a normal form of φ 8. By Lemma 5.16, $⊢\mathsf{trans}\left(\phi \right)\leftrightarrow \mathsf{trans}\left(\mathit{nf}\right(\phi \left)\right)$. But neither φ nor $\mathit{nf}\left(\phi \right)$ contain ${\mathrm{P}}_{\mathrm{RE}}$ or →, so they are literally equal to their translations. Thus, $⊢\phi \leftrightarrow \mathit{nf}\left(\phi \right)$, just as desired. □

Lemma 5.20. 

For all φ and α of ${\mathcal{L}}_1^{+}(\mathbf{\Sigma })$:

1. 

${\mathrm{P}}_{\mathrm{RE}}\left(\alpha \right)<\left[\alpha \right]\phi$.

2. 

If $\alpha \stackrel{A}{⟶}\beta$, then $\left[\beta \right]\phi <\neg \left[\beta \right]\phi <\left[\alpha \right]{\square }_{\mathcal{C}}^{\ast }\phi$.

3. 

If $\left[\alpha \right]{\square }_{\mathcal{C}}^{\ast }\psi$ is a normal form sentence and $\alpha \stackrel{A}{⟶}\beta$, then ${\square }_A\left[\beta \right]{\square }_{\mathcal{C}}^{\ast }\psi$ and $\left[\beta \right]{\square }_{\mathcal{C}}^{\ast }\psi$ are again normal forms.

4. 

Every subterm of a normal form is a normal form.

5. 

If α is a normal-form action and $\alpha \stackrel{A}{⟶}\beta$, then β is a normal-form action as well.

Proof. 

Part (1) is an easy calculation. In part (2), we use the fact that $⟦\alpha ⟧$ and $⟦\beta ⟧$ are the same number, by Proposition 5.9. We use the fact here (and here only) that $⟦{\square }^{\ast }⟧\left(a\right)=a+1$ rather than $⟦{\square }^{\ast }⟧\left(a\right)=a$. The remaining parts are also easy using the characterization of normal forms of Lemma 5.17. □

5.2.4. The Function $f\left(\phi \right)$

The last piece of business in this section is to define the function $f\left(\phi \right)$ from Lemma 5.4 and then to prove the required properties.

Definition 5.21. 

For t, an action or a sentence, let $s\left(t\right)$ be the set of subsentences of t, including t itself (if t is a sentence). This includes all sentences occurring in actions which occur in $\phi$ and their subsentences. We define a function $f:\mathcal{NF}\to \mathcal{P}\left(\mathcal{NF}\right)$ by recursion on the well-founded relation < as follows:

$$\begin{array}{cccc}f\left(p\right)\hfill & =& & \left\{p\right\}\hfill \\ f(\neg \phi )\hfill & =& & f\left(\phi \right)\cup \{\neg \phi \}\hfill \\ f(\phi \wedge \psi )\hfill & =& & f\left(\phi \right)\cup f\left(\psi \right)\cup \{\phi \wedge \psi \}\hfill \\ f\left({\square }_A\phi \right)\hfill & =& & f\left(\phi \right)\cup \left\{{\square }_A\phi \right\}\hfill \\ f\left({\square }_{\mathcal{B}}^{\ast }\phi \right)\hfill & =& & f\left(\phi \right)\cup \left\{{\square }_{\mathcal{B}}^{\ast }\phi \right\}\cup \{{\square }_A{\square }_{\mathcal{B}}^{\ast }\phi :A\in \mathcal{B}\}\hfill \\ f\left(\left[\alpha \right]{\square }_{\mathcal{C}}^{\ast }\phi \right)\hfill & =& \bigcup \hfill & \{s\left({\square }_A\left[\beta \right]{\square }_{\mathcal{C}}^{\ast }\phi \right):\alpha \stackrel{{\mathcal{C}}^{\ast }}{⟶}\beta \&A\in \mathcal{C}\}\hfill \\ & & \cup \hfill & \bigcup \{f\left(\psi \right):(\exists \beta )\alpha \stackrel{{\mathcal{C}}^{\ast }}{⟶}\beta \&\psi \in s\left(\beta \right)\}\hfill \\ & & \cup \hfill & \bigcup \{f\left(\mathit{nf}\left({\mathrm{P}}_{\mathrm{RE}}\left(\beta \right)\right)\right):\alpha \stackrel{{\mathcal{C}}^{\ast }}{⟶}\beta \}\hfill \\ & & \cup \hfill & f\left({\square }_{\mathcal{C}}^{\ast }\phi \right)\hfill \\ & & \cup \hfill & \bigcup \{f\left(\mathit{nf}\left(\left[\beta \right]\phi \right)\right):\alpha \stackrel{{\mathcal{C}}^{\ast }}{⟶}\beta \}\hfill \end{array}$$

The definition makes sense because the calls to f on the right-hand sides are all smaller than the arguments on the left-hand sides; see Lemma 5.20.)

Lemma 5.22. 

For all $\phi \in \mathcal{NF}$:

1. 

$\phi \in f\left(\phi \right)$.

2. 

$f\left(\phi \right)$ is a finite set of normal form sentences.

3. 

If $\psi \in f\left(\phi \right)$, then $s\left(\psi \right)\subseteq f\left(\phi \right)$.

4. 

If $\psi \in f\left(\phi \right)$, then $f\left(\psi \right)\subseteq f\left(\phi \right)$.

5. 

If $\left[\gamma \right]{\square }_{\mathcal{C}}^{\ast }\chi \in f\left(\phi \right)$, $\gamma \stackrel{{\mathcal{C}}^{\ast }}{⟶}\delta$, and $A\in \mathcal{C}$, then $f\left(\phi \right)$ also contains ${\square }_A\left[\delta \right]{\square }_{\mathcal{C}}^{\ast }\chi$, $\left[\delta \right]{\square }_{\mathcal{C}}^{\ast }\chi$, $\mathit{nf}\left({\mathrm{P}}_{\mathrm{RE}}\right(\delta \left)\right)$, and $\mathit{nf}\left(\right[\delta \left]\chi \right)$.

Proof. 

Part (1) is by cases on φ. The only interesting case is for $\left[\alpha \right]{\square }_{\mathcal{C}}^{\ast }\phi$, and this is a subsentence of ${\square }_A\left[\alpha \right]{\square }_{\mathcal{C}}^{\ast }\phi$ for any $A\in \mathcal{C}$.

All of other the parts are by induction on φ in the well-ordered <. For part (2), we use Lemma 5.20.

In part (3), we argue by induction on normal forms.

The result is immediate when φ is an atomic sentence p, and the induction steps for ¬, ∧, and ${\square }_A$ are easy. For ${\square }_{\mathcal{B}}^{\ast }\phi$, note that since $\phi <{\square }_{\mathcal{B}}^{\ast }\phi$, our induction hypothesis implies the result for φ; we verify it for ${\square }_{\mathcal{B}}^{\ast }\phi$. When ψ is ${\square }_{\mathcal{B}}^{\ast }\phi$, then

$$s\left(\psi \right)=s\left(\phi \right)\cup \left\{{\square }_{\mathcal{B}}^{\ast }\phi \right\}\subseteq f\left(\phi \right)\cup \left\{{\square }_{\mathcal{B}}^{\ast }\phi \right\}\subseteq f\left({\square }_{\mathcal{B}}^{\ast }\phi \right).$$

And then, when ψ is ${\square }_A{\square }_{\mathcal{B}}^{\ast }\phi$ for some $A\in \mathcal{B}$, we have

$$s\left(\psi \right)=s\left({\square }_{\mathcal{B}}^{\ast }\phi \right)\cup \left\{{\square }_A{\square }_{\mathcal{B}}^{\ast }\phi \right\}\subseteq f\left({\square }_{\mathcal{B}}^{\ast }\phi \right).$$

To complete part (3), we consider $\left[\alpha \right]{\square }_{\mathcal{C}}^{\ast }\phi$. If there is some $\chi <\left[\alpha \right]{\square }_{\mathcal{C}}^{\ast }\phi$ such that $\psi \in f\left(\chi \right)$ and $f\left(\chi \right)\subseteq f\left(\left[\alpha \right]{\square }_{\mathcal{C}}^{\ast }\phi \right)$, then we argue as follows: by induction hypothesis, $s\left(\psi \right)\subseteq f\left(\chi \right)$; and by hypothesis $f\left(\chi \right)\subseteq f\left(\left[\alpha \right]{\square }_{\mathcal{C}}^{\ast }\phi \right)$. This covers all of the cases except for ψ a subsentence of ${\square }_A\left[\beta \right]{\square }_{\mathcal{C}}^{\ast }\phi$. And here, $s\left(\psi \right)\subseteq s\left({\square }_A\left[\beta \right]{\square }_{\mathcal{C}}^{\ast }\phi \right)\subseteq f\left(\left[\alpha \right]{\square }_{\mathcal{C}}^{\ast }\phi \right)$.

In Part (4), we again argue by induction on normal forms. The result is immediate when φ is an atomic sentence p. The induction steps for ¬, ∧, and ${\square }_A$ are easy. For ${\square }_{\mathcal{B}}^{\ast }\phi$, note that since $\phi <{\square }_{\mathcal{B}}^{\ast }\phi$, our induction hypothesis implies the result for φ; we verify it for ${\square }_{\mathcal{B}}^{\ast }\phi$. The only interesting case is when ψ is ${\square }_A{\square }_{\mathcal{B}}^{\ast }\phi$ for some $A\in \mathcal{B}$. And in this case

$$f\left(\psi \right)=f\left({\square }_{\mathcal{B}}^{\ast }\phi \right)\cup \left\{{\square }_A{\square }_{\mathcal{B}}^{\ast }\phi \right\}\subseteq f\left({\square }_{\mathcal{B}}^{\ast }\phi \right).$$

To complete part (4), we consider $\left[\alpha \right]{\square }_{\mathcal{C}}^{\ast }\phi$. If there is some $\chi <\left[\alpha \right]{\square }_{\mathcal{C}}^{\ast }\phi$ such that $\psi \in f\left(\chi \right)$ and $f\left(\chi \right)\subseteq f\left(\left[\alpha \right]{\square }_{\mathcal{C}}^{\ast }\phi \right)$, then we are easily done by the induction hypothesis. This covers all of the cases except for ψ of the form $\left[\beta \right]{\square }_{\mathcal{C}}^{\ast }\phi$ or of the form ${\square }_A\left[\beta \right]{\square }_{\mathcal{C}}^{\ast }\phi$. (If ψ is a subsentence of some β, then $f\left(\psi \right)\subseteq f\left(\left[\alpha \right]{\square }_{\mathcal{C}}^{\ast }\phi \right)$ directly. If ψ is a subsentence of ${\square }_{\mathcal{C}}^{\ast }\phi$, then by induction hypothesis, $f\left(\psi \right)\subseteq f\left({\square }_{\mathcal{C}}^{\ast }\phi \right)$; and directly, $f\left({\square }_{\mathcal{C}}^{\ast }\phi \right)\subseteq f\left(\left[\alpha \right]{\square }_{\mathcal{C}}^{\ast }\phi \right)$.) For $\left[\beta \right]{\square }_{\mathcal{C}}^{\ast }\phi$, we use the transitivity of $\stackrel{{\mathcal{C}}^{\ast }}{⟶}$ to check that $f\left(\left[\beta \right]{\square }_{\mathcal{C}}^{\ast }\phi \right)\subseteq f\left(\left[\alpha \right]{\square }_{\mathcal{C}}^{\ast }\phi \right)$. And now the case of ${\square }_A\left[\beta \right]{\square }_{\mathcal{C}}^{\ast }\phi$ follows:

$$f\left({\square }_A\left[\beta \right]{\square }_{\mathcal{C}}^{\ast }\phi \right)=f\left(\left[\beta \right]{\square }_{\mathcal{C}}^{\ast }\phi \right)\cup \left\{{\square }_A\left[\beta \right]{\square }_{\mathcal{C}}^{\ast }\phi \right\}\subseteq f\left(\left[\alpha \right]{\square }_{\mathcal{C}}^{\ast }\phi \right).$$

For part (5), assume that $\left[\gamma \right]{\square }_{\mathcal{C}}^{\ast }\chi \in f\left(\phi \right)$. By part (2), $\left[\gamma \right]{\square }_{\mathcal{C}}^{\ast }\chi$ is a normal form. The definition of f implies that ${\square }_A\left[\delta \right]{\square }_{\mathcal{C}}^{\ast }\chi$, $\left[\delta \right]{\square }_{\mathcal{C}}^{\ast }\chi$, $\mathit{nf}\left({\mathrm{P}}_{\mathrm{RE}}\right(\delta \left)\right)$, and $\mathit{nf}\left(\right[\delta \left]\chi \right)$ all belong to $f\left(\left[\gamma \right]{\square }_{\mathcal{C}}^{\ast }\chi \right)$, and then part (4) tells us that $f\left(\left[\gamma \right]{\square }_{\mathcal{C}}^{\ast }\chi \right)\subseteq f\left(\phi \right)$. □

5.2.5. Summary

The purpose of this section was to prove Lemmas 5.2–5.4 in Section 5. Lemma 5.2 is Corollary 5.19. Lemma 5.3 comes from Corollary 5.19 and Lemma 5.20. Lemma 5.4 is contained in Lemma 5.22.

5.3. Strong Completeness for ${\mathcal{L}}_0(\mathbf{\Sigma })$

Recall that in the languages ${\mathcal{L}}_0(\mathbf{\Sigma })$, we do not have the common-knowledge operators ${\square }_{\mathcal{B}}^{\ast }$ or the action iterations ${\pi }^{\ast }$. At this point, we can put together several results from our previous work to obtain a completeness theorem for languages of the form ${\mathcal{L}}_0(\mathbf{\Sigma })$. The overall ideas are: (1) we need a logical system which is strong enough to translate each sentence of ${\mathcal{L}}_0(\mathbf{\Sigma })$ to a normal form; (2) this normal form will be a purely modal sentence; and (3) the system should be at least as strong as multimodal K.

Proposition 5.23. 

Every sentence φ of ${\mathcal{L}}_0(\mathbf{\Sigma })$ is provably equivalent to a sentence ${\phi }^{\ast }$ in which there are no occurrences of ⊔, $\mathrm{crash}$, ;, or $\mathrm{skip}$.

Theorem 5.24. 

The logical system for ${\mathcal{L}}_0(\mathbf{\Sigma })$ is strongly complete: for all sets $T\subseteq {\mathcal{L}}_0(\mathbf{\Sigma })$, $T⊢\phi$ iff $T\vDash \phi$.

Proof. 

The soundness half being easy, we only need to show that if $T\vDash \phi$, then $T⊢\phi$.

First, we may assume that the symbols ⊔, $crash$, ;, and $skip$ do not occur in T or φ. Thus, we may work with ${\mathcal{L}}_0(\mathbf{\Sigma })\cap {\mathcal{L}}_1^{+}(\mathbf{\Sigma })$. In particular, we have normal forms.

Next, for each χ of ${\mathcal{L}}_0(\mathbf{\Sigma })$, $⊢\chi \leftrightarrow \mathit{nf}\left(\chi \right)$. As a result, $T⊢\mathit{nf}\left(\chi \right)$ for all $\chi \in T$.

Finally, write $\mathit{nf}\left(T\right)$ for $\left\{\mathit{nf}\right(\chi ):\chi \in T\}$. By soundness, $\mathit{nf}\left(T\right)\vDash \mathit{nf}\left(\phi \right)$. Since our system extends the standard complete proof system of modal logic, $\mathit{nf}\left(T\right)⊢\mathit{nf}\left(\phi \right)$. So $T⊢\mathit{nf}\left(\phi \right)$. As we know, $⊢\phi \leftrightarrow \mathit{nf}\left(\phi \right)$. So we have our desired conclusion: $T⊢\phi$. □

5.4. Weak Completeness for ${\mathcal{L}}_1(\mathbf{\Sigma })$

The proof of completeness and decidability of ${\mathcal{L}}_1(\mathbf{\Sigma })$ is based on the filtration argument for completeness of PDL due to Kozen and Parikh [15]. We show that every consistent φ has a finite model, and that the size of the model is recursive in φ. As in the last section, we depend on the results of Lemmas 5.2–5.4.

The Set $\Delta =\Delta \left(\phi \right)$

Fix a sentence φ. We set $\Delta =f\left(\phi \right)$ (i.e., we drop φ from the notation). This set Δ is the version for our logic of the Fischer–Ladner closure of φ, originating in [17]. Let $\Delta =\{{\psi }_1,\dots ,{\psi }_n\}$. Given a maximal consistent set U of ${\mathcal{L}}_1(\mathbf{\Sigma })$, let

$$U^{\ast }=\underline{+}{\psi }_1\wedge \cdots \wedge \underline{+}{\psi }_n,$$

where the signs are taken in accordance with membership in U. That is, if ${\psi }_i\in U$, then ψ is a conjunct of $U^{\ast }$; but if ${\psi }_i\notin U$, then $\neg {\psi }_i$ is a conjunct.

Two (standard) observations are in order. Notice that if $U^{\ast }\ne V^{\ast }$, then $U^{\ast }\wedge V^{\ast }$ is inconsistent. Also, for all $\psi \in \Delta$,

$$⊢\psi \leftrightarrow \bigvee \{W^{\ast }:W\mathrm{is}\mathrm{maximal}\mathrm{consistent}\mathrm{and}\psi \in W\}.$$

(15)

and

$$⊢\neg \psi \leftrightarrow \bigvee \{W^{\ast }:W\mathrm{is}\mathrm{maximal}\mathrm{consistent}\mathrm{and}\neg \psi \in W\}.$$

(16)

(The reason is that ψ is equivalent to the disjunction of all complete conjunctions which contain it. However, some of those complete conjunctions are inconsistent and these can be dropped from the big disjunction. The others are consistent and, hence, can be extended to maximal consistent sets.)

Definition 5.25. 

We consider maximal consistent sets U in the logic for ${\mathcal{L}}_1(\mathbf{\Sigma })$. Let $U\equiv V$ if $U^{\ast }=V^{\ast }$ (if $U\cap \Delta =V\cap \Delta$). The filtration $\mathcal{F}$ is the model whose worlds are the equivalence classes $\left[U\right]$ in this relation. Furthermore, we set

$$\left[U\right]\stackrel{A}{⟶}\left[V\right]in\mathcal{F}iffwhenever{\square }_A\psi \in U\cap \Delta ,thenalso\psi \in V.$$

(17)

We complete the specification of a state model with the valuation:

$${\parallel p\parallel }_{\mathcal{F}}=\{\left[U\right]:p\in U\cap \Delta \}.$$

(18)

The definitions in Equations (18) and (17) are independent of the choice of representatives: we use part (1) of Lemma 5.4 to see that if ${\square }_A\chi \in \Delta$, then also $\chi \in \Delta$.

Proposition 5.26. 

If $U^{\ast }\wedge {\diamond }_A{V}^{\ast }$ is consistent, then $\left[U\right]{\to }_A\left[V\right]$.

Proof. 

Assume ${\square }_A\psi \in U\cap \Delta$ and toward a contradiction that $\psi \notin V$. Since $\psi \in \Delta$ and $\neg \psi \in V$, we have $⊢V^{\ast }\to \neg \psi$. Thus, $⊢{\diamond }_A{V}^{\ast }\to {\diamond }_A\neg \psi$, and so $⊢U^{\ast }\wedge {\diamond }_A{V}^{\ast }\to {\square }_A\psi \wedge {\diamond }_A\neg \psi$. Hence $U^{\ast }\wedge {\diamond }_A{V}^{\ast }$ is inconsistent. □

Definition 5.27. 

Let $\langle \alpha \rangle {\diamond }_{\mathcal{C}}^{\ast }\psi$ be a normal form. A good path from $\left[V_0\right]$ for $\langle \alpha \rangle {\diamond }_{\mathcal{C}}^{\ast }\psi$ is a path in $\mathcal{F}$

$$\left[V_0\right]{\to }_{A_1}\left[V_1\right]{\to }_{A_2}\cdots {\to }_{A_{k-1}}\left[V_{k-1}\right]{\to }_{A_k}\left[V_k\right]$$

(19)

such that $k\ge 0$, each $A_i\in \mathcal{C}$, and such that there exist actions

$$\alpha ={\alpha }_0{\to }_{A_1}{\alpha }_1{\to }_{A_2}\cdots {\to }_{A_{k-1}}{\alpha }_{k-1}{\to }_{A_k}{\alpha }_k$$

such that ${\mathrm{P}}_{\mathrm{RE}}\left({\alpha }_i\right)\in V_i$ for all $0\le i\le k$, and $\langle {\alpha }_k\rangle \psi \in V_k$.

The idea behind a good path comes from considering Lemma 4.11 in $\mathcal{F}$. Of course, the special case of that result would require that $\langle \mathcal{F},\left[V_i\right]\rangle \vDash {\mathrm{P}}_{\mathrm{RE}}\left({\alpha }_i\right)$ rather than ${\mathrm{P}}_{\mathrm{RE}}\left({\alpha }_i\right)\in V_i$, and similarly for $\langle {\alpha }_k\rangle \psi$ and $V_k$. The exact formulation above was made in order that the Truth Lemma will go through for sentences of the form $\langle \alpha \rangle {\diamond }_{\mathcal{C}}^{\ast }\psi$ (see the final paragraphs of the proof of Lemma 5.30).

Lemma 5.28. 

Let $\left[\alpha \right]{\square }_{\mathcal{C}}^{\ast }\psi \in \Delta$. If there is a good path from $\left[V_0\right]$ for $\langle \alpha \rangle {\diamond }_{\mathcal{C}}^{\ast }\neg \psi$, then $\langle \alpha \rangle {\diamond }_{\mathcal{C}}^{\ast }\neg \psi \in V_0$.

Proof. 

By induction on the length k of the path. If $k=0$, then $\langle \alpha \rangle \neg \psi \in V_0$. If $\langle \alpha \rangle {\diamond }_{\mathcal{C}}^{\ast }\neg \psi \notin V_0$, then $\left[\alpha \right]{\square }_{\mathcal{C}}^{\ast }\psi \in V_0$. By Lemma 5.4, part (2), we have $\mathit{nf}\left(\left[\alpha \right]\psi \right)\in V_0$. This is a contradiction.

Assume the result for k, and suppose that there is a good path from $\left[V_0\right]$ for $\langle \alpha \rangle {\diamond }_{\mathcal{C}}^{\ast }\neg \psi$ of length $k+1$. We adopt the notation from (19) for this good path. Then there is a good path of length k from $\left[V_1\right]$ for $\langle {\alpha }_1\rangle {\diamond }_{\mathcal{C}}^{\ast }\neg \psi$. Also, $\left[{\alpha }_1\right]{\square }_{\mathcal{C}}^{\ast }\psi \in \Delta$, by Lemma 5.4, part (2). By induction hypothesis, $\langle {\alpha }_1\rangle {\diamond }_{\mathcal{C}}^{\ast }\neg \psi \in V_1$.

If $\langle \alpha \rangle {\diamond }_{\mathcal{C}}^{\ast }\neg \psi \notin V_0$, then $\left[\alpha \right]{\square }_{\mathcal{C}}^{\ast }\psi \in V_0$. $V_0$ contains $\left[\alpha \right]{\square }_{\mathcal{C}}^{\ast }\psi \wedge \mathit{nf}\left({\mathrm{P}}_{\mathrm{RE}}\left(\alpha \right)\right)\to {\square }_A\left[{\alpha }_1\right]{\square }_{\mathcal{C}}^{\ast }\psi$. (That is, this sentence is valid by Lemma 4.21, part (2). Hence, it belongs to every maximal consistent set.) So $V_0$ contains ${\square }_A\left[{\alpha }_1\right]{\square }_{\mathcal{C}}^{\ast }\psi$. This sentence belongs to Δ by Lemma 5.4, part (2). Now by definition of $\stackrel{A}{⟶}$ in $\mathcal{F}$, we see that $\left[{\alpha }_1\right]{\square }_{\mathcal{C}}^{\ast }\psi \in V_1$. This is a contradiction to our observation at the end of the previous paragraph. □

Lemma 5.29. 

If ${V_0}^{\ast }\wedge \langle \alpha \rangle {\diamond }_{\mathcal{C}}^{\ast }\psi$ is consistent, then there is a good path from $\left[V_0\right]$ for $\langle \alpha \rangle {\diamond }_{\mathcal{C}}^{\ast }\psi$.

Proof. 

For each β such that $\alpha \stackrel{{\mathcal{C}}^{\ast }}{⟶}\beta$, let $S_{\beta }$ be the (finite) set of all $\left[W\right]\in \mathcal{F}$ such that there is no good path from $\left[W\right]$ for $\langle \beta \rangle {\diamond }_{\mathcal{C}}^{\ast }\psi$. We need to see that $\left[V_0\right]\notin S_{\alpha }$; suppose toward a contradiction that $\left[V_0\right]\in S_{\alpha }$. Let

$${\chi }_{\beta }=\bigvee \{W^{\ast }:W\in S_{\beta }\}.$$

Note that $\neg {\chi }_{\beta }$ is logically equivalent to $\bigvee \{X^{\ast }:\left[X\right]\in \mathcal{F}\mathrm{and}X\notin S_{\beta }\}$. Since we assumed $\left[V_0\right]\in S_{\alpha }$, we have $⊢{V_0}^{\ast }\to {\chi }_{\alpha }$.

We first claim for β such that $\alpha \stackrel{{\mathcal{C}}^{\ast }}{⟶}\beta$, ${\chi }_{\beta }\wedge \langle \beta \rangle \psi$ is inconsistent. Otherwise, there would be $\left[W\right]\in S_{\beta }$ such that ${\chi }_{\beta }\wedge \langle \beta \rangle \psi \in W$. Note that, by the partial-functionality axiom, $⊢\langle \beta \rangle \psi \to \mathrm{pre}\left(\beta \right)$. But then the one-point path $\left[W\right]$ is a good path from $\left[W\right]$ for $\langle \beta \rangle {\diamond }_{\mathcal{C}}^{\ast }\psi$. Thus, $\left[W\right]\notin S_{\beta }$, and this is a contradiction. So indeed, ${\chi }_{\beta }\wedge \langle \beta \rangle \psi$ is inconsistent. Therefore, $⊢{\chi }_{\beta }\to \left[\beta \right]\neg \psi$.

We next show that for all $A\in \mathcal{C}$ and all β such that $\beta {\to }_A\gamma$, ${\chi }_{\beta }\wedge {\mathrm{P}}_{\mathrm{RE}}\left(\beta \right)\wedge {\diamond }_A\neg {\chi }_{\gamma }$ is inconsistent. Otherwise, there would be $\left[W\right]\in S_{\beta }$ with ${\chi }_{\beta }$, ${\mathrm{P}}_{\mathrm{RE}}\left(\beta \right)$, and ${\diamond }_A\neg {\chi }_{\gamma }$ in it. Then, $\bigvee \{{\diamond }_A{X}^{\ast }:X\notin S_{\gamma }\}$, being equivalent to ${\diamond }_A\neg {\chi }_{\gamma }$, would belong to W. It follows that ${\diamond }_A{X}^{\ast }\in W$ for some $\left[X\right]\notin S_{\gamma }$. By Proposition 5.26, $\left[W\right]{\to }_A\left[X\right]$. Since $\left[X\right]\notin S_{\gamma }$, there is a good path from $\left[X\right]$ for $\langle \gamma \rangle {\diamond }_{\mathcal{C}}^{\ast }\psi$. But since $\beta {\to }_A\gamma$ and W contains $\mathrm{pre}\left(\beta \right)$, we also have a good path from $\left[W\right]$ for $\langle \beta \rangle {\diamond }_{\mathcal{C}}^{\ast }\psi$. This again contradicts $\left[W\right]\in S_{\beta }$. As a result, for all relevant A, β, and γ, $⊢{\chi }_{\beta }\wedge {\mathrm{P}}_{\mathrm{RE}}\left(\beta \right)\to {\square }_A{\chi }_{\gamma }.$

By the Action Rule, $⊢{\chi }_{\alpha }\to \left[\alpha \right]{\square }_{\mathcal{C}}^{\ast }\neg \psi$. Now $⊢{V_0}^{\ast }\to {\chi }_{\alpha }$. So $⊢{V_0}^{\ast }\to \left[\alpha \right]{\square }_{\mathcal{C}}^{\ast }\neg \psi$. This contradicts the assumption with which we began this proof. □

Lemma 5.30 (Truth Lemma). 

Consider a sentence φ, and also the set $\Delta =f\left(\phi \right)$. For all $\chi \in \Delta$ and $\left[U\right]\in \mathcal{F}$: $\chi \in U$ if $\langle \mathcal{F},\left[U\right]\rangle \vDash \chi$.

Proof. 

We argue by induction on the well-founded < that if $\chi \in \Delta$, then: $\chi \in U$ if $\langle \mathcal{F},\left[U\right]\rangle \vDash \chi$. The case of χ atomic is trivial. Now assume this Truth Lemma for sentences $<\chi$. Recall that $\Delta \subseteq \mathcal{NF}$, our set of normal forms (see Section 5.2.3). We argue by cases on χ.

The cases that χ is either a negation or conjunction are trivial.

Suppose next that $\chi \equiv {\square }_A\psi$. Suppose ${\square }_A\psi \in U$; we show $\langle \mathcal{F},\left[U\right]\rangle \vDash {\square }_A\psi$. Let $\left[V\right]$ be such that $\left[U\right]\stackrel{A}{⟶}\left[V\right]$. Then by definition of $\stackrel{A}{⟶}$, $\psi \in V$. The induction hypothesis applies to ψ, since $\psi <{\square }_A\psi$, and since $\psi \in \Delta$ by Lemma 5.4, part (1). So by induction hypothesis, $\langle \mathcal{F},\left[V\right]\rangle \vDash \psi$. This gives half of our equivalence. Conversely, suppose that $\langle \mathcal{F},\left[U\right]\rangle \vDash {\square }_A\psi$. Suppose towards a contradiction that ${\diamond }_A\neg \psi \in U$. So $U^{\ast }\wedge {\diamond }_A\neg \psi$ is consistent. We use Equation (16) and the fact that ${\diamond }_A$ distributes over disjunctions to see that $U^{\ast }\wedge {\diamond }_A\neg \psi$ is logically equivalent to $\bigvee (U^{\ast }\wedge {\diamond }_A{V}^{\ast })$, where the disjunction is taken over all V which contain $\neg \psi$. Since $U^{\ast }\wedge {\diamond }_A\neg \psi$ is consistent, one of the disjuncts $U^{\ast }\wedge {\diamond }_A{V}^{\ast }$ must be consistent. The induction hypothesis again applies, and we use it to see that $\langle \mathcal{F},\left[V\right]\rangle \vDash \neg \psi$. By Proposition 5.26, $\left[U\right]\stackrel{A}{⟶}\left[V\right]$. We conclude that $\langle \mathcal{F},\left[U\right]\rangle \vDash {\diamond }_A\neg \psi$, and this is a contradiction.

For χ of the form ${\square }_{\mathcal{C}}^{\ast }\psi$, we use the standard argument for PDL (see Kozen and Parikh [15]). This is based on lemmas that parallel Lemmas 5.28 and 5.29. The work is somewhat easier than what we do below for sentences of the form $\left[\alpha \right]{\square }_{\mathcal{C}}^{\ast }\psi$, and so we omit these details.

We conclude with the case when χ is a normal form sentence of the form $\left[\alpha \right]{\square }_{\mathcal{C}}^{\ast }\psi \in \Delta$. Assume that $\left[\alpha \right]{\square }_{\mathcal{C}}^{\ast }\psi \in \Delta$. First, suppose that $\left[\alpha \right]{\square }_{\mathcal{C}}^{\ast }\psi \notin U$. Then, by Lemma 5.29, there is a good path from $\left[U\right]$ for $\langle \alpha \rangle {\diamond }_{\mathcal{C}}^{\ast }\neg \psi$. We want to apply Lemma 4.11 in $\mathcal{F}$ to assert that $\langle \mathcal{F},\left[U\right]\rangle \vDash \langle \alpha \rangle {\diamond }_{\mathcal{C}}^{\ast }\neg \psi$. Let k be the length of the good path. For $i\le k$, ${\mathrm{P}}_{\mathrm{RE}}\left({\alpha }_i\right)\in U_i$. Now each $\mathit{nf}\left({\mathrm{P}}_{\mathrm{RE}}\left({\alpha }_i\right)\right)$ belongs to Δ by Lemma 5.4, part (2), and is $<\left[\alpha \right]{\square }_{\mathcal{C}}^{\ast }\psi$. So by induction hypothesis, $\langle \mathcal{F},\left[U_i\right]\rangle \vDash \mathit{nf}\left({\mathrm{P}}_{\mathrm{RE}}\left({\alpha }_i\right)\right)$. By soundness, $\langle \mathcal{F},\left[U_i\right]\rangle \vDash {\mathrm{P}}_{\mathrm{RE}}\left({\alpha }_i\right)$. We also need to check that $\langle \mathcal{F},\left[U_k\right]\rangle \vDash \langle {\alpha }_k\rangle \neg \psi$. For this, recall from Lemma 5.3 that Δ contains $\mathit{nf}(\neg \left[{\alpha }_k\right]\psi )\le \neg \left[{\alpha }_k\right]\psi <\left[\alpha \right]{\square }_{\mathcal{C}}^{\ast }\psi$. Since the path is good, $U_k$ contains $\langle {\alpha }_k\rangle \neg \psi$; thus, it contains $\neg \left[{\alpha }_k\right]\psi$; and, finally, it contains $\mathit{nf}(\neg \left[{\alpha }_k\right]\psi )$. By induction hypothesis, $\langle \mathcal{F},\left[U_k\right]\rangle \vDash \mathit{nf}(\neg \left[{\alpha }_k\right]\psi )$. By soundness, $\langle \mathcal{F},\left[U_k\right]\rangle \vDash \neg \left[{\alpha }_k\right]\psi$. Thus, $\langle \mathcal{F},\left[U_k\right]\rangle \vDash \langle {\alpha }_k\rangle \neg \psi$. Now it does follow from Lemma 4.11 that $\langle \mathcal{F},\left[U\right]\rangle \vDash \langle \alpha \rangle {\diamond }_{\mathcal{C}}^{\ast }\neg \psi$.

Going the other way, suppose that $\langle \mathcal{F},\left[U\right]\rangle \vDash \langle \alpha \rangle {\diamond }_{\mathcal{C}}^{\ast }\neg \psi$. By Lemma 4.11, we obtain a path in $\mathcal{F}$ witnessing this. The argument of the previous paragraph shows that this path is a good path from $\left[U\right]$ for $\langle \alpha \rangle {\diamond }_{\mathcal{C}}^{\ast }\neg \psi$. By Lemma 5.28, U contains $\langle \alpha \rangle {\diamond }_{\mathcal{C}}^{\ast }\neg \psi$. This completes the proof. □

Theorem 5.31 (Completeness). 

For all φ, $⊢\phi$ if $\vDash \phi$. Moreover, this relation is decidable.

Proof. 

By Lemma 5.2, $⊢\phi \leftrightarrow \mathit{nf}\left(\phi \right)$. Let φ be consistent. By the Truth Lemma, $\mathit{nf}\left(\phi \right)$ holds at some world in the filtration $\mathcal{F}$. So $\mathit{nf}\left(\phi \right)$ has a model; thus, φ has one, too. This establishes completeness. For decidability, note that the size of the filtration is computable in the size of the original φ. (Another proof of decidability: we show in Section 6.1 that ${\mathcal{L}}_1(\mathbf{\Sigma })$ can be translated into propositional dynamic logic (PDL) fairly directly, and that logic is decidable. Neither argument gives a good estimate of the complexity.) □

5.5. Extensions to the Completeness Theorem

We briefly mention extensions of the Completeness Theorem 5.31.

First, consider the case of S5 (or K45) actions. We change our logical system by restricting to these S5 actions, and we add the S5 axioms to our logical system. We interpret this new system on S5 models. It is easy to check that applying an S5 action to an S5 model gives another S5 model. Further, the S5 actions are closed under composition. Finally, if α is an S5 action and $\alpha {\to }_A\beta$, then β also is an S5 action. These easily imply the soundness of the new axioms. For completeness, we need only check that if we assume the S5 axioms, then the filtration $\mathcal{F}$ from the previous section has the property that each $\stackrel{A}{⟶}$ is an equivalence relation. This is a standard exercise in modal logic (see, e.g., Fagin et al. [18], Theorem 3.3.1).

Second, we also have completeness not only for the languages ${\mathcal{L}}_1(\mathbf{\Sigma })$, but also for the languages in [6] that are constructed from families $\mathcal{S}$ of action signatures. This construction is most significant in the case when $\mathcal{S}$ is an infinite set of signatures; for example, $\mathcal{S}$ might contain a copy of every finite signature. In that setting, the language $\mathcal{L}\left(\mathcal{S}\right)$ would not be the language of any finite signature. But for the (weak) completeness result of this section, the advantage of the extended definition is lost. The point is that for single sentences, we may restrict attention to a finite subset of $\mathcal{S}$. And for finite sets $\mathcal{S}$, $\mathcal{L}\left(\mathcal{S}\right)$ is literally the language of the coproduct signature

$$\oplus \{\mathbf{\Sigma }:\mathbf{\Sigma }\in \mathcal{S}\}.$$

We already have completeness for such languages.

Our final extension concerns the move from actions as we have been working with them to actions which change the truth values of atomic sentences. If we make this move, then the axiom of Atomic Permanence is no longer sound. However, it is easy to formulate the relevant axioms. For example, if we have an action α which effects the change $p:=p\wedge \neg q$, then we would take an axiom $\left[\alpha \right]p\leftrightarrow \left({\mathrm{P}}_{\mathrm{RE}}\right(\alpha )\to p\wedge \neg q)$. Having made these changes, all of the rest of the work we have done goes through. In this way, we get a completeness theorem for this logic.

Endnotes

Special cases of Theorem 5.24 for some of the target logics are due to Plaza [1], Gerbrandy [2,3], and Gerbrandy and Groeneveld [4]. The proofs in these sources also go via translation to modal logic.

6. Results on Expressive Power

In this section, we study a number of expressive power issues related to our logics. The four subsections are for the most part independent.

6.1. Translation of ${\mathcal{L}}_1(\mathbf{\Sigma })$ into PDL

In this section, Σ is an arbitrary action signature. In Section 5.2.3, we saw normal forms for ${\mathcal{L}}_0(\mathbf{\Sigma })$ and ${\mathcal{L}}_1(\mathbf{\Sigma })$. We showed in that section that every sentence in ${\mathcal{L}}_1(\mathbf{\Sigma })$ is provably equivalent to its normal form, and the normal forms of sentences of ${\mathcal{L}}_0(\mathbf{\Sigma })$ are exactly the purely modal sentences. This proves that in terms of expressive power, ${\mathcal{L}}_0(\mathbf{\Sigma })$ is equivalent to ${\mathcal{L}}_0$, ordinary modal logic.

Further, we can show that ${\mathcal{L}}_1(\mathbf{\Sigma })$ and, indeed, the full language $\mathcal{L}(\mathbf{\Sigma })$ is a sublogic of ${\mathcal{L}}_0^{\omega }$, the extension of modal logic with countable Boolean conjunction and disjunction. The idea is contained in the following clauses:

$$\begin{array}{ccc}{\left({\square }_{\mathcal{B}}^{\ast }\phi \right)}^t\hfill & =& \underset{\langle A_1,\dots ,A_n\rangle \in {\mathcal{B}}^{\ast }}{\bigwedge }{({\square }_{A_1}\cdots {\square }_{A_n}\phi )}^t\hfill \\ {\left(\left[\alpha \right]{\square }_{\mathcal{B}}^{\ast }\psi \right)}^t\hfill & =& \underset{\langle A_1,\dots ,A_n\rangle \in {\mathcal{B}}^{\ast }}{\bigwedge }{(\left[\alpha \right]{\square }_{A_1}\cdots {\square }_{A_n}\psi )}^t\hfill \\ {\left({\left[\pi \right]}^{\ast }\phi \right)}^t\hfill & =& \underset{n}{\bigwedge }{\left({\left[\pi \right]}^n\phi \right)}^t\hfill \end{array}$$

It is natural to ask whether there are any finite logics which have been previously studied and into which our logics can be embedded. One possibility is the Modal Iteration Calculus ($MIC$) introduced in Dawar, Grädel, and Kreutzer [19]. The full language $\mathcal{L}\left({\mathbf{\Sigma }}_{\mathrm{pub}}\right)$ is a sublanguage of $MIC$; see [14] for details. It is likely that this result extends to all other finite action signatures. In another direction, we ask whether the fragments ${\mathcal{L}}_1(\mathbf{\Sigma })$ are sublogics of previously studied systems.

Theorem 6.1. 

Every sentence of ${\mathcal{L}}_1(\mathbf{\Sigma })$ is equivalent to a sentence of PDL.

Proof. 

(Sketch) We argue by induction on the well-order < introduced and studied in Section 5. It is sufficient to show that each sentence in the set $\mathcal{NF}$ of normal forms of ${\mathcal{L}}_1(\mathbf{\Sigma })$ is equivalent to a sentence of PDL. (The normal forms were introduced in Section 5.2.3, and the reader may wish to look back at Lemma 5.17.) We just give the main induction step.

Suppose that $\left[\alpha \right]{\square }_{\mathcal{C}}^{\ast }\phi$ is a normal-form sentence. Our induction hypothesis implies that each $\psi <\left[\alpha \right]{\square }_{\mathcal{C}}^{\ast }\phi$ is equivalent to some PDL sentence ${\psi }^{\prime }$. We shall show that $\langle \alpha \rangle {\diamond }_{\mathcal{C}}^{\ast }$ is itself equivalent to some PDL sentence; hence, $\left[\alpha \right]{\square }_{\mathcal{C}}^{\ast }\phi$ also has this property. For this, we use the semantic equivalent given in Lemma 4.11. Recall first that there are only finitely many β such that $\alpha \stackrel{{\mathcal{C}}^{\ast }}{⟶}\beta$. Let X be the (finite) set of all such β such that $\alpha \stackrel{{\mathcal{C}}^{\ast }}{⟶}\beta$. That is, the actions β reachable from α by a path labeled by agents in the set $\mathcal{C}$. We consider X as a sub-action structure of Ω.

We consider $\mathcal{C}\cup X$, and we assume that this union is disjoint. We consider the set ${(\mathcal{C}\cup X)}^{\ast }$ of all finite words on this set. We are interested in finite $\mathcal{C}$-labeled paths through X beginning at α and ending at an arbitrary element of X. At this point, we shall develop our proof only by example.

Suppose that $\mathcal{C}=\{A,B\}$ and that $X=\{\alpha ,\beta \}$, with $\alpha \stackrel{A}{⟶}\alpha$, $\alpha \stackrel{B}{⟶}\beta$, and $\beta \stackrel{A}{⟶}\alpha$. Then one of the paths of interest would be

$$\alpha A\alpha B\beta A\alpha$$

(Note that this corresponds to $\alpha \stackrel{A}{⟶}\alpha \stackrel{B}{⟶}\beta \stackrel{A}{⟶}\alpha$.) We are only interested in paths that respect the structure of Ω. By Kleene’s Theorem, the set P of finite paths of this type beginning at our fixed action α is a regular language on $\mathcal{C}\cup X$. In our example, P is given by the regular expression

$$({\left(\alpha {\left(A\alpha \right)}^{\ast }\left(B\beta A\right)\right)}^{\ast }(ϵ+B\beta ).$$

With each such regular expression we associate a PDL program that represents it. In our example, we would have

$$(?{{\mathrm{P}}_{\mathrm{RE}}}^{\prime }\left(\alpha \right);{({(\langle A\rangle ;?{{\mathrm{P}}_{\mathrm{RE}}}^{\prime }\left(\alpha \right))}^{\ast };(\langle B\rangle ;?{{\mathrm{P}}_{\mathrm{RE}}}^{\prime }\left(\beta \right);\langle A\rangle ))}^{\ast };(?\mathsf{true}+\langle B\rangle ;?{{\mathrm{P}}_{\mathrm{RE}}}^{\prime }\left(\beta \right)).$$

(The notation ${{\mathrm{P}}_{\mathrm{RE}}}^{\prime }\left(\gamma \right)$ means the PDL translation of ${\mathrm{P}}_{\mathrm{RE}}\left(\gamma \right)$; such a PDL sentence exists since ${\mathrm{P}}_{\mathrm{RE}}\left(\gamma \right)<\left[\alpha \right]{\square }_{\mathcal{C}}^{\ast }\phi$.) Again, this is a PDL program $\pi =\pi (X,\alpha )$ whose denotation ${⟦\pi ⟧}_{\mathbf{S}}$ in a state model $\mathbf{S}$ is the set of pairs $(s,t)$ of states such that there is a path

$$s=s_0{\to }_{A_1}{s}_1{\to }_{A_2}\cdots {\to }_{A_{k-1}}{s}_{k-1}{\to }_{A_k}{s}_k$$

and also a sequence of actions of the same length k,

$$\alpha ={\alpha }_0{\to }_{A_1}{\alpha }_1{\to }_{A_2}\cdots {\to }_{A_{k-1}}{\alpha }_{k-1}{\to }_{A_k}{\alpha }_k$$

such that each $A_i\in \mathcal{C}$, each $s_i\in {⟦{\mathrm{P}}_{\mathrm{RE}}\left({\alpha }_i\right)⟧}_{\mathbf{S}}$ for all $0\le i\le k$, and, finally, such that $s_k=t$. Consider now the PDL sentence $\langle \pi \rangle {\left(\langle {\alpha }_k\rangle \phi \right)}^{\prime }$. (As above, ${\left(\langle {\alpha }_k\rangle \phi \right)}^{\prime }$ means the PDL translation of $\langle {\alpha }_k\rangle \phi$. This exists because $\left[{\alpha }_k\right]\phi <\left[\alpha \right]{\square }_{\mathcal{C}}^{\ast }\phi$; see Lemma 5.17.) A state s satisfies $\langle \pi \rangle {\left(\langle {\alpha }_k\rangle \phi \right)}^{\prime }$ in $\mathbf{S}$ if there is some $(s,t)\in {⟦\pi ⟧}_{\mathbf{S}}$ such that $t\in {⟦\langle {\alpha }_k\rangle \phi ⟧}_{\mathbf{S}}$. Putting together our description of ${⟦\pi ⟧}_{\mathbf{S}}$ with this, we see that $(s,t)\in {⟦\pi ⟧}_{\mathbf{S}}$ iff $s\in {⟦\langle \alpha \rangle {\diamond }_{\mathcal{C}}^{\ast }⟧}_{\mathbf{S}}$; see Lemma 4.11. □

Remark 6.2. 

Theorem 6.1 also follows from the closure of a different system, epistemic PDL (not discussed in this paper), under action modalities. This was proved by Jan van Eijck [20], and it also appears in [9]. The method of proof is very similar to what we have presented.

At this point, we know that ${\mathcal{L}}_1(\mathbf{\Sigma })$ is a sublogic of PDL. So it is interesting to ask whether this extends to the full logic $\mathcal{L}(\mathbf{\Sigma })$; recall that this last language has the operation of program iteration ${\pi }^{\ast }$. It turns out that $\mathcal{L}(\mathbf{\Sigma })$ lacks the finite-model property even when Σ is as simple as the signature of public announcements and, indeed, when the only sentence announced publically and repeatedly is $\diamond \mathsf{true}$ (see Section 6.4, below). Since PDL has the finite model property, we see that $\mathcal{L}(\mathbf{\Sigma })$ is not a sublogic of PDL. In fact, it also shows that $\mathcal{L}(\mathbf{\Sigma })$ is not even a sublogic of the modal mu-calculus.

6.2. ${\mathcal{L}}_1\left({\mathbf{\Sigma }}_{pub}\right)$ Is More Expressive Than ${\mathcal{L}}_1$

Recall that ${\mathcal{L}}_1$ in this paper is multi-agent modal logic together with the common-knowledge operators ${\square }_{\mathcal{B}}^{\ast }$ for sets of agents. Our main result here is that ${\mathcal{L}}_1$ is strictly weaker than ${\mathcal{L}}_1\left({\mathbf{\Sigma }}_{\mathrm{pub}}\right)$, the logic obtained by adding public announcements to ${\mathcal{L}}_1$.

We define a rank $\left|\phi \right|$ on sentences from ${\mathcal{L}}_1\left({\mathbf{\Sigma }}_{\mathrm{pri}}\right)$. Let $\left|p\right|=0$ for p atomic, $|\neg \phi |=\left|\phi \right|$, $|\phi \wedge \psi |=max\left(\right|\phi |,|\psi \left|\right)$, $|{\diamond }_A\phi |=1+|\phi |$, for all $A\in \mathcal{A}$, and $|{\diamond }_{\mathcal{B}}^{\ast }\phi |=1+|\phi |$ for all $\mathcal{B}\subseteq \mathcal{A}$.

6.2.1. Games for ${\mathcal{L}}_1$

The main technique in the proof is an adaptation of Fraisse–Ehrenfeucht games to the setting of modal logic. Let $(\mathbf{S},s)$ and $(\mathbf{T},t)$ be states; i.e., model-world pairs. By recursion on the natural number n, we define a game $G_n((\mathbf{S},s),(\mathbf{T},t))$. For $n=0$, $II$ immediately wins if the following holds: for all $p\in \mathsf{AtSen}$, $(\mathbf{S},s)\vDash p$ if $(\mathbf{T},t)\vDash p$. And if s and t differ on some atomic sentence, I immediately wins. Continuing, here is how we define $G_{n+1}((\mathbf{S},s),(\mathbf{T},t))$. As in the case of the $G_0$ games, we first check if s and t differ on some atomic sentence. If they do, then I immediately wins. Otherwise, the play continues. Now I can make two types of moves.

• A ${\diamond }_A$-move: I has a choice of playing from $\mathbf{S}$ or from $\mathbf{T}$, and also some agent A. If I chooses $\mathbf{S}$, then I continues by choosing some $s^{\prime }$ such that $s\stackrel{A}{⟶}{s}^{\prime }$ in $\mathbf{S}$. Then $II$ replies with some $t^{\prime }\in T$ such that $t\stackrel{A}{⟶}{t}^{\prime }$. Of course, if I had chosen in $\mathbf{T}$, then $II$ would have chosen in S. Either way, points $s^{\prime }$ and $t^{\prime }$ are determined, and the two players then play $G_n((\mathbf{S},s^{\prime }),(\mathbf{T},t^{\prime }))$.
• A ${\diamond }_{\mathcal{B}}^{\ast }$-move: I plays by selecting $\mathbf{S}$ (or $\mathbf{T}$, but we ignore this symmetric case below), and some set $\mathcal{B}$ of agents, and then I continues by playing some $s^{\prime }$ (say) reachable from s in the reflexive-transitive closure $\stackrel{{\mathcal{B}}^{\ast }}{⟶}$ of $\stackrel{\mathcal{B}}{⟶}$; $II$ responds with a point $t^{\prime }$ in the other model, $\mathbf{T}$, which is similarly related to t.

We write $(\mathbf{S},s){\sim }_n(\mathbf{T},t)$ if $II$ has a winning strategy in the game $G_n((\mathbf{S},s),(\mathbf{T},t))$. It is easy to check that by induction on m that if $(\mathbf{S},s){\sim }_n(\mathbf{T},t)$ and $m<n$, then $(\mathbf{S},s){\sim }_m(\mathbf{T},t)$.

Proposition 6.3. 

If $(\mathbf{S},s){\sim }_n(\mathbf{T},t)$, then for all φ with $\left|\phi \right|\le n$, $(\mathbf{S},s)\vDash \phi$ if $(\mathbf{T},t)\vDash \phi$.

The proof is standard, except perhaps for the easy extra step for ${\diamond }^{\ast }$ moves.

We have two results that show that public announcements add expressive power to ${\mathcal{L}}_1$. The first is for one agent on arbitrary models, and the second is for two agents on equivalence relations.

In the first result, let $\mathcal{A}$ be a singleton $\left\{A\right\}$. We drop the A from the notation.

Theorem 6.4. 

The ${\mathcal{L}}_1\left({\mathbf{\Sigma }}_{pub}\right)$ sentence $\langle \mathrm{Pub}p\rangle {\diamond }^{\ast }q$ is not expressible in ${\mathcal{L}}_1$, even by a set of sentences.

Proof. 

Fix a number n. We first show that $\langle Pubp\rangle {\diamond }^{\ast }q$ is not expressible by any single sentence of ${\mathcal{L}}_1$ of rank n. Let $A_n$ be the cycle

$$a_0\to a_1\to \cdots \to a_{n+2}\to a_{n+3}\to \cdots a_{2n+4}=a_0.$$

We set p to true everywhere except $a_{n+2}$ and q true only at $a_0$.

Announcing p means that we delete $a_{n+2}$. So, $A_n\left(Pubp\right)$ splits into two disjoint pieces. This means that in $A_n\left(Pubp\right)$, $a_1$ does not satisfy ${\diamond }^{\ast }q$. But $a_{n+3}$ does satisfy it.

We show that $a_1$ and $a_{n+3}$ agree on all sentences of ${\mathcal{L}}_1$ of rank $\le n$. For this, we show that $II$ has a winning strategy in the n-round game on between $(A_n,a_{n+1})$ and $(A_n,a_{n+3})$. Then we appeal to Proposition 6.3. $II$’s strategy is as follows: if I ever makes a ${\diamond }^{\ast }$ move, $II$ should make a move on the other side to the exact same point. (Recall that $A_n$ is a cycle.) Thereafter, $II$ should mimic I’s moves exactly. Since the play will end with the same point in the two structures, $II$ wins. But if I never makes a ${\diamond }^{\ast }$ move, the play will consist of n⋄-moves. $II$ should simply make the same moves in the appropriate structures. Since $a_{n+2}$ is $n+1$ steps from $a_1$, and $a_0=a_{2n+4}$ is $n+1$ steps from $a_{n+3}$, $II$ will win the play in this case.

So at this point we conclude that for all n, $\langle Pubp\rangle {\diamond }^{\ast }q$ is not expressible by any single sentence of ${\mathcal{L}}_1$ of rank n. We conclude by extending this to show that $\langle Pubp\rangle {\diamond }^{\ast }q$ is not expressible by any set of sentences of ${\mathcal{L}}_1$. Suppose towards a contradiction that $\langle Pubp\rangle {\diamond }^{\ast }q$ were equivalent to the set $T\subseteq {\mathcal{L}}_1$. Consider the following models $\mathcal{A}$ and $\mathcal{B}$: $\mathcal{A}={\oplus }_{n\ge 0}(A_n,a_1^n)$; i.e., take the disjoint union of the models $\oplus A_n$, and then identify all points $a_1^n$. We also rename the common $a_1^n$ point to be a, and we take this as the distinguished point. So we consider $(\mathcal{A},a)$. Similarly, let $\mathcal{B}={\oplus }_{n\ge 0}(A_n,a_{n+3}^n)$. For clarity we will rename each point $a_j^m$ to be $b_j^m$. And we write b for the distinguished point of $\mathcal{B}$. The construction insures that $(\mathcal{A},a)\vDash \neg \langle Pubp\rangle {\diamond }^{\ast }q$ and $(\mathcal{B},b)\vDash \langle Pubp\rangle {\diamond }^{\ast }q$.

By definition of T, $(\mathcal{B},b)\vDash \phi$ for all $\phi \in T$. Let $\phi \in T$ be such that $(\mathcal{A},a)\vDash \neg \phi$. Let $m=\left|\phi \right|$. Let

$$\mathcal{C}=\oplus (\{(A_n,a_1^n):n\ne m\}\cup \left\{(A_m,a_{m+3}^m)\right\}).$$

Notice that we switched exactly one of the identified points. Just as before, we will rename the points of $\mathcal{C}$ and call the overall distinguished point c. It is easy to check that $(\mathcal{C},c)\vDash \langle Pubp\rangle {\diamond }^{\ast }q$. And since this sentence is equivalent to T, we also have $(\mathcal{C},c)\vDash \phi$. But we now show that $(\mathcal{A},a)$ and $(\mathcal{C},c)$ agree on all sentences of rank $\le m$. This implies that $(\mathcal{A},a)\vDash \phi$, giving the needed contradiction.

Here is a winning strategy for $II$ in the m-round game between $(\mathcal{A},a)$ and $(\mathcal{C},c)$. If I opens with anything besides $c_{m+3}^m$ or $a_1^m$, $II$ should play the corresponding point on the other side and, thereafter, play in the obvious way. If I opens with $c_{m+3}^m$, $II$ should play with $a_1^m$ and, thereafter, play with basically the same strategy as in the first part of this theorem; similarly, if I opens with $a_1^m$, $II$ should reply $c_{m+3}^m$ and, thereafter, play via the strategy in the first part of this proof, where we dealt with single sentences. □

6.2.2. Partition Models

Often in epistemic logic one is concerned with models in which every accessibility relation $\stackrel{A}{⟶}$ is an equivalence relation. We can obtain a version of Theorem 6.4 which shows that even on this smaller class of models, public announcements add expressive power to ${\mathcal{L}}_1$. However, we must use two agents: with one agent and an equivalence relation ${\square }^{\ast }\phi$ is equivalent to $\square \phi$. Thus, every sentence in ${\mathcal{L}}_1\left({\mathbf{\Sigma }}_{\mathrm{pub}}\right)$ on one-agent equivalence relations is equivalent to a purely modal sentence.

Theorem 6.5. 

The ${\mathcal{L}}_1\left({\mathbf{\Sigma }}_{pub}\right)$ sentence $\langle Pubp\rangle {\diamond }_{A,B}^{\ast }q$ is not expressible by any set of sentences of ${\mathcal{L}}_1$, even on the class of models in which $\stackrel{A}{⟶}$ and $\stackrel{B}{⟶}$ are equivalence relations.

Proof. 

We fix a number N and first show that $\langle Pubp\rangle {\diamond }^{\ast }q$ is not expressible by any single sentence of ${\mathcal{L}}_1$ of rank N. Let n be the smallest even number strictly larger than N. Let $C_n$ be as defined in Section 3.2 above. Note that $C_n$ does have the property that $\stackrel{A}{⟶}$ and $\stackrel{B}{⟶}$ are equivalence relations. In addition, ${\left(\stackrel{A}{⟶}\right)}^{\ast }$ is the same relation as $\stackrel{A}{⟶}$. So, ${\square }_A^{\ast }\phi$ is equivalent to ${\square }_A\phi$ (and similarly for B). Finally, ${(\stackrel{A}{⟶}\cup \stackrel{B}{⟶})}^{\ast }$ is the universal relation. So if any point whatsoever satisfies a sentence ${\square }_{A,B}^{\ast }\phi$, then all points satisfy it.

The analysis of Section 3.2 shows that the points $a_{n+1}$ and $a_{3n+1}$ differ on our sentence $\langle Pubp\rangle {\diamond }_{A,B}^{\ast }q$.

We continue by showing that $II$ has a winning strategy in the n-round game on $C_n$ from $a_{n+1}$ and $a_{3n+1}$. If I ever makes a ${\diamond }^{\ast }$ move, then $II$ should move to the same point and, thereafter, mimic I perfectly. Thus, we may assume that I never makes any ${\diamond }^{\ast }$ moves. In this case, I will never move either point to $a_1$, $a_{2n+1}$, or $a_{4n+1}$. In other words, all points in the play will satisfy $p\wedge \neg q$. So, as long as I plays ⋄-moves, $II$ can follow arbitrarily. Once again, since the game goes for n rounds, this will be a winning strategy.

At this point we know that $\langle Pubp\rangle {\diamond }^{\ast }q$ is not expressible by any single sentence of ${\mathcal{L}}_1$ of rank $n>N$. We use the same idea as in Theorem 6.4 to show that $\langle Pubp\rangle {\diamond }^{\ast }q$ is not expressible by any set of sentences of ${\mathcal{L}}_1$. In fact, virtually the same proof goes through. □

6.3. ${\mathcal{L}}_1\left({\mathbf{\Sigma }}_{pri}\right)$ Is More Expressive Than ${\mathcal{L}}_1\left({\mathbf{\Sigma }}_{pub}\right)$

It is natural to assume that privacy adds expressive power to logics of communication. The result of this section is the first result we know that establishes this. In it, we assume that our set of agents is the doubleton $\{A,B\}$.

Theorem 6.6. 

The sentence χ of ${\mathcal{L}}_1\left({\mathbf{\Sigma }}_{pri}\right)$ from (8) and repeated below

$$\chi \equiv \langle {\mathrm{Pri}}^{A}p,\mathsf{true}\rangle {\diamond }_A^{\ast }{\diamond }_B\neg p$$

cannot be expressed by any sentence of ${\mathcal{L}}_1\left({\mathbf{\Sigma }}_{pub}\right)$, and ${\diamond }_A\chi$ cannot be expressed by any set of sentences of ${\mathcal{L}}_1\left({\mathbf{\Sigma }}_{pub}\right)$.

We define a function $\left|\phi \right|$ on $\mathcal{L}\left({\mathbf{\Sigma }}_{\mathrm{pub}}\right)$: $\left|p\right|=0$ for p atomic, $|\neg \phi |=\left|\phi \right|$, $|\phi \wedge \psi |=max\left(\right|\phi |,|\psi \left|\right)$, $|{\diamond }_A\phi |=1+|\phi |$, $|{\diamond }_B\phi |=1$, $|{\diamond }_{\mathcal{B}}^{\ast }\phi |=|\phi |$ for all $\mathcal{B}\subseteq \mathcal{A}$, and $\left|\right[Pub\phi \left]\psi \right|=max\left(\right|\phi |,|\psi \left|\right)$.

Lemma 6.7. 

Let $\phi \in \mathcal{L}\left({\mathbf{\Sigma }}_{pub}\right)$, and let $1\le k\le n$. If $n-k\ge \left|\phi \right|$, then

$$({\mathbf{S}}_n,a)\vDash \phi iff({\mathbf{S}}_n,c_k)\vDash \phi iff({\mathbf{T}}_n,a)\vDash \phi .$$

Proof. 

By induction on φ. The base step for atomic p and the induction steps for the Boolean connectives are all trivial.

Here is the induction step for ${\diamond }_A\phi$. Fix k with $n-k\ge |{\diamond }_A\phi |=1+|\phi |$. Thus, $n-k>n-(k+1)\ge \left|\phi \right|$. We prove the needed equivalences in a cycle.

Assume first that $({\mathbf{S}}_n,a)\vDash {\diamond }_A\phi$. The only arrows from a in ${\mathbf{S}}_i$ are to $a\stackrel{A}{⟶}a$ and $a\stackrel{A}{⟶}b$. If $({\mathbf{S}}_n,a)\vDash \phi$, then the reflexive arrow on $c_k$ and the induction hypothesis show that $({\mathbf{S}}_n,c_k)\vDash {\diamond }_A\phi$. If $({\mathbf{S}}_n,b)\vDash \phi$, then clearly $({\mathbf{S}}_n,c_k)\vDash {\diamond }_A\phi$ via $c_k\stackrel{A}{⟶}b$.

Second, assume that $({\mathbf{S}}_n,c_k)\vDash {\diamond }_A\phi$. We show that $({\mathbf{T}}_n,a)\vDash {\diamond }_A\phi$. Notice that one of the following holds: $({\mathbf{S}}_n,c_k)\vDash \phi$, $({\mathbf{S}}_n,b)\vDash \phi$, or $({\mathbf{S}}_n,c_{k+1})\vDash \phi$. The first case is handled easily by the induction hypothesis. In the second, we have by (9) that $({\mathbf{T}}_n,b)\vDash \phi$; hence $({\mathbf{T}}_n,a)\vDash {\diamond }_A\phi$. We are left with the case $({\mathbf{S}}_n,c_{k+1})\vDash \phi$. Since $n-(k+1)\ge \left|\phi \right|$, the induction hypothesis implies that $({\mathbf{T}}_n,a)\vDash \phi$. Since $a\stackrel{A}{⟶}a$, $({\mathbf{T}}_n,a)\vDash {\diamond }_A\phi$.

Finally, assume that $({\mathbf{T}}_n,a)\vDash {\diamond }_A\phi$. We verify that $({\mathbf{S}}_n,a)\vDash {\diamond }_A\phi$. In view of the fact that $a\stackrel{A}{⟶}{c}_1$ in $\mathbf{T}$, one of the following holds: $({\mathbf{T}}_n,a)\vDash \phi$, $({\mathbf{T}}_n,b)\vDash \phi$, or $({\mathbf{T}}_n,c_1)\vDash \phi$. The only important case is the last. Since $n-1\ge n-k\ge \left|\phi \right|$, our induction hypothesis implies that in this case, $({\mathbf{S}}_n,a)\vDash {\diamond }_A\phi$, as desired.

We continue with the induction step for ${\diamond }_B\phi$. Recall that $|{\diamond }_B\phi |=1$. Since we assume $n-k\ge 1$, we have $k<n$. There are no B-arrows from $c_k$ or from a. All three needed statements in our lemma are false, so all three are equivalent.

Next, we have the induction step for ${\diamond }_{\mathcal{B}}^{\ast }\phi$, where $\mathcal{B}$ is either $\left\{A\right\}$, $\left\{B\right\}$, or $\{A,B\}$. With two agents, $\mathcal{B}$ can be $\left\{A\right\}$, $\left\{B\right\}$ or $\{A,B\}$ here. Note that $\stackrel{B}{⟶}$ is already transitive, so all the work for ${\diamond }_B^{\ast }\phi$ has been done above already. Also, $\stackrel{B}{⟶}$ is a subrelation of $\stackrel{A}{⟶}$ in both ${\mathbf{S}}_n$ and ${\mathbf{T}}_n$. Thus, we only need to work with $\mathcal{B}=\left\{A\right\}$ in this induction step.

Assume first that $({\mathbf{S}}_n,a)\vDash {\diamond }_{\mathcal{B}}^{\ast }\phi$. There are a number of cases. If $({\mathbf{S}}_n,a)\vDash \phi$, then by induction hypothesis, $({\mathbf{S}}_n,c_k)\vDash \phi$. So, $({\mathbf{S}}_n,c_k)\vDash {\diamond }_{\mathcal{B}}^{\ast }\phi$ as well. The other case is where $a\stackrel{{\mathcal{B}}^{\ast }}{⟶}x$, $x\vDash \phi$, and x is among the points b, $c_1$, …, $c_n$. Note in this case that $c_k\stackrel{{\mathcal{B}}^{\ast }}{⟶}x$ as well: all non-null paths from a go through b, and $c_k\stackrel{A}{⟶}b$. Thus, in this case, we have $({\mathbf{S}}_n,c_k)\vDash {\diamond }_{\mathcal{B}}^{\ast }\phi$.

Next, assume that $({\mathbf{S}}_n,c_k)\vDash {\diamond }_{\mathcal{B}}^{\ast }\phi$. Let x be such that $c_k\stackrel{{\mathcal{B}}^{\ast }}{⟶}x$ and $({\mathbf{S}}_n,x)\vDash \phi$. Clearly, $x\ne a$. By (9), $({\mathbf{T}}_n,x)\vDash \phi$. Also, $a\stackrel{A}{⟶}b\stackrel{{\mathcal{B}}^{\ast }}{⟶}{c}_k\stackrel{{\mathcal{B}}^{\ast }}{⟶}x$. So $({\mathbf{T}}_n,a)\vDash {\diamond }_{\mathcal{B}}^{\ast }\phi$.

Suppose, finally, that $({\mathbf{T}}_n,a)\vDash {\diamond }_A^{\ast }\phi$. If $({\mathbf{T}}_n,a)\vDash \phi$, then by induction hypothesis we have $({\mathbf{S}}_n,a)\vDash \phi$. So, in this case, $({\mathbf{S}}_n,a)\vDash {\diamond }_{\mathcal{B}}^{\ast }\phi$ as well. The other case is where $({\mathbf{T}}_n,x)\vDash \phi$ for some $x\ne a$. By (9) again, $({\mathbf{S}}_n,x)\vDash \phi$. And in ${\mathbf{S}}_n$, $a\stackrel{{\mathcal{B}}^{\ast }}{⟶}x$. Thus $({\mathbf{S}}_n,a)\vDash {\diamond }_{\mathcal{B}}^{\ast }\phi$, as desired.

The most interesting step is the induction step for $\left[Pub\phi \right]\psi$. Fix k with $n-k>\left|\right[Pub\phi \left]\psi \right|=max\left(\right|\phi |,|\psi \left|\right)$. Thus, $n-k\ge \left|\phi \right|,\left|\psi \right|$, and our induction hypothesis applies to both φ and ψ. In particular, the following are equivalent:

$$({\mathbf{S}}_n,a)\vDash \phi ({\mathbf{S}}_n,c_k)\vDash \phi ({\mathbf{T}}_n,a)\vDash \phi$$

(20)

Let us save on some notation by defining

$${\mathbf{S}}_n^{\ast }=\mathbf{S}\otimes ({\mathbf{\Sigma }}_{\mathrm{pub}},Pub,\phi )$$

and, similarly, for ${\mathbf{T}}_n^{\ast }$. Moreover

$${⟦\left[Pub\phi \right]\psi ⟧}_{{\mathbf{S}}_n}=\{x\in S_n:\mathrm{if}x\in {⟦\phi ⟧}_{{\mathbf{S}}_n},then(x,Pub)\in {⟦\psi ⟧}_{{\mathbf{S}}_n^{\ast }}\}$$

(21)

A similar equation holds for ${\mathbf{T}}_n$.

Case I: $({\mathbf{S}}_n,a)⊭\phi$. Since $n-k\ge \left|\phi \right|$, we have by (20) that $({\mathbf{S}}_n,c_k)⊭\phi$, and $({\mathbf{T}}_n,a)⊭\phi$. So, automatically, all three of the relevant model-world pairs satisfy our sentence $\left[Pub\phi \right]\psi$.

Case II: $({\mathbf{S}}_n,a)\vDash \phi$ and $({\mathbf{S}}_n,b)⊭\phi$. Then by induction hypothesis, $({\mathbf{S}}_n,c_k)\vDash \phi$, and $({\mathbf{T}}_n,a)\vDash \phi$, and by (9), $({\mathbf{T}}_n,b)⊭\phi$. In ${\mathbf{S}}_n^{\ast }$ and ${\mathbf{T}}_n^{\ast }$, each point satisfies p and has no $\stackrel{B}{⟶}$ -successors, and every point has an $\stackrel{A}{⟶}$ -successor (itself). Thus, the following are equivalent:

$$({\mathbf{S}}_n^{\ast },(a,Pub))\vDash \psi ({\mathbf{S}}_n^{\ast },(c_k,Pub))\vDash \psi ({\mathbf{T}}_n^{\ast },(a,Pub))\vDash \psi$$

(22)

In more detail, the three model-world pairs above are all bisimilar to a one-point model which is a point satisfying p with a loop for $\stackrel{A}{⟶}$. Hence, we have (22). This implies that the following are indeed equivalent:

$$({\mathbf{S}}_n,a)\vDash \left[Pub\phi \right]\psi ({\mathbf{S}}_n,c_k)\vDash \left[Pub\phi \right]\psi ({\mathbf{T}}_n,a)\vDash \left[Pub\phi \right]\psi .$$

(23)

Case III: $({\mathbf{S}}_n,a)\vDash \phi$, $({\mathbf{S}}_n,b)\vDash \phi$, and for some ℓ such that $1\le \mathcal{\ell }\le n$, $({\mathbf{S}}_n,c_{\mathcal{\ell }})⊭\phi$. We take the smallest such ℓ. Since $1\le k$, $n-1\ge n-k\ge \left|\phi \right|$. So $({\mathbf{S}}_n,c_1)\vDash \phi$ by induction hypothesis. Thus, $\mathcal{\ell }>1$. Let $m=\mathcal{\ell }-1$. Then $m\ge 1$. The point $(c_m,{Pri}^A)$ in the updated model ${\mathbf{S}}_i^{\ast }$ has A arrows only to itself and to $(b,Pub)$. Indeed, the model is

What we have drawn is the part of the model accessible from the points shown. We also have not drawn the reflexive A arrows. Notice that there are no B arrows whatsoever. As before, p is true at all points accept $(b,Pub)$. This model is bisimilar to

Again, we have omitted the A loops on both points. The same happens with ${\widehat{\mathbf{T}}}_n$; the edge $a\stackrel{A}{⟶}{c}_1$ in ${\mathbf{T}}_n$ does not change things. Note that the bisimulations relate $(c_k,Pub)$ to $(a,Pub)$. The bisimulation shows the same equivalences (22) which we saw above, and this leads to the desired equivalences in (23).

Case IV: $({\mathbf{S}}_n,a)\vDash \phi$, $({\mathbf{S}}_n,b)\vDash \phi$, and for all ℓ such that $1\le \mathcal{\ell }\le n$, $({\mathbf{S}}_n,c_{\mathcal{\ell }})\vDash \phi$. That is, φ holds at all worlds of ${\mathbf{S}}_n$. Recall that $n-k\ge \left|\psi \right|$. So our induction hypothesis tells us that the following are equivalent

$$({\mathbf{S}}_n,a)\vDash \psi ({\mathbf{S}}_n,c_k)\vDash \psi ({\mathbf{T}}_n,a)\vDash \psi$$

(24)

In this case, the models ${\mathbf{S}}_n$ and ${\mathbf{S}}_n^{\ast }$ are isomorphic, via $x\mapsto (Pub,x)$. That is, we are making a public announcement of a sentence φ that holds at all worlds of our model ${\mathbf{S}}_n$. But in this case we claim that φ is also true at all worlds x of ${\mathbf{T}}_n$. This follows from (9) for $x\ne a$, and for $x=a$ it follows from (20) and the first assumption in this case. So ${\mathbf{T}}_n$ and ${\mathbf{T}}_n^{\ast }$ are isomorphic, again via $x\mapsto (Pub,x)$. Thus, we have the equivalences in (22). These, together with those in (20), imply those in (23), once again.

This completes the induction, and, hence, the proof of our lemma. □

It follows from what we have seen that our sentence $\chi \equiv \langle {Pri}^{A}p,\mathsf{true}\rangle {\diamond }_A^{\ast }{\diamond }_B\neg p$ is not equivalent to any single sentence of ${\mathcal{L}}_1\left({\mathbf{\Sigma }}_{\mathrm{pub}}\right)$. We would like to see that some sentence of ${\mathcal{L}}_1\left({\mathbf{\Sigma }}_{\mathrm{pri}}\right)$ is not equivalent to any set of sentences of ${\mathcal{L}}_1\left({\mathbf{\Sigma }}_{\mathrm{pub}}\right)$. For this, we add a ${\diamond }_A$ and consider ${\diamond }_A\langle {Pri}^{A}p,\mathsf{true}\rangle {\diamond }_A^{\ast }{\diamond }_B\neg p$. We begin with a general model-theoretic construction which will be used in the remainder of this section.

Definition 6.8. 

Let I be any set; let $A\in \mathcal{A}$; and for each $i\in I$, let $(H_i,h_i)$ be a model-world pair. Let h be a new world. Take disjoint copies of the $H_i$’s and add an A arrow from h to each $h_i$. All other arrows are within the $H_i$’s and stay the same as in $H_i$. No atomic sentences are true at h. Atomic sentences true in the worlds belonging to the copy of $H_i$ in ${⨁}_{i\in I}(H_i,h_i)$ are precisely those true at the corresponding worlds of $H_i$.

Lemma 6.9. 

Let φ be a sentence in ${\mathcal{L}}_1\left({\mathbf{\Sigma }}_{pub}\right)$. Let I be any set, and for $i\in I$, let $(H_i,h_i)$ and $(K_i,k_i)$ be model-world pairs. Assume that for all $i\in I$, $(H_i,h_i)$ and $(K_i,k_i)$ agree on all $\psi \in {\mathcal{L}}_1\left({\mathbf{\Sigma }}_{pub}\right)$ with $\left|\psi \right|\le \left|\phi \right|$. Then, $({⨁}_{i\in I}(H_i,h_i),h)$ and $({⨁}_i(K_i,k_i),k)$ agree on φ.

Proof. 

By induction on φ. It is clear for atomic sentences. The induction steps for Boolean connectives are trivial. We omit the easy arguments for the induction steps for ⋄ and ${\diamond }^{\ast }$ with various subscripts. It remains to consider the case when $\phi =\left[Pub{\phi }_1\right]{\phi }_2$. (The cases where we announce to $\left\{A\right\}$ or to $\left\{B\right\}$ are similar.) Fix I, and $(H_i,h_i)$ and $(K_i,k_i)$ for $i\in I$, and assume that these agree on sentences ψ with $\left|\psi \right|\le |\left[Pub{\phi }_1\right]{\phi }_2|=max(|{\phi }_1|,|{\phi }_2\left|\right)$. In particular, for each $i\in I$, $(H_i,h_i)\vDash {\phi }_1$ if and only if $(K_i,k_i)\vDash {\phi }_1$. Let

$$J=\{i\in I:(H_i,h_i)\vDash {\phi }_1\}=\{i\in I:(K_i,k_i)\vDash {\phi }_1\}.$$

For $i\in J$, let $(H_i,h_i^{\prime })$ and $(K_i^{\prime },k_i^{\prime })$ be obtained by “updating $(H_i,h_i)$ and $(K_i,k_i)$ by $\left[Pub{\phi }_1\right]$”. That is,

$$H_i^{\prime }=H_i\otimes ({\mathbf{\Sigma }}_{\mathrm{pub}},Pub,{\phi }_1)$$

and similarly for $K_i^{\prime }$. By our semantics of public announcements for all $i\in J$, $(H_i,h_i^{\prime })$ and $(K_i^{\prime },k_i^{\prime })$ agree on ${\phi }_2$. Therefore, by our inductive hypothesis

$$(\underset{i\in J}{⨁}{H}_i^{\prime },h)\vDash {\phi }_2\mathrm{iff}(\underset{i\in J}{⨁}{K}_i^{\prime },k)\vDash {\phi }_2.$$

However,

$$(\underset{i\in I}{⨁}{H}_i,h)\vDash \phi \mathrm{iff}(\underset{i\in I}{⨁}{H}_i,h)\vDash {\phi }_1\mathrm{implies}(\underset{i\in J}{⨁}{H}_i^{\prime },h^{\prime })\vDash {\phi }_2,$$

and

$$(\underset{i\in I}{⨁}{K}_i,k^{\prime })\vDash \phi \mathrm{iff}(\underset{i\in I}{⨁}{K}_i,k)\vDash {\phi }_1\mathrm{implies}(\underset{i\in J}{⨁}{K}_i^{\prime },k^{\prime })\vDash {\phi }_2,$$

and we are done. □

At long last, we complete the proof of Theorem 6.6.

Recall that χ is $\langle {Pri}^{A}p,\mathsf{true}\rangle {\diamond }_A^{\ast }{\diamond }_B\neg p$. Assume towards a contradiction that the sentence at the end of our theorem, ${\diamond }_A\chi$, was equivalent to a set Φ of sentences in ${\mathcal{L}}_1\left({\mathbf{\Sigma }}_{\mathrm{pub}}\right)$. Let N be the set of natural numbers $\ge 1$. For each $i\in N$, consider ${\mathbf{S}}_i$ and ${\mathbf{T}}_i$ from Definition 3.1. Let $s_i=a$. In this notation, $({\mathbf{S}}_i,s_i)⊭\chi$. Also, writing $t_i$ for a, we also have $({\mathbf{T}}_i,t_i)\vDash \chi$. Moreover, for all i, $({\mathbf{S}}_i,s_i)$ and $({\mathbf{T}}_i,t_i)$ agree on sentences of ${\mathcal{L}}_1\left({\mathbf{\Sigma }}_{\mathrm{pub}}\right)$ of rank $\le i-1$. (We are using Lemma 6.7 with $k=1$.)

We consider $({⨁}_{i\in N}{S}_i,s)$ from above, with the new point being called s. Notice that $({⨁}_{i\in N}{S}_i,s)⊭{\diamond }_A\chi$. So, we have some ${\phi }^{\ast }\in \mathsf{\Phi }$ such that $(⨁S_i,s)⊭{\phi }^{\ast }$. Let $n^{\ast }=\left|{\phi }^{\ast }\right|+1$. Let $({\mathbf{S}}_i^{\prime },s_i^{\prime })$ be $({\mathbf{S}}_i,s_i)$ for $i\ne n^{\ast }$, and let $({\mathbf{S}}_{n^{\ast }},s_{n^{\ast }}^{\prime })$ be $({\mathbf{T}}_{n^{\ast }},t_{n^{\ast }})$. Then, for all i, $({\mathbf{S}}_i,s_i)$ and $({\mathbf{S}}_i^{\prime },s_i^{\prime })$ agree on all sentences ψ of ${\mathcal{L}}_1\left({\mathbf{\Sigma }}_{\mathrm{pub}}\right)$ with $\left|\psi \right|\le n^{\ast }-1=\left|{\phi }^{\ast }\right|$. By Lemma 6.9, $({⨁}_{i\in N}{S}_i,s)$ and $({⨁}_{i\in N}{S}_i^{\prime },s^{\prime })$ agree on ${\phi }^{\ast }$. (In this, $s^{\prime }$ is the new point in $({⨁}_{i\in N}{S}_i^{\prime },s^{\prime })$.) This tells us that $({⨁}_{i\in N}{S}_i^{\prime },s^{\prime })⊭{\phi }^{\ast }$. A fortiori, $({⨁}_{i\in N}{S}_i^{\prime },s^{\prime })⊭{\diamond }_A\chi$. Since $s^{\prime }\stackrel{A}{⟶}{s}_{n^{\ast }}$ in this model, we see that $({\mathbf{T}}_{n^{\ast }},t_{n^{\ast }})⊭\chi$. But this contradicts a fact which we recalled above.

6.4. $\mathcal{L}\left({\mathbf{\Sigma }}_{pub}\right)$ Lacks the Finite-Model Property

We conclude with a result on iterating epistemic actions. We gave a semantics of sentences of the form $\left[{\alpha }^{\ast }\right]\phi$ earlier in the paper. The ability to iterate actions is useful in algorithms and even in informal presentations of scenarios. As it happens, the iteration operation on actions makes our systems quite expressive, so much so that the finite-model property fails for ${\mathcal{L}}_1(\mathbf{\Sigma })$ as soon as Σ contains public announcements.

Proposition 6.10. 

${[Pub\diamond \mathsf{true}]}^{\ast }\diamond \square \mathsf{false}$ is satisfiable, but not in any finite model.

Proof. 

A state s in a model $\mathbf{S}$ is called an end state if s has no successors. For each model $\mathbf{S}$, let ${\mathbf{S}}^{\prime }$ be the same model, except with the end states removed. ${\mathbf{S}}^{\prime }$ is isomorphic to what we have written earlier as $\mathbf{S}\otimes (Pub\diamond \mathsf{true})$, that is, the result of publically announcing that some world is possible. So we see that our sentence ${[Pub\diamond \mathsf{true}]}^{\ast }\diamond \square \mathsf{false}$ holds of s just in case the following holds for all n:

• $s\in {\mathbf{S}}^{\left(n\right)}$, the n-fold application of the derivative operation to $\mathbf{S}$.
• s has some child which is an end node (and, hence, t would not belong to ${\mathbf{S}}^{(n+1)}$).

It is clear that any model of ${[Pub\diamond \mathsf{true}]}^{\ast }\diamond \square \mathsf{false}$ must be infinite, since the sets $S^{(n+1)}\setminus S^{\left(n\right)}$ are pairwise disjoint and non-empty.

There are well-known models of ${[Pub\diamond \mathsf{true}]}^{\ast }\diamond \square \mathsf{false}$. One would be the set of decreasing sequences of natural numbers, with $s\to t$ if t is a one-point extension of s. The end nodes are the sequences that end in 0. For each n, ${\mathbf{S}}^{\left(n\right)}$ is the submodel consisting of the sequences which end in n. □

This has several dramatic consequences for this work. First, it means that the logics cannot be translated into the modal mu-calculus, since that logic is known to have the finite-model property. More importantly, we have the following extension of this result:

Theorem 6.11. 

(Miller and Moss [14]). Concerning $\mathcal{L}\left({\mathbf{\Sigma }}_{pub}\right)$:

1. 

$\{\phi :\phi issatisfiable\}$ is ${\Sigma }_1^1$-complete.

2. 

$\{\phi :\phi is satisfiable on a finite \left(tree\right) model\}$ is ${\Sigma }_1^0$-complete.

Indeed, these even hold when $\mathcal{L}\left({\mathbf{\Sigma }}_{\mathrm{pub}}\right)$ is replaced by small fragments, such as the fragment built from $[Pub\diamond \mathsf{true}]$, ${\diamond }^{\ast }$, ⋄, and Boolean connectives (yet without atomic sentences); or, the fragment built from arbitrary iterated relativizations and modal logic (without ${\diamond }^{\ast }$). These negative results go via reduction from domino problems.

The upshot is that logics which allow for arbitrary finite iterations of epistemic actions are not going to be axiomatizable.

We feel that our results on expressive power are just a sample of what could be done in this area. We did not investigate the next natural questions. These questions have to do with notions of “suspicion” and “common knowledge of suspicion”. It would take us too far afield to mention them here, but one could see, for example, Refs. [6,21] for precise definitions. Do announcements with suspicious outsiders extend the expressive power of modal logic with all secure private announcements and common knowledge operators? And, then, do announcements with common knowledge of suspicion add further expressive power?

6.5. Conclusions

This paper advanced the subject of dynamic epistemic logic (DEL) by introducing logical systems for the logical languages which it studied and also by obtaining a number of results about those logical systems. Prior to this paper, there had been logical systems: see, for example, [1,2,3,4]. These were mainly interested in what has become known as public-announcement logic (PAL), and while these papers point out forcefully that common knowledge was an important topic for the area, they did not obtain completeness theorems for PAL with common knowledge. Our advance on these was (a) to add to PAL the ability to express a much wider array of epistemic actions; (b) to use action signatures in the syntax, and updates, program models, and the update product in the semantics; and (c) to obtain the completeness of the all the logical systems proposed, including common-knowledge operators. This paper did not go into much detail on why one would want to add epistemic operators beyond public announcement; this was done in [6,21] and many other papers. It did formulate logical systems as desired; a look at the first three sections of this paper shows that this formulation takes a lot of work. It also obtained the completeness results for these logical systems, and it did so by calling on results on the canonical action model and also results in term rewriting theory. Those particular results have not been superseded: while others (for example, [7]) have obtained completeness theorems, the logics involved were different, and the proofs also were different. As a final contribution, this paper was perhaps the first to obtain expressive-power results. In addition to being mathematically interesting, they suggest that the large amount of work needed to formulate the syntax and semantics of the logics in this paper is worthwhile. For example, since the logic of private announcements goes beyond what could be expressed in PAL, one really needs a bigger logical system if one wants a general account of private announcements.

An early version of this paper, and several other papers, played an important part in advancing the DEL area. At the present time (2023), there are over 1000 references to [5], the first version of this paper. It is beyond anyone’s ability to look at all of them, regardless of how (or even whether) they used the ideas here or modified them. We know that many of the important contributions to the area of dynamic epistemic logic (broadly conceived) do go beyond what we did here. They modify the overall framework, and they aim at applications which go beyond what one could treat using what we did. Still, we maintain that the published (and unpublished) preliminary versions of this paper made an important contribution to the area. We also think that the current, more polished version is a smaller but still significant further contribution, adding both more technical results and a better, clearer formulation of the main concepts and setting of contemporary dynamic epistemic logic.