format: text

text:
# Complete Axiomatizations for Reasoning About Knowledge and Time11footnote 1This paper incorporates results from [HV86], [HV88b], and [Mey94].

## 1 Introduction

It has recently been argued that knowledge is a useful tool for analyzing the behavior and interaction of agents in a distributed system (see \[FHMV95\] and the references therein). When analyzing a system in terms of knowledge, not only is the current state of knowledge of the agents in the system relevant, but also how that state of knowledge changes over time. A formal propositional logic of knowledge and time was first proposed by Sato \[Sat77\]; many others have since been proposed \[FHV91, Leh84, LR86, PR85, Spa90\]. Unfortunately, while these logics often use similar or identical notation, they differ in a number of significant respects.

In \[HV89\], logics for knowledge and time were categorized along two major dimensions: the language used and the assumptions made on the underlying distributed system. The properties of knowledge in a system turn out to depend in subtle ways on these assumptions. The assumptions considered in \[HV89\] concern whether agents have unique initial states, operate synchronously or asynchronously, have perfect recall, and whether they satisfy a condition called no learning. There are 16 possible combinations of these assumptions on the underlying system. Together with 6 choices of language, this gives us 96 logics in all. All the logics considered in the papers mentioned above fit into the framework. In \[HV89, HV88a\], the complexity of these logics is completely characterized; the results of these papers show how the subtle interplay of the parameters can have a tremendous impact on complexity. The complexity results show that some of these logics cannot be characterized axiomatically, since the set of valid formulas for these logics is not recursively enumerable. Of these 96 logics, 48 involve linear time and 48 involve branching time. (The distinction between linear and branching time essentially amounts to whether or not we can quantify over the possible executions of a program.) To keep this paper to manageable length, we focus here on the linear time logics, and provide axiomatic characterizations of all the linear time logics for which an axiomatization is possible at all (i.e., for those logics for which the set of valid formulas is r.e.).

The rest of this paper is organized as follows. In the next section, we provide formal definitions for the logics we consider. In Section 2, we review the syntax and semantics of all the logics of knowledge and time that we consider here. In particular, we review the four assumptions on the underlying system that we axiomatize in this paper. In Section 3, we state the axioms for all the systems. In Section 4, we introduce the notion of enriched systems, which form the basis for all our completeness proofs. In Section 5, we prove soundness and completeness for the axiom systems described in Section 3. The definition of no learning that we use here is slightly different from that used in \[FHMV95, HV86\], although they agree in many cases of interest. We discuss the motivation for our change in Section 6. We conclude with some further discussion in Section 7.

## 2 The Formal Model: Language and Systems

The material in this section is largely taken from \[HV89\], and is repeated here to make this paper self-contained. The reader is encouraged to consult \[HV89\] for further details and motivation.

The logics we are considering are all propositional. Thus, we start out with primitive propositions $`p`$, $`q`$, …and we close the logics under negation and conjunction, so that if $`\phi `$ and $`\psi `$ are formulas, so are $`\neg \phi `$ and $`\phi \psi `$. In addition, we close off under modalities for knowledge and time, as discussed below. As usual, we view true as an abbreviation for $`\neg (p\neg p)`$, $`\phi \psi `$ as an abbreviation for $`\neg (\neg \phi \neg \psi )`$, and $`\phi \psi `$ as an abbreviation for $`\neg \phi \psi `$.

If we have $`m`$ agents (in distributed systems applications, this would mean a system with $`m`$ processors), we add the modalities $`K_1`$, …, $`K_m`$. Thus, if $`\phi `$ is a formula, so is $`K_i\phi `$ (read “agent $`i`$ knows $`\phi `$”). We take $`L_i\phi `$ to be an abbreviation for $`\neg K_i\neg \phi `$. In some cases we also want to talk about common knowledge, so we add the modalities $`E`$ and $`C`$ into the language; $`E\phi `$ says that everyone knows $`\phi `$, while $`C\phi `$ says $`\phi `$ is common knowledge.

There are two basic temporal modalities (sometimes called operators or connectives): a unary operator $``$ and a binary operator $`U`$. Thus, if $`\phi `$ and $`\psi `$ are formulas, then so are $`\phi `$ (read “next time $`\phi `$”) and $`\phi U\psi `$ (read “$`\phi `$ until $`\psi `$”). $`\mathrm{}\phi `$ is an abbreviation for $`\text{true}U\phi `$, while $`\mathrm{}\phi `$ is an abbreviation for $`\neg \mathrm{}\neg \phi `$. Intuitively, $`\phi `$ says that $`\phi `$ is true at the next point (one time unit later), $`\phi U\psi `$ says that $`\phi `$ holds until $`\psi `$ does, $`\mathrm{}\phi `$ says that $`\phi `$ is eventually true (either in the present or at some point in the future), and $`\mathrm{}\phi `$ says that $`\phi `$ is always true (in the present and at all points in the future). In \[HV89\], branching time operators are also considered, which have quantifiers over runs. For example, $``$ is a branching time operator such that $`\phi `$ is true when $`\phi `$ is true for all possible futures. Since we do not consider branching time operators in this paper, we omit the formal definition here. We take $`\text{CKL}_m`$ to be the language for $`m`$ agents with all the modal operators for knowledge and linear time discussed above; $`\text{KL}_m`$ is the restricted version without the common knowledge operator.

A system for $`m`$ agents consists of a set $``$ of runs, where each run $`r`$ is a function from $`IN`$ to $`L^{m+1}`$, where $`L`$ is some set of local states. There is a local state for each agent, together with a local state for the environment; intuitively, the environment keeps track of all the relevant features of the system not described by the agents’ local states, such as messages in transit but not yet delivered. Thus, $`r(n)`$ has the form $`l_e,l_1,\mathrm{},l_m`$, where $`l_e`$ is the state of the environment, and $`l_i`$ is the local state of agent $`i`$, for $`i=1,\mathrm{},m`$; such a tuple is called a global state. (Formally, we could view a system as a tuple $`(,L,m)`$, making the $`L`$ and $`m`$ explicit. We have chosen not to do so in order to simplify notation. The $`L`$ and $`m`$ should always be clear from context.) An interpreted system $``$ for $`m`$ agents is a tuple $`(,\pi )`$ where $``$ is a system for $`m`$ agents, and $`\pi `$ maps every point $`(r,n)\times IN`$ to a truth assignment $`\pi (r,n)`$ to the primitive propositions (so that $`\pi (r,n)(p)\{\mathrm{𝐭𝐫𝐮𝐞},\mathrm{𝐟𝐚𝐥𝐬𝐞}\}`$ for each primitive proposition $`p`$).222Note that while we are being consistent with \[HV89\] here, in \[FHMV95\], $`\pi `$ is taken to be a function from global states (not points) to truth values. Essentially, this means that in \[FHMV95\] a more restricted class of structures is considered, where $`\pi `$ is forced to be the same at any two points associated with the same global state. Clearly our soundness results hold in the more restricted class of structures. It is also easy to see that our completeness results hold in the more restricted class too. All our completeness proofs have (or can be easily modified to have) the property that a structure is constructed where each point is associated with a different global state, and thus is an instance of the more restrictive structures used in \[FHMV95\].

We now give semantics to $`\text{CKL}_m`$ and $`\text{KL}_m`$. Given an interpreted system $`=(,\pi )`$, we write $`(,r,n)\phi `$ if the formula $`\phi `$ is true at (or satisfied by) the point $`(r,n)`$ of interpreted system $``$. We define $``$ inductively for formulas of $`\text{CKL}_m`$ (for $`\text{KL}_m`$ we just omit the clauses involving $`C`$ and $`E`$). In order to give the semantics for formulas of the form $`K_i\phi `$, we need to introduce one new notion. If $`r(n)=l_1,\mathrm{},l_m`$, $`r^{}(n^{})=l_1^{},\mathrm{},l_m^{}`$, and $`l_i=l_i^{}`$, then we say that $`r(n)`$ and $`r^{}(n^{})`$ are indistinguishable to agent $`i`$ and write $`(r,n)_i(r^{},n^{})`$. Of course, $`_i`$ is an equivalence relation on global states (inducing an equivalence relations on points). $`K_i\phi `$ is defined to be true at $`(r,n)`$ exactly if $`\phi `$ is true at all the points whose associated global state is indistinguishable to $`i`$ from that of $`(r,n)`$. We proceed as follows:

* $`(,r,n)p`$ for a primitive proposition $`p`$ iff $`\pi (r,n)(p)=\mathrm{𝐭𝐫𝐮𝐞}`$
* $`(,r,n)\phi \psi `$ iff $`(,r,n)\phi `$ and $`(,r,n)\psi `$
* $`(,r,n)\neg \phi `$ iff $`(,r,n)`$ $`\vDash ̸`$ $`\phi `$
* $`(,r,n)K_i\phi `$ iff $`(,r^{},n^{})\phi `$ for all $`(r^{},n^{})`$ such that $`(r,n)_i(r^{},n^{})`$
* $`(,r,n)E\phi `$ iff $`(,r^{},n^{})K_i\phi `$ for $`i=1,\mathrm{},m`$
* $`(,r,n)C\phi `$ iff $`(,r^{},n^{})E^k\phi `$, for $`k=1,2,\mathrm{}`$ (where $`E^1\phi =E\phi `$ and $`E^{k+1}\phi =EE^k\phi `$)
* $`(,r,n)\phi `$ iff $`(,r,n+1)\phi `$
* $`(,r,n)\phi U\psi `$ iff there is some $`n^{}n`$ such that $`(,r,n^{})\psi `$, and for all $`n^{\prime \prime }`$ with $`nn^{\prime \prime }<n^{}`$, we have $`(,r,n^{\prime \prime })\phi `$.

There is a graphical interpretation of the semantics of $`C`$ which we shall find useful in the sequel. Fix an interpreted system $``$. A point $`(r^{},n^{})`$ in $``$ is reachable from a point $`(r,n)`$ if there exist points $`(r_0,n_0),\mathrm{},(r_k,n_k)`$ such that $`(r,n)=(r_0,n_0)`$, $`(r^{},n^{})=(r_k,n_k)`$, and for all $`j=0,\mathrm{},k1`$ there exists $`i`$ such that $`(r_j,n_j)_i(r_j+1,n_j+1)`$. The following result is well known (and easy to check).

###### Lemma 2.1

: \[HM92\] $`(,r,n)C\phi `$ iff $`(,r^{},n^{})\phi `$ for all points $`(r^{},n^{})`$ reachable from $`(r,n)`$.

As usual, we define a formula $`\phi `$ to be valid with respect to a class $`𝒞`$ of interpreted systems iff $`(,r,n)\phi `$ for all interpreted systems $`𝒞`$ and points $`(r,n)`$ in $``$. A formula $`\phi `$ is satisfiable with respect to $`𝒞`$ iff for some $`𝒞`$ and some point $`(r,n)`$ in $``$, we have $`(,r,n)\phi `$.

We now turn our attention to formally defining the classes of interpreted systems of interest. For some of these definitions, it will be useful to give a number of equivalent presentations.

Perfect recall means, intuitively, that an agent’s local state encodes everything that has happened (for that agent’s point of view) thus far in the run. To make this precise, define agent $`i`$’s local-state sequence at the point $`(r,n)`$ to be the sequence $`l_0,\mathrm{},l_k`$ of states that agent $`i`$ takes on in run $`r`$ up to and including time $`n`$, with consecutive repetitions omitted. For example, if from time 0 through 4 in run $`r`$ agent $`i`$ goes through the sequence $`l,l,l^{},l,l`$ of states, its history at $`(r,4)`$ is just $`l,l^{},l`$. Roughly speaking, agent $`i`$ has perfect recall if it “remembers” its history. More formally, we say that agent $`i`$ has perfect recall (alternatively, agent $`i`$ does not forget) in system $``$ if at all points $`(r,n)`$ and $`(r^{},n^{})`$ in $``$, if $`(r,n)_i(r^{},n^{})`$, then $`r`$ has the same local-state sequence at both $`(r,n)`$ and $`(r^{},n^{})`$.

There are a number of equivalent characterizations of perfect recall. One characterization that will prove particularly useful in the comparison with the concept of no learning, which we are about to define, is the following. Let $`S=(s_0,s_1,s_2,\mathrm{})`$ and $`T=(t_0,t_1,t_2,\mathrm{})`$ be two (finite or infinite) sequences and let $``$ be a relation on the elements of $`S`$ and $`T`$. Then we say that $`S`$ and $`T`$ are $``$-concordant if there is some $`k`$ ($`k`$ may be $`\mathrm{}`$) and nonempty consecutive intervals $`S_1,\mathrm{},S_k`$ of $`S`$ and $`T_1,\mathrm{},T_k`$ of $`T`$ such that for all $`sS_j`$ and $`tT_j`$, we have $`st`$, for $`j=1,\mathrm{},k`$.

###### Lemma 2.2

: \[HV86, Mey94\] The following are equivalent.

* Agent $`i`$ has perfect recall in system $``$.
* For all points $`(r,n)_i(r^{},n^{})`$ in $``$, $`((r,0),\mathrm{},(r,n))`$ is $`_i`$-concordant with $`((r^{},0),\mathrm{},(r^{},n^{}))`$.
* For all points $`(r,n)_i(r^{},n^{})`$ in $``$, if $`n>0`$, then either $`(r,n1)_i(r^{},n^{})`$ or there exists a number $`l<n^{}`$ such that $`(r,n1)_i(r^{},l)`$ and for all $`k`$ with $`l<kn^{}`$ we have $`(r,n)_i(r^{},k)`$.
* For all points $`(r,n)_i(r^{},n^{})`$ in $``$, if $`kn`$, then there exists $`k^{}n^{}`$ such that $`(r,k)_i(r^{},k^{})`$.

Proof: The implications from (a) to (b), from (b) to (c) and from (c) to (d) are straightforward. The implication from (d) to (a) can be proved by a straightforward induction on $`n+n^{}`$.

This lemma shows that perfect recall requires an unbounded number of local states in general, since agent $`i`$ may have an infinite number of distinct histories in a given system. A system where agent $`i`$ has perfect recall is shown in Figure 1, where the vertical lines denote runs (with time 0 at the top) and all points that $`i`$ cannot distinguish are enclosed in the same region.

We remark that the official definition of perfect recall given here is taken from \[FHMV95\]. In \[HV86\], part (d) of Lemma 2.2 was taken as the definition of perfect recall (which was called no forgetting in that paper).

Roughly speaking, no learning is the dual notion to perfect recall. Perfect recall says that if the agent considers run $`r^{}`$ possible at the point $`(r,n)`$, in that there is a point $`(r^{},n^{})`$ that the agent cannot distinguish from $`(r,n)`$, then the agent must have considered $`r^{}`$ possible at all times in the past (i.e., at all points $`(r,k)`$ with $`kn`$); it is not possible that the agent once considered $`r^{}`$ impossible and then forgot this fact. No learning says that if the agent considers $`r^{}`$ possible at $`(r,n)`$, then the agent will consider $`r^{}`$ possible at all times in the future; the agent will not learn anything that will allow him to distinguish $`r`$ from $`r^{}`$. More formally, we define an agent’s future local-state sequence at $`(r,n)`$ to be the sequence of local states $`l_0,l_1,\mathrm{}`$ that the agent takes on in run $`r`$, starting at $`(r,n)`$, with consecutive repetitions omitted. We say agent $`i`$ does not learn in system $``$ if at all points $`(r,n)`$ and $`(r^{},n^{})`$ in $``$, if $`(r,n)_i(r^{},n^{})`$, then $`r`$ has the same future local-state sequence at both $`(r,n)`$ and $`(r^{},n^{})`$.

Just as with perfect recall, there are a number of equivalent formulations of no learning.

###### Lemma 2.3

: The following are equivalent.

* Agent $`i`$ does not learn in system $``$.
* For all points $`(r,n)_i(r^{},n^{})`$ in $``$, $`((r,n),(r,n+1),\mathrm{})`$ is $`_i`$-concordant with $`((r^{},n^{}),(r^{},n^{}+1),\mathrm{})`$.
* For all points $`(r,n)_i(r^{},n^{})`$ in $``$, either $`(r,n+1)_i(r^{},n^{})`$ or there exists a number $`l>n^{}`$ such that $`(r,n+1)_i(r^{},l)`$ and for all $`k`$ with $`l>kn^{}`$ we have $`(r,n)_i(r^{},k)`$.

Notice that we have no analogue to part (d) of Lemma 2.2 in Lemma 2.3 (where $``$ is replaced by $``$). The analogue of (d) is strictly weaker than (a), (b), and (c), although they are equivalent in synchronous systems (which we are about to define formally). It was just this analogue of (d) that was used to define no learning in \[HV86, HV89\]. We examine the differences between the notions carefully in Section 6, where we provide more motivation for the definition chosen here.

In a synchronous system, we assume that every agent has access to a global clock that ticks at every instant of time, and the clock reading is part of its state. Thus, in a synchronous system, each agent always “knows” the time. More formally, we say that a system $``$ is synchronous if for all agents $`i`$ and all points $`(r,n)`$ and $`(r^{},n^{})`$, if $`(r,n)_i(r^{},n^{})`$, then $`n=n^{}`$.333 We remark that in \[HV86\], a slightly weaker definition is given: There, a system is said to be synchronous if for all runs $`r`$, if $`(r,n)_i(r,n^{})`$ then $`n=n^{}`$. It is easy to show (by induction on $`n`$) that the two definitions are equivalent for systems where agents have perfect recall. In general, however, they are different. The definition given here is the one used in \[FHMV95, HV89\]. Observe that in a synchronous system where $`(r,n)_i(r^{},n)`$, an easy induction on $`n`$ shows that if $`i`$ has perfect recall and $`n>0`$, then $`(r,n1)_i(r^{},n1)`$, while if $`i`$ does not learn, then $`(r,n+1)_i(r^{},n+1)`$.

Finally, we say that a system $``$ has a unique initial state if for all runs $`r,r^{}`$, we have $`r(0)=r^{}(0)`$. Thus, if $``$ is a system with a unique initial state, then we have $`(r,0)_i(r^{},0)`$ for all runs $`r,r^{}`$ in $``$ and all agents $`i`$.

We say that $`=(,\pi )`$ is an interpreted system where agents have perfect recall (resp., agents do not learn, time is synchronous, there is a unique initial state) exactly if $``$ is a system with that property. We use $`𝒞_m`$ to denote the class of all interpreted systems for $`m`$ agents, and add the superscripts $`\mathrm{𝑛𝑙}`$, $`\mathrm{𝑝𝑟}`$, $`\mathrm{𝑠𝑦𝑛𝑐}`$, and $`\mathrm{𝑢𝑖𝑠}`$ to denote particular subclasses of $`𝒞_m`$. Thus, for example, we use $`𝒞_m^{\mathrm{𝑛𝑙},\mathrm{𝑝𝑟}}`$ to denote the set of all interpreted systems with $`m`$ agents that have perfect recall and do not learn. We omit the subscript $`m`$ when it is clear from context.

The results of \[HV89, HV88a\] (some of which are based on earlier results of Ladner and Reif \[LR86\]) are summarized in Table 1. For $`\phi \text{KL}_m`$, we define $`\text{ad}(\phi )`$ to be the greatest number of alternations of distinct $`K_i`$’s along any branch in $`\phi `$’s parse tree. For example, $`\text{ad}(K_1\neg K_2K_1p)=3`$; temporal operators are not considered, so that $`\text{ad}(K_1\mathrm{}K_1p)=1`$. (In Table 1, we do not consider the language $`\text{CKL}_1`$. This is because if $`m=1`$, then $`C\phi `$ is equivalent to $`K_1\phi `$. Thus, $`\text{CKL}_1`$ is equivalent to $`\text{KL}_1`$.) We omit the definitions of complexity classes such as $`\mathrm{\Pi }_1^1`$ and nonelementary time $`(\text{ex}(\text{ad}(\phi )+1,c|\phi |)`$ here. (Note that $`c`$ is a constant in the latter expression.) All that matters for our purposes is that for the cases where the complexity is $`\mathrm{\Pi }_1^1`$ or co-r.e., there can be no recursive axiomatization; the validity problem is too hard. We provide complete axiomatizations here for the remaining cases.

## 3 Axiom Systems

In this section, we describe the axioms and inference rules that we need for reasoning about knowledge and time for various classes of systems, and state the completeness results. The proofs of these results are deferred to Section 5.

For reasoning about knowledge alone, the following system, with axioms K1–K5 and rules of inference R1–R2, is well known to be sound and complete \[FHMV95, Hin62\]:

* K1. All tautologies of propositional logic
* K2. $`K_i\phi K_i(\phi \psi )K_i\psi `$, $`i=1,\mathrm{},m`$
* K3. $`K_i\phi \phi `$, $`i=1,\mathrm{},n`$
* K4. $`K_i\phi K_iK_i\phi `$, $`i=1,\mathrm{},m`$
* K5. $`\neg K_i\phi K_i\neg K_i\phi `$, $`i=1,\mathrm{},m`$
* R1. From $`\phi `$ and $`\phi \psi `$ infer $`\psi `$
* R2. From $`\phi `$ infer $`K_i\phi `$, $`i=1,\mathrm{},m`$

This axiom system is known as $`\mathrm{S5}_m`$.

For reasoning about the temporal operators individually, the following system (together with K1 and R1), is well known to be sound and complete \[FHMV95, GPSS80\]:

* T1. $`(\phi )(\phi \psi )\psi `$
* T2. $`(\neg \phi )\neg \phi `$
* T3. $`\phi U\psi \psi (\phi (\phi U\psi ))`$
* RT1. From $`\phi `$ infer $`\phi `$
* RT2. From $`\phi ^{}\neg \psi \phi ^{}`$ infer $`\phi ^{}\neg (\phi U\psi )`$

The system containing the above axioms and inference rules for both knowledge and time is called $`\mathrm{S5}_m^U`$. $`\mathrm{S5}_m^U`$ is easily seen to be sound for $`𝒞_m`$, the class of all systems for $`m`$ agents. Given that there is no necessary connection between knowledge and time in $`𝒞_m`$, it is perhaps not surprising that $`\mathrm{S5}_m^U`$ should be complete with respect to $`𝒞_m`$ as well. Interestingly, even if we impose the requirements of synchrony or uis, $`\mathrm{S5}_m^U`$ remains complete; our language is not rich enough to capture these conditions.

###### Theorem 3.1

: $`\mathrm{S5}_m^U`$ is a sound and complete axiomatization for the language $`\text{KL}_m`$ with respect to $`𝒞_m`$, $`𝒞_m^{\mathrm{𝑠𝑦𝑛𝑐}}`$, $`𝒞_m^{\mathrm{𝑢𝑖𝑠}}`$, and $`𝒞_m^{\mathrm{𝑠𝑦𝑛𝑐},\mathrm{𝑢𝑖𝑠}}`$, for all $`m`$.

We get the same lack of interaction between knowledge in the classes $`𝒞_m`$, $`𝒞_m^{\mathrm{𝑠𝑦𝑛𝑐}}`$, $`𝒞_m^{\mathrm{𝑢𝑖𝑠}}`$, and $`𝒞_m^{\mathrm{𝑠𝑦𝑛𝑐},\mathrm{𝑢𝑖𝑠}}`$ even when we add common knowledge. It is well known that the following two axioms and inference rule characterize common knowledge \[FHMV95, HM92\]:

* C1. $`E\phi _{i=1}^mK_i\phi `$
* C2. $`C\phi E(\phi C\phi `$)
* RC1. From $`\phi E(\psi \phi )`$ infer $`\phi C\psi `$

Let $`\mathrm{S5C}_m^U`$ be the result of adding C1, C2, and RC1 to $`\mathrm{S5}_m^U`$. We then have the following extension of Theorem 3.1.

###### Theorem 3.2

: $`\mathrm{S5C}_m^U`$ is a sound and complete axiomatization for the language $`\text{CKL}_m`$ with respect to $`𝒞_m`$, $`𝒞_m^{\mathrm{𝑠𝑦𝑛𝑐}}`$, $`𝒞_m^{\mathrm{𝑢𝑖𝑠}}`$, and $`𝒞_m^{\mathrm{𝑠𝑦𝑛𝑐},\mathrm{𝑢𝑖𝑠}}`$, for all $`m`$.

If we restrict attention to systems with perfect recall or no learning, then knowledge and time do interact. We start by stating five axioms of interest, and then discuss them.

* KT1. $`K_i\mathrm{}\phi \mathrm{}K_i\phi `$, $`i=1,\mathrm{},m`$
* KT2. $`K_i\phi K_i\phi `$, $`i=1,\mathrm{},m`$.
* KT3. $`K_i\phi _1(K_i\phi _2\neg K_i\phi _3)L_i((K_i\phi _1)U[(K_i\phi _2)U\neg \phi _3])`$, $`i=1,\mathrm{},m`$
* KT4. $`K_i\phi _1UK_i\phi _2K_i(K_i\phi _1UK_i\phi _2)`$, $`i=1,\mathrm{},m`$.
* KT5. $`K_i\phi K_i\phi `$, $`i=1,\mathrm{},m`$.

Axiom KT1 was first discussed by Ladner and Reif \[LR86\]. Informally, this axiom states that if a proposition is known to be always true, then it is always known to be true. It is not hard to show, using Lemma 2.2, that axiom KT1 holds with perfect recall, that is, KT1 is valid in $`𝒞_m^{\mathrm{𝑝𝑟}}`$. It was conjectured in an early draft of \[FHMV95\] that the system $`\mathrm{S5}_m^U+\mathrm{KT1}`$, would be complete for $`𝒞_m^{\mathrm{𝑝𝑟}}`$. However, it was shown in \[Mey94\] that this conjecture was false. To get completeness we need a stronger axiom: KT3.

It is not hard to see that KT3 is valid in systems with perfect recall. A formal proof is provided in Section 5, but we can give some intuition here. Suppose $`(,r,n)K_i\phi _1(K_i\phi _2\neg K_i\phi _3)`$. That means that $`(,r,n+1)\neg K_i\phi _3`$, so there must be some point $`(r^{},n^{})_i(r,n+1)`$ such that $`(,r^{},n^{})\neg \phi _3`$. Because agent $`i`$ has perfect recall, there must exist some $`k^{}n^{}`$ such that $`(r^{},k^{})_i(r,n)`$. It is not hard to show, using Lemma 2.2(c), that $`(,r^{},k^{})K_i\phi _1U(K_i\phi _2U\neg \phi _3)`$. It follows that $`(,r,n)L_i(K_i\phi _1U(K_i\phi _2U\neg \phi _3))`$.

In the presence of the other axioms, KT3 implies KT1.

###### Lemma 3.3

: KT1 is provable in $`\mathrm{S5}_m^U+\mathrm{KT3}`$.

Proof: Note that by purely temporal reasoning, we can show $`\mathrm{}\phi \mathrm{}\mathrm{}\phi `$. Using R2 and K2, this implies that $`K_i\mathrm{}\phi K_i\mathrm{}\mathrm{}\phi `$. Now if $`\phi _1=\phi _2=\mathrm{𝑡𝑟𝑢𝑒}`$, then KT3 simplifies to $`\neg K_i\phi _3\neg K_i\mathrm{}\phi _3`$. In particular, taking the contrapositive, substituting $`\phi _3=\mathrm{}\phi `$, and using T2, we obtain $`K_i\mathrm{}\mathrm{}\phi K_i\mathrm{}\phi `$, which yields $`K_i\mathrm{}\phi K_i\mathrm{}\phi `$ by the equivalence noted above. It is also straightforward to show that $`\mathrm{}\phi \phi `$, from which it follows, using K2 and R2, that $`K_i\mathrm{}\phi K_i\phi `$. The axiom KT1 now follows using the rule RT2.

KT3 turns out to be strong enough to give us completeness, with or without the condition uis.

###### Theorem 3.4

: $`\mathrm{S5}_m^U+\mathrm{KT3}`$ is a sound and complete axiomatization for the language $`\text{KL}_m`$ with respect to $`𝒞_m^{\mathrm{𝑝𝑟}}`$ and $`𝒞_m^{\mathrm{𝑝𝑟},\mathrm{𝑢𝑖𝑠}}`$, for all $`m`$.

Theorem 3.1 shows that requiring synchrony or uis does not have an impact when we consider the class of all systems—$`𝒞_m`$, $`𝒞_m^{\mathrm{𝑠𝑦𝑛𝑐}}`$, $`𝒞_m^{\mathrm{𝑢𝑖𝑠}}`$, and $`𝒞_m^{\mathrm{𝑠𝑦𝑛𝑐},\mathrm{𝑢𝑖𝑠}}`$ are all axiomatized by $`\mathrm{S5}_m^U`$—and Theorem 3.4 shows that adding uis does not have an impact in the presence of perfect recall. However, requiring synchrony does have an impact in the presence of perfect recall. It is easy to see that KT2 is valid in $`𝒞_m^{\mathrm{𝑝𝑟},\mathrm{𝑠𝑦𝑛𝑐}}`$, and it clearly is not valid in $`𝒞_m^{\mathrm{𝑝𝑟}}`$. Moreover, KT2 suffices for completeness in $`𝒞_m^{\mathrm{𝑝𝑟},\mathrm{𝑠𝑦𝑛𝑐}}`$; we do not need the complications of KT3.

###### Theorem 3.5

: $`\mathrm{S5}_m^U+\mathrm{KT2}`$ is a sound and complete axiomatization for the language $`\text{KL}_m`$ with respect to $`𝒞_m^{\mathrm{𝑝𝑟},\mathrm{𝑠𝑦𝑛𝑐}}`$ and $`𝒞_m^{\mathrm{𝑝𝑟},\mathrm{𝑠𝑦𝑛𝑐},\mathrm{𝑢𝑖𝑠}}`$, for all $`m`$.

KT4 is the axiom that characterizes no learning. More precisely, we have

###### Theorem 3.6

: $`\mathrm{S5}_m^U+\mathrm{KT4}`$ is a sound and complete axiomatization for the language $`\text{KL}_m`$ with respect to $`𝒞_m^{\mathrm{𝑛𝑙}}`$ for all $`m`$.

Unlike previous cases, the uis assumption is not innocuous in the presence of nl. For one thing, it is not hard to check that assuming uis leads to extra properties. Indeed, as Table 1 shows, if $`m2`$, then assuming a unique initial state along with no learning results in a class of systems that do not have a recursive axiomatic characterization, since the validity problem is co-r.e. On the other hand, if there is only one agent in the picture, things simplify. No learning together with uis implies perfect recall. Thus, we get

###### Theorem 3.7

: $`\mathrm{S5}_m^U+\mathrm{KT3}+\mathrm{KT4}`$ is a sound and complete axiomatization for the language $`\text{KL}_m`$ with respect to $`𝒞_m^{\mathrm{𝑛𝑙},\mathrm{𝑝𝑟}}`$ for all $`m`$. Moreover, it is a sound and complete axiomatization for the language $`\text{KL}_1`$ with respect to $`𝒞_1^{\mathrm{𝑛𝑙},\mathrm{𝑝𝑟},\mathrm{𝑢𝑖𝑠}}`$.

In synchronous systems with no learning, things again become simpler. KT5, the converse of KT2, suffices to characterize such systems.

###### Theorem 3.8

: $`\mathrm{S5}_m^U+\mathrm{KT5}`$ is a sound and complete axiomatization for the language $`\text{KL}_m`$ with respect to $`𝒞_m^{\mathrm{𝑛𝑙},\mathrm{𝑠𝑦𝑛𝑐}}`$.

Of course, it follows from Theorem 3.8 that KT4 can be derived in the system $`\mathrm{S5}_m^U+\mathrm{KT5}`$ (although this result takes some work to prove directly).

Not surprisingly, if we combine perfect recall, no learning, and synchrony, then KT2 and KT5 give us a complete axiomatization.

###### Theorem 3.9

: $`\mathrm{S5}_m^U+\mathrm{KT2}+\mathrm{KT5}`$ is a sound and complete axiomatization for the language $`\text{KL}_m`$ with respect to $`𝒞_m^{\mathrm{𝑛𝑙},\mathrm{𝑝𝑟},\mathrm{𝑠𝑦𝑛𝑐}}`$ for all $`m`$.

Finally, it can be shown that when we combine no learning, synchrony, and uis, then not only do all agents consider the same worlds possible initially, but they consider the same worlds possible at all times. As a result, the axiom $`K_i\phi K_j\phi `$ is valid in this case. This allows us to reduce to the single-agent case. Moreover, as we observed above, in the single-agent case, no learning and uis imply perfect recall. Thus, we get the following result.

###### Theorem 3.10

: $`\mathrm{S5}_m^U+\mathrm{KT2}+\mathrm{KT5}+\{K_i\phi K_1\phi \}`$ is a sound and complete axiomatization for the language $`\text{KL}_m`$ with respect to $`𝒞_m^{\mathrm{𝑛𝑙},\mathrm{𝑠𝑦𝑛𝑐},\mathrm{𝑢𝑖𝑠}}`$ and $`𝒞_m^{\mathrm{𝑛𝑙},\mathrm{𝑝𝑟},\mathrm{𝑠𝑦𝑛𝑐},\mathrm{𝑢𝑖𝑠}}`$ for all $`m`$.

A glance at Table 1 shows that we have now provided axiomatizations for all the cases where complete axiomatizations exist. (Notice that for the language $`\text{CKL}_m`$, if $`m=1`$, then common knowledge reduces to knowledge, while if $`m>1`$, then complete axiomatizations can exist only for $`𝒞_m`$, $`𝒞_m^{\mathrm{𝑠𝑦𝑛𝑐}}`$, $`𝒞_m^{uis}`$, $`𝒞_m^{sync,uis}`$, $`𝒞_m^{\mathrm{𝑛𝑙},\mathrm{𝑠𝑦𝑛𝑐},\mathrm{𝑢𝑖𝑠}}`$, and $`𝒞_m^{\mathrm{𝑛𝑙},\mathrm{𝑝𝑟},\mathrm{𝑠𝑦𝑛𝑐},\mathrm{𝑢𝑖𝑠}}`$. The first four cases were dealt with in Theorem 3.2, while in the last two, as we have observed, common knowledge reduces to the knowledge of agent 1.)

## 4 A Framework for Completeness Proofs

In this section we develop a general framework for completeness proofs that reduces the work required in each of the different completeness results to a single lemma.

A formula $`\psi `$ is said to be consistent in a logic $`L`$ if it is not the case that $`_L\neg \psi `$. For each of the pairs of logic $`L`$ and class of systems $`𝒞`$ we consider, the proof that $`L`$ is complete with respect to $`𝒞`$ proceeds by constructing for every formula $`\psi `$ consistent with respect to $`L`$, a system in $`𝒞`$ containing a point at which $`\psi `$ is true. All the results in this section hold for every logic containing $`\mathrm{S5}_m^U`$, except for Lemma 4.8, which mentions common knowledge. This lemma holds for every logic containing $`\mathrm{S5C}_m^U`$. Rather than mentioning the logic $`L`$ explicitly in each case, we just write $``$ rather than $`_L`$; the intended logic(s) will be clear from context. We also fix the formula $`\psi `$, which is assumed to be consistent with respect to $`L`$.

A finite sequence $`\sigma =i_1i_2\mathrm{}i_k`$ of agents, possibly equal to the null sequence $`ϵ`$, is called an index if $`i_li_{l+1}`$ for all $`l<k`$. We write $`|\sigma |`$ for the length $`k`$ of such a sequence; the null sequence has length equal to 0.

If $`S`$ is a set, and $`S^{}`$ is the set of all finite sequences over $`S`$, we define the absorptive concatenation function $`\mathrm{\#}`$ from $`S^{}\times S`$ to $`S^{}`$ as follows. Given a sequence $`\sigma `$ in $`S^{}`$ and an element $`x`$ of $`S`$, we take $`\sigma \mathrm{\#}x=\sigma `$ if the final element of $`\sigma `$ is $`x`$. If the final element of $`\sigma `$ is not equal to $`x`$ then we take $`\sigma \mathrm{\#}x`$ to be $`\sigma x`$, i.e. the result of concatenating $`x`$ to $`\sigma `$. We shall have two distinct uses for this function, applying it to primarily to sequences of agents, and sometimes to sequences of “instantaneous states” of agents in the context of asynchronous systems.

If $`\psi CKL_m`$, for each $`k0`$, we define the $`k`$-closure $`cl_k(\psi )`$, and for each agent $`i`$, we define the $`k,i`$-closure $`cl_{k,i}(\psi )`$. The definition of these sets proceeds by mutual recursion: First, we let the basic closure $`cl_0(\psi )`$ be the smallest set containing $`\psi `$ that is closed under subformulas, contains $`\neg \phi `$ if it contains $`\phi `$ and $`\phi `$ is not of the form $`\neg \phi ^{}`$, contains $`EC\phi `$ if it contains $`C\phi `$, and contains $`K_1\phi ,\mathrm{},K_n\phi `$ if it contains $`E\phi `$. (Of course, the last two clauses do not apply if $`\psi `$ is in $`KL_m`$, and thus does not mention common knowledge.) If $`i`$ is a agent, we take $`cl_{k,i}(\psi )`$ to be the union of $`cl_k(\psi )`$ with the set of formulas of the form $`K_i(\phi _1\mathrm{}\phi _n)`$ or $`\neg K_i(\phi _1\mathrm{}\phi _n)`$, where the $`\phi _l`$ are distinct formulas in $`cl_k(\psi )`$. Finally, $`cl_{k+1}(\psi )`$ is defined to be $`_{i=1}^mcl_{k,i}(\psi )`$.

If $`X`$ is a finite set of formulas we write $`\phi _X`$ for the conjunction of the formulas in $`X`$. A finite set $`X`$ of formulas is said to be consistent if $`\phi _X`$ is consistent. If $`X`$ is a finite set of formulas and $`\phi `$ is a formula we write $`X\phi `$ when $`\phi _X\phi `$. Clearly if $`X\phi _1`$ and $`\phi _1\phi _2`$ then $`X\phi _2`$.

Suppose $`Cl`$ is a finite set of formulas with the property that for all $`\phi Cl`$, either $`\neg \phi Cl`$ or $`\phi `$ is of the form $`\neg \phi ^{}`$ and $`\phi ^{}Cl`$. (Note that the sets $`cl_k(\psi )`$ and $`cl_{k,i}(\psi )`$ have this property.) We define an atom of $`Cl`$ to be a maximal consistent subset of $`Cl`$. Evidently, if $`X`$ is an atom of $`Cl`$ and $`\phi Cl`$, then either $`X\phi `$ or $`X\neg \phi `$. Thus, we have that

###### Lemma 4.1

: $`_{X\mathrm{an}\mathrm{atom}\mathrm{of}Cl}\phi _X`$.

We begin the construction of the model of $`\psi `$ by first constructing a pre-model, which is a structure $`S,,_1,\mathrm{},_n`$ consisting of a set $`S`$ of states, a binary relation $``$ on $`S`$, and for each agent $`i`$ an equivalence relation $`_i`$ on $`S`$. Recall from Section 2 that for a formula $`\phi \text{KL}_m`$, the alternation depth $`\text{ad}(\phi )`$ is the number of alternations of distinct operators $`K_i`$ in $`\phi `$. Let $`d=\text{ad}(\psi )`$ if $`\psi \text{KL}_m`$; otherwise (that is, if $`\psi `$ mentions the modal operator $`C`$), let $`d=0`$.

The set $`S`$ consists of all the pairs $`(\sigma ,X)`$ such that $`\sigma `$ is an index, $`|\sigma |d`$, and

1. if $`\sigma =ϵ`$ then $`X`$ is an atom of $`cl_d(\psi )`$, and
2. if $`\sigma =\tau i`$ then $`X`$ is an atom of $`cl_{k,i}(\psi )`$, where $`k=d|\sigma |`$.

The relation $``$ is defined so that $`(\sigma ,X)(\tau ,Y)`$ iff $`\tau =\sigma `$ and the formula $`\phi _X\phi _Y`$ is consistent. If $`X`$ is an atom we write $`X/K_i`$ for the set of formulas $`\phi `$ such that $`K_i\phi X`$. We say that states $`(\sigma ,X)`$ and $`(\tau ,Y)`$ are $`i`$-adjacent if $`\sigma \mathrm{\#}i=\tau \mathrm{\#}i`$. The relation $`_i`$ is defined so that $`(\sigma ,X)_i(\tau ,Y)`$ iff $`\sigma `$ and $`\tau `$ are $`i`$-adjacent and $`X/K_i=Y/K_i`$. Clearly, $`i`$-adjacency is an equivalence relation, as is the relation $`_i`$.

A $`\sigma `$-state (for $`\psi `$) is a pair $`(\sigma ,X)`$ as above. Thus $`(\sigma ,X)`$ is the unique $`\sigma `$-state with atom $`X`$. If $`s=(\sigma ,X)`$ is a state, we define $`\phi _s`$ to be the formula $`\phi _X`$, and write $`s\phi `$ for $`\phi _s\phi `$. We say that the state $`s`$ directly decides a formula $`\phi `$ if either (a) $`\phi X`$ or (b) $`\neg \phi X`$ or (c) $`\phi =\neg \phi ^{}`$ and $`\phi ^{}X`$. Note that this implies that either $`s\phi `$ or $`s\neg \phi `$. In case this latter condition holds we say simply that $`s`$ decides $`\phi `$. Note that if $`\sigma =\tau i`$ then each $`\sigma `$-state directly decides every formula in $`cl_{d|\sigma |,i}(\psi )`$. Also, every $`ϵ`$-state directly decides every formula in $`cl_d(\sigma )`$.

###### Lemma 4.2

: If $`s`$ and $`t`$ are $`i`$-adjacent states, then the same formulas of the form $`K_i\phi `$ are directly decided by $`s`$ and $`t`$.

Proof: Suppose that $`s`$ and $`t`$ are $`i`$-adjacent, $`s`$ is a $`\sigma `$-state, $`t`$ is a $`\tau `$-state. Clearly if $`\sigma =\tau `$, then $`s`$ and $`t`$ directly decide the same formulas (and, a fortiori, the same formulas of the form $`K_i\phi `$) since they are both maximal consistent subsets of the same set of formulas. If $`\sigma \tau `$, then either $`\sigma =\tau i`$ or $`\tau =\sigma i`$. By symmetry, it suffices to deal with the case $`\sigma =\tau i`$. By definition, $`s`$ directly decides the $`K_i`$-formulas in $`\text{cl}_{d|\sigma |,i}(\psi )`$, while $`t`$ directly decides the $`K_i`$-formulas in $`\text{cl}_{d|\tau |,j}(\psi )`$ if $`\tau =\tau ^{}j`$ or $`\text{cl}_d(\psi )`$ if $`\tau =ϵ`$. We leave it to the reader to check that it follows that the $`K_i`$-formulas directly decided by both $`s`$ and $`t`$ are precisely those in $`\text{cl}_{d|\sigma |,i}(\psi )`$.

If $`s`$ is a $`\sigma `$-state, we take $`\mathrm{\Phi }_{s,i}`$ to be the disjunction of the formulas $`\phi _t`$, where $`t`$ ranges over the $`\sigma `$-states satisfying $`s_it`$, and we take $`\mathrm{\Phi }_{s,i}^+`$ to be the disjunction of the formulas $`\phi _t`$, where $`t`$ ranges over the $`(\sigma \mathrm{\#}i)`$-states satisfying $`s_it`$.444It can be shown that if $`|\sigma \mathrm{\#}i|d`$, then $`\mathrm{\Phi }_{s,i}`$ is logically equivalent to $`\mathrm{\Phi }_{s,i}^+`$, but we do not need this fact here. Observe that because $`_i`$ is an equivalence relation we have that if $`s_it`$ then $`\mathrm{\Phi }_{s,i}=\mathrm{\Phi }_{t,i}`$ and $`\mathrm{\Phi }_{s,i}^+=\mathrm{\Phi }_{t,i}^+`$. The following result lists a number of knowledge formulas decided by states.

###### Lemma 4.3

:

If $`s`$ is a $`\sigma `$-state and $`t`$ is a $`\sigma `$-state or $`(\sigma \mathrm{\#}i)`$-state such that $`s_it`$, then $`sK_i\neg \phi _t`$.

For all $`\sigma `$-states $`s`$, we have $`sK_i\mathrm{\Phi }_{s,i}`$; in addition, if $`|\sigma \mathrm{\#}i|d`$, then $`sK_i\mathrm{\Phi }_{s,i}^+`$.

For all $`\sigma `$-states $`s`$ and $`(\sigma \mathrm{\#}i)`$-states $`t`$ with $`s_it`$, we have $`sL_i\phi _t`$.

If $`s`$ is a $`\sigma `$-state and $`t`$ is a $`(\sigma \mathrm{\#}i)`$-state such that $`s_it`$, then $`t\neg K_i\mathrm{\Phi }_{s,i}^+`$.

Proof: For (a), suppose that $`s_it`$, where $`s=(\sigma ,X)`$ and $`t=(\tau ,Y)`$, where $`\tau `$ is either $`\sigma `$ or $`\sigma \mathrm{\#}i`$. Then $`X/K_iY/K_i`$ so either there exists a formula $`K_i\phi X`$ such that $`K_i\phi Y`$ or there exists a formula $`K_i\phi Y`$ such that $`K_i\phi X`$. As the states $`s`$ and $`t`$ are $`i`$-adjacent, by Lemma 4.2, in either case the formula $`K_i\phi `$ is directly decided by both the states $`s`$ and $`t`$. In the first case, we have that $`\phi _t\neg K_i\phi `$ and hence, using R2, that $`K_i(K_i\phi \neg \phi _t)`$. By K4 we obtain from the fact that $`K_i\phi X`$ that $`sK_iK_i\phi `$. It now follows using K2 that $`sK_i\neg \phi _t`$. In the second case, we have that $`\phi _tK_i\phi `$, hence, using R2, that $`K_i(\neg K_i\phi \neg \phi _t)`$. By K4 we obtain from the fact that $`\neg K_i\phi X`$ that $`sK_i\neg K_i\phi `$. It now follows using K2 that $`sK_i\neg \phi _t`$.

For (b), by Lemma 4.1, we have that $`_{X\mathrm{an}\mathrm{atom}\mathrm{of}cl_{k,i}(\psi )}\phi _X`$. Hence, by R2 we obtain that $`K_i_{\sigma \mathrm{states}t}\phi _t`$. It follows from this using (a) and K2 that $`sK_i\mathrm{\Phi }_{s,i}`$. If $`|\sigma \mathrm{\#}i|d`$, then a similar argument shows that $`sK_i\mathrm{\Phi }_{s,i}^+`$.

For (c), suppose that $`s=(\sigma ,X)_i(\sigma \mathrm{\#}i,Y)=t`$ and $`k=d|\sigma \mathrm{\#}i|`$. We claim first that if $`W=Ycl_k(\psi )`$, then $`sK_i\neg \phi _tK_i\neg \phi _W`$. This is because the fact that $`Y`$ is a subset of $`cl_{k,i}(\psi )`$ implies that all formulas $`\phi `$ in $`YW`$ are of the form $`K_i\phi ^{}`$ or $`\neg K_i\phi ^{}`$, hence $`\phi X`$ if and only if $`\phi Y`$. Also, by K4 and K5 we have that $`sK_iK_i\phi ^{}`$ when $`K_i\phi ^{}X`$ and $`sK_i\neg K_i\phi ^{}`$ when $`K_i\phi ^{}X`$. It follows using K2 that $`sK_i\phi _{YW}`$. Since $`\phi _t`$ is equivalent to $`\phi _W\phi _{YW}`$, we obtain using K2 that $`sK_i\neg \phi _tK_i\neg \phi _W`$.

Now by K3 we have $`\phi _tL_i\phi _t`$. Further, the argument of the previous paragraph also shows $`tK_i\neg \phi _tK_i\neg \phi _W`$, so we obtain that $`tL_i\phi _W`$. But $`\neg \phi _W`$ is equivalent to the disjunction of a subset $`\{\phi _1,\mathrm{},\phi _n\}`$ of $`cl_k(\psi )`$. Let $`\alpha `$ be the formula $`K_i(\phi _1\mathrm{}\phi _n)`$, which is equivalent to $`K_i\neg \phi _W`$. It follows from the definition of $`cl_{k,i}(\psi )`$ that $`\alpha `$ is in $`cl_{k,i}(\psi )`$, hence directly decided by both $`t`$ and $`s`$. Consequently, $`\alpha `$ is not in $`Y`$, since $`t\neg \alpha `$. Because $`X/K_i=Y/K_i`$, the formula $`\alpha `$ is not in $`X`$ either, so $`s\neg \alpha `$. Applying the fact that $`\alpha `$ is equivalent to $`K_i\neg \phi _W`$, we see that $`sL_i\phi _W`$. The equivalence of the previous paragraph now yields that $`sL_i\phi _t`$.

For (d), note that if $`t`$ and $`v`$ are distinct $`(\sigma \mathrm{\#}i)`$-states then $`t\neg \phi _v`$. Thus, if $`s`$ is a $`\sigma `$-state such that $`s_it`$ then $`t\neg \mathrm{\Phi }_{s,i}^+`$, which implies, using K3, that $`t\neg K_i\mathrm{\Phi }_{s,i}^+`$.

If $`T`$ is a set of states, then we write $`\phi _T`$ for the disjunction of the formulas $`\phi _t`$ for $`t`$ in $`T`$. Using RT1, T1, and T2, the following result is immediate from the fact that $`s\to ̸t`$ implies $`\phi _s\neg \phi _t`$, together with the fact that $`_{s\mathrm{a}\sigma \mathrm{state}}\phi _s`$, which follows from Lemma 4.1.

###### Lemma 4.4

: Let $`s`$ be a state and let $`T`$ be the set of states $`t`$ such that $`st`$. Then $`s\phi _T`$

The next result provides a useful way to derive formulas containing the until operator.

###### Lemma 4.5

: For all formulas $`\alpha ,\beta `$ and $`\gamma `$, if $`\alpha \neg \gamma `$ and $`\alpha (\alpha (\neg \beta \neg \gamma ))`$ then $`\alpha \neg (\beta U\gamma )`$.

Proof: Suppose that $`\alpha \neg \gamma (\alpha (\neg \beta \neg \gamma ))`$. By T3, we obtain that $`\alpha (\beta U\gamma )\neg \gamma (\beta U\gamma )(\alpha (\neg \beta \neg \gamma ))`$. Since, by T3 again, $`\beta U\gamma \neg (\neg \beta \neg \gamma )`$, it follows using T1 and RT1 that $`\alpha (\beta U\gamma )\neg \gamma (\alpha (\beta U\gamma ))`$. Now using RT2 we obtain $`\alpha (\beta U\gamma )\neg (\beta U\gamma )`$, which implies that $`\alpha \neg (\beta U\gamma )`$.

The following shows that the pre-model almost satisfies the truth definitions for formulas in the basic closure. Note that every state directly decides all formulas in the basic closure. Define a $``$-sequence of states to be a (finite or infinite) sequence $`s_1,s_2,\mathrm{}`$ such that $`s_1s_2\mathrm{}`$.

###### Lemma 4.6

: For all $`\sigma `$-states $`s`$, we have

1. if $`\phi \text{cl}_0(\psi )`$, then for all states $`t`$ such that $`st`$, we have $`s\phi `$ iff $`t\phi `$,
2. If $`K_i\phi \text{cl}_0(\psi )`$, then $`s\neg K_i\phi `$ iff there is some $`\sigma `$-state $`t`$ such that $`s_it`$ and $`t\neg \phi `$. Moreover, if $`|\sigma \mathrm{\#}i|d`$, then $`s\neg K_i\phi `$ iff there is some $`(\sigma \mathrm{\#}i)`$-state $`t`$ such that $`s_it`$ and $`t\neg \phi `$.
3. if $`\phi _1U\phi _2\text{cl}_0(\psi )`$ then $`s\phi _1U\phi _2`$ iff there exists a $``$-sequence $`s=s_0s_1\mathrm{}s_n`$, where $`n0`$, such that $`s_n\phi _2`$, and $`s_k\phi _1`$ for all $`k<n`$.

Proof: For part (a), suppose first that $`s\phi `$ and $`st`$. Since $`\phi cl_0(\psi )`$, it follows that $`t\phi `$ or $`t\neg \phi `$. But, by T1 and T2, the latter would contradict the assumption that $`\phi _s\phi _t`$ is consistent. Hence we have $`t\phi `$. Conversely, suppose that $`st`$ and $`t\phi `$. Using T1, we have $`\phi _t\phi `$. Since $`\phi cl_0(\psi )`$ we have either $`s\phi `$ or $`s\neg \phi `$. But the latter would contradict $`st`$, so we obtain $`s\phi `$.

For the “if” direction of part (b), note that the fact that $`K_i\phi `$ is in $`cl_0(\psi )`$ implies that if $`s_it`$ and $`sK_i\phi `$, then $`tK_i\phi `$, hence $`t\phi `$ by K3. For the converse, suppose that $`t\phi `$ for all $`\sigma `$-states $`t`$ with $`s_it`$. Then $`\mathrm{\Phi }_{s,i}\phi `$, hence $`K_i\mathrm{\Phi }_{s,i}K_i\phi `$, using K2 and R2. By Lemma 4.3(b), we have $`sK_i\mathrm{\Phi }_{s,i}`$. It follows immediately that $`sK_i\phi `$. If $`|\sigma \mathrm{\#}i|d`$, a similar argument shows that if $`t\phi `$ for all $`(\sigma \mathrm{\#}i)`$-states $`t`$ such that $`s_it`$, then $`sK_i\phi `$.

For part (c), note that if $`\phi _1U\phi _2`$ is in $`cl_0(\psi )`$, then every state directly decides each of the formulas $`\phi _1`$, $`\phi _2`$, and $`\phi _1U\phi _2`$. We first show that if there exists a sequence of states $`s=s_0s_1\mathrm{}s_n`$ such that $`s_n\phi _2`$ and $`s_k\phi _1`$ for all $`k<n`$ then $`s\phi _1U\phi _2`$. We proceed by induction on $`n`$. The case $`n=0`$ is immediate from T3. For the general case, notice that it follows from the induction hypothesis that $`s_1(\phi _1U\phi _2)`$. Since $`s_0s_1`$, it follows that $`\phi _{s_0}(\phi _1U\phi _2)`$ is consistent. By assumption, we also have $`s_0\phi _1`$. Using T3, we see that $`s_0\neg (\phi _1U\phi _2)`$ would be a contradiction. Hence $`s_0\phi _1U\phi _2`$.

The converse follows immediately from Lemma 4.7 below.

###### Lemma 4.7

: If $`\phi _s\phi _1U\phi _2`$ is consistent, then there exists a $``$-sequence $`s=s_0s_1\mathrm{}s_n`$, such that $`\phi _{s_n}\phi _2`$ is consistent, and $`\phi _{s_k}\phi _1`$ is consistent for all $`k<n`$.

Proof: Suppose by way of contradiction that $`\phi _s\phi _1U\phi _2`$ is consistent and no appropriate $``$-sequence exists. Let $`T`$ be the smallest set $`S`$ of states such that (i) $`sS`$, and (ii) if $`tS`$, $`tu`$, and $`s_u\phi _1`$ is consistent, then $`uS`$. Then we have that $`t\neg \phi _2`$ for all $`tT`$, so $`\phi _T\neg \phi _2`$. In addition, for each $`tT`$ and state $`u`$ such that $`tu`$, we have either $`uT`$ or $`u\neg \phi _1\neg \phi _2`$. Thus, using Lemma 4.4, we obtain $`\phi _T(\phi _T(\neg \phi _1\neg \phi _2))`$. It now follows using Lemma 4.5 that $`\phi _T\neg (\phi _1U\phi _2)`$. In particular, since $`sT`$, we have $`s\neg (\phi _1U\phi _2)`$, which contradicts the assumption that $`\phi _s\phi _1U\phi _2`$ is consistent.

For the next result, recall that when the formula $`\psi `$ contains the common knowledge operator we take $`d=0`$, so that all states are $`ϵ`$-states.

###### Lemma 4.8

: If $`C\phi cl_0(\psi )`$, then $`s\neg C\phi `$ iff there is a state $`t`$ reachable from $`s`$ through the relations $`_i`$ such that $`t\neg \phi `$.

Proof: The implication from right to left is a straightforward consequence of the fact that if $`t\neg \phi `$ then $`t\neg C\phi `$, by C1, C2 and K3, together with the fact that if $`t_it^{}`$, then $`tC\phi `$ if and only if $`t^{}C\phi `$. (Proof of the latter fact: If $`tC\phi `$ then $`tK_iC\phi `$ by C1 and C2. Hence, since $`t_it^{}`$ and $`K_iC\phi cl_0(\psi )`$, we must have $`t^{}C\phi `$. The opposite direction follows symmetrically.) This leaves only the implication from left to right, for which we prove the contrapositive. Suppose that no state containing $`\neg \phi `$ is reachable from $`s`$ by means of a sequence of steps through the relations $`_i`$. Let $`T`$ be the set of states reachable from $`s`$. By Lemma 4.3(a), if $`t`$ and $`t^{}`$ are states with $`t_it^{}`$ then $`tK_i\neg \phi _t^{}`$. It follows from this that $`tK_i\phi _T`$ for every state $`tT`$ and agent $`i`$. Thus, because $`\phi _T\phi `$ we have $`\phi _TE(\phi _T\phi )`$. By RC1 it follows that $`\phi _TC\phi `$. Since $`sT`$, it is immediate that $`sC\phi `$.

We say that an infinite $``$-sequence of states ($`s_0,s_1,\mathrm{}`$), where $`s_n=(\sigma ,X_n)`$ for all $`n`$, is acceptable if for all $`n0`$, if $`\phi _1U\phi _2X_n`$ then there exists an $`mn`$ such that $`s_m\phi _2`$ and $`s_k\phi _1`$ for all $`k`$ with $`nk<m`$.

###### Definition 4.9

:  An enriched system for $`\psi `$ is a pair $`(,\mathrm{\Sigma })`$, where $``$ is a set of runs and $`\mathrm{\Sigma }`$ is a partial function mapping points in $`\times 𝐍`$ to states for $`\psi `$ such that the following hold, for all runs $`r`$:

1. If $`\mathrm{\Sigma }(r,n)`$ is defined then $`\mathrm{\Sigma }(r,n^{})`$ is defined for all $`n^{}>n`$, and $`\mathrm{\Sigma }(r,n),\mathrm{\Sigma }(r,n+1),\mathrm{}`$ is an acceptable $``$-sequence.
2. For all points $`(r,n)_i(r^{},n^{})`$, if $`\mathrm{\Sigma }(r,n)`$ is defined then $`\mathrm{\Sigma }(r^{},n^{})`$ is defined and $`\mathrm{\Sigma }(r,n)_i\mathrm{\Sigma }(r^{},n^{})`$.
3. If $`\mathrm{\Sigma }(r,n)`$ and $`s`$ are $`\sigma `$-states such that $`\mathrm{\Sigma }(r,n)_is`$, then there exists a point $`(r^{},n^{})`$ such that $`(r,n)_i(r^{},n^{})`$ and $`\mathrm{\Sigma }(r^{},n^{})=s`$.
4. if $`C\phi cl_0(\psi )`$ and $`\mathrm{\Sigma }(r,n)\neg C\phi `$, then there exists a point $`(r^{},n^{})`$ reachable from $`(r,n)`$ such that $`\mathrm{\Sigma }(r^{},n^{})\neg \phi `$.

An enriched+ system for $`\psi `$ is a pair $`(,\mathrm{\Sigma })`$ satisfying conditions 1, 2, and the following modification of 3:

* If $`\mathrm{\Sigma }(r,n)`$ is a $`\sigma `$-state and $`s`$ is a $`(\sigma \mathrm{\#}i)`$-state such that $`\mathrm{\Sigma }(r,n)_is`$, then there exists a point $`(r^{},n^{})`$ such that $`(r,n)_i(r^{},n^{})`$ and $`\mathrm{\Sigma }(r^{},n^{})=s`$.

Given an enriched (resp., enriched+) system $`(,\mathrm{\Sigma })`$, we obtain an interpreted system $`=(,\pi )`$ by defining the valuation $`\pi `$ on basic propositions $`p`$ by $`\pi (r,n)(p)=\mathrm{𝐭𝐫𝐮𝐞}`$ just when $`\mathrm{\Sigma }(r,n)`$ is defined and $`\mathrm{\Sigma }(r,n)p`$. The following theorem gives a sufficient condition for a formula in the basic closure to hold at a point in this standard system. If $`\sigma `$ is the index $`i_1\mathrm{\#}\mathrm{}\mathrm{\#}i_k`$, let $`K_\sigma \phi `$ be an abbreviation for $`K_{i_1}\mathrm{}K_{i_k}\phi `$. (If $`\sigma =ϵ`$, then we take $`K_\sigma \phi `$ to be $`\phi `$.)

###### Theorem 4.10

:

* If $`(,\mathrm{\Sigma })`$ is an enriched system for $`\psi `$, $``$ is the associated interpreted system, $`\phi `$ is in the basic closure $`cl_0(\psi )`$, and $`\mathrm{\Sigma }(r,n)`$ is defined, then $`(,r,n)\phi `$ if and only if $`\mathrm{\Sigma }(r,n)\phi `$.
* If $`(,\mathrm{\Sigma })`$ is an enriched+ system for $`\psi \text{KL}_m`$, $``$ is the associated standard system, $`\phi `$ is in the basic closure $`cl_0(\psi )`$, $`\mathrm{\Sigma }(r,n)`$ is a $`\sigma `$-state, and $`\text{ad}(K_\sigma \phi )d`$, then $`(,r,n)\phi `$ if and only if $`\mathrm{\Sigma }(r,n)\phi `$.

Proof: We first prove part (a). We proceed by induction on the complexity of $`\phi `$. If $`\phi `$ is a propositional constant then the result is immediate from the definition of $``$. The cases where $`\phi `$ is of the form $`\neg \phi _1`$ or $`\phi _1\phi _2`$ are similarly trivial. This leaves five cases:

Case 1: Suppose that $`\phi `$ is of the form $`\phi _1`$. Then $`(,r,n)\phi `$ if and only if $`(,r,n+1)\phi _1`$. Note that $`\mathrm{\Sigma }(r,n+1)`$ must be defined by Condition 1 of Definition 4.9. Since $`\phi _1`$ is a subformula of $`\phi `$ it is in $`cl_0(\psi )`$, so it follows by the induction hypothesis that $`(,r,n+1)\phi _1`$ holds precisely when $`\mathrm{\Sigma }(r,n+1)\phi _1`$. By Condition 1, $`\mathrm{\Sigma }(r,n)\mathrm{\Sigma }(r,n+1)`$, so we obtain from Lemma 4.6(a) that $`\mathrm{\Sigma }(r,n+1)\phi _1`$ if and only if $`\mathrm{\Sigma }(r,n)\phi _1`$. Putting the pieces together, we get $`(,r,n)\phi `$ if and only if $`\mathrm{\Sigma }(r,n)\phi `$.

Case 2: Suppose that $`\phi `$ is of the form $`\phi _1U\phi _2`$. Then the subformulas $`\phi _1`$ and $`\phi _2`$ are also in $`cl_0(\psi )`$. Note also that by Condition 1 of Definition 4.9, $`\mathrm{\Sigma }(r,n^{})`$ is defined for all $`n^{}n`$, and $`\mathrm{\Sigma }(r,n),\mathrm{\Sigma }(r,n+1),\mathrm{}`$ is an admissible $``$-sequence. Thus, if $`\mathrm{\Sigma }(r,n)\phi _1U\phi _2`$, then by Lemma 4.6(c) there exists some $`n^{}n`$ such that $`\mathrm{\Sigma }(r,n^{})\phi _2`$ and $`\mathrm{\Sigma }(r,k)\phi _1`$ for $`nk<n^{}`$. By the induction hypothesis, this implies that $`(,r,n^{})\phi _2`$ and $`(,r,k)\phi _1`$ for $`nk<n^{}`$. In other words, we have $`(,r,n)\phi _1U\phi _2`$. Conversely, if $`(,r,n)\phi _1U\phi _2`$, then by the induction hypothesis and the semantics of $`U`$ we have that there exists some $`n^{}n`$ such that $`\mathrm{\Sigma }(r,n^{})\phi _2`$ and $`\mathrm{\Sigma }(r,k)\phi _1`$ for $`nk<n^{}`$. Since $`\mathrm{\Sigma }(r,n)\mathrm{\Sigma }(r,n+1)\mathrm{}\mathrm{\Sigma }(r,n^{})`$, it follows using Lemma 4.6(c) that $`\mathrm{\Sigma }(r,n)\phi _1U\phi _2`$.

Case 3: Suppose that $`\phi `$ is of the form $`K_i\phi _1`$. We first show that $`\mathrm{\Sigma }(r,n)K_i\phi _1`$ implies $`(,r,n)K_i\phi _1`$. Assume $`\mathrm{\Sigma }(r,n)K_i\phi _1`$ and suppose that $`(r,n)_i(r^{},n^{})`$. Then by Condition 2 of Definition 4.9, we have that that $`\mathrm{\Sigma }(r^{},n^{})`$ is defined and $`\mathrm{\Sigma }(r,n)_i\mathrm{\Sigma }(r^{},n^{})`$. Since $`K_i\phi cl_0(\psi )`$ we obtain $`\mathrm{\Sigma }(r,n^{})K_i\phi _1`$. By K3 this implies $`\mathrm{\Sigma }(r,n^{})\phi _1`$. Since $`\phi cl_0(\psi )`$, by the induction hypothesis, we obtain that $`(,r^{},n^{})\phi _1`$. This shows that $`(,r^{},n^{})\phi _1`$ for all points $`(r^{},n^{})_i(r,n)`$. That is, we have $`(,r,n)K_i\phi _1`$.

For the converse, suppose that $`\mathrm{\Sigma }(r,n)\neg K_i\phi _1`$ and that $`\mathrm{\Sigma }(r,n)`$ is a $`\sigma `$-state. By Lemma 4.6(b), there exists a $`\sigma `$-state $`t`$ such that $`\mathrm{\Sigma }(r,n)_it`$ and $`t\neg \phi _1`$. By Condition 3 of Definition 4.9, there exists a point $`(r^{},n^{})`$ such that $`(r,n)_i(r^{},n^{})`$ and $`\mathrm{\Sigma }(r^{},n^{})=t`$. Using the induction hypothesis we obtain that $`(,r^{},n^{})\neg \phi _1`$. It follows that $`(,r,n)\neg K_i\phi _1`$.

Case 4: If $`\phi `$ is of the form $`E\phi _1`$, the result follows easily from the induction hypothesis, using axiom C1.

Case 5: Suppose $`\phi `$ is of the form $`C\phi _1`$. By Condition 2 of Definition 4.9 we have that $`\mathrm{\Sigma }(r^{},n^{})`$ is defined for all $`(r^{},n^{})`$ reachable from $`(r,n)`$. An easy induction on the length of the path from $`(r,n)`$ to $`(r^{},n^{})`$, using the fact that $`K_iC\phi _1`$ is in the basic closure and axioms C1, C2, and K3, can be used to show that $`\mathrm{\Sigma }(r^{},n^{})C\phi _1`$ for each point $`(r^{},n^{})`$ reachable from $`(r^{},n)`$. Using C1, C2, and K3, it is easy to see that $`\mathrm{\Sigma }(r^{},n^{})\phi _1`$. By the induction hypothesis, this implies that $`(,r^{},n^{})\phi _1`$. Thus, $`(,r,n)C\phi _1`$.

For the converse, suppose that $`\mathrm{\Sigma }(r,n)\neg C\phi _1`$. Then by Condition 4 of Definition 4.9, we have $`\mathrm{\Sigma }(r^{},n^{})\neg \phi _1`$ for some point $`(r^{},n^{})`$ reachable from $`(r,n)`$. By the induction hypothesis, we have that $`(,r^{},n^{})\neg \phi _1`$, and hence $`(,r,n)\neg C\phi _1`$.

For part (b), since $`\psi \text{KL}_m`$, we only need to check the analogues of cases 1, 2, and 3 above. The proofs in cases 1 and 2 are identical to those above. The proof of case 3 is also quite similar, but we must be a little careful in applying the inductive hypothesis. So suppose that $`\phi `$ is of the form $`K_i\phi _1`$, $`\mathrm{\Sigma }(r,n)`$ is a $`\sigma `$-state, and $`\text{ad}(K_\sigma \phi )d`$. The implication from left to right, showing that if $`\mathrm{\Sigma }(r,n)K_i\phi `$ then $`(,r,n)K_i\phi `$ is identical to that above. We just need the observation that if $`(r,n)_i(r^{},n^{})`$, then $`\mathrm{\Sigma }(r^{},n^{})`$ is a $`\tau `$-state, where $`\tau \mathrm{\#}i=\sigma \mathrm{\#}i`$. It follows that $`\text{ad}(K_\tau \phi )\text{ad}(K_{\sigma \mathrm{\#}i}\phi )\text{ad}(K_\sigma K_i\phi )d`$, so we can apply the inductive hypothesis to conclude that $`(,r^{},n^{})\phi _1`$. For the converse, the proof is again similar. Note that if $`\text{ad}(K_\sigma K_i\phi )d`$, then $`|\sigma \mathrm{\#}i|d`$, so by Lemma 4.6(b), there exists a $`(\sigma \mathrm{\#}i)`$-state $`t`$ such that $`\mathrm{\Sigma }(r,n)_it`$ and $`t\neg \phi _1`$. By Condition 3 of Definition 4.9, there exists a point $`(r^{},n^{})`$ such that $`(r,n)_i(r^{},n^{})`$ and $`\mathrm{\Sigma }(r^{},n^{})=t`$. Since $`\text{ad}(K_{\sigma \mathrm{\#}i}\phi )=\text{ad}(K_\sigma K_i\phi )d`$, using the induction hypothesis we obtain that $`(,r^{},n^{})\neg \phi _1`$. It follows that $`(,r,n)\neg K_i\phi _1`$.

###### Corollary 4.11

: If $`(,\mathrm{\Sigma })`$ is an enriched (resp., enriched+) system for $`\psi `$, $``$ is the associated interpreted system, and $`(r,n)`$ is a point of $``$ such that $`\mathrm{\Sigma }(r,n)`$ is an $`ϵ`$-state and $`\mathrm{\Sigma }(r,n)\psi `$, then $`(,r,n)\psi `$.

We apply this corollary in all our completeness proofs, constructing an appropriate enriched or enriched+ system in all cases.

## 5 Proofs of Soundness and Completeness

We are now in a position to prove the completeness results claimed in Section 3. Sections 5.1-5.3 will deal with the cases involving only perfect recall, synchrony and unique initial states. The cases involving no learning are a little more complex, and are dealt with in Sections 5.4-5.7.

### 5.1 Dealing with $`𝒞_m`$, $`𝒞_m^{\mathrm{𝑠𝑦𝑛𝑐}}`$, $`𝒞_m^{\mathrm{𝑢𝑖𝑠}}`$, and $`𝒞_m^{\mathrm{𝑠𝑦𝑛𝑐},\mathrm{𝑢𝑖𝑠}}`$ (Theorems 3.1 and 3.2)

The fact that S5C$`{}_{}{}^{U}{}_{m}{}^{}`$ is sound for $`𝒞_m`$, the class of all systems, is straightforward and left to the reader (see also \[FHMV95\]). To prove completeness of S5$`{}_{}{}^{U}{}_{m}{}^{}`$ for the language $`\text{KL}_m`$ and of S5C$`{}_{}{}^{U}{}_{m}{}^{}`$ for the language $`\text{CKL}_m`$ with respect to $`𝒞_m`$, $`𝒞_m^{\mathrm{𝑠𝑦𝑛𝑐}}`$, $`𝒞_m^{\mathrm{𝑢𝑖𝑠}}`$, and $`𝒞_m^{\mathrm{𝑠𝑦𝑛𝑐},\mathrm{𝑢𝑖𝑠}}`$, we construct an enriched system, and use Corollary 4.11. The proof proceeds in the same way whether or not common knowledge is in the language. We assume here that the language includes common knowledge and that we are dealing with the axiom system S5C$`{}_{}{}^{U}{}_{m}{}^{}`$ when constructing the states in the enriched structure. Recall that in this case we work with $`ϵ`$-states only.

The following result suffices for the generation of the acceptable sequences required for the construction of an enriched system in the cases not involving no learning; a more complex construction will be required in the presence of no learning.

###### Lemma 5.1

: Every finite $``$-sequence of states can be extended to an infinite acceptable sequence.

Proof: To see this, first note that for every $`\sigma `$-state $`s`$ there exists a state $`t`$ with $`st`$. For otherwise, $`s\neg \phi _t`$ for all $`\sigma `$-states $`t`$, which contradicts $`_{t\mathrm{a}\sigma \mathrm{state}}\phi _t`$. (Note that $`_{t\mathrm{a}\sigma \mathrm{state}}\phi _t`$ follows from Lemma 4.1 and RT1.) Thus every finite sequence of states can be extended to an infinite sequence, and it remains to show that the obligations arising from the until formulas can be satisfied.

Suppose the finite $``$-sequence is $`s_0\mathrm{}s_n`$, where $`s_k=(\sigma ,X_k)`$ for $`k=1\mathrm{}n`$. Now, for any formula $`\phi _1U\phi _2X_0`$, it follows using T3 and the fact that the $`s_i`$ directly decide each of the formulas $`\phi _1`$, $`\phi _2`$, and $`\phi _1U\phi _2`$ that either the obligation imposed by $`\phi _1U\phi _2`$ at $`s_0`$ is already satisfied in the sequence $`(s_0,\mathrm{},s_n)`$, or else $`s_n\phi _1U\phi _2`$ and $`s_k\phi _1`$ for $`0kn`$. In the latter case, by Lemma 4.6(c), there exists a sequence $`s_ns_{n+1}\mathrm{}s_n^{}`$ such that $`s_n^{}\phi _2`$ and $`s_k\phi _1`$ for $`nk<n^{}`$. This gives a finite extension of the original sequence that satisfies the obligation imposed by $`\phi _1U\phi _2`$ at $`s_0`$. Applying this argument to the remaining obligations at $`s_0`$, we eventually obtain a finite sequence that satisfies all the obligations at $`s_0`$. We may then move on to $`s_1`$ and apply the same procedure. It is clear that in the limit we obtain an acceptable sequence extending the original sequence.

For each agent $`i`$, define the function $`O_i`$ to map the state $`(\sigma ,U)`$ to the pair $`(\sigma \mathrm{\#}i,U/K_i)`$. $`O_i`$ is also used later in our other constructions. Given a state $`s`$, we call $`O_i(s)`$ agent $`i`$’s current information at $`s`$. Let $`x`$ be a new object not equal to any state. We say that a sequence $`S=(x,x,\mathrm{},x,s_N,s_{N+1},\mathrm{})`$ is an acceptable sequence from $`N`$ if it starts with $`N`$ copies of $`x`$ and the suffix $`(s_N,s_{N+1},\mathrm{})`$ is an acceptable $``$-sequence of states for $`\psi `$. Given a sequence $`S`$ acceptable from $`N`$, we define a run $`r`$ as follows. For each agent $`i`$, take $`r_i(n)=(n,S)`$ when $`n<N`$ and $`r_i(n)=(n,O_i(s_n))`$ otherwise. For the environment component $`e`$, take $`r_e(n)=S_n`$.

Let $`^{\mathrm{𝑠𝑦𝑛𝑐}}`$ be the set of all runs so obtained, and define the partial function $`\mathrm{\Sigma }`$ on points in $`^{\mathrm{𝑠𝑦𝑛𝑐}}\times 𝐍`$ so that $`\mathrm{\Sigma }(r,n)=s_n`$ when $`r`$ is derived from a sequence $`(x,x,\mathrm{},x,s_N,s_{N+1},\mathrm{})`$ acceptable from $`N`$ and $`nN`$, and $`\mathrm{\Sigma }(r,n)`$ is undefined otherwise.

###### Lemma 5.2

: The pair $`(^{\mathrm{𝑠𝑦𝑛𝑐}},\mathrm{\Sigma })`$ is an enriched system.

Proof: It is immediate from the construction that $`(^{\mathrm{𝑠𝑦𝑛𝑐}},\mathrm{\Sigma })`$ satisfies conditions 1 and 2 of Definition 4.9. To see that it satisfies Condition 3, suppose that $`(r,n)`$ is a point such that $`\mathrm{\Sigma }(r,n)`$ is defined and $`\mathrm{\Sigma }(r,n)_is`$. By Lemma 5.1 there exists an acceptable sequence $`(s_n,s_{n+1},\mathrm{})`$ with $`s=s_n`$. Let $`r^{}`$ be the run obtained from the sequence $`(x,\mathrm{},x,s_n,s_{n+1},\mathrm{})`$. Then it is immediate that $`(r,n)_i(r^{},n^{})`$ and $`\mathrm{\Sigma }(r^{},n^{})=s`$. Finally, to see that it satisfies Condition 4, suppose that $`C\phi cl_0(\psi )`$ and $`\mathrm{\Sigma }(r,n)\neg C\phi `$. By Lemma 4.8, there is a state $`t`$ reachable from $`\mathrm{\Sigma }(r,n)`$ through the relations $`_i`$ such that $`t\neg \phi `$. An easy inductive argument on the length of the path from $`\mathrm{\Sigma }(r,n)`$ to $`t`$, using Condition 3, shows that there is a point $`(r^{},n^{})`$ reachable from $`(r,n)`$ through the relations $`_i`$ such that $`\mathrm{\Sigma }(r^{},n^{})=t`$. Thus, the enriched system satisfies condition 4.

Clearly the system $`^{\mathrm{𝑠𝑦𝑛𝑐}}`$ is synchronous, so the interpreted system $``$ derived from $`(^{\mathrm{𝑠𝑦𝑛𝑐}},\mathrm{\Sigma })`$ is also synchronous. Let $`s`$ be an $`ϵ`$-state such that $`s\psi `$. Such a state must exist because $`\psi `$ was assumed consistent. By Lemma 5.1 there exists an acceptable sequence $`(s_0,s_1,\mathrm{})`$ with $`s=s_0`$. Let $`r`$ be the corresponding run in $`^{\mathrm{𝑠𝑦𝑛𝑐}}`$. Corollary 4.11 implies that $`(,r,0)\psi `$. This establishes the completeness of the axiomatization S5C$`{}_{m}{}^{}{}_{}{}^{U}`$ for the language $`\text{CKL}_m`$ (resp., of S5$`{}_{m}{}^{}{}_{}{}^{U}`$ for the language $`\text{KL}_m`$) with respect to the classes of systems $`𝒞_m`$ and $`𝒞_m^{\mathrm{𝑠𝑦𝑛𝑐}}`$. To establish completeness of these axiomatizations for the corresponding languages with respect to the classes of systems $`𝒞_m^{\mathrm{𝑢𝑖𝑠}}`$ and $`𝒞_m^{\mathrm{𝑠𝑦𝑛𝑐},\mathrm{𝑢𝑖𝑠}}`$, we make use of the following result, which shows that sound and complete axiomatizations for the class of systems satisfying some subset of the properties of perfect recall and synchrony are also sound and complete axiomatizations for the class of systems with the same subset of these properties, but with unique initial states in addition. This completes the proofs of Theorem 3.1 and 3.2.

###### Lemma 5.3

: Suppose $`x`$ is a subset of $`\{\mathrm{𝑝𝑟},\mathrm{𝑠𝑦𝑛𝑐}\}`$. If $`\phi \text{CKL}_m`$ is satisfiable with respect to $`𝒞_m^x`$, then it is also satisfiable with respect to $`𝒞_m^{x,\mathrm{𝑢𝑖𝑠}}`$.

Proof: Suppose $`=(,\pi )𝒞_m^x`$. We define a system $`^{}`$ by adding a new initial state to each run in $``$. Formally, we define the system $`^{}=(^{},\pi ^{})`$ as follows. Let $`l`$ be some local state that does not occur in $``$ and let $`s_e`$ be any state of the environment. For each run $`r`$, let $`r^+`$ be the run such that $`r^+(0)=(s_e,l,\mathrm{},l)`$ and $`r^+(n+1)=r(n)`$. Let $`^{}=\{r^+:r\}`$. The valuation $`\pi ^{}`$ is given by $`\pi ^{}(r,0)(p)=\mathrm{𝐟𝐚𝐥𝐬𝐞}`$ and $`\pi ^{}(r,n+1)(p)=\pi (r,n)(p)`$, for $`n0`$ and propositions $`p`$. It is clear that $`^{}`$ is a system with unique initial states. Moreover, if $``$ is synchronous, then so is $`^{}`$, and if $``$ is a system with perfect recall then so is $`^{}`$. A straightforward induction on the construction of the formula $`\phi \text{CKL}_m`$ now shows that, for all points $`(r,n)`$ in $``$, we have $`(,r,n)\phi `$ iff $`(^{},r^+,n+1)\phi `$.

### 5.2 Dealing with $`𝒞_m^{\mathrm{𝑝𝑟}}`$ and $`𝒞_m^{\mathrm{𝑝𝑟},\mathrm{𝑢𝑖𝑠}}`$ (Theorem 3.4)

We want to show that S5$`{}_{m}{}^{U}+\mathrm{KT3}`$ is sound and complete with respect to $`𝒞_m^{\mathrm{𝑝𝑟}}`$. We first consider soundness. As we observed above, all axioms and rules of inference other than KT3 are known to be sound in all systems, so their soundness in systems $`𝒞_m^{\mathrm{𝑝𝑟}}`$ is immediate. The next result establishes soundness of KT3.

###### Lemma 5.4

: All instances of KT3 are valid in $`𝒞_m^{\mathrm{𝑝𝑟}}`$.

Proof: To show that KT3 is sound, we assume that $`(,r,n)K_i\phi _1(K_i\phi _2\neg K_i\phi _3)`$. We show that $`(,r,n)L_i((K_i\phi _1)U[(K_i\phi _2)U\neg \phi _3])`$. Now it follows from the assumption that $`(,r,n+1)\neg K_i\phi _3`$, so there exists a point $`(r^{},n^{})`$ such that $`(r,n+1)_i(r^{},n^{})`$ and $`(,r^{},n^{})\neg \phi _3`$. Since $`𝒞_m^{\mathrm{𝑝𝑟}}`$, by condition (d) of Lemma 2.2 either (i) $`(r,n)_i(r^{},n^{})`$ or (ii) there exists a number $`l<n^{}`$ such that $`(r,n)_i(r^{},l)`$ and $`(r,n+1)_i(r^{},k)`$ for all $`k`$ with $`l<kn^{}`$. We claim that in either case $`(,r,n)L_i((K_i\phi _1)U[(K_i\phi _2)U\neg \phi _3])`$. In case (i), since $`(,r^{},n^{})\neg \phi _3`$, we have $`(,r^{},n^{})(K_i\phi _1)U[(K_i\phi _2)U\neg \phi _3]`$. The desired conclusion is then immediate from the fact that $`(r,n)_i(r^{},n^{})`$. In case (ii), since $`(,r,n)K_i\phi _1`$, and $`(r,n)_i(r^{},l)`$, we have that $`(,r^{},l)K_i\phi _1`$. Similarly, because $`(,r,n+1)K_i\phi _2`$, we obtain that $`(,r^{},k)K_i\phi _2`$ for all $`k`$ with $`l<kn^{}`$. Together with $`(,r^{},n^{})\neg \phi _3`$, this implies that $`(,r^{},l)(K_i\phi _1)U[(K_i\phi _2)U\neg \phi _3]`$. Again, since $`(r,n)_i(r^{},l)`$, we obtain that $`(,r,n)L_i((K_i\phi _1)U[(K_i\phi _2)U\neg \phi _3])`$.

We now establish a lemma characterizing the interaction of knowledge and time in the pre-model. This result will enable us to satisfy the perfect recall requirement in using the pre-model to construct an interpreted system. It is convenient to introduce the notation $`[s]_i`$, where $`s`$ is a state, for the set of $`(\sigma \mathrm{\#}i)`$-states $`t`$ such that $`s_it`$. The reader is encouraged to compare the following result with condition (d) of Lemma 2.2.

###### Lemma 5.5

: Suppose that the axiomatization includes KT3. Then for all $`\sigma `$-states $`s,t`$ and for all $`(\sigma \mathrm{\#}i)`$-states $`t^{}`$, if $`st`$ and $`t_it^{}`$, then either (a) $`s_it^{}`$ or (b) there exists a $`(\sigma \mathrm{\#}i)`$-state $`s^{}`$ such that $`s_is^{}`$ and there exists a sequence of $`(\sigma \mathrm{\#}i)`$-states $`u_0u_1\mathrm{}u_n=t^{}`$, where $`n0`$, such that $`s^{}u_0`$ and $`u_l_iu_{l+1}`$ for all $`l=0\mathrm{}n1`$.

Proof: We derive a contradiction from the assumption that $`st`$ and $`t_it^{}`$, but $`s_it^{}`$ and for all $`(\sigma \mathrm{\#}i)`$-states $`s^{}`$ such that $`s_is^{}`$ and all sequences of $`(\sigma \mathrm{\#}i)`$-states $`u_0u_1\mathrm{}u_n`$ such that $`s^{}u_0`$ and $`u_i_iu_{i+1}`$ for $`i=0\mathrm{}n1`$, we have $`u_nt^{}`$. Let $`T`$ be the smallest set of $`(\sigma \mathrm{\#}i)`$-states such that

1. if $`v[s]_i`$, $`vv^{}`$, and $`v^{}[t]_i`$ then $`v^{}T`$, and
2. if $`vT`$, $`vv^{}`$, and $`v^{}[t]_i`$ then $`v^{}T`$.

Because $`s_it^{}`$, it follows from the fact that $`_i`$ is an equivalence relation that the intersection $`[s]_i[t]_i`$ is empty. Additionally, $`t^{}`$ is not in $`T`$, for otherwise we could find a sequence of the sort presumed not to exist. Thus, for all $`vT`$, we have $`\phi _v\neg \phi _t^{}`$. This implies that $`\phi _T\neg \phi _t^{}`$. Let $`T^{}`$ be the set of $`(\sigma \mathrm{\#}i)`$-states $`v^{}`$ such that $`vv^{}`$ for some $`vT`$. We want to show that

$$v^{}\phi _T(\neg K_i\mathrm{\Phi }_{t,i}^+\neg \phi _t^{})$$
(1)
for all $`v^{}T^{}`$. If $`v^{}T`$, then clearly we have $`v^{}\phi _T`$, so (1) holds. If $`v^{}T`$, then the second condition in the definition of $`T`$ implies that $`v^{}`$ is not in $`[t]_i`$. It follows using Lemma 4.3(d) that $`v^{}\neg K_i\mathrm{\Phi }_{t,i}^+`$. Further, $`t_iv^{}`$ implies that $`v^{}t^{}`$, so $`v^{}\neg \phi _t^{}`$. Thus, again we have (1). Since (1) holds for all $`v^{}T`$, it follows that $`\phi _T^{}(\phi _T(\neg K_i\mathrm{\Phi }_{t,i}^+\neg \phi _t^{}))`$. Now by Lemma 4.4, we have $`\phi _T\phi _T^{}`$, so using T1 and RT1 we obtain that $`\phi _T(\phi _T(\neg K_i\mathrm{\Phi }_{t,i}^+\neg \phi _t^{}))`$. Combining this with $`\phi _T\neg \phi _t^{}`$ and using Lemma 4.5, we get that $`\phi _T\neg (K_i\mathrm{\Phi }_{t,i}^+U\phi _t^{})`$. In particular, we obtain $`v\neg (K_i\mathrm{\Phi }_{t,i}^+U\phi _t^{})`$ for all states $`v`$ in $`T`$.

We now repeat this argument to obtain a similar conclusion for the elements of $`[s]_i`$. Since $`t^{}`$ is not in $`[s]_i`$ we have that $`v[s]_i`$ implies $`v\neg \phi _t^{}`$. Further, since $`[s]_i[t]_i`$ is empty we also have by Lemma 4.3(d) that $`v[s]_i`$ implies $`v\neg K_i\mathrm{\Phi }_{t,i}^+`$. Using T3 this yields that $`\mathrm{\Phi }_{s,i}^+\neg (K_i\mathrm{\Phi }_{t,i}^+U\phi _t^{})`$.

Let $`P`$ be the set of $`(\sigma \mathrm{\#}i)`$-states $`v^{}`$ such that $`vv^{}`$ for some $`v[s]_i`$. Let $`v^{}P`$. We want to show that

$$v^{}\mathrm{\Phi }_{s,i}^+(\neg K_i\mathrm{\Phi }_{s,i}^+\neg (K_i\mathrm{\Phi }_{t,i}^+U\phi _t^{})).$$
(2)
If $`v^{}[s]_i`$ then clearly $`v^{}\mathrm{\Phi }_{s,i}^+`$, so (2) holds. If $`v^{}[s]_i`$, then, by Lemma 4.3(d), we have that $`v^{}\neg K_i\mathrm{\Phi }_{s,i}^+`$. We now consider two subcases: (a) $`v^{}T`$ and (b) $`v^{}T`$. If $`v^{}T`$ then, as we showed earlier, we have $`v^{}\neg (K_i\mathrm{\Phi }_{t,i}^+U\phi _t^{})`$. If $`v^{}T`$, then by the definition of $`T`$ it follows that $`t_iv^{}`$. By Lemma 4.3(d), this implies that $`v^{}\neg K_i\mathrm{\Phi }_{t,i}^+`$. Further, since $`t_it^{}`$, we also obtain that $`v^{}t^{}`$, so $`v^{}\neg \phi _t^{}`$. Using T3, this yields $`v^{}\neg (K_i\mathrm{\Phi }_{t,i}^+U\phi _t^{})`$, and again we have (2). Using Lemma 4.4, we obtain that $`\mathrm{\Phi }_{s,i}^+[\mathrm{\Phi }_{s,i}^+(\neg K_i\mathrm{\Phi }_{s,i}^+\neg (K_i\mathrm{\Phi }_{t,i}^+U\phi _t^{}))]`$. Applying Lemma 4.5 to this and the result of the preceding paragraph establishes that $`\mathrm{\Phi }_{s,i}^+\neg (K_i\mathrm{\Phi }_{s,i}^+U(K_i\mathrm{\Phi }_{t,i}^+U\phi _t^{}))`$.

It follows using Lemma 4.3(b), R2, and K2 that $`sK_i\neg (K_i\mathrm{\Phi }_{s,i}^+U(K_i\mathrm{\Phi }_{t,i}^+U\phi _t^{}))`$. By KT3, we obtain $`s\neg (K_i\mathrm{\Phi }_{s,i}^+(K_i\mathrm{\Phi }_{t,i}^+L_i\phi _t^{}))`$. Since, by Lemma 4.3(b), $`sK_i\mathrm{\Phi }_{s,i}^+`$, we obtain using T2 that $`s\neg (K_i\mathrm{\Phi }_{t,i}^+L_i\phi _t^{}))`$. Because $`st`$, we have that $`\phi _s\phi _t`$ is consistent, so it follows that $`\phi _t\neg (K_i\mathrm{\Phi }_{t,i}^+L_i\phi _t^{})`$ is consistent. But, by Lemma 4.3, $`tK_i\mathrm{\Phi }_{t,i}^+L_i\phi _t^{}`$, so this is a contradiction.

We are now ready to define, for each consistent $`\psi `$, an enriched+ system for $`\psi `$ that establishes completeness of $`\mathrm{S5}_m^U+KT3`$ with repect to $`𝒞_m^{\mathrm{𝑝𝑟}}`$. The runs of this system are those derived from the acceptable sequences $`(s_0,s_1,\mathrm{})`$ (of states for $`\psi `$) by putting $`r_e(n)=s_n`$ and $`r_i(n)=O_i(s_0)\mathrm{\#}\mathrm{}\mathrm{\#}O_i(s_n)`$, for each agent $`i`$ and $`n0`$. Thus, $`r_i(n)`$ is the sequence of current information that agent $`i`$ has had up to time $`n`$. Let $`^{\mathrm{𝑝𝑟}}`$ be the set of runs defined in this way. The function $`\mathrm{\Sigma }`$ is given by $`\mathrm{\Sigma }(r,n)=s_n`$ for each $`n0`$.

###### Lemma 5.6

: Suppose that the axiomatization includes KT3. Then $`(^{\mathrm{𝑝𝑟}},\mathrm{\Sigma })`$ is an enriched+ system.

Proof: It is clear that $`(^{\mathrm{𝑝𝑟}},\mathrm{\Sigma })`$ satisfies Conditions 1 and 2 of Definition 4.9. It remains to show that Condition 3 holds. So suppose that $`\mathrm{\Sigma }(r,n)`$ is a $`\sigma `$-state and $`\mathrm{\Sigma }(r,n)_is`$ for some $`(\sigma \mathrm{\#}i)`$-state $`s`$. We must find a point $`(r^{},n^{})`$ such that $`\mathrm{\Sigma }(r^{},n^{})=s`$.

The proof proceeds by induction on $`n`$. The result for $`n=0`$ is immediate, since we can take $`r^{}`$ to be an acceptable sequence starting from $`s`$ (such a sequence exists by Lemma 5.1), so $`\mathrm{\Sigma }(r^{},0)=s`$ and clearly $`(r,0)_i(r^{},0)`$.

Now suppose $`n>0`$ and the result holds for $`n1`$. Because $`\mathrm{\Sigma }(r,n1)\mathrm{\Sigma }(r,n)`$ and $`\mathrm{\Sigma }(r,n)_is`$, it follows by Lemma 5.5 that either (a) $`\mathrm{\Sigma }(r,n1)_is`$ or (b) there exists a $`(\sigma \mathrm{\#}i`$)-state $`s^{}`$ such that $`\mathrm{\Sigma }(r,n1)_is^{}`$ and there exists a sequence of $`(\sigma \mathrm{\#}i)`$-states $`u_0u_1\mathrm{}u_k`$ such that $`s^{}u_0`$, $`u_l_iu_{l+1}`$ for $`l=0\mathrm{}k1`$, and $`u_k=s`$. By the induction hypothesis, there exists for any $`(\sigma \mathrm{\#}i)`$-state $`t`$ with $`\mathrm{\Sigma }(r,n1)_it`$ a point $`(r^{},n^{})`$ such that $`(r,n1)_i(r^{},n^{})`$ and $`\mathrm{\Sigma }(r^{},n^{})=t`$. In case (a), we take $`t=s`$, and we then have that $`\mathrm{\Sigma }(r,n1)_i\mathrm{\Sigma }(r,n)`$ and $`\mathrm{\Sigma }(r^{},n^{})=s`$. It follows that $`(r,n)_i(r^{},n1)`$, and by the transitivity of $`_i`$, we also have $`(r,n)_i(r^{},n^{})`$. Hence we are done. In case (b), we take $`t=s^{}`$. Suppose that $`r^{}`$ is derived from the sequence $`(v_0,v_1,\mathrm{})`$. Let $`r^{\prime \prime }`$ be any run derived from an acceptable sequence with initial segment $`(v_0,\mathrm{},v_n^{},u_0,\mathrm{},u_k)`$. Again, such a run exists by Lemma 5.1. By construction, $`\mathrm{\Sigma }(r^{\prime \prime },n^{}+k+1)=u_k=s`$. Moreover, since $`r_i^{\prime \prime }(n^{})=r_i^{}(n^{})=r_i(n1)`$ and $`O_i(u_l)=O_i(s)`$ for all $`l=0,\mathrm{},k`$, we have $`r_i^{\prime \prime }(n^{}+k+1)=r_i^{\prime \prime }(n^{})\mathrm{\#}O_i(u_0)\mathrm{\#}\mathrm{}\mathrm{\#}O_i(u_k)=r_i(n1)\mathrm{\#}O_i(s)=r_i(n)`$, and hence $`(r,n)_i(r^{\prime \prime },n^{}+k+1)`$.

Now take any $`ϵ`$-state $`s`$ such that $`s\psi `$, and let $`r`$ be a run derived from an acceptable sequence starting with $`s`$. By construction, the system $``$ obtained from the enriched+ system is in $`𝒞_m^{\mathrm{𝑝𝑟}}`$, and by Corollary 4.11, we have $`(,r,0)\psi `$. Thus, $`\psi `$ is satisfiable in $`𝒞_m^{\mathrm{𝑝𝑟}}`$. By Lemma 5.3, $`\psi `$ is also satisfiable in systems in $`𝒞_m^{\mathrm{𝑝𝑟},\mathrm{𝑢𝑖𝑠}}`$. Since this argument applies to any formula $`\psi `$ consistent with respect to $`\mathrm{S5}_m^U+KT3`$, this completes the proof of Theorem 3.4.

### 5.3 Dealing with $`𝒞_m^{\mathrm{𝑝𝑟},\mathrm{𝑠𝑦𝑛𝑐}}`$ and $`𝒞_m^{\mathrm{𝑝𝑟},\mathrm{𝑠𝑦𝑛𝑐},\mathrm{𝑢𝑖𝑠}}`$ (Theorem 3.5)

We now show that $`\mathrm{S5}_m^U+KT2`$ is sound and complete with respect to $`\text{KL}_m`$ for the classes of systems $`𝒞_m^{\mathrm{𝑝𝑟},\mathrm{𝑠𝑦𝑛𝑐}}`$ and $`𝒞_m^{\mathrm{𝑝𝑟},\mathrm{𝑠𝑦𝑛𝑐},\mathrm{𝑢𝑖𝑠}}`$. For soundness, the following result suffices.

###### Lemma 5.7

: All instances of KT2 are valid in $`𝒞_m^{\mathrm{𝑝𝑟},\mathrm{𝑠𝑦𝑛𝑐}}`$.

Proof: Let $``$ be a system in $`𝒞_m^{\mathrm{𝑝𝑟},\mathrm{𝑠𝑦𝑛𝑐}}`$ and let $`r`$ be a run of $``$. Suppose that $`(,r,n)K_i\phi `$. If $`(r,n+1)_i(r^{},n^{})`$, then by synchrony we must have $`n^{}=n+1`$. Thus, by perfect recall and synchrony, we have $`(r,n)_i(r^{},n^{}1)`$. It follows that $`(,r^{},n^{}1)\phi `$, which implies that $`(,r^{},n^{})\phi `$. This shows that $`(,r^{},n^{})\phi `$ for all $`(r^{},n^{})_i(r,n+1)`$. Thus, we have $`(,r,n+1)K_i\phi `$, and hence $`(,r,n)K_i\phi `$.

Before constructing an enriched+ system for the completeness part, we first note a property of the pre-model, analogous to Lemma 5.5.

###### Lemma 5.8

: Suppose that the axiomatization includes KT2. Then for all $`\sigma `$-states $`s,t`$ with $`st`$, we have that for all $`(\sigma \mathrm{\#}i)`$-states $`t^{}`$ with $`t_it^{}`$ there exists a $`(\sigma \mathrm{\#}i)`$-state $`s^{}`$ such that $`s_is^{}`$ and $`s^{}t^{}`$.

Proof: By way of contradiction, suppose that $`s,t`$ are $`\sigma `$-states with $`st`$ that $`t^{}`$ is a $`(\sigma \mathrm{\#}i)`$-state such that $`t_it^{}`$, but that for all $`(\sigma \mathrm{\#}i)`$-states $`s^{}`$ such that $`s_is^{}`$, we have that $`s^{}\neg \phi _t^{}`$. By T2, we have that $`s^{}\neg \phi _t^{}`$ for all $`(\sigma \mathrm{\#}i)`$-states $`s^{}`$ such that $`s_is^{}`$. By Lemma 4.3(b), it follows that $`sK_i\neg \phi _t^{}`$. By KT2, we have that $`sK_i\neg \phi _t^{}`$. Since $`st`$, it follows that $`\phi _tK_i\neg \phi _t^{}`$ is consistent. However, since $`t_it^{}`$, by Lemma 4.3(c), we have $`tL_i\phi _t^{}`$. This is a contradiction.

To construct the enriched+ system, we now take $`^{\mathrm{𝑝𝑟},\mathrm{𝑠𝑦𝑛𝑐}}`$ to be the set of runs $`r`$ derived from acceptable sequences $`(s_0,s_1,\mathrm{})`$ of states for the formula $`\psi `$ by putting $`r_e(n)=s_n`$ and $`r_i(n)=O_i(s_0)\mathrm{}O_i(s_n)`$, for each agent $`i`$ and $`n0`$. The notation $`O_i(s_0)\mathrm{}O_i(s_n)`$ is meant to denote the sequence formed by concatening $`O_i(s_0),O_i(s_1),\mathrm{},O_i(s_n)`$. Thus, the length of the sequence is $`n+1`$, which enforces synchrony. Again, the function $`\mathrm{\Sigma }`$ is given by $`\mathrm{\Sigma }(r,n)=s_n`$ for each $`n0`$.

###### Lemma 5.9

: Suppose that the axiomatization includes KT2. Then $`(^{\mathrm{𝑝𝑟},\mathrm{𝑠𝑦𝑛𝑐}},\mathrm{\Sigma })`$ is an enriched+ system.

Proof: Conditions 1 and 2 of the definition of an enriched+ system are immediate. To show that Condition 3 holds, suppose that $`\mathrm{\Sigma }(r,n)`$ is a $`\sigma `$-state, and $`t`$ is a $`(\sigma \mathrm{\#}i)`$-state such that $`\mathrm{\Sigma }(r,n)_it`$. Suppose that $`r`$ is derived from the acceptable sequence $`(s_0,s_1,\mathrm{})`$, so $`\mathrm{\Sigma }(r,n)=s_n`$. It follows from Lemma 5.8 that there exists a $``$-sequence $`t_0\mathrm{}t_n`$ such that $`t_n=t`$ and $`s_j_it_j`$ for $`j=1\mathrm{}n`$. By Lemma 5.1, this sequence may be extended to an infinite acceptable sequence. Taking $`r^{}`$ to be the run derived from this sequence, we see that $`(r,n)_i(r^{},n)`$ and $`\mathrm{\Sigma }(r^{},n)=t`$.

Take $`^{\mathrm{𝑝𝑟},\mathrm{𝑠𝑦𝑛𝑐}}`$ to be the system obtained from $`(^{\mathrm{𝑝𝑟},\mathrm{𝑠𝑦𝑛𝑐}},\mathrm{\Sigma })`$. By construction, this system is in $`𝒞^{\mathrm{𝑝𝑟},\mathrm{𝑠𝑦𝑛𝑐}}`$. Now take any $`ϵ`$-state $`s`$ such that $`s\psi `$, and let $`r`$ be a run derived from an acceptable sequence starting with $`s`$. By construction, the system $``$ obtained from the enriched+ system is in $`𝒞_m^{\mathrm{𝑝𝑟},\mathrm{𝑠𝑦𝑛𝑐}}`$, and by Corollary 4.11, we have $`(,r,0)\psi `$. Thus, $`\psi `$ is satisfiable in $`𝒞_m^{\mathrm{𝑝𝑟},\mathrm{𝑠𝑦𝑛𝑐}}`$. By Lemma 5.3, $`\psi `$ is also satisfiable in systems in $`𝒞_m^{\mathrm{𝑝𝑟},\mathrm{𝑠𝑦𝑛𝑐},\mathrm{𝑢𝑖𝑠}}`$. Since this argument applies to any formula $`\psi `$ consistent with respect to $`\mathrm{S5}_m^U+KT2`$, this completes the proof of Theorem 3.5.

### 5.4 Dealing with $`𝒞_m^{\mathrm{𝑛𝑙}}`$ (Theorem 3.6)

We want to show that $`\mathrm{S5}_m^U+\mathrm{KT4}`$ is sound and complete for $`\text{KL}_m`$ with respect to $`𝒞_m^{\mathrm{𝑛𝑙}}`$. For soundness, it suffices to show that KT4 is valid in $`𝒞_m^{\mathrm{𝑛𝑙}}`$. This is straightforward.

###### Lemma 5.10

: All instances of KT4 are valid in $`𝒞_m^{\mathrm{𝑛𝑙}}`$.

Proof: Suppose that $`𝒞_m^{\mathrm{𝑛𝑙}}`$ and $`(,r,n)K_i\phi UK_i\psi `$. We want to show that $`(,r,n)K_i(K_i\phi UK_i\psi )`$. Thus, if $`(r^{},n^{})_i(r,n)`$, we must show that $`(,r^{},n^{})K_i\phi UK_i\psi `$. Since $`(,r,n)K_i\phi UK_i\psi `$, there exists $`ln`$ such that $`(,r,l)K_i\psi `$ and $`(,r,k)K_i\phi \neg K_i\psi `$ for all $`k`$ with $`nk<l`$. Note that this means that if $`nk<l`$, then $`r_i(k)r_i(l)`$. Since $`𝒞_m^{\mathrm{𝑛𝑙}}`$ and $`(r,n)_i(r^{},n^{})`$, there must be some $`l^{}n^{}`$ such that $`((r,n),\mathrm{},(r,l))`$ is $`_i`$-concordant with $`((r,n^{}),\mathrm{},(r,l^{}))`$. Thus, there exists some $`h`$, a partition $`S_1,\mathrm{},S_h`$ of the sequence $`((r,n),\mathrm{},(r,l))`$, and a partition $`T_1,\mathrm{},T_h`$ of the sequence $`((r^{},n^{}),\mathrm{},(r,l^{}))`$ such that for all $`j=1,\mathrm{},h`$, we have $`(r,k)_i(r^{},k^{})`$ for all points $`(r,k)S_j`$ and $`(r^{},k^{})T_j`$. It easily follows that $`(,r^{},n^{})K_i\phi UK_i\psi `$, as desired.

For completeness, we define an appropriate enriched+ system. As we shall see, the demands of no learning make this a little more subtle than in the case of no forgetting.

For the remainder of this section, consistency and provability are with respect to a logic that includes $`\mathrm{S5}_m^U+\mathrm{KT4}`$. Fix a consistent formula $`\psi `$ such that $`\text{ad}(\psi )=d`$.

Our first step is to prove an analogue of Lemma 5.5.

###### Lemma 5.11

: Suppose that the axiomatization includes KT4. If $`s`$ is a $`\sigma `$-state, $`t`$ is a $`(\sigma \mathrm{\#}i)`$-state, $`s_it`$, and $`ss^{}`$, then there exists a sequence $`t_0,\mathrm{},t_k`$ such that (a) $`t=t_0`$, (b) $`t_j_is`$ for $`j<k`$, (c) $`t_jt_{j+1}`$ for $`j<k`$, and (d) $`s^{}_it_k`$.

Proof: If $`s^{}_it`$, then we can take the sequence to consist only of $`t`$, and we are done. Otherwise, since $`\phi _s\phi _s^{}`$ is consistent, it follows from Lemma 4.3(b) that $`\phi _sK_i\mathrm{\Phi }_{s,i}^+UK_i\mathrm{\Phi }_{s^{},i}^+`$ is consistent. Moreover, by Lemma 4.3(c), we have that $`\phi _sL_i\phi _t`$. Thus, $`\phi _sL_i\phi _tK_i\mathrm{\Phi }_{s,i}^+UK_i\mathrm{\Phi }_{s^{},i}^+`$ is consistent. Using KT4, it follows that $`\phi _tK_i\mathrm{\Phi }_{s,i}^+UK_i\mathrm{\Phi }_{s^{},i}^+`$ is consistent. The result now follows from Lemma 4.7.

Unfortunately, Lemma 5.11 does not suffice to construct an enriched+ system. Roughly speaking, the problem is the following. In the case of perfect recall, we used Lemma 5.5 to show that, given a $``$-sequence $`S=(s_0,\mathrm{},s_n)`$ of $`\sigma `$-states and a $`(\sigma \mathrm{\#}i)`$-state $`t`$ such that $`s_n_it`$, we can construct a $``$-sequence $`T`$ of $`(\sigma \mathrm{\#}i)`$-states ending with $`t`$ such that $`S`$ is $`_i`$-concordant with $`T`$. There is no problem then extending $`T`$ to an acceptable sequence. Moreover, we can extend $`S`$ and $`T`$ independently to acceptable sequences; all that matters is that the finite prefixes of these sequences—namely, $`S`$ and $`T`$—are $`_i`$-concordant. With no learning, on the other hand, it is the infinite suffixes that must be $`_i`$-concordant. Given a $``$-sequence $`S=(s_0,\mathrm{})`$ of $`\sigma `$-states and a $`(\sigma \mathrm{\#}i)`$-state $`t`$ such that $`s_0_it`$, using Lemma 5.11, we can find a $``$-sequence $`T`$ starting with $`t`$ that is $`_i`$-concordant with $`S`$. This suggests that it is possible to find the appropriate sequences for the construction of runs satisfying the no learning condition. Unfortunately, it does not follow from the acceptability of $`S`$ that $`T`$ is also acceptable. This makes it necessary to work with a smaller set of sequences than the set of all acceptable sequences, and to build up the sequences $`S`$ and $`T`$ simultaneously. To ensure that the appropriate obligations are satisfied at all points in the set of runs constructed, we need to work not just with single states, but with trees of states.

A $`k`$-tree for $`\psi `$ (with $`kd`$) is a set $`S`$ of $`\sigma `$-states for $`\psi `$ with $`|\sigma |k`$ with a unique $`ϵ`$-state such that if $`sS`$ is a $`\sigma `$-state then

* if $`t`$ is a $`(\sigma \mathrm{\#}i)`$-state such that $`s_it`$ and $`|\sigma \mathrm{\#}i|k`$, then $`tS`$,
* if $`\sigma =\tau \mathrm{\#}i`$, then there is a $`\tau `$-state $`t`$ in $`S`$ such that $`s_it`$.

We extend the $``$ relation to $`k`$-trees as follows. If $`S_1`$ and $`S_2`$ are $`k`$-trees for $`\psi `$, then $`S_1_fS_2`$ if $`f`$ is a function associating with each $`\sigma `$-state $`sS_1`$ a finite sequence of $`\sigma `$-states in $`S_1S_2`$ such that

* if $`f(s)=(s_0,\mathrm{},s_k)`$, then

+ $`s=s_0`$,
    + $`s_0\mathrm{}s_k`$,
    + $`s_0,\mathrm{},s_{k1}S_1`$ and $`s_kS_2`$;
* if $`s_is^{}`$, then $`f(s)`$ and $`f(s^{})`$ are $`_i`$-concordant;
* for at least one $`sS_1`$, the sequence $`f(s)`$ has length at least 2.

Given two sequences of $`\sigma `$-states $`\alpha =(s_0,\mathrm{},s_k)`$ and $`\beta =(t_0,\mathrm{})`$, where $`\alpha `$ is finite, the fusion of $`\alpha `$ and $`\beta `$, denoted $`\alpha \beta `$ is defined only if $`s_k=t_0`$; in this case, it is the sequence $`(s_0,s_{k1},t_0,\mathrm{})`$. Given an infinite sequence $`𝒮=S_0_{f_0}S_1_{f_1}S_2_{f_2}\mathrm{}`$ of $`k`$-trees, we say a sequence $`\alpha `$ of $`\sigma `$-states is compatible with $`𝒮`$ if there exists some $`h`$, and $`\sigma `$-states $`s_h`$, $`s_{h+1},\mathrm{}`$ with $`s_jS_j`$ for $`jh`$, such that $`\alpha =f_h(s_h)f_{h+1}(s_{h+1})\mathrm{}`$. (Implicit in this notation is the assumption that this fusion product is defined, so that the last state in $`f_j(s_j)`$ is the same as the first state in $`f_{j+1}(s_{j+1})`$, for $`jh`$.) A $``$-sequence $`(t_0,t_1,\mathrm{})`$ of $`\sigma `$-states is a compression of $`(s_0,s_1,\mathrm{})`$ if (1) $`t_0=s_0`$, and (b) if $`t_j=s_h`$, then $`t_{j+1}`$ is $`s_h^{}`$, where $`h^{}`$ is the least integer greater than $`h`$ such that $`s_{h^{}1}s_h^{}`$ and $`s_h=\mathrm{}=s_{h^{}1}`$. (If no such $`h^{}`$ exists, then $`t_j`$ is the last element of the compression.) $`𝒮`$ is acceptable if every $``$-sequence that is a compression of some sequence compatible with $`𝒮`$ is infinite and acceptable. Our goal is to construct an acceptable sequence of $`d`$-trees; we shall use this to define the enriched+ system.

Note that by Lemma 4.3, the formula $`\phi _s`$ essentially describes the subtree below $`s`$ of any $`k`$-tree containing $`s`$. Given a $`k`$-tree $`S`$ and a $`\sigma `$-state $`s`$ in $`S`$, we inductively define a formula $`\text{tree}_{S,s}`$ that describes all of $`S`$ from the point of view of $`s`$. If $`s`$ is an $`ϵ`$-state, then $`\text{tree}_{S,s}=\phi _s`$. Otherwise, if $`s`$ is a ($`\tau \mathrm{\#}i`$)-state, where $`\tau \tau \mathrm{\#}i`$, then

$$\text{tree}_{S,s}=\phi _s\underset{\{\tau \mathrm{states}t:s_it\}}{}L_i\text{tree}_{S,t}.$$

If $`S`$ and $`T`$ are $`k`$-trees, $`sS`$, and $`tT`$, then we write $`(S,s)^+(T,t)`$ if there exists a sequence of $`k`$-trees $`S_0,\mathrm{},S_l`$ and functions $`f_0,\mathrm{},f_{l1}`$ such that $`S_0_{f_0}\mathrm{}_{f_{l1}}S_l`$, $`S_0=S`$, $`S_l=T`$, $`f_j(s)=(s)`$ for $`jl2`$, and $`f_{l1}(s)=(s,t)`$.

###### Lemma 5.12

: Suppose that the axiomatization includes KT4, $`S`$ is a $`k`$-tree, and $`s`$ is a $`\sigma `$-state in $`S`$, where $`|\sigma |=k`$.

* If $`t`$ is a $`\sigma `$-state and $`\text{tree}_{S,s}(\phi _t\xi )`$ is consistent, then there exists a $`k`$-tree $`T`$ such that $`tT`$, $`(S,s)^+(T,t)`$, and $`\text{tree}_{T,t}\xi `$ is consistent.
* $`\text{tree}_{S,s}_{\{(T,t):(S,s)^+(T,t)\}}\text{tree}_{T,t}`$ is provable.
* If $`\text{tree}_{S,s}\phi U\phi ^{}`$ is consistent, then for some $`l0`$ there is a sequence $`S_0,\mathrm{},S_l`$ of $`k`$-trees and states $`s_0,\mathrm{},s_l`$ such that (i) $`s_jS_j`$, (ii) $`(S,s)=(S_0,s_0)`$, (iii) $`(S_j,s_j)^+(S_{j+1},s_{j+1})`$ for $`j=0,\mathrm{},l1`$, (iv) $`\text{tree}_{S_j,s_j}\phi `$ is consistent for $`j=0,\mathrm{},l1`$, and (v) $`\text{tree}_{S_l,s_l}\phi ^{}`$ is consistent.

Proof: We proceed by induction on $`k`$. The case that $`k=0`$ is immediate using standard arguments, since then $`\text{tree}_{S,s}`$ is just $`\phi _s`$.

So suppose $`k>0`$ and $`\sigma =\tau \mathrm{\#}i`$, with $`\sigma \tau `$. We first prove part (a) in the case that $`\xi `$ is of the form $`K_i\xi ^{}`$, then part (b), then prove the general case of (a), and then prove (c). First consider (a) in the case that $`\xi `$ is of the form $`K_i\xi ^{}`$. Note that $`\text{tree}_{S,s}(\phi _tK_i\xi ^{})`$ implies $`\text{tree}_{S,s}K_i\mathrm{\Phi }_{s,i}UK_i(\xi ^{}\mathrm{\Phi }_{t,i})`$. From the definition of $`k`$-tree, it follows that there is a $`\tau `$-state $`s^{}`$ in $`S`$ such that $`s_is^{}`$. Let $`S^{}`$ be the $`(k1)`$-tree consisting of all $`\sigma ^{}`$-states in $`S`$ with $`|\sigma ^{}|k1`$. From KT4, it follows that

$$\text{tree}_{S^{},s^{}}K_i\mathrm{\Phi }_{s,i}UK_i(\xi ^{}\mathrm{\Phi }_{t,i})$$

is consistent. Applying part (c) of the inductive hypothesis, we get a sequence $`S_0,\mathrm{},S_l`$ of ($`k1`$)-trees and states $`s_0,\mathrm{},s_l`$ such that (i) $`s_jS_j`$, (ii) $`(S^{},s^{})=(S_0,s_0)`$, (iii) $`(S_j,s_j)^+(S_{j+1},s_{j+1})`$ for $`j=0,\mathrm{},l1`$, (iv) $`\text{tree}_{S_j,s_j}K_i\mathrm{\Phi }_{s,i}`$ is consistent for $`j=0,\mathrm{},l1`$, and (v) $`\text{tree}_{S_l,s_l}K_i(\xi ^{}\mathrm{\Phi }_{t,i})`$ is consistent. It follows by definition that there is a sequence $`T_0,\mathrm{},T_m`$ of $`(k1)`$-trees and functions $`f_0,\mathrm{},f_{m1}`$ such that $`T_0_{f_0}\mathrm{}_{f_{m1}}T_m`$, $`T_0=S_0`$, and $`T_m=S_l`$. Moreover, there are elements $`t_0,\mathrm{},t_m`$ such that $`t_0=s^{}`$, $`t_m=s_l`$, if $`j<m`$, then $`t_j=s_j^{}`$ for some $`j^{}j`$, and if $`t_j=t_{j+1}`$, then $`f_j(t_j)=(t_j)`$, while if $`t_jt_{j+1}`$, then $`f_j(t_j)=(t_j,t_{j+1})`$, for $`j=0,\mathrm{},m1`$.

Let $`T_j^{}`$ be the unique $`k`$-tree extending $`T_j`$, for $`j=0,\mathrm{},m`$. Since $`\phi _{t_j}K_i\mathrm{\Phi }_{s,i}`$ is consistent for $`j<m`$, we have that $`t_j_is`$, and so $`sT_j^{}`$ for $`j<m`$. Similarly, we have that $`tT_m^{}`$. We now show how to construct $`f_j^{}`$, for $`j<m`$. For each state $`u^{}T_j^{}T_j`$, there must exist a state $`uT_j`$ and an agent $`j^{}`$ such that $`u_j^{}u^{}`$. (There may be more than one such state $`u`$, of course. In this case, in the construction below, we can pick $`u`$ arbitrarily.) It easily follows from Lemma 5.11 that there exists a sequence $`\alpha _u^{}`$ starting with $`u^{}`$ that is $`_j^{}`$-concordant with $`f_j(u)`$. Moreover, we can take $`\alpha _{t_j}=(s)`$ for $`j<m1`$, and take $`\alpha _{t_{m1}}=(s,t)`$. We define $`f_j^{}`$ so that it agrees with $`f_j`$ on $`T_j`$, and for each $`u^{}T_j^{}T_j`$, we have $`f_j^{}(u^{})=\alpha _u^{}`$.

Notice that $`T_0^{}=S`$. If $`m>0`$, it follows immediately from the definition that $`(S,s)^+(T_m,t)`$, and that $`\text{tree}_{T_m,t}K_i\xi ^{}`$ is consistent. If $`m=0`$, it is easy to check that we must have $`tS`$, for we have $`s^{}_it`$. Since we also have $`s^{}_is`$, it follows that $`s_it`$. Define $`f`$ so that $`f(u)=(u)`$ for $`us`$ and $`f(s)=(s,t)`$. Then $`(S,s)_f(S,t)`$. Since $`st`$, we have $`(S,s)^+(S,t)`$. This completes the proof of part (a).

To prove part (b), suppose not. Then $`\text{tree}_{S,s}_{\{(T,t):(S,s)^+(T,t)\}}\neg \text{tree}_{T,t}`$ is consistent. Straightforward temporal reasoning shows that there must be some $`u`$ such that

$$\text{tree}_{S,s}(\phi _u\underset{\{(T,t):(S,s)^+(T,t)\}}{}\neg \text{tree}_{T,t})$$
(3)
is consistent. Now $`\neg \text{tree}_{T,t}`$ is equivalent to $`\neg \phi _t_{\{\tau \mathrm{states}t^{}:t^{}_it\}}K_i\neg \text{tree}_{T,t^{}}`$. Thus, it follows that the consistency of (3) implies that for each tree $`T`$ such that $`(S,s)^+(T,u)`$, there is a $`\tau `$-state $`t_T_iu`$ such that

$$\text{tree}_{S,s}(\phi _uK_i(\underset{\{T:(S,s)^+(T,u)\}}{}\neg \text{tree}_{T,t_T}))$$
(4)
is consistent. By part (a), there exists a $`k`$-tree $`T^{}`$ and $`t^{}T^{}`$ such that $`(S,s)^+(T^{},t^{})`$ and $`\text{tree}_{T^{},t^{}}\phi _uK_i(_{\{T:(S,s)^+(T,u)\}}\neg \text{tree}_{T,t_T})`$ is consistent. But this means that $`t^{}=u`$. Thus, we have a contradiction, since $`\text{tree}_{T^{},u}K_i\neg \text{tree}_{T^{},t_T^{}}`$ is inconsistent.

The general case of (a) follows easily from (b). Part (c) also follows from part (b), using arguments much like those of Lemma 4.7; we omit details here.

###### Lemma 5.13

: Suppose that the axiomatization includes KT4 and $`\psi `$ is consistent. Then there is an acceptable sequence of $`d`$-trees such that $`\psi `$ is true at the root of the first tree.

Proof: The key part of the proof is to show that given a finite sequence $`S_0_{f_0}\mathrm{}_{f_{l1}}S_l`$ of $`d`$-trees and a $`\sigma `$-state $`s`$ in $`S_l`$ such that $`s\phi `$ (resp., $`s\phi _1U\phi _2`$), we can extend the sequence of trees in such a way as to satisfy this obligation. This follows easily from Lemmas 5.11 and 5.12. In more detail, suppose $`s\phi _1U\phi _2`$. Let $`S^{}`$ be consist of all $`\tau `$-states in $`S_l`$, with $`|\tau |k=|\sigma |`$. By Lemma 5.12, we can find a sequence of $`k`$-trees starting with $`S^{}`$ that satisfies this obligation. Using Lemma 5.11, we can extend this to a sequence of $`d`$-trees starting with $`S_l`$ that satisfies the obligation. The argument in the case that $`s_k\phi `$ is similar. We can then take care of the obligations one by one, and construct an acceptable sequence, in the obvious way.

Since $`\psi `$ is consistent, there must be some tree $`S`$ with root $`s_0`$ such that $`s_0\psi `$. We just extend $`S`$ as above to complete the proof.

Once we have an acceptable sequence $`𝒮`$ of $`d`$-trees as in Lemma 5.13, we can easily construct the enriched+ system much as we did in the case of perfect recall. Given a $``$-sequence $`s_0s_1\mathrm{}`$ the $`\mathrm{𝑛𝑙}`$-run $`r`$ derived from it is defined so that $`r_e(n)=s_n`$ and $`r_i(n)=O_i(s_n)\mathrm{\#}O_i(s_{n+1})\mathrm{\#}\mathrm{}`$, for each agent $`i`$ and $`n0`$. Thus, while for perfect recall, we take $`r_i(n)`$ to consist of the agent’s current information up to time $`n`$, for no learning, we take $`r_i(n)`$ to consist of the current information from time $`n`$ on. The construction stresses the duality between perfect recall and no learning. Let $`^{\mathrm{𝑛𝑙}}`$ consist of all the $`\mathrm{𝑛𝑙}`$-runs derived from $``$-sequences that are compressions of sequences of states compatible with $`𝒮`$. Again, the function $`\mathrm{\Sigma }`$ is given by $`\mathrm{\Sigma }(r,n)=s_n`$ for each $`n0`$.

###### Lemma 5.14

: Suppose the axiomatization includes KT4. Then $`(^{\mathrm{𝑛𝑙}},\mathrm{\Sigma })`$ is an enriched+ system.

Proof: Again, Conditions 1 and 2 in the definition of enriched+ system follow immediately from the construction. For Condition 3, suppose that $`(r,n)`$ is a point in the system, $`\mathrm{\Sigma }(r,n)`$ is a $`\sigma `$-state, and $`s`$ is a $`(\sigma \mathrm{\#}i)`$-state with $`s_i\mathrm{\Sigma }(r,n)`$. Suppose $`𝒮=S_0_{f_0}S_1_{f_1}S_2_{f_2}\mathrm{}`$. By definition, the run $`\mathrm{𝑛𝑙}`$-run $`r`$ is derived from the compression of some sequence $`(s_0,s_1,s_2,\mathrm{})`$ of $`\sigma `$-states compatible with $`𝒮`$. Suppose $`\mathrm{\Sigma }(r,n)`$ is in the interval of this sequence from $`S_k`$. Then $`s`$ must also be in $`S_k`$. Let $`(t_0,t_1,\mathrm{})`$ be the (unique) sequence compatible with $`𝒮`$ that starts at $`s`$ in $`S_k`$. Let $`r^{}`$ be the run derived from the compression of this sequence. Then, by definition, we have $`\mathrm{\Sigma }(r^{},0)=s`$ and $`(r,n)_i(r^{},0)`$.

Take $`^{\mathrm{𝑛𝑙}}`$ to be the system obtained from $`(^{\mathrm{𝑛𝑙}},\mathrm{\Sigma })`$. By construction, this system is in $`𝒞^{\mathrm{𝑛𝑙}}`$. Now take any $`ϵ`$-state $`s`$ such that $`s\psi `$, and let $`r`$ be a run derived from the compression of a sequence compatible with $`𝒮`$ starting with $`s`$. It follows that $`(,r,0)\psi `$. Thus, $`\psi `$ is satisfiable in $`𝒞_m^{\mathrm{𝑛𝑙}}`$. This completes the proof of Theorem 3.6.

### 5.5 Dealing with $`𝒞_m^{\mathrm{𝑛𝑙},\mathrm{𝑝𝑟}}`$ and $`𝒞_1^{\mathrm{𝑛𝑙},\mathrm{𝑝𝑟},\mathrm{𝑢𝑖𝑠}}`$ (Theorem 3.7)

We now want to show that $`\mathrm{S5}_m^U+\mathrm{KT3}+\mathrm{KT4}`$ is sound and complete for $`\text{KL}_m`$ with respect to $`𝒞_m^{\mathrm{𝑛𝑙},\mathrm{𝑝𝑟}}`$. Soundness is immediate from Lemmas 5.4 and 5.10.

For completeness, we construct an enriched+ system much as in the proof of Theorem 3.6, using $`k`$-trees. By Lemma 5.13, there is an acceptable sequence $`𝒮`$ of $`d`$-trees such that $`\psi `$ is true at the root of the first tree. Given a $``$-sequence $`(s_0,s_1,\mathrm{}.)`$, the nl-nf run $`r`$ derived from it is defined so that $`r_e(n)=s_n`$ and $`r_i(n)=(O_i(s_0)\mathrm{\#}O_i(s_1)\mathrm{\#}\mathrm{}\mathrm{\#}O_i(s_n),O_i(s_n)\mathrm{\#}O_i(s_{n+1})\mathrm{\#}\mathrm{})`$, for each agent $`i`$ and $`n0`$. Thus, the agents’ local states enforce both perfect recall (by keeping track of all the information up to time $`n`$) and no learning (by keeping track of the current information from time $`n`$ on). Let $`^{\mathrm{𝑛𝑙},\mathrm{𝑝𝑟}}`$ consist of all nl-nf-runs that are derived from $``$-sequences that have a suffix that is the compression of a sequence of states compatible with $`𝒮`$. Note that now we consider $``$-sequences whose suffixes are compressions of sequences compatible with $`𝒮`$. The reason to allow the greater generality of suffixes will become clear shortly. Since $`𝒮`$ is acceptable, it is easy to see that every such $``$-sequence must be infinite and acceptable. Again, the function $`\mathrm{\Sigma }`$ is given by $`\mathrm{\Sigma }(r,n)=s_n`$ for each $`n0`$.

###### Lemma 5.15

: Suppose the axiomatization includes KT3 and KT4. Then $`(^{\mathrm{𝑛𝑙},\mathrm{𝑝𝑟}},\mathrm{\Sigma })`$ is an enriched+ system.

Proof: As usual, Conditions 1 and 2 in the definition of enriched+ system follow immediately from the construction. For Condition 3, suppose that $`(r,n)`$ is a point in the system, $`\mathrm{\Sigma }(r,n)`$ is a $`\sigma `$-state, and $`s`$ is a $`(\sigma \mathrm{\#}i)`$-state. Suppose $`𝒮=S_0_{f_0}S_1_{f_1}S_2_{f_2}\mathrm{}`$. By definition, the run $`\mathrm{𝑛𝑙}`$$`\mathrm{𝑝𝑟}`$-run $`r`$ is derived from a $``$-sequence $`(s_0,s_1,\mathrm{})`$ that has a suffix $`(s_N,s_{N+1},\mathrm{})`$ that is the compression of some sequence $`(t_0,t_1,t_2,\mathrm{})`$ of $`\sigma `$-states compatible with $`𝒮`$, and $`\mathrm{\Sigma }(r,n)=s_n`$. There are now two cases to consider. If $`nN`$, then there exists some $`k`$ such that $`s_n`$ is in $`S_k`$. Then $`s`$ must also be in $`S_k`$. Let $`(u_0,u_1,\mathrm{})`$ be the unique sequence compatible with $`𝒮`$ that starts with $`s`$ in $`S_k`$. By Lemma 5.5, there exist $`\sigma \mathrm{\#}i`$-states $`v_0\mathrm{}v_h`$ such that $`v_h=s`$ and $`(v_0,\mathrm{},v_h)`$ is $`_i`$-compatible with $`(s_0,\mathrm{},s_n)`$. Consider the $``$-sequence formed from the fusion of $`(v_0,\mathrm{},v_h)`$ and the compression of $`(u_0,u_1,\mathrm{})`$. By construction, the $`\mathrm{𝑛𝑙}`$$`\mathrm{𝑝𝑟}`$-run $`r^{}`$ derived from this $``$-sequence is in $`^{\mathrm{𝑛𝑙},\mathrm{𝑝𝑟}}`$, $`\mathrm{\Sigma }(r^{},h)=s`$, and $`(r,n)_i(r^{},h)`$.

Now suppose $`n<N`$. By Lemma 5.5, there exist $`(\sigma \mathrm{\#}i)`$-states $`v_0\mathrm{}v_h`$ such that $`v_h=s`$ and $`(v_0,\mathrm{},v_h)`$ is $`_i`$-concordant with $`(s_0,\mathrm{},s_n)`$. Moreover, by Lemma 5.11, this sequence can be extended to a sequence $`(v_0,\mathrm{}.v_k)`$ that is $`_i`$-concordant with $`(s_0,\mathrm{},s_N)`$. Since $`s_NS_M`$ for some $`M`$, we must have $`v_kS_M`$. Let $`(u_0,u_1,\mathrm{})`$ be the unique sequence compatible with $`𝒮`$ that starts at $`v_k`$ in $`S_M`$. Consider the $``$-sequence formed from the fusion of $`(v_0,\mathrm{},v_k)`$ and the compression of $`(u_0,u_1,\mathrm{})`$. By construction, the $`\mathrm{𝑛𝑙}`$$`\mathrm{𝑝𝑟}`$-run $`r^{}`$ derived from this $``$-sequence is in $`^{\mathrm{𝑛𝑙},\mathrm{𝑝𝑟}}`$, $`\mathrm{\Sigma }(r^{},h)=s`$, and $`(r,n)_i(r^{},h)`$.

Again, we complete the proof by taking $`^{\mathrm{𝑛𝑙},\mathrm{𝑝𝑟}}`$ to be the system obtained from $`(^{\mathrm{𝑛𝑙},\mathrm{𝑝𝑟}},\mathrm{\Sigma })`$. By construction, this system is in $`𝒞^{\mathrm{𝑛𝑙},\mathrm{𝑝𝑟}}`$ and satisfies $`\psi `$. This shows that $`\mathrm{S5}_m^U+\mathrm{KT3}+\mathrm{KT4}`$ is a sound and complete axiomatization for the language $`\text{KL}_m`$ with respect to $`𝒞_m^{\mathrm{𝑛𝑙},\mathrm{𝑝𝑟}}`$ for all $`m`$.

The fact that it is also a sound and complete axiomatization for the language $`\text{KL}_1`$ with respect to $`𝒞_1^{\mathrm{𝑛𝑙},\mathrm{𝑝𝑟},\mathrm{𝑢𝑖𝑠}}`$ follows immediately from the following lemma.

###### Lemma 5.16

: The formula $`\psi \text{KL}_1`$ is satisfiable with respect to $`𝒞_1^{\mathrm{𝑛𝑙},\mathrm{𝑝𝑟}}`$ (resp., $`𝒞_1^{nl,\mathrm{𝑝𝑟},\mathrm{𝑠𝑦𝑛𝑐}}`$) iff it is satisfiable with respect to $`𝒞_1^{\mathrm{𝑛𝑙},\mathrm{𝑝𝑟},\mathrm{𝑢𝑖𝑠}}`$ (resp., $`𝒞_1^{\mathrm{𝑛𝑙},\mathrm{𝑝𝑟},\mathrm{𝑠𝑦𝑛𝑐},\mathrm{𝑢𝑖𝑠}}`$).

Proof: Clearly if $`\psi `$ is satisfiable with respect to $`𝒞_1^{\mathrm{𝑛𝑙},\mathrm{𝑝𝑟},\mathrm{𝑢𝑖𝑠}}`$ (resp., $`𝒞_1^{\mathrm{𝑛𝑙},\mathrm{𝑝𝑟},\mathrm{𝑠𝑦𝑛𝑐},\mathrm{𝑢𝑖𝑠}}`$) it is satisfiable with respect to $`𝒞_1^{\mathrm{𝑛𝑙},\mathrm{𝑝𝑟}}`$ (resp., $`𝒞_1^{\mathrm{𝑛𝑙},\mathrm{𝑝𝑟},\mathrm{𝑠𝑦𝑛𝑐}}`$). For the converse, suppose that $`(,r^{},n^{})\psi `$, where $`=(,\pi )𝒞_1^{\mathrm{𝑛𝑙},\mathrm{𝑝𝑟}}`$. For each run $`r`$, define the run $`r^+`$ just as in Lemma 5.3, to be the result of adding a new initial state to $`r`$. Let $`^{}=\{r^+:(r,0)_1(r^{},0)\}`$. Define $`\pi ^{}`$ as on $`^{}`$ as in Lemma 5.3, so that $`\pi ^{}(r^+,0)(p)=\mathrm{𝐟𝐚𝐥𝐬𝐞}`$ for all primitive propositions $`p`$, and $`\pi ^{}(r^+,n+1)=\pi (r,n)`$. Let $`^{}=(^{},\pi ^{})`$. Clearly $`^{}𝒞_1^{\mathrm{𝑛𝑙},\mathrm{𝑝𝑟},\mathrm{𝑢𝑖𝑠}}`$, and if $``$ is synchronous, then so is $`^{}`$. We claim that $`(^{},r^+,n+1)\phi `$ iff $`(,r,n)\phi `$ for all formulas $`\phi \text{KL}_1`$ and all $`r^+^{}`$. We prove this by induction on the structure of $`\phi `$. The only nontrivial case is if $`\phi `$ is of the form $`K_1\phi ^{}`$. But this case is immediate from the observation that if $`r^+^{}`$, $`r^{}`$, and $`(r,n)_1(r^{},n^{})`$, then since $``$ is a system of perfect recall, we must have $`(r,0)_1(r^{},0)`$, and hence $`(r^{})^+^{}`$. We leave details of the proof of the claim to the reader. From the claim, it follows that $`\psi `$ is satisfiable in $`𝒞_1^{\mathrm{𝑛𝑙},\mathrm{𝑝𝑟},\mathrm{𝑢𝑖𝑠}}`$, and that if $`\psi `$ is satisfiable in $`𝒞_1^{\mathrm{𝑛𝑙},\mathrm{𝑝𝑟},\mathrm{𝑠𝑦𝑛𝑐}}`$, then it is also satisfiable in $`𝒞_1^{\mathrm{𝑛𝑙},\mathrm{𝑝𝑟},\mathrm{𝑠𝑦𝑛𝑐},\mathrm{𝑢𝑖𝑠}}`$.

### 5.6 Dealing with $`𝒞_m^{\mathrm{𝑛𝑙},\mathrm{𝑠𝑦𝑛𝑐}}`$ (Theorem 3.8)

We now want to show that $`\mathrm{S5}_m^U+\mathrm{KT5}`$ is sound and complete for $`\text{KL}_m`$ with respect to $`𝒞_m^{\mathrm{𝑛𝑙},\mathrm{𝑠𝑦𝑛𝑐}}`$. Soundness follows from the following lemma.

###### Lemma 5.17

: All instances of KT5 are valid in $`𝒞_m^{\mathrm{𝑛𝑙},\mathrm{𝑠𝑦𝑛𝑐}}`$.

Proof: Suppose $`𝒞_m^{\mathrm{𝑛𝑙},\mathrm{𝑠𝑦𝑛𝑐}}`$ and $`(,r,n)K_i\phi `$. We want to show that $`(,r,n)K_i\phi `$. Thus, suppose that $`(r^{},n^{})_i(r,n)`$. We must show that $`(,r^{},n^{})\phi `$. By synchrony, we must have $`n^{}=n`$. Moreover, by no learning and synchrony, we have that $`(r,n+1)_i(r^{},n+1)`$. Since $`(,r,n+1)K_i\phi `$, it follows that $`(,r^{},n+1)\phi `$, and hence that $`(,r^{},n)\phi `$, as desired.

For completeness, we construct an enriched+ system much as in the proof of Theorem 3.6, using $`k`$-trees, with an appropriate strengthening of the $``$ relation.

We start by proving the following analogue of Lemma 5.11.

###### Lemma 5.18

: Suppose that the axiomatization includes KT5. If $`s`$ is a $`\sigma `$-state, $`t`$ is a $`(\sigma \mathrm{\#}i)`$-state, $`s_it`$, and $`ss^{}`$, then there exists a $`(\sigma \mathrm{\#}i)`$-state $`t^{}`$ such that $`tt^{}`$ and $`s^{}_it^{}`$.

Proof: Since $`\phi _s\phi _s^{}`$ is consistent, it follows from Lemma 4.3(b) that $`\phi _{s_0}K_i\mathrm{\Phi }_{s^{},i}^+`$ is consistent. Moreover, by Lemma 4.3(c), we have that $`\phi _sL_i\phi _t`$. Thus, $`\phi _sL_i\phi _tK_i\mathrm{\Phi }_{s^{},i}^+`$ is consistent. Using KT5, it follows that $`\phi _sL_i\phi _tK_i\mathrm{\Phi }_{s^{},i}^+`$ is consistent. It follows that $`\phi _t\mathrm{\Phi }_{s^{},i}^+`$ is consistent. Hence, there is some $`(\sigma \mathrm{\#}i)`$-state $`t^{}`$ such that $`s^{}_it^{}`$ and $`\phi _t\phi _t^{}`$ is consistent. Thus, we have $`s^{}_it^{}`$ and $`tt^{}`$.

If $`S`$ and $`T`$ are $`k`$-trees, $`sS`$, and $`tT`$, we define $`(S,s)^{\mathrm{𝑠𝑦𝑛𝑐},+}(T,t)`$ if $`S_fT`$ for some $`f`$ such that $`f(s)=(s,t)`$ and $`f(s^{})`$ has length 2 for all $`s^{}S`$. We now get the following simplification of Lemma 5.12.

###### Lemma 5.19

: Suppose that the axiomatization includes KT5, $`S`$ is a $`k`$-tree, and $`s`$ is a $`\sigma `$-state in $`S`$, where $`|\sigma |=k`$.

* If $`\text{tree}_{S,s}(\phi _t\xi )`$ is consistent, then there exists a $`k`$-tree $`T`$ and $`tT`$ such that $`(S,s)^{\mathrm{𝑠𝑦𝑛𝑐},+}(T,t)`$ and $`\text{tree}_{T,t}\xi `$ is consistent.
* $`\text{tree}_{S,s}_{\{(T,t):(S,s)^{\mathrm{𝑠𝑦𝑛𝑐},+}(T,t)\}}\text{tree}_{T,t}`$ is provable.
* If $`\text{tree}_{S,s}\phi U\phi ^{}`$ is consistent, then there is a sequence $`S_0,\mathrm{},S_l`$ of $`k`$-trees and states $`s_0,\mathrm{},s_l`$ such that (i) $`s_jS_j`$, (ii) $`(S,s)=(S_0,s_0)`$, (iii) $`(S_j,s_j)^{\mathrm{𝑠𝑦𝑛𝑐},+}(S_{j+1},s_{j+1})`$ for $`j=0,\mathrm{},l1`$, (iv) $`\text{tree}_{S_j,s_j}\phi `$ is consistent for $`j=0,\mathrm{},l1`$, and (v) $`\text{tree}_{S_l,s_l}\phi ^{}`$ is consistent.

Proof: The proof is like that of Lemma 5.12, using Lemma 5.18 instead of Lemma 5.11. We leave details to the reader.

We can then define a $`\mathrm{𝑠𝑦𝑛𝑐}`$-acceptable sequence of trees by replacing $`^+`$ by $`^{\mathrm{𝑠𝑦𝑛𝑐},+}`$ in the definition of acceptable sequence of trees. Using Lemma 5.19, we can show that if the axiom system contains KT5, then we can construct an infinite $`\mathrm{𝑠𝑦𝑛𝑐}`$-acceptable sequence $`𝒮=S_0^{\mathrm{𝑠𝑦𝑛𝑐},+}S_1^{\mathrm{𝑠𝑦𝑛𝑐},+}S_2^{\mathrm{𝑠𝑦𝑛𝑐},+}\mathrm{}`$ of $`d`$-trees. As in Section 5.1, we use an object $`x`$ not equal to any state. Given a $``$-sequence $`s_Ns_{N+1}\mathrm{}`$ starting at $`s_NS_N`$ the $`\mathrm{𝑛𝑙}`$$`\mathrm{𝑠𝑦𝑛𝑐}`$-run $`r`$ derived from it is defined so that $`r_e(n)=s_n`$ for $`nN`$, else $`r_e(n)=x`$, and for each agent $`i`$, if $`nN`$ then $`r_i(n)=(n,O_i(s_n)O_i(s_{n+1})\mathrm{})`$, else $`r_i(n)=(n,x^{Nn}O_i(s_n)O_i(s_{n+1})\mathrm{})`$. Thus, the local state of the agent enforces synchrony (by encoding the time) and enforces no learning. Let $`^{\mathrm{𝑛𝑙},\mathrm{𝑠𝑦𝑛𝑐}}`$ consist of all $`\mathrm{𝑛𝑙}`$$`\mathrm{𝑠𝑦𝑛𝑐}`$-runs derived from $``$-sequences compatible with $`𝒮`$, and define $`\mathrm{\Sigma }`$ by taking $`\mathrm{\Sigma }(r,n)=s_n`$ for $`nN`$ and $`\mathrm{\Sigma }(r,n)`$ undefined for $`n<N`$.

###### Lemma 5.20

: Suppose the axiomatization includes KT5. Then $`(^{\mathrm{𝑛𝑙},\mathrm{𝑠𝑦𝑛𝑐}},\mathrm{\Sigma })`$ is an enriched+ system.

Proof: The proof is essentially the same as that of Lemma 5.14. We leave details to the reader.

We complete the proof of Theorem 3.8 just as we did all the previous proofs.

### 5.7 Dealing with $`𝒞_m^{\mathrm{𝑛𝑙},\mathrm{𝑝𝑟},\mathrm{𝑠𝑦𝑛𝑐}}`$ (Theorem 3.9)

We now want to show that $`\mathrm{S5}_m^U+\mathrm{KT2}+\mathrm{KT5}`$ is sound and complete for $`\text{KL}_m`$ with respect to $`𝒞_m^{\mathrm{𝑛𝑙},\mathrm{𝑝𝑟},\mathrm{𝑠𝑦𝑛𝑐}}`$. Soundness follows from Lemmas 5.7 and 5.17.

For completeness, we construct an enriched+ system by combining the ideas of the proofs of Theorems 3.7 and 3.8. Using Lemma 5.19, we can show that if the axiom system contains KT5, then we can construct an infinite $`\mathrm{𝑠𝑦𝑛𝑐}`$-acceptable sequence $`𝒮`$ of $`d`$-trees. Given a $``$-sequence $`s_0s_1\mathrm{}`$, the $`\mathrm{𝑛𝑙}`$$`\mathrm{𝑝𝑟}`$$`\mathrm{𝑠𝑦𝑛𝑐}`$-run $`r`$ derived from it is defined so that $`r_e(n)=s_n`$ and $`r_i(n)=(O_i(s_1)\mathrm{}O_i(s_n),O_i(s_n)O_i(s_{n+1})\mathrm{})`$. Thus, the local state of the agent enforces both no forgetting and no learning. It also enforces synchrony, since the agent can determine $`n`$ from the length of the first of the two seqeunces in its local state. Let $`^{\mathrm{𝑛𝑙},\mathrm{𝑝𝑟},\mathrm{𝑠𝑦𝑛𝑐}}`$ consist of all $`\mathrm{𝑛𝑙}`$$`\mathrm{𝑝𝑟}`$$`\mathrm{𝑠𝑦𝑛𝑐}`$-runs derived from $``$-sequences with suffixes that are compatible with $`𝒮`$; again, we define $`\mathrm{\Sigma }`$ by taking $`\mathrm{\Sigma }(r,n)=s_n`$.

Using ideas similar to those in earlier proofs, we can now prove the following result.

###### Lemma 5.21

: Suppose the axiomatization includes KT2 and KT5. Then $`(^{\mathrm{𝑛𝑙},\mathrm{𝑝𝑟},\mathrm{𝑠𝑦𝑛𝑐}},\mathrm{\Sigma })`$ is an enriched+ system.

We complete the proof of Theorem 3.9 just as we did the earlier proofs.

### 5.8 Dealing with $`𝒞_m^{\mathrm{𝑛𝑙},\mathrm{𝑠𝑦𝑛𝑐},\mathrm{𝑢𝑖𝑠}}`$ and $`𝒞_m^{\mathrm{𝑛𝑙},\mathrm{𝑝𝑟},\mathrm{𝑠𝑦𝑛𝑐},\mathrm{𝑢𝑖𝑠}}`$ (Theorem 3.10)

Finally, we want to show that $`\mathrm{S5}_m^U+\mathrm{KT2}+\mathrm{KT5}+\{K_i\phi K_1\phi \}`$ is sound and complete for $`\text{KL}_m`$ with respect to $`𝒞_m^{\mathrm{𝑛𝑙},\mathrm{𝑠𝑦𝑛𝑐},\mathrm{𝑢𝑖𝑠}}`$ and $`𝒞_m^{\mathrm{𝑛𝑙},\mathrm{𝑝𝑟},\mathrm{𝑠𝑦𝑛𝑐},\mathrm{𝑢𝑖𝑠}}`$. Soundness follows easily using the following result, which is Proposition 3.9 in \[HV89\] (restated using our notation).

###### Proposition 5.22

:

1. $`𝒞_m^{\mathrm{𝑛𝑙},\mathrm{𝑠𝑦𝑛𝑐},\mathrm{𝑢𝑖𝑠}}=C_m^{\mathrm{𝑛𝑙},\mathrm{𝑝𝑟},\mathrm{𝑠𝑦𝑛𝑐},\mathrm{𝑢𝑖𝑠}}`$.
2. Any formula $`\phi `$ in $`\text{KL}_m`$ is equivalent in $`𝒞_m^{\mathrm{𝑛𝑙},\mathrm{𝑠𝑦𝑛𝑐},\mathrm{𝑢𝑖𝑠}}`$ to the formula $`\phi ^{}`$ that results by replacing all occurrences of $`K_i`$, $`i2`$, by $`K_1`$.

It follows from part (a) of Proposition 5.22 that the same axioms characterize $`𝒞_m^{\mathrm{𝑛𝑙},\mathrm{𝑠𝑦𝑛𝑐},\mathrm{𝑢𝑖𝑠}}`$ and $`𝒞_m^{\mathrm{𝑛𝑙},\mathrm{𝑝𝑟},\mathrm{𝑠𝑦𝑛𝑐},\mathrm{𝑢𝑖𝑠}}`$. Now using Theorems 5.7 and 5.17, the soundness of KT2 and KT5 follows. The soundness of $`K_i\phi K_1\phi `$ follows from part (b).

For completeness, using the axiom $`K_i\phi K_1\phi `$, it suffices to show the completeness of $`\mathrm{S5}_1^U+\mathrm{KT2}+\mathrm{KT5}`$ with respect to $`𝒞_1^{\mathrm{𝑛𝑙},\mathrm{𝑝𝑟},\mathrm{𝑠𝑦𝑛𝑐},\mathrm{𝑢𝑖𝑠}}`$. By Theorem 3.9, this axiomatization is complete with respect to $`𝒞_1^{\mathrm{𝑛𝑙},\mathrm{𝑝𝑟},\mathrm{𝑠𝑦𝑛𝑐}}`$. The result now follows using Lemma 5.16.

## 6 Remarks on No Learning

We noted in Section 2 that the definition of no learning adopted in this paper differs from that used in \[HV86, HV89\]. We now comment on the reason for this change and the relationship between these alternative definitions of no learning.

First, recall from part (d) of Lemma 2.2 that that agent $`i`$ has perfect recall in system $``$ if and only if

* for all points $`(r,n)_i(r^{},n^{})`$ in $``$, if $`kn`$, then there exists $`k^{}n^{}`$ such that $`(r,k)_i(r^{},k^{})`$.

Intuitively, no learning is the dual of perfect recall, so it seems reasonable to define no learning by replacing references to the past in a definition of perfect recall by references to the future. This was done in \[HV86, HV89\], where the definition given for no learning was the following future time variant of condition ($``$), which we call no learning, to distinguish it from our current definition: Agent $`i`$ does not learn in system $``$ if and only if

* for all points $`(r,n)_i(r^{},n^{})`$ in $``$, if $`kn`$ then there exists $`k^{}n^{}`$ such that $`(r,k)_i(r^{},k^{})`$.

The following lemma states a number of relations holding between condition ($``$) and the other properties we have considered in this paper.

###### Lemma 6.1

:

1. If agent $`i`$ does not learn in system $``$ then agent $`i`$ does not learn in system $``$.
2. If system $``$ is synchronous or if agent $`i`$ has perfect recall in $``$, then agent $`i`$ does not learn in $``$ iff agent $`i`$ does not learn in $``$.

Proof: We first show (a). Suppose that agent $`i`$ does not learn in $``$. Assume that $`(r,n)_i(r^{},n^{})`$ and let $`kn`$. Since $`i`$ does not learn, the future local state sequences at $`(r,n)`$ and $`(r^{},n^{})`$ are equal. It follows that there exists $`k^{}n^{}`$ such that $`(r,k)_i(r^{},k^{})`$. Thus, agent $`i`$ does not learn.

For (b), it follows from part (a) that it suffices to show the implication from no learning to no learning. We consider the cases of synchrony and perfect recall independently. In each case, we show that if $`(r,n)_i(r^{},n^{})`$ then there exists $`kn^{}`$ such that the sequences $`((r,n),(r,n+1))`$ and $`((r^{},n^{})\mathrm{}(r^{},k))`$ are $`_i`$-concordant. It then follows by Lemma 2.3 that agent $`i`$ does not learn.

Assume first that $``$ is a synchronous system, and that $`(r,n)_i(r^{},n^{})`$. By synchrony, we must have $`n=n^{}`$. By no learning, there exists $`kn`$ such that $`(r,n+1)_i(r^{},k)`$. By synchrony, $`k`$ must equal $`n+1`$. It is immediate that $`((r,n),(r,n+1))`$ and $`((r^{},n^{}),(r^{},n^{}+1))`$ are $`_i`$-concordant.

Next, assume that agent $`i`$ has perfect recall in $``$, and that $`(r,n)_i(r^{},n^{})`$. By no learning, there exists $`kn^{}`$ such that $`(r,n+1)_i(r^{},k)`$. By perfect recall, agent $`i`$’s local state sequences $`(r,n+1)`$ and $`(r^{},k)`$ are identical, as are the local state sequences at $`(r,n)`$ and $`(r^{},n^{})`$. It follows that the sequences $`((r,n),(r,n+1))`$ and $`((r^{},n^{}),\mathrm{},(r^{},k))`$ are $`_i`$-concordant.

Thus, in the context of either synchrony or perfect recall, no learning and no learning are equivalent. However, in systems without synchrony or perfect recall, no learning is strictly weaker than no learning, as the following example shows. Consider the system $`=\{r^1,r^2\}`$ for a single agent, where the runs are defined by:

$$r^1(n)=\{\begin{array}{cc}(s_e,a)\hfill & \text{if }n=0\hfill \\ (s_e,b)\hfill & \text{if }n>0\text{ is odd }\hfill \\ (s_e,c)\hfill & \text{if }n>0\text{ is even }\hfill \end{array}$$

where $`s_e`$ is some state of the environment, and $`a,b,c`$ are local states of agent 1, and similarly

$$r^2(n)=\{\begin{array}{cc}(s_e,a)\hfill & \text{if }n=0\hfill \\ (s_e,c)\hfill & \text{if }n>0\text{ is odd }\hfill \\ (s_e,d)\hfill & \text{if }n>0\text{ is even }\hfill \end{array}$$

This system clearly satisfies $`\mathrm{𝑢𝑖𝑠}`$ and condition ($``$), so we have no learning (for both agents). However, agent 1’s future local state sequences from the points $`(r^1,0)_1(r^2,0)`$ are not $`_1`$-concordant, so we do not have no learning. Thus, no learning and no learning are distinct in general.

This raises the question of which of variant to take as the definition of no learning for the cases $`𝒞^{\mathrm{𝑛𝑙}}`$ and $`𝒞^{\mathrm{𝑢𝑖𝑠},\mathrm{𝑛𝑙}}`$. The origin of this notion in the literature lies in Ladner and Reif’s paper \[LR86\], where it is motivated as arising in the context of blindfold games. Their logic LLP assumes perfect recall, so is not decisive on the distinction. However, it seems that the behavior in the above example is somewhat unnatural for this application, and the definition we have adopted in this paper better fits the intuition of a player in a blindfold game following a fixed linear strategy, but with some uncertainty about timing. It is such examples that in fact led us to use the current definition of no learning.

It is worth noting that the example above also shows that the axiom KT4 is not sound with respect to the class of systems satisfying ($``$). Define the interpretation $`\pi `$ of the propositions $`p`$ and $`q`$ on runs $`r`$ by $`\pi (r,n)(p)=\mathrm{𝐭𝐫𝐮𝐞}`$ iff $`r_1(n)=a`$ and $`\pi (r,n)(q)=\mathrm{𝐭𝐫𝐮𝐞}`$ iff $`r_1(n)=b`$. Let $`=(,\pi )`$. It is then readily seen that $`(,r^1,0)K_1pUK_1q`$ but not $`(,r^1,0)K_1(K_1pUK_1q)`$. Hence KT4 fails in this system. (This example is a future time version of an example used in \[Mey94\] to show that the axiom KT1 is incomplete for systems with perfect recall.) We have not investigated the issue of axiomatization using no learning rather than no learning in the two cases where there is a difference—$`𝒞_m^{nl}`$ and $`𝒞_1^{nl,uis}`$. We conjecture that, while there will be a relatively clean complete axiomatization in these cases, it will not be as elegant as the one proposed here. That is, the axiom that captures no learning will be somewhat more complicated than KT4. This conjecture is in line with our feeling that no learning is the “right” definition, not no learning.

We remark that the complexity results of \[HV86, HV89\] are proved in the context of no learning, but it is relatively straightforward to show that the same results hold if we use the definition of no learning instead.

## 7 Discussion

While we have looked in this paper at the effect on axiomatization of some combinations of classes of systems and language (48 in all!), there are certainly other cases of interest. One issue we have already mentioned is that of braching time versus linear time. Basing the temporal fragment of the language on branching time yields another 48 logics, whose complexity is studied in \[HV86\]. We would conjecture that the obvious translations of the axioms we have presented here deal with branching time, with similar proofs of completeness, but this remains to be verified.

It is worth remarking that our results are very sensitive to the language studied. As we have seen, the language considered in this paper is too coarse to reflect some properties of systems. In the absence of the other properties, synchrony and unique initial states do not require additional axioms. This may no longer be true for richer languages. For example, if we allow past-time operators \[LPZ85\], we need not only the additional axioms capturing the properties of these, but also new axioms describing the interaction of knowledge and time. Suppose that we add an operator $``$ such that $`(,r,n)\phi `$ if $`n1`$ and $`(,r,n1)\phi `$. Notice that $`\neg \text{true}`$ expresses the property “the time is 0” and $`\neg \text{true}`$ expresses the property “the time is 1”. Similarly, we can inductively define formulas that express the property “the time is $`m`$” for each $`m0`$. If time=m is an abbreviation for this formula, then $`\mathrm{𝑡𝑖𝑚𝑒}=mK_i(\mathrm{𝑡𝑖𝑚𝑒}=m)`$ is valid in $`𝒞^{\mathrm{𝑠𝑦𝑛𝑐}}`$, for each time m.

On the other hand, by adding past time operators we can simplify the axiom for perfect recall. Introducing the operator $`S`$ for “since”, we may show that the formula

$$(K_i\phi )S(K_i\psi )K_i((K_i\phi )S(K_i\psi ))$$

is valid in $`𝒞^{\mathrm{𝑝𝑟}}`$. This axiom very neatly expresses the meaning of perfect recall, and a comparison with KT4 shows clearly the sense in which perfect recall is a dual of no learning. Techniques similar to those developed in this paper may be used to prove that this axiom, together with the usual axioms for past time \[LPZ85\] and for knowledge, yields a complete axiomatization for $`𝒞^{\mathrm{𝑝𝑟}}`$.

Besides changes to the language, there are also additional properties of systems worth considering. One case of interest is the class of asynchronous message passing systems of \[FHMV95\]. That extra axioms are required in such systems is known (\[FHMV95\] Exercise 8.8), but the question of complete axiomatization is still open.