Reasoning About Common Knowledge with Infinitely Many Agents

Joseph Y. Halpern^{∗} Computer Science Department Cornell University halpern@cs.cornell.edu

Richard A. Shore^{§} Mathematics Department Cornell University shore@math.cornell.edu

May 14, 2003

Abstract

Complete axiomatizations and exponential-time decision procedures are provided for reasoning about knowledge and common knowledge when there are infinitely many agents. The results show that reasoning about knowledge and common knowledge with infinitely many agents is no harder than when there are finitely many agents, provided that we can check the cardinality of certain set differences G − G′, where G and G′ are sets of agents. Since our complexity results are independent of the cardinality of the sets G involved, they represent improvements over the previous results even when the sets of agents involved are finite. Moreover, our results make clear the extent to which issues of complexity and completeness depend on how the sets of agents involved are represented.

∗Supported in part by NSF under grant IRI-96-25901.

§Supported in part by NSF Grants DMS-9802843, DMS-0100035 and DOD MURI Grant SA1515PG.

1 Introduction

Reasoning about knowledge and common knowledge has been shown to be widely applicable in distributed computing, AI, and game theory. (See [FHMV95] for numerous examples.) Complete axioms for reasoning about knowledge and common knowledge are well known in the case of a fixed finite set of agents. However, in many applications, the set of agents is not known in advance and has no a priori upper bound (think of software agents on the web or nodes on the Internet, for example); it is often easiest to model the set of agents as an infinite set. Infinite sets of agents also arise in game theory and economics (where reasoning about knowledge and common knowledge is quite standard; see, for example, [Aum76, Gea94]). For example, when analyzing a game played with two teams, we may well want to say that everyone on team 1 knows that everyone on team 2 knows some fact p, or that it is common knowledge among the agents on team 1 that p is common knowledge among the agents on team 2. We would want to say this even if the teams consist of infinitely many agents. Since economies are often modeled as consisting of infinitely many (even uncountably many) agents, this type of situation arises when economies are viewed as teams in a game.

The logics for reasoning about the knowledge of groups of agents contain modal operators K_{i} (where K_{i}φ is read “agent i knows φ”), E_{G} (where E_{G}φ is read “everyone in group G knows φ”), and C_{G} (where C_{G}φ is read “φ is common knowledge among group G”). The operators E_{G} and C_{G} make perfect sense even if we allow the sets G to be infinite—their semantic definitions remain unchanged. If the set of agents is finite, so that, in particular, G is finite, there is a simple axiom connecting E_{G}φ to K_{i}φ, namely, E_{G}φ ⇔ ∧_{i∈G}K_{i}φ. Once we allow infinite groups G of agents, there is no obvious analogue for this axiom. Nevertheless, in this paper, we show that there exist natural sound and complete axiomatizations for reasoning about knowledge and common knowledge even if there are infinitely many agents.

It is also well known that if there are finitely many agents, then there is a decision procedure that decides if a formula φ is satisfiable (or valid) that runs in time exponential in |φ|, where φ is the length of the formula viewed as a string of symbols. We prove a similar result for a language with infinitely many agents. However, two issues arise (that, in fact, are also relevant even if there are only finitely many agents, although they have not been considered before):

• In the statement of the complexity result in [FHMV95], E_{G} and C_{G} are both viewed as having length 2 + 2|G| (where |G| is the cardinality of G). Clearly we cannot use this definition here if we want to get interesting complexity results, since |G| may be infinite. Even if we restrict our attention to finite sets G, we would like a decision procedure that treats these sets in a uniform way, independently of their cardinality. Here we view E_{G} as having length 1 and C_{G} as having length 3, independent of the cardinality of G. (See, for example, the proof of Proposition 3.5 for the role of independence and the definition of Sub(φ) in the proof of Theorem 4.5 for an indication as to why C_{G} has length 3 rather than 1.) Even with this definition of length, we prove that the complexity of the satisfiability problem is still essentially exponential time. (We discuss below what “essentially” means.) Thus our results improve previously-known results even if there are only finitely many agents.

• In the earlier proofs, it is implicitly assumed that the sets G are presented in such a way that there is no difficulty in testing membership in G. As we show here, in order to decide if certain formulas are satisfiable, we need to be able to test if certain subsets of agents of the form G_{0} − (G_{1} ∪ … ∪ G_{k}) are empty, where G_{0}, …, G_{k} are sets of agents. In fact, if we are interested in a notion of knowledge that satisfies positive introspection—that is, if agent i knows φ, then she knows that she knows it—then we also must be able to check whether such subsets are singletons. And if we are interested in a notion of knowledge that satisfies negative introspection—that is, if agent i does not know φ, then she knows that she does not know it—then we must be able to check whether such subsets have cardinality m, for certain finite m. The difficulty of deciding these questions depends in part on how G_{0}, …, G_{k} are presented and which sets of agents we can talk about in the language. For example, if G_{0}, …, G_{k} are recursive sets, deciding if G_{0} −(G_{1} ∪…∪G_{k}) is nonempty may not even be recursive. Here, we provide a decision procedure for satisfiability that runs in time exponential in |φ| provided that we have oracles for testing appropriate properties of sets of the form G_{0} − (G_{1} ∪ … ∪ G_{k}). Moreover, we show that any decision procedure must be able to answer the questions we ask. In fact, we actually prove a stronger result, providing a tight bound on the complexity of deciding satisfiability that takes into account the complexity of answering questions about the cardinality of G_{0} − (G_{1} ∪ … ∪ G_{k}). Again, this issue is of significance even if there are only finitely many agents. For example, in the SDSI approach to security [RL96], there are names, which can be viewed as representing sets of agents. SDSI provides a (nondeterministic) algorithm for computing the set of agents represented by a name. If we want to make statements such as “every agent represented by name n knows φ” (statements that we believe will be useful in reasoning about security [HvdM99, HvdMS99]) then the results of this paper show that to decide validity in the resulting logic, we need more than just an algorithm for resolving the agents represented by a given name. We also need algorithms for resolving which agents are represented by one name and not another. More generally, if we assume that we have a separate language for representing sets of agents, our results characterize the properties of sets that we need to be able to decide in order to reason about the group knowledge of these agents.

In the next section, we briefly review the syntax and semantics of the logic of common knowledge. In Section 3 we state the main results and prove them under some simplifying assumptions that allow us to bring out the main ideas of the proof. We drop these assumptions in Section 4, where we provide the proofs of the full results.

2 Syntax and Semantics: A Brief Review

Syntax: We start with a (possibly infinite) set A of agents. Let G be a set of nonempty subsets of A. (Note that we do not require G to be closed under union, intersection, or complementation; it can be an arbitrary collection of subsets.) We get the language L_{G}^{C}(Φ) by starting with a set Φ of primitive propositions, and closing under ∧, ¬, and the modal operators K_{i}, for i ∈ A, and E_{G}, C_{G}, for G ∈ G. Thus, if p, q ∈ Φ, i ∈ A, and G, G′ ∈ G, then K_{i}C_{G}(p ∧ E_{G′}q) ∈ L_{G}^{C}(Φ). Let L_{G}^{E} be the sublanguage of L_{G}^{C} that does not include the C_{G} operators. Let |φ| be the length of the formula viewed as a string of symbols, where the modal operators K_{i} and E_{G} are counted as having length 1 and C_{G} is counted as having length 3 (even if G is an infinite set of agents) and all primitive propositions are counted as having length 1.

In [FHMV95, HM92], A is taken to be the set {1, …, n}; in [HM92], G is taken to be the singleton {{1, …, n}} (so that we can only talk about every agent in A knowing φ and common knowledge among the agents in A), while in [FHMV95], G is taken to consist of all nonempty subsets of A. We are being deliberately vague here as to how the infinite sets which appear in the subscripts of E and C are represented. The details of the representation are not relevant to our results. However, it turns out to be quite critical that the representation is such that certain questions about the cardinality of sets can be answered easily. This is discussed in much more detail when we state the results.

Semantics: As usual, formulas in L_{G}^{C} are either true or false at a world in a Kripke structure. Formally, a Kripke structure M over A and Φ is a tuple (S, π, {K_{i} : i ∈ A}), where S is a set of states or possible worlds, π associates with each state in S a truth assignment to the primitive propositions in Φ (so that π(s) : Φ → {true, false}), and K_{i} is a binary relation on S for each agent i ∈ A. We occasionally write K_{i}(s) for {t : (s, t) ∈ K_{i}}.

We define the truth relation ⊧ as follows:

(M, s) ⊧ p (for p ∈ Φ) iff π(s)(p) = true

(M, s) ⊧ φ ∧ ψ iff both (M, s) ⊧ φ and (M, s) ⊧ ψ

(M, s) ⊧ ¬φ iff (M, s) |̸= φ

(M, s) ⊧ K_{i}φ iff (M, t) ⊧ φ for all t ∈ K_{i}(s)

(M, s) ⊧ E_{G}φ iff (M, s) ⊧ K_{i}φ for all i ∈ G

(M, s) ⊧ C_{G}φ iff (M, s) ⊧ E_{G}^{k}φ for k = 1, 2, 3, …, where E_{G}^{k} is defined inductively by taking E_{G}^{1}φ =_{def} E_{G}φ and E_{G}^{k+1}φ =_{def} E_{G}E_{G}^{k}φ.

We say that t is G-reachable from s in M if there exist s_{0}, …, s_{k} with s = s_{0}, t = s_{k}, and (s_{i}, s_{i+1}) ∈ ∪_{i∈G}K_{i}. For later use, we extend this definition so that if S′ ⊆ S, we say that t is G-reachable from s in S′ if s_{0}, …, s_{k} ∈ S′. The following characterization of common knowledge is well known [FHMV95].

Lemma 2.1: (M, s) ⊧ C_{G}φ iff (M, t) ⊧ φ for all t that are G-reachable from s in M.

Let M_{A}(Φ) be the class of all Kripke structures over A and Φ (with no restrictions on the K_{i} relations). We are also interested in various subclasses of M_{A}(Φ), obtained by restricting the K_{i} relations. In particular, we consider M_{A}^{r}(Φ), M_{A}^{rt}(Φ), M_{A}^{rst}(Φ), and M_{A}^{elt}(Φ), the class of all structures over A and Φ where the K_{i} relations are reflexive (resp., reflexive and transitive; reflexive, symmetric, and transitive; Euclidean,^{1} serial, and transitive). For the remainder of this paper, we take Φ to be fixed, and do not mention it, writing, for example L_{G}^{C} and M_{A} rather than L_{G}^{C}(Φ) and M_{A}(Φ).

As usual, we define a formula to be valid in a class M of structures if (M, s) ⊧ φ for all M ∈ M and all states s in M; similarly, φ is satisfiable in M if (M, s) ⊧ φ for some M ∈ M and some s in M.

1Recall that a relation R is Euclidean if (s, t), (s, u) ∈ R implies that (t, u) ∈ R.

Axioms: The following are the standard axioms and rules that have been considered for knowledge; They holds for all i ∈ A. Prop. All substitution instances of tautologies of propositional calculus. K1. (K_{i}φ ∧ K_{i}(φ ⇒ ψ)) ⇒ K_{i}ψ. K2. K_{i}φ ⇒ φ. K3. ¬K_{i}false. K4. K_{i}φ ⇒ K_{i}K_{i}φ. K5. ¬K_{i}φ ⇒ K_{i}¬K_{i}φ. MP. From φ and φ ⇒ ψ infer ψ. KGen. From φ infer K_{i}φ. Technically, Prop and K1–K5 are axiom schemes, rather than single axioms. K1, for example, holds for all formulas φ and ψ. A formula such as K_{1}q ∨ ¬K_{1}q is an instance of axiom Prop (since it is a substitution instance of the propositional tautology p∨¬p, obtained by substituting K_{1}q for p).

We will be interested in the following axioms and rule for reasoning about everyone knows, which hold for all G ∈ G. E1. E_{G}φ ⇒ K_{i}φ if i ∈ G. E2. (∧_{i∈A′}K_{i}φ ∧ ∧_{G′∈G′}E_{G′}φ) ⇒ E_{G}φ if A′ is a finite subset of A, G′ is a finite subset of G,

and G ⊆ (A′ ∪ (∪G′)). E3. (E_{G}φ ∧ E_{G}(φ ⇒ ψ)) ⇒ E_{G}ψ. E4. E_{G}(E_{G}φ ⇒ φ). E5. E_{G}φ ⇒ φ. E6. ¬φ ⇒ E_{G}¬E_{G}φ. E7. From ¬(φ_{1} ∧ … ∧ φ_{k}) infer ¬(E_{G_{1}}φ_{1} ∧ … ∧ E_{G_{k}}φ_{k}) if G_{1} ∩ … ∩ G_{k} ≠ ∅. EGen. From φ infer E_{G}φ.

E2 can be viewed as a generalization of the axiom E_{G}φ ⇒ E_{G′}φ if G′ ⊆ G (of which E1 is a special case if we identify K_{i}φ with E_{{i}}φ, as we often do in the paper). Essentially it says that if K_{i}φ holds for all agents i ∈ G (and perhaps some other agents i ∉ G) then E_{G}φ holds. Since, if G is infinite, we cannot write the infinite conjunction of K_{i}φ for all i ∈ G, we approximate as well as we can within the constraints of the language. As long as E_{G′}φ and K_{i}φ holds for sets G′ and agents i whose union contains G, then certainly E_{G}φ holds.

If A is finite (so that all the sets in G are finite) we can simplify E1 and E2 to E. E_{G}φ ⇔ ∧_{i∈G}K_{i}φ.

It is easy to see that E follows from E1 and E2 (in the presence of Prop and MP) and every instance of E1 and E2 follows from E if A is finite. E is used instead of E1 and E2 in [FHMV95, HM92]. Note that E2 is recursive iff deciding if G−(A′ ∪(∪G′)) = ∅ is recursive. (We determine precisely which such questions we must be able to answer in Proposition 3.3.)

E3 and EGen are the obvious analogues of K1 and KGen for E_{G}. We do not need them in the case that A is finite; it is easy to see that they follow from K1, KGen, and E. In the case that A is infinite, however, they are necessary.

Axiom E4 is sound in M_{A}^{r}, M_{A}^{rt}, M_{A}^{rst}, and M_{A}^{elt}. It is easy to see that E4 follows from K2, E1, and EGen, so will not be needed in systems that contain these axioms. Moreover, it is not hard to show that E4 follows from E1, E2, and K5 if the set of agents is finite. However, it does not follow from these axioms if the set of agents is infinite. Thus, it will have to be explicitly included in systems containing K5 but not K2.

Axiom E5 follows from K2 and E1. Moreover, we use it only in systems that already include K2 and E1. Nevertheless, for technical reasons, it is useful to list it separately. Similarly, it is not hard to see that E7 is a derivable rule in any system that includes Prop, MP, K1, K3, E1, E4, and EGen (we prove this in Section 4.4). While we use E7 only in such systems, like E5, it is useful to list it separately.

Axiom E6 (with E_{G} replaced by K_{i}) is the standard axiom used to characterize symmetric K_{i} relations [FHMV95]. It follows easily from K2, K5, E1, and E2 if A is finite. However, like E4, it must be specifically included if A is infinite.

Finally, we have the following well-known axiom and inference rule for common knowledge:

C1. C_{G}φ ⇒ E_{G}(φ ∧ C_{G}φ).

RC1. From φ ⇒ E_{G}(ψ ∧ φ) infer φ ⇒ C_{G}ψ.

Historically, in the case of one agent, the system with axioms and rules Prop, K1, MP, and KGen has been called K; adding K2 to K gives us T; adding K4 to T gives us S4; adding K5 to S4 gives us S5; replacing K2 by K3 in S5 gives us KD45. We use the subscript G to emphasize the fact that we are considering systems with sets of agents coming from G rather than only one agent and the superscript C to emphasize that we add E1–E3, EGen, C1, and RC1 to the system. In this way, we get the systems K_{G}^{C}, T_{G}^{C}, and S4_{G}^{C}. Thus, K_{G}^{C} consists of Prop, K1, MP, KGen, E1, E2, E3, EGen, C1, and RC1; we get S4_{G}^{C} by adding K2 and K4 to K_{G}^{C}. We get KD45_{G}^{C} by adding K3–K5 and E4 to K_{G}^{C} and we get S5_{G}^{C} by adding K2, K4, K5 and E6 to K_{G}^{C}. See Table 1 for a summary of these systems and the associated axioms and structures.

One of the two main results of this paper shows that each of these axiom systems is sound and complete with respect to an appropriate class of structures. For example, K_{G}^{C} is a sound and complete axiomatization with respect to M_{A} and S5_{G}^{C} is a sound and complete axiomatization with respect to M_{A}^{rst}. In the case that A is finite, this result is well known (see [FHMV95, HM92]—as mentioned earlier, E is used in the axiomatization instead of E1–E3 and EGen). What is perhaps surprising is that E1–E3 and EGen suffice even if A is infinite. For example, suppose that G just consists of the singleton A. In that case, E2 becomes vacuous. Thus, while

System Axioms  Structures Properties of K_{i}
K_{G}^{C} Prop, K1, MP, KGen, M none

E1, E2, E3, EGen, C1, RC1

T_{G}^{C}  K_{G}^{C}, K2  M^{r}  reflexive
S4_{G}^{C}  K_{G}^{C}, K2, K4  M^{rt}  reflexive, transitive
KD45_{G}^{C} K_{G}^{C}, K3, K4, K5, E4  M^{elt}  Euclidean, serial, transitive
S5_{G}^{C}  K_{G}^{C}, K2,K4,K5, E6  M^{rst}  reflexive, symmetric, transitive

Table 1: Axioms Systems and Structures

the axioms force E_{A}φ to imply that each agent in A knows φ, we have no way of expressing the converse. Indeed, it is easy to construct a structure for the axioms with the standard interpretations of all the K_{i} relations but a nonstandard one of E_{A}, where all the agents in A know φ and yet E_{A}φ does not hold. Consider, for example, a structure with a single state s for the language with an infinite set A of agents. Suppose that every primitive proposition p is true at s, K_{i} is empty for all i ∈ A, and K_{i} is interpreted in the usual way for all i ∈ A (so that K_{i}φ is true at s for all formulas φ). For E_{A}, however, we say that E_{A}φ holds at s if and only if it is provable in, say, K_{G}^{C}. Of course, there are obviously standard models in which E_{A}p does not hold and so (by the soundness of the axioms for standard interpretations) E_{A}p is not provable. Thus, in this interpretation, E_{A}p does not hold at s while K_{i}p does for every i ∈ A. Finally, it is clear that all the axioms of K_{G}^{C} are true in this structure. Similar examples can be given to show that E4 and E6 do not follow from the specified other axioms when the set of agents is infinite.

3 The Main Results and a Proof in a Simplified Setting

In this section, we state the two main results of this paper—complete axiomatizations and decision procedures. We then provide a proof of a simpler version of these results that illustrates some of the main ideas. We first state the completeness results.

Theorem 3.1: For formulas in the language L_{G}^{C}:

(a) K_{G}^{C} is a sound and complete axiomatization with respect to M_{A},

(b) T_{G}^{C} is a sound and complete axiomatization with respect to M_{A}^{r},

(c) S4_{G}^{C} is a sound and complete axiomatization with respect to M_{A}^{rt},

(d) S5_{G}^{C} is a sound and complete axiomatization with respect to M_{A}^{rst},

(e) KD45_{G}^{C} is a sound and complete axiomatization with respect to M_{A}^{elt}.

Before stating the results regarding complexity, we first show that questions about certain facts regarding sets of the form G_{0} − (G_{1} ∪ … ∪ G_{k}) are reducible to satisfiability. We are not just interested in sets of the form G_{0} − (G_{1} ∪ … ∪ G_{k}) for G_{1}, …, G_{k} ∈ G. For example, when dealing with M^{rt}, it turns out that we are interested in sets H of this form if |H| = 1. But if H_{1} is such a set, then we are also interested in sets of the form H_{2} = G_{0} − (G_{1} ∪ … G_{k} ∪ H_{1}). And if |H_{2}| = 1, then we can also include H_{2} in the union, and so on. The following definition makes this precise.

Definition 3.2: Given a set J of subsets of A and an integer m ≥ 1, define a sequence J_{0}^{m}, J_{1}^{m}, … of sets of subsets of A inductively as follows. Let J_{0}^{m} = J. Suppose that we have defined J_{0}^{m}, …, J_{k}^{m}. Then J_{k+1}^{m} = J_{k}^{m} ∪{G−∪H : G ∈ J , H ⊆ J_{k}^{m}, H finite, |G−∪H| ≤ m}. Let J^{m} = ∪_{i}J_{i}^{m}; let Ĵ^{m} = {G − ∪H : G ∈ J , H ⊆ J^{m}, H finite}. For uniformity, we take Ĵ^{0} = {G − ∪H : G ∈ J , H ⊆ J , H finite}.

For example, if A = {1, 2, 3, …} and J = {A, {1}, {1, 2}, {1, 2, 3}, {1, 2, 3, 4}, …}, then J_{1}^{1} = J ∪ {∅, {2}, {3}, …}, since {k} = {1, …, k} − {1, …, k − 1}. Of course, J_{m}^{1} = J_{1}^{1} for m ≥ 1, since all singletons are already present in J_{1}^{1}. Similarly, J_{1}^{2} = J_{1}^{1} ∪ {{n, n + 1} : n = 1, 2, 3} and J_{2}^{2} consists of J_{1}^{2} and all doubletons.

Let J^{∗} be the algebra generated by J (that is, the Boolean combinations of sets in J). It is useful to talk about the length of a description of various sets in J^{∗} (particularly those in Ĵ^{m} for some m). Formally, we assume we have a language whose primitive objects consist of the elements of J and the symbols ∪ and − (for set difference). The length of a description is then the number of symbols of J that appear in it. Notice that, in general, an element of J^{∗} may have several different descriptions. We are not always careful to distinguish a set from its description. (We hope that the reader will be able to tell which is intended from context.) We use l(G) to denote the length of the description of G ∈ J^{∗}.

Let G_{A} = G ∪ {{i} : i ∈ A}. Throughout the paper (and, in particular, in the proof of the next proposition), for ease of exposition, we identify E_{{i}} with K_{i}, for i ∈ A (which allows us to write E_{G} for each G ∈ G_{A}).

Proposition 3.3:

(a) The question of whether |G| > 0 for G ∈ Ĝ_{A}^{0} is reducible (in time linear in l(G)) to the satisfiability problem for the language L_{G}^{E} with respect to all of M_{A}, M_{A}^{r}, M_{A}^{rt}, M_{A}^{rst}, and M_{A}^{elt}.

(b) The questions of whether |G| > 0 and |G| > 1 for G ∈ Ĝ_{A}^{1} are each reducible (in time linear in l(G)) to the satisfiability problem for the language L_{G}^{E} with respect to all of M_{A}^{rt}, M_{A}^{rst}, and M_{A}^{elt}.

(c) For all m ≥ 1, the question of whether |G| > m for G ∈ Ĝ_{A}^{m} is reducible (in time linear in l(G) + m) to the satisfiability problem for L_{G}^{E} with respect to M_{A}^{rst} and M_{A}^{elt}.

(d) The question of whether |G_{1} ∩ … ∩ G_{k}| > 0, for G_{1}, …, G_{k} ∈ G_{A} is reducible (in time linear in k) to the satisfiability problem for L_{G}^{E} with respect to M_{A}^{elt}.

Proof: For part (a), suppose that G ∈ Ĝ_{A}^{0}. Thus, G = G_{0}−(G_{1}∪…∪G_{k}) for some G_{0}, …, G_{k} ∈ G_{A}. Consider the formula φ_{a} =_{def} ¬E_{G_{0}}p∧E_{G_{1}}p∧…∧E_{G_{k}}p, where p is a primitive proposition. Clearly φ_{a} is satisfiable in M_{A}, M_{A}^{r}, M_{A}^{rt}, M_{A}^{rst}, or M_{A}^{elt} iff |G_{0} − (G_{1} ∪ … ∪ G_{k})| > 0.

For part (b), given G, we construct two formulas φ_{G,p} and ψ_{G} with the following properties.

• φ_{G,p} is satisfiable in M_{A}^{t} (i.e., the class of structures where the K_{i} relations are transitive) iff |G| > 0.

• For all structures M and states s in M, if (M, s) ⊧ φ_{G,p}, then (M, s) ⊧ ¬K_{j}p for some j ∈ G.

• ψ_{G} is satisfiable in M_{A}^{t} iff |G| > 1.

• |φ_{G,p}| and |ψ_{G}| are both linear in l(G).

This, of course, suffices to prove the result.

We construct the formulas φ_{G,p} by induction on the least h such that G = G′ − ∪H and H ⊆ (G_{A})_{h}^{1}. (We are here thinking of G as specified by its description.) If H ⊆ (G_{A})_{0}^{1} = G_{A}, suppose that H = {G_{1}, …, G_{k}}. Then we take φ_{G,p} to be ¬E_{G′}p ∧ E_{G_{1}}p ∧ … ∧ E_{G_{k}}p. This clearly has the desired properties.

Now suppose that H ⊆ (G_{A})_{h}^{1} for h ≥ 1. Without loss of generality, we can assume that H = {G_{1}, …, G_{k′}, G_{k′+1}, …, G_{k}}, where G_{1}, …, G_{k′} ∈ G_{A} and, for j = k′ + 1, …, k, G_{j} ∈ (G_{A})_{h}^{1} − G_{A} is of the form G′_{j} − ∪H_{j} with G′_{j} ∈ G_{A}, H_{j} ⊆ (G_{A})_{h−1}^{1}, and |G_{j}| = 1. Define φ_{G,p} as

¬E_{G′}¬(¬p ∧ ⋀_{j=k′+1}^{k}φ_{G_{j},p_{j}}) ∧ E_{G_{1}}p ∧ … ∧ E_{G_{k′}} p ∧ ⋀_{j=k′+1}^{k}E_{G′_{j}}p_{j},

where we assume that the sets of primitive propositions that appear in φ_{G_{j},p_{j}}, j = k′ + 1, …, k, are mutually exclusive and do not include p.^{2}

Now suppose that φ_{G,p} is true at some state s in a structure M ∈ M_{A}^{t}. Then for some i ∈ G′, we must have (M, s) ⊧ ¬K_{i}¬(¬p ∧ ⋀_{j=k′+1}^{k} φ_{G_{j},p_{j}}). We cannot have i ∈ G_{1} ∪ … ∪ G_{k′}, since (M, s) ⊧ E_{G_{j}}p for j = 1, …, k′. Nor can we have i ∈ G_{j} for j = k′ +1, …, k. For suppose that G_{j} = {i_{j}}, j ∈ {k′ + 1, …, k}. Then (M, s) ⊧ ¬K_{i}¬φ_{G_{j},p_{j}} ∧ E_{G′_{j}}p_{j}. From the second property of φ_{G,p}, it follows that M ⊧ φ_{G_{j},p_{j}} ⇒ ¬K_{i_{j}}p, so (M, s) ⊧ ¬K_{i}K_{i_{j}}p_{j} ∧ K_{i_{j}}p_{j}. We cannot have i = i_{j} by transitivity. It follows that G ≠ ∅.

Conversely, if G ≠ ∅, we show that φ_{G,p} is satisfiable in M_{A}^{rst} (and hence also in M_{A}^{rt} and M_{A}^{elt}). We actually prove a stronger result. We show that if G_{1}, …, G_{k} are nonempty and the formulas φ_{G_{1},p_{1}}, …, φ_{G_{k},p_{k}} involve disjoint sets of primitive propositions, then φ_{G_{1},p_{1}} ∧ … ∧ φ_{G_{k},p_{k}} is satisfiable in a structure in M_{A}^{rst} of a certain form. To make this precise, suppose that M = (S, π, {K_{i} : i ∈ A}), s ∈ S, S′ is a set of states disjoint from S, and s′ ∈ S′. We say that M is embedded in the structure M′ = (S ∪ S′, π′, {K′_{i} : i ∈ A}) at (s, s′) if

1. π′|_{S} = π and K′_{i}|_{S×S} = K_{i} for i ∈ A,

2. if (t, t′) ∈ K′_{i} for t ∈ S and t′ ∈ S′, then t = s and t′ = s′.

We show by induction on h that if G_{j} = G′_{j} − ∪H_{j}, H_{j} ⊆ (G_{A})_{h}^{1}, |G_{j}| > 0 for j = 1, …, k, and the formulas φ_{G_{1},p_{1}}, …, φ_{G_{k},p_{k}} involve disjoint sets of primitive propositions, then for all i_{1}, …, i_{k} such that i_{j} ∈ G_{j}, there exists a structure M ∈ M_{A}^{rst} and a state s in M such that:

2Here we are implicitly assuming that the set of primitive propositions is infinite, so that this can be done.

With more effort, we can prove a similar result even if the set is finite, using the techniques of [Hal95].

1. (M, s) ⊧ φ_{G_{1},p_{1}} ∧ … ∧ φ_{G_{k},p_{k}},

2. ∃t_{1}, …, t_{k} such that (s, t_{j}) ∈ K_{i_{j}} and (M, t_{j}) ⊧ ¬p_{j},

3. K_{i}(s) = {s} for i ∉ {i_{1}, …, i_{k}},

4. for all structures M′ and states s′ in M′ such that M is embedded in M′ at (s, s′) and (M′, s′) ⊧ p_{1} ∧ … ∧ p_{k}, we have that (M′, s) ⊧ φ_{G_{1},p_{1}} ∧ … ∧ φ_{G_{k},p_{k}}.

If h = 0, then it is easy to construct such a structure. Given i_{1}, …, i_{k} such that i_{j} ∈ G_{j} (where the i_{j} are not necessarily distinct) we construct a structure M with states s, t_{1}, …, t_{k} (where t_{j} = t_{j′} if i_{j} = i_{j′}) such that (M, t_{j}) ⊧ ⋀_{{j′:i_{j′}=i_{j}}} ¬p_{j′} ∧ ⋀_{{j′:i_{j′}≠i_{j}}} p_{j′}, (M, s) ⊧ p_{1} ∧ … ∧ p_{k}, and K_{i} is the smallest equivalence relation that includes (s, t_{j}) if i = i_{j}. It is easy to check that M has the required properties.

For the inductive step, suppose that we are given i_{1}, …, i_{k} such that i_{j} ∈ G_{j}. Note that the first conjunct of φ_{G_{j},p_{j}} has the form ¬E_{G′_{j}}¬(¬p_{j} ∧ ⋀_{k=1}^{m_{j}} φ_{G_{jk},p_{jk}}). By the induction hypothesis, we can find a structure M_{j} with state space S_{j} and a state s_{j} in S_{j} with the properties above such that (M, s_{j}) ⊧ ¬p_{j} ∧ ⋀_{k=1}^{m_{j}} φ_{G_{jk},p_{jk}}. (That we can get (M, s_{j}) ⊧ ⋀_{k=1}^{m_{j}} φ_{G_{jk},p_{jk}} is an immediate consequence of the induction hypothesis. Since p_{j} does not appear in φ_{G_{jk},p_{jk}} for k = 1, …, m_{j}, by construction of φ_{G_{j},p_{j}}, we can then extend the structure so as to make (M, s_{j}) ⊧ ¬p_{j} without changing any of the desired properties.) If i_{j} = i_{j′}, we can also assume without loss of generality that M_{j} = M_{j′} and s_{j} = s_{j′}. (For example, suppose that i_{1} = i_{2}. To make M_{1} = M_{2}, we need to show that we can find a structure M′ and state s′ such that (M′, s′) ⊧ ¬p_{1} ∧ ¬p_{2} ∧ ⋀_{k=1}^{m_{1}} φ_{G_{1k},p_{1k}} ∧ ⋀_{k=2}^{m_{2}} φ_{G_{2k},p_{2k}}; but this is immediate from the induction hypothesis and the fact that p_{1} and p_{2} do not appear in φ_{G_{1k},p_{1k}} for k = 1, …, m_{1} or φ_{G_{2k},p_{2k}} for k = 1, …, m_{2}.) Let S consist of S_{1} ∪ … ∪ S_{k} together with a new state s. We define M ∈ M_{A}^{rst} so that each of the structures M_{j} is embedded in M at (s_{j}, s) and the relation in K_{i_{j}} in M is the smallest equivalence relation that makes this true such that (s, s_{j}) ∈ K_{i_{j}}. For i ∉ {i_{1}, …, i_{k}}, define K_{i} to be the smallest equivalence relation that makes each of the M_{j}’s embedded in M. Thus, for i ∉ {i_{1}, …, i_{k}}, the K_{i} relation in M is essentially the union of the K_{i} relations in the M_{j}’s together with (s, s), while the K_{i_{j}} relation in M is the union of the K_{i_{j}} relations in the M_{j}’s together with (s, s), (s, s_{j}), and (s_{j}, s). We define the interpretation π in M so that (M, s) ⊧ p_{j} for j = 1, …, k. Since K_{i}(s) = {s} for i ∉ {i_{1}, …, i_{k}}, it now easily follows that (M, s) ⊧ φ_{G_{1},p_{1}} ∧ … φ_{G_{k},p_{k}}. We leave it to the reader to check that all the other requirements in the construction hold as well. This completes the inductive step.

Of course, the fact that φ_{G,p} is satisfiable if |G| > 0 is now immediate.

Finally, define ψ_{G} to be φ_{G,p} ∧ E_{G′}(q ∧ (¬p ⇒ φ_{G,q})), where we assume that the primitive propositions that appear in φ_{G,p} and φ_{G,q} are disjoint.

We claim that ψ_{G} is not satisfiable in M_{A}^{t} if |G| ≤ 1. Clearly it is not satisfiable in M_{A}^{t} if |G| = 0, since φ_{G,p} is not. So suppose, by way of contradiction, that G = {i} and (M, s) ⊧ ψ_{G} for some M ∈ M_{A}^{t}. Then, thanks to the properties of φ_{G,p} and φ_{G,q}, we must have (M, s) ⊧ ¬K_{i}p ∧ K_{i}(q ∧ (¬p ⇒ ¬K_{i}q)). It is easy to see that this gives us a contradiction. On the other hand, if |G| > 1, we can construct a structure in M_{A}^{t} (in fact, in M_{A}^{rst}) satisfying ψ_{G} as follows. Suppose that i, i′ ∈ G and φ_{G,p} is of the form

¬E_{G′}¬(¬p ∧ ⋀_{j=k′+1}^{k} φ_{G_{j},p_{j}}) ∧ E_{G_{1}}p ∧ … ∧ E_{G_{k′}} p ∧ ⋀_{j=k′+1}^{k} E_{G′_{j}}p_{j}.

We know that |G_{k′+1}| = ⋯ = |G_{k}| = 1, so by our previous argument, we can find a structure M′ = (S′, …) ∈ M_{A}^{rst} and states s′, t′ ∈ S′ such that (M′, s′) ⊧ φ_{G,q} ∧ ⋀_{j=k′+1}^{k} φ_{G_{j},p_{j}}, (s′, t′) ∈ K_{i′}, (M′, t′) ⊧ ¬q, and K_{i}(s′) = {s′}. Since p does not appear in φ_{G,q}, we can assume without loss of generality that (M′, s′) ⊧ ¬p. Now let M ∈ M_{A}^{rst} be a structure whose state space is S′ ∪{s}, where s is a fresh state not in S′, such that M′ is embedded in M at (s, s′), (s, s′) ∈ K_{i}, (M, s) ⊧ p ∧ q ∧ p_{k′+1} ∧ … ∧ p_{k}, and K_{j}(s) = {s} for j ≠ i. It is easy to see that (M, s) ⊧ ψ_{G}.

For part (c), we construct formulas φ_{m,G,p} such that

• if (M, s) ⊧ φ_{m,G,p} for M ∈ M_{A}^{elt} (and hence also for M ∈ M_{A}^{rst}), then there exist m + 1 distinct agents i_{1}, …, i_{m+1} ∈ G such that (M, s) ⊧ ¬K_{i_{j}}¬p, j = 1, …, m + 1;

• |φ_{m,G,p}| = O(l(G) + m);

• if |G| > m, then φ_{m,G,p} is satisfiable in M_{A}^{rst} (and hence in M_{A}^{elt}).

We first define an auxiliary family of formulas. If G′, G_{1}, …, G_{k} ⊆ G_{A}, let ψ_{m,G′,G_{1},...,G_{k},p} be the formula

E_{G_{1}}q_{0} ∧ … ∧ E_{G_{k}}q_{0}∧
¬E_{G′}¬(p_{0} ∧ p_{1} ∧ q_{1} ∧ E_{G′}(p_{0} ⇒ p_{1} ∧ q_{1}))∧
… ∧ ¬E_{G′}¬(p_{0} ∧ p_{m+1} ∧ q_{m+1} ∧ E_{G′}(p_{0} ⇒ p_{m+1} ∧ q_{m+1}))∧
E_{G′}((p_{0} ⇒ (p ∧ ¬q_{0})) ∧ (q_{1} ⇔ ¬p_{2} ∧ q_{2}) ∧ (q_{2} ⇔ ¬p_{3} ∧ q_{3}) ∧ … ∧ (q_{m+1} ⇔ true)),

where p_{0}, …, p_{m+1}, q_{0}, …, q_{m+1} are fresh primitive propositions distinct from p. Observe that |ψ_{m,G′,G_{1},...,G_{k},p}| is O(k + m). It is easy to check that the last clause forces q_{i}, for 1 ≤ i ≤ m, to be equivalent to ¬p_{i+1} ∧ … ∧ ¬p_{m+1}, at least in the worlds G′-reachable in one step. Thus, in these worlds, the formulas p_{i} ∧ q_{i}, i = 1, …, m + 1, are mutually exclusive. Clearly if (M, s) ⊧ ψ_{m,G′,G_{1},...,G_{k},p} for M ∈ M_{A}^{elt}, then there must be agents i_{1}, …, i_{m+1} in G′ − (G_{1} ∪ … ∪ G_{k}) such that (M, s) ⊧ ¬K_{i_{j}}¬(p_{0} ∧ p_{j} ∧ q_{j} ∧ E_{G′}(p_{0} ⇒ p_{j} ∧ q_{j})). (Note that we cannot have i_{j} ∈ G′ ∩ (G_{1} ∪ … ∪ G_{k}) since (M, s) ⊧ E_{G_{j}}q_{0} ∧ E_{G′}(p_{0} ⇒ ¬q_{0})). Thus, there must exist states t_{j}, j = 1, …, m + 1 such that (s, t_{j}) ∈ K_{i_{j}} and (M, t_{j}) ⊧ p_{0} ∧ p_{j} ∧ q_{j} ∧ E_{G′}(p_{0} ⇒ p_{j} ∧ q_{j}). To see that these agents i_{j} must be distinct, suppose that i_{j} = i_{j′} for j < j′. By the Euclidean property, we have (t_{j}, t_{j′}) ∈ K_{i_{j}}. Since (M, t_{j}) ⊧ E_{G′}(p_{0} ⇒ p_{j} ∧ q_{j}), we must have (M, t_{j′}) ⊧ p_{j} ∧ q_{j}. But since (M, t_{j′}) ⊧ q_{j} ⇔ (¬p_{j} ∧ … ∧ ¬p_{m+1}), this is inconsistent with the fact that (M, t_{j′}) ⊧ p_{j′}. Since (M, s) ⊧ E_{G′}(p_{0} ⇒ p), it follows that (M, s) ⊧ ¬K_{i_{j}}¬p for j = 1, …, m + 1. Conversely, it is easy to see that if |G′ − (G_{1} ∪ … ∪ G_{k})| > m then ψ_{m,G′,G_{1},...,G_{k},p} is satisfiable in M_{A}^{rst}. We leave the details to the reader.

We now construct the formulas φ_{m,G,p} by induction on the least h such that G = G′ − ∪H and H ⊆ (G_{A})_{h}^{m}. If H = {G_{1}, …, G_{k}} ⊆ (G_{A})_{0}^{m} = G_{A}, then we take φ_{m,G,p} = ψ_{m,G′,G_{1},...,G_{k},p}. Now suppose that H ⊆ (G_{A})_{h}^{m} for h > 0. Without loss of generality, we can assume that H = {G_{1}, …, G_{k′}, G_{k′+1}, …, G_{k}}, where G_{1}, …, G_{k′} ∈ G_{A} and, for j = k′ + 1, …, k, G_{j} ∈ (G_{A})_{h−1}^{m} is of the form G′_{j} − ∪H_{j} with G′_{j} ∈ G_{A}, H_{j} ⊆ (G_{A})_{h−1}^{m}, and |G_{j}| ≤ m. Suppose that |G_{j}| = m_{j}. By induction, for j = k′ + 1, …, k, we can construct formulas φ_{m_{j}−1,G_{j},p} and the formula ψ_{m,G′,G_{1},...,G_{k′},p} such that if (M, s) ⊧ φ_{m_{j}−1,G_{j},p}, then for each agent i ∈ G_{j}, we have (M, s) ⊧ ¬K_{i}¬p. Without loss of generality, we can assume that, other than p, the sets of primitive propositions mentioned in the formulas φ_{m_{j}−1,G_{j},p} are disjoint, and these sets are all disjoint from the set of primitive propositions in ψ_{m,G′,G_{1},...,G_{k′},p}. Let φ_{m,G,p} be the formula

ψ_{m,G′,G_{1},...,G_{k′},p′} ∧ ⋀_{j=k′+1}^{m} φ_{m_{j}−1,G_{j},p} ∧ E_{G′}(p′ ⇒ E_{G′}¬p).

The argument that this formula has the required properties is almost identical to that for ψ_{m,G′,G_{1},...,G_{k},p}; we leave details to the reader.

Finally, for part (d), consider the formula φ_{d} defined as

E_{G_{1}}p_{1} ∧ … ∧ E_{G_{k−1}}p_{k−1} ∧ E_{G_{k}}(¬p_{1} ∨ … ∨ ¬p_{k−1}).

We leave it to the reader to check that φ_{d} is satisfiable in M_{A}^{elt} iff G_{1} ∩ … ∩ G_{k} = ∅.

We already saw that for axiom E2 to be recursive, we need to be able to decide whether |G_{0} − (G_{1} ∪ … ∪ G_{k})| ≥ 1 (or, equivalently, whether G_{0} ⊆ G_{1} ∪ … ∪ G_{k}) for G_{0}, …, G_{k} ∈ G_{A}. Proposition 3.3 shows that if there is no recursive algorithm for answering such questions, the satisfiability problem for the logic (even without C_{G} operators) is also not decidable. For simplicity here, we assume we have oracles that can answer the questions that we need to answer (according to Proposition 3.3) in unit time; we consider the complexity of querying the oracle in more detail in Section 4.5. More precisely, let O_{m} be an oracle that, for a set G ∈ Ĝ_{A}^{m}, tells us whether |G| > k, for any k < m. (Thus, queries to oracle O_{m} have the form (G, k).) Let O′ be an oracle that tells us whether G_{1} ∩ … ∩ G_{k} = ∅, for G_{1}, …, G_{k} ∈ G_{A}.

Theorem 3.4: There is a constant c > 0 (independent of A) and an algorithm that, given as input a formula φ ∈ L_{G}^{C}, decides if φ is satisfiable in M_{A} (resp., M_{A}^{r}, M_{A}^{rt}, M_{A}^{rst}, M_{A}^{elt}) and runs in time 2^{c|φ|} given oracle O_{0} (resp., O_{0}, O_{1}, O_{|φ|}, both O_{|φ|} and O′), where queries to the oracle take unit time. Moreover, if G contains a subset with at least two elements, then there exists a constant d > 0 (independent of A) such that every algorithm for deciding the satisfiability of formulas in M_{A} (resp., M_{A}^{r}, M_{A}^{rt}, M_{A}^{rst}, M_{A}^{elt}) runs in time at least 2^{d|φ|}, even given access to oracle O_{0} (resp., O_{0}, O_{1}, O_{|φ|}, both O_{|φ|} and O′), for infinitely many formulas φ.

Before proving Theorems 3.1 and 3.4, we prove a somewhat simpler theorem that allows us to both explain intuitively why the results are true and point out some of the difficulties in proving them.

Proposition 3.5: If there is an oracle that decides if G = ∅ for each Boolean combination G of elements in G_{A}, then, for every formula φ ∈ L_{G}^{C}, we can effectively find a formula φ^{σ} in a language L_{G′}^{C}, where G′ consists of all nonempty subsets of a set A′ of at most 2^{|φ|} agents, such that |φ^{σ}| = |φ| and φ is satisfiable in M_{A} iff φ^{σ} is satisfiable in M_{A′}.

Proof: Given φ, let G_{φ} be the set of subsets G of agents such that E_{G} or C_{G} appears in φ. (Recall that we are identifying K_{i} with E_{{i}}, so that {i} ∈ G_{φ} if K_{i} appears in φ.) Note that |G_{φ}| ≤ |φ|.

Suppose that G = {G_{1}, …, G_{N}}. An atom over G is a nonempty set of the form G′_{1}∩…∩G′_{N}, where G′_{i} = G_{i} or G′_{i} = \overline{G_{i}}. Clearly there are at most 2^{N} atoms over G. Let A′ consist of the atoms over G_{φ}. Note that |A′| ≤ 2^{|φ|}. Define σ : A → A′ by taking σ(i) to be the unique atom over G_{φ} containing i. We extend σ to a map from 2^{A} → 2^{A′} by taking σ(G) = {σ(i) : i ∈ G} (= {H ∈ G_{φ} : H ⊆ G}). Translate φ to φ^{σ} by replacing all occurrences of E_{G} and C_{G} in φ by E_{σ(G)}, and C_{σ(G)}, respectively. Clearly |φ| = |φ^{σ}|. (Note that it is important here that we take the length of E_{G} and C_{G} to be independent of G.)

If φ is satisfiable, let (M, s) witness that fact. Convert M into a structure M^{σ} over A′ with the same state space by setting (s, t) ∈ K_{A} iff (s, t) ∈ ∪_{j∈A}K_{j} for each A ∈ A′. An easy induction shows that for every formula ψ with sets (of agents) chosen from G_{φ}, we have (M, s) ⊧ ψ if and only if (M^{σ}, s) ⊧ ψ^{σ}. The only point that needs any comment is that E_{G} (and so also C_{G}) has the same meaning in M (in terms of reachability) as E_{σ(G)} (C_{σ(G)}) in M^{σ}, by the definition of σ(G) and the K_{A} relations. Thus (M^{σ}, s) ⊧ φ^{σ} as required.

For the other direction, suppose that (M′, s) ⊧ φ^{σ} for some structure M′ over A′. We define a structure M over A by defining K_{i} = K_{σ(i)}. Again, an easy induction shows that for every formula ψ with sets chosen from G_{φ}, (M′, s) ⊧ ψ if and only if (M, s) ⊧ ψ^{σ}. Once again, the only point to notice is that E_{G} (and so also C_{G}) has the same meaning in M′ (in terms of reachability) as E_{σ(G)} (C_{σ(G)}) in M by the definition of σ(G) and the relations K_{j}. Thus (M, s) ⊧ φ as required.

Corollary 3.6: Given an oracle that decides, for each Boolean combination G of elements in G_{A}, whether G = ∅, there is a constant c > 0 (independent of A) and an algorithm that, given as input a formula φ ∈ L_{G}^{C}, decides if φ ∈ L_{G}^{C} is satisfiable in M_{A} and runs in time 2^{c2^{|φ|}}.

Proof: Clearly, to check if φ is satisfiable, it suffices to check if φ^{σ} is satisfiable. In [HM92], there is an exponential time algorithm for checking satisfiability. However, this algorithm presumes that the set of agents is fixed. A close look at the algorithm actually shows that it runs in time 2^{cm|φ|}, where m is the number of agents. In our translation, the set of agents is exponential in |φ|, giving us a double-exponential time algorithm.

Corollary 3.7: If G ∪ {∅} is closed under intersection and complementation, then K_{G}^{C} is a sound and complete axiomatization for the language L_{G}^{C} with respect to M_{A}.

Proof: Soundness is straightforward, so we focus on completeness. Suppose that φ is valid. By Proposition 3.5, so is φ^{σ}. Since A′ is finite, K_{G′}^{C} is a complete axiomatization for L_{G′}^{C} with respect to M_{A′}. Thus, K_{G′}^{C} ⊢ φ^{σ}. We can translate this proof step by step to a proof of φ in K_{G}^{C}. We simply replace every formula ψ that appears in the proof of φ^{σ} by ψ^{τ}, where ψ^{τ} is obtained by replacing each occurrence of K_{A} in ψ by E_{A} unless A = {i} is a singleton, in which case we replace K_{A} by K_{i}, and replacing each occurrence of E_{G}, and C_{G} in ψ by E_{∪G}, and C_{∪G}, respectively. Since we have assumed G ∪ {∅} is closed under complementation and intersection, G is closed under union, and hence ψ^{τ} is a formula in L_{G}^{C}.

It is easy to check that the translated proof is still a proof over the language L_{G}^{C}: Tautologies become tautologies as (φ ∨ ψ)^{τ} = φ^{τ} ∨ ψ^{τ} and similarly for negations. Instances of MP in the proof of φ^{σ} become instances of MP in the proof of φ because (φ → ψ)^{τ} = φ^{τ} → ψ^{τ}. Instances of KGen in the proof of φ^{σ} become instances of EGen or KGen in the proof of φ; similarly, instances of K1 are converted to instances of K1 or E1. It is easy to see that instances of E1, E2, E3, EGen, C1, and RC1 are converted to legitimate instances of the same axiom.

While Corollaries 3.6 and 3.7 are close to our desired theorems, they also make clear the difficulties we need to overcome in order to prove Theorems 3.1 and 3.4. Specifically,

• we need to cut the complexity down from double-exponential to single exponential;

• we need to prove completeness without assuming that G ∪ {∅} is closed under complementation and intersection;

• we want to use an oracle that tests only whether a set of the form G_{0} − (G_{1} ∪ … ∪ G_{k}) is nonempty, rather than one that applies to arbitrary Boolean combinations;

• we want to extend these results to the case that the K_{i} relations satisfy properties like transitivity.

With regard to the last point, while in general it is relatively straightforward to extend completeness and complexity results to deal with relations that have properties like transitivity, it is not so straightforward in this case. For example, even if M ∈ M_{A}^{rt}, the relations in the structure M^{σ} constructed in Proposition 3.5 are not necessarily transitive. As shown in Proposition 3.3, we need a different oracle to deal with transitivity.

4 Proving the Main Results

In this section, we prove Theorems 3.1 and 3.4. The structure of the proof is similar to that of Corollaries 3.6 and 3.7; we describe step by step the modifications required to deal with the problems raised in the previous section. It is convenient to split the proof into four cases, depending on the class of structures considered.

4.1 The Proof for M_{A} and M_{A}^{r}

In Proposition 3.5 we showed that we could translate a formula φ to a formula φ^{σ} such that φ was satisfiable in M_{A} iff φ^{σ} was satisfiable in M_{A′}, where A′ consisted of the atoms over G_{φ}. Our goal is to maintain the translation idea, but use as our target set of agents a set whose elements we can determine with the oracles at our disposal (for testing the nonemptiness of certain set differences). As a first step, we try to abstract the key ingredients of Proposition 3.5. Suppose that we have a set A′ of agents and a partial map σ : A → A′. Again, we can extend σ to a map from 2^{A} to 2^{A′}: σ(G) = {σ(i) : i ∈ G}. Given a formula φ, let φ^{σ} be the formula that results by replacing all the occurrences of G in φ by σ(G). In Proposition 3.5, A′ is the set of atoms over G_{φ} and σ(i) is the unique atom containing i. We were able to show that, for that choice of A′ and σ, the formulas φ and φ^{σ} were equisatisfiable. What does it take to obtain such a result in general? The following result shows that we need to be able to find a mapping τ : A′ → 2^{A} − {∅} with one key property.

Proposition 4.1: Given a formula φ and a partial map σ : A → A′ such that σ(G) ≠ ∅ for all G ∈ G_{φ}, suppose that there is a mapping τ : A′ → 2^{A} − {∅} such that for all G ∈ G_{φ}, we have ∪{τ(A) : A ∈ σ(G)} = G. Then φ is satisfiable in M_{A} (resp., M_{A}^{r}) iff φ^{σ} is satisfiable in M_{A′} (resp., M_{A′}^{r}).

Proof: Given φ and σ, suppose there exists a mapping τ with the property above. We show that φ and φ^{σ} are equisatisfiable.

First suppose that (M, s) ⊧ φ, where M ∈ M_{A}. We convert M = (S, π, {K_{i} : i ∈ A}) into a structure M′ = (S, π, {K_{A} : A ∈ A′}) by defining K_{A} = ∪{K_{i} : i ∈ τ(A)}. Notice that the assumed property of τ implies that for all G ∈ G_{φ}, we have

∪_{A∈σ(G)}K_{A} = ∪_{A∈σ(G)} ∪_{i∈τ(A)} K_{i} = ∪_{i∈G}K_{i}.

An easy induction on the structure of ψ now shows that (M, t) ⊧ ψ if and only if (M′, t) ⊧ ψ^{σ} for all t ∈ S and all formulas ψ ∈ L_{G_{φ}}^{C}. Also note that if M ∈ M_{A}^{r}, then M′ ∈ M_{A′}^{r} (since the union of reflexive relations is reflexive).

For the opposite direction, suppose (M′, s) ⊧ φ^{σ} for some M′ = (S, π, {K_{A} : A ∈ A′}) ∈ M_{A′}. Define M = (S, π, {K_{i} : i ∈ A}) ∈ M_{A} by setting K_{i} = K_{σ(i)} if σ(i) is defined and the empty relation otherwise. Note that for all G ∈ G_{φ} we have

∪_{i∈G}K_{i} = ∪_{i∈G}K_{σ(i)} = ∪_{A∈σ(G)}K_{A}.

Again, an easy induction on the structure of ψ shows that (M, t) ⊧ ψ if and only if (M′, t) ⊧ ψ^{σ} for all t ∈ S and all formulas ψ ∈ L_{G_{φ}}^{C}.

If M′ ∈ M_{A}^{r}, we modify the construction slightly by taking K_{i} = {(t, t) : t ∈ S} if σ(i) is undefined. Since σ(G) ≠ ∅ for G ∈ G_{φ}, it is easy to check that we still have ∪_{i∈G}K_{i} = ∪_{i∈G}K_{σ(i)}, so the modified construction works for the reflexive case.

For the mapping σ of Proposition 3.5 we can take τ to be the identity, but this requires an oracle for nonemptiness of atoms. We now show how to choose A′ and define maps σ and τ in a way that requires only information about whether sets of the form G_{0} − (G_{1} ∪ … ∪ G_{k}) are empty.

Definition 4.2: Given a set G of sets of agents and G ∈ G, a set H ⊆ G is a G-maximal subset of G if G − ∪H ≠ ∅ and G − ((∪H) ∪ G′) = ∅ for all G′ ∈ G − H. Let R(G) = {(G, H) : G ∈ G, H is a G-maximal subset of G}.

Note that we can check whether H is a G-maximal subset of G by doing at most |G| tests of the form (G − ∪H′) = ∅, and we can find all pairs (G, H) in R(G_{φ}) by doing at most |G|2^{|G|−1} such tests.

The following lemma gives some technical properties of R(G) that will be used frequently.

Lemma 4.3: Suppose that (G, H) ∈ R(G) for some set G of subsets of A.

(a) G − ∪H is an atom over G and, in fact, G − ∪H = ∩(G − H) ∩ (∩_{H∈H}\overline{H}).

(b) If (G′, H) ∈ R(G), then (G − ⋃ H) = (G′ − ⋃ H).

(c) If (G′, H′) ∈ R(G) and H ≠ H′, then (G − ⋃ H) ∩ (G′ − ⋃ H′) = ∅.

Proof: For part (a), first observe that since H is a G-maximal subset of G, for H ∉ H, we have G − ∪(H ∪ {H}) = ∅; i.e., G − ∪H ⊆ H. Thus, if H ∉ H, we have G − ∪H = (G ∩ H) − ∪H. Thus, G − ∪H = G ∩ (∩_{H∈H}\overline{H}) = ∩(G − H) ∩ (∩_{H∈H}\overline{H}), as desired. By definition, G − ∪H is an atom over G.

Part (b) is immediate from part (a), since it is clear that G − ∪H is independent of G and depends only on H.

For part (c), suppose that H ≠ H′. Without loss generality, there is some H ∈ H − H′. It follows immediately from part (a) that G − ∪H and G′ − ∪H′ are distinct atoms (hence disjoint), since G − ∪H ⊆ \overline{H} and G′ − ∪H′ ⊆ H.

If (G, H) ∈ R(G), let A_{H}^{G} denote the atom associated with H defined in Lemma 4.3(a). It is independent of G by Lemma 4.3(b). We omit G, writing simply A_{H}, when it is clear from the context which set G we have in mind.

We now show how to define a translation satisfying the hypotheses of Proposition 4.1 using the elements of R(G_{φ}) identified according to the second coordinate alone.

Given a formula φ, let A^{φ} = {H : ∃G[(G, H) ∈ R(G_{φ})]}. Define σ_{1} : A → A^{φ} by setting σ_{1}(i) = H if i ∈ A_{H} (as defined after Lemma 4.3) and undefined otherwise. As before, we extend σ_{1} to 2^{A} by defining σ_{1}(G) = {σ_{1}(i) : i ∈ G}.

Lemma 4.4: Define τ : A^{φ} → 2^{A} by setting τ(H) = ∩(G_{φ} − H). Then

(a) σ_{1}(G) = {H ∈ A^{φ} : ∃G′ ∈ G_{φ}((G′, H) ∈ R(G_{φ})), G ∉ H},

(b) σ_{1}(G) ≠ ∅ for G ∈ G_{φ},

(c) τ(H) ≠ ∅ for H ∈ A^{φ},

(d) ∪{τ(H) : H ∈ σ_{1}(G)} = G.

Proof: For part (a), first suppose that G ∉ H and (G′, H) ∈ R(G_{φ}) for some G′ ∈ G_{φ}. Then by Lemma 4.3(a), it follows that A_{H} ⊆ G. Since A_{H} ≠ ∅, there is some i ∈ A_{H}. Since i ∈ G and σ_{1}(i) = H, it follows that H ∈ σ_{1}(G). For the opposite inclusion, suppose that H ∈ σ_{1}(G). Then H = σ_{1}(i) for some i ∈ G ∩ A_{H}. Since G ∩ A_{H} ≠ ∅, it follows from the definition of A_{H} that G ∉ H.

For part (b), given G, note that there must be some G-maximal subset H. Thus, (G, H) ∈ R(G_{φ}). Since G − ∪H ≠ ∅, we must have G ∉ H. By part (a), H ∈ σ_{1}(G), so σ_{1}(G) ≠ ∅.

For part (c), suppose that H ∈ A^{φ}. Then there exists some G such that (G, H) ∈ R(G_{φ}), and hence G − ∪H ≠ ∅. It suffices to show that ∩(G_{φ} − H) ⊇ G − ∪H. This follows from Lemma 4.3(a).

For part (d), we first show that ∪{τ(H) : H ∈ σ_{1}(G)} ⊆ G. Note that if H ∈ σ_{1}(G), then by part (a), G ∈ G_{φ} −H. Thus, τ(H) = ∩(G_{φ} −H) ⊆ G. For the opposite containment, suppose that i ∈ G. Let H^{i} = {G′ ∈ G_{φ} : i ∉ G′}. Since i ∈ G − ∪H^{i}, there must be a G-maximal subset H of G_{φ} containing H^{i}. By part (a), we have H ∈ σ_{1}(G). Moreover, since H^{i} ⊆ H, for all H′ ∈ G_{φ} − H, we have i ∈ H′. Thus, i ∈ ∩(G_{φ} − H). It follows that i ∈ ∪_{H∈σ_{1}(G)} ∩ (G_{φ} − H), as desired.

Since |A^{φ}| ≤ 2^{|φ|}, we have now reduced satisfiability with infinitely many agents to satisfiability with finitely many agents, at least for M_{A} and M_{A}^{r}, using only tests that we know we need to be able to perform in any case. We next must deal with the problem we observed in the proof of Corollary 3.6, that is, there may be exponentially many agents in the subgroups mentioned in φ^{σ_{1}}. This is done in the following result. In this result, we assume that the complexity of checking whether i ∈ G is no worse than linear in |A|. While we do not assume this in general, it is true for the A′ and sets G that arise in the translation of Proposition 4.1, which suffices for our application of the result to the proof of Theorem 3.4.

Theorem 4.5: If A is finite and there is an algorithm for deciding if i ∈ G for G ∈ G that runs in time linear in |A|, then there is a constant c > 0 (independent of A) and an algorithm that, given as input a formula φ ∈ L_{G}^{C}, decides if φ is satisfiable in M_{A} (resp., M_{A}^{r}) and runs in time O(|A|2^{c|φ|}).

Proof: We first present an algorithm that decides if φ is satisfiable in M_{A}; we then show how to modify it to deal with M_{A}^{r}. The algorithm is just a slight modification of standard decision procedures [FHMV95, HM92]. (Far more serious modifications are needed to prove the analogous result for the M_{A}^{rt}, M_{A}^{rst}, and M_{A}^{elt}; see Theorems 4.9, 4.16, and 4.20.)

Let Sub(φ) be the set of subformulas of φ together with E_{G}(ψ ∧ C_{G}ψ) and ψ ∧ C_{G}ψ for each subformula C_{G}ψ of φ. Sub^{+}(φ) consists of the formulas in Sub(φ) and their negations. An easy induction on |φ| shows that |Sub(φ)| ≤ |φ|, so |Sub^{+}(φ)| ≤ 2|φ|. (Here we need to use the fact that we take the length of C_{G} to be 3.)

Let S^{1} consist of all subsets s of Sub^{+}(φ) that are maximally consistent in that (a) for each formula ψ ∈ Sub(φ), either ψ ∈ s or ¬ψ ∈ s, (b) they are propositionally consistent (for example, we cannot have all of ψ ∧ ψ′, ¬ψ, and ¬ψ′ in s), and (c) they contain E_{G}(ψ ∧ C_{G}ψ) iff they contain C_{G}ψ. Note that there are at most 2^{|φ|} sets in S^{1}.

For s ∈ S^{1} and G ∈ G_{A}, we define s/E_{G} = {ψ : E_{G}ψ ∈ s} (again, we identify K_{i} with E_{\{i\}}). Define s/\overline{K_{i}} = ∪_{i∈G}(s/E_{G}). Define a binary relation K_{i} on S^{1} for each i ∈ A by taking (s, t) ∈ K_{i} iff s/\overline{K_{i}} ⊆ t. We now define a sequence S^{j} of subsets of S^{1}. Suppose that we have defined S^{1}, …, S^{j}. S^{j+1} consists of all states s in S^{j} that seem consistent, in that the following two conditions hold:

1. If ¬E_{G}ψ ∈ s, then there is some t ∈ S^{j} such that (s, t) ∈ ∪_{i∈G}K_{i} and ¬ψ ∈ t.

2. If ¬C_{G}ψ ∈ s, then there is some t ∈ S^{j} such that t is G-reachable from s in S^{j} and ¬ψ ∈ t.

If S^{j} ≠ S^{j+1} then we continue the construction. Otherwise the construction terminates; in this case, the algorithm returns “φ is satisfiable” if φ ∈ s for some state s ∈ S^{j+1} and returns “φ is unsatisfiable” otherwise.

Since S^{j} ⊇ S^{j+1}, S^{1} has at most 2^{|φ|} elements, and there are |A| relations, it is easy to see that the whole procedure can be carried out in time O(|A|2^{c|φ|}) for some c > 0.

It remains to show that the algorithm is correct. First suppose that φ is satisfiable. In that case, (M, s_{0}) ⊧ φ for some structure M = (S, π, {K′_{i} : i ∈ A}) ∈ M_{A}. We can associate with each state s ∈ S the state s^{∗} in S^{1} consisting of all the formulas ψ ∈ Sub(φ) such that (M, s) ⊧ ψ. It is easy to see that if (s, t) ∈ K′_{i} then (s^{∗}, t^{∗}) ∈ K_{i}. A straightforward induction shows that the states s^{∗} for s ∈ S always seem consistent, and thus are in S^{j} for all j. Moreover, φ ∈ s_{0}^{∗}. Thus, the algorithm declares that φ is satisfiable, as desired.

Conversely, suppose that the algorithm declares that φ is satisfiable. We construct a structure M = (S, π, {K′_{i} : i ∈ A}) over A and Φ in which φ is satisfied as follows. Let j be the stage at which the algorithm terminates. Let S = S^{j}. Define π so that π(s)(p) = true iff p ∈ s, for s ∈ S and p ∈ Φ. For each i ∈ A, we take K′_{i} to be the restriction of K_{i} to S^{j}. A straightforward induction on the structure of formulas shows that for all formulas ψ ∈ Sub(φ) and states s ∈ S, we have (M, s) ⊧ ψ iff ψ ∈ s. (The cases for E_{G}ψ and C_{G}ψ use the appropriate clauses of the definition of seeming inconsistent and the choice of j.) Since φ ∈ s for some s^{∗} ∈ S, it follows that (M, s^{∗}) ⊧ φ, so φ is satisfiable.

To deal with M_{A}^{r}, the only change necessary is that in going from S^{1} to S^{2} in the construction, we also eliminate s ∈ S^{1} if (s, s) ∉ K_{i} for some i ∈ A. This guarantees that the K_{i} relations are reflexive. The remainder of the proof goes through unchanged.

Proof of Theorem 3.4 for M_{A} and M_{A}^{r}: The deterministic exponential time lower bound in Theorem 3.4 follows from the lower bound in the case where A is finite, which is proved in [HM92, Theorem 6.19] using techniques developed by Fischer and Ladner [FL79] for PDL. The sets G that arise in the lower bound proof have cardinality 2, so oracles are of no help here.

For the upper bound, suppose that we are given a formula φ. We first compute the set R(G_{φ}). This can be done with at most |φ|2^{|φ|} calls to oracle O_{0}, since |G_{φ}| ≤ |φ| and we need only check, for each G ∈ G_{φ} and H ⊆ G_{φ}, whether G − H = ∅.

Consider the mapping σ_{1} of Lemma 4.4. By part (a) of Lemma 4.4, we can compute the formula φ^{σ_{1}} using ≤ |φ|2^{|φ|} calls to oracle O_{0}. By Proposition 4.1 and Lemma 4.4, the formulas φ and φ^{σ_{1}} are equisatisfiable. By Theorem 4.5, we can decide if φ^{σ_{1}} is satisfiable in time O(2^{c|φ|}) for some c > 0 (since |φ^{σ_{1}}| = |φ| and the set A^{φ} of agents that appear in φ^{σ_{1}} has size at most 2^{|φ|}).

We now want to prove Theorem 3.1 in the case of M_{A} and M_{A}^{r}. The idea is the same as that of Corollary 3.7. If φ is valid, then so is φ^{σ_{1}}. We can then appeal to completeness in the case of finitely many agents to get a proof of φ^{σ_{1}} that we can then “pull back” to a proof of φ. There is only one difficulty that we encounter when trying to put this idea into practice. Exactly how do we pull back the proof? For example, suppose that the proof of φ^{σ_{1}} involves a formula ψ with an operator K_{H}. In general, there will be many agents i ∈ A such that σ_{1}(i) = H. One option is to replace K_{H} by E_{σ_{1}^{−1}(H)}, that is, replace H by all i such that σ_{1}(i) = H. (This is what was done in the proof of Corollary 3.7.) The problem with this is that there is no guarantee that the resulting set is in G. Alternatively, we could replace K_{H} by K_{i} for some i such that σ_{1}(i) = H. But if so, which one?

We actually take the latter course here. We solve the problem of which i to choose by showing that there is a proof of φ^{σ_{1}} in which the only modal operators that arise in any formula used in the proof are modal operators that appear in φ^{σ_{1}} (Lemma 4.7). For these operators, there is a canonical way to do the replacement (Lemma 4.6). While it may seem almost trivial that the only operators that should be needed in the proof of φ^{σ_{1}} are ones that already appear in the formula, this is not the case for the standard completeness proof [FHMV95, HM92], since in the proof of the validity of a formula of the form E_{G}ψ, the modal operators K_{i} are used for i ∈ G, although these operators may not appear in ψ. It is important that we use the axioms E1 and E2 in doing the proof, rather than the axiom E; otherwise the result would not hold. Indeed, the result does not quite hold in the case of T_{G}^{C}; we need to augment it with E5.

Lemma 4.6: The mapping σ_{1} (when viewed as a map with domain 2^{A}) is injective on G_{φ}.

Proof: Suppose that G ≠ G′. Without loss of generality, suppose that i ∈ G − G′. Then there is a G-maximal set H that includes G′. By Lemma 4.4(a), we have H ∈ σ_{1}(G). Since G′ ∈ H, it follows from Lemma 4.4(a) that H ∉ σ_{1}(G′). Thus, σ_{1}(G) ≠ σ_{1}(G′).

For the next lemma, we write AX ⊢_{φ} ψ if there is a proof of φ in AX that involves only modal operators that appear in φ. Let (T_{G}^{C})^{+} consist of T_{G}^{C} augmented with the axiom E5. Although E5 follows from E1 and K2, using E5 allows us to be able to write proofs of φ that use only the modal operators in φ.

Lemma 4.7: If A is finite and φ ∈ L_{G}^{C} is valid with respect to M_{A} (resp., M_{A}^{r}), then K_{G}^{C} ⊢_{φ} φ (resp., (T_{G}^{C})^{+} ⊢_{φ} φ).

Proof: We first consider the case of M_{A}. Since φ is valid, ¬φ is not satisfiable. That means, when we apply the construction in the proof of Theorem 4.5 to ¬φ, all the sets containing ¬φ are eliminated. For each state s ∈ S^{1}, let φ_{s} be the conjunction of all the formulas in s.

We prove the result by showing, by induction on j, that

if a state s ∈ S^{j} does not seem consistent, then φ_{s} is K_{G}^{C}-inconsistent, i.e., K_{G}^{C} ⊢_{φ} ¬φ_{s}. (1)

To see that (1) suffices to prove the lemma, note that standard propositional reasoning (i.e., using Prop and MP) shows that, for any formula ψ ∈ Sub(¬φ),

K_{G}^{C} ⊢_{φ} ψ ⇔ ∨_{{s∈S^{1}:ψ∈s}}φ_{s}.

(Here we need the observation that by EGen, E3, C1 and RC1, nothing is lost by our assumption that C_{G}ψ ∈ s iff E_{G}(ψ ∧ C_{G}ψ) ∈ s.) Negating both sides of ⇔, we get

K_{G}^{C} ⊢_{φ} ¬ψ ⇔ ∧_{{s∈S^{1}:ψ∈s}}¬φ_{s}.  (2)

Thus, if K_{G}^{C} ⊢_{φ} ¬φ_{s} for each set s containing ¬φ, it follows by standard propositional reasoning that K_{G}^{C} ⊢_{φ} φ, as desired.

While this general approach to proving completeness is quite standard, we must take extra care because of our insistence on restricting to symbols that appear in φ, particularly when dealing with the case when a state seems inconsistent due to a formula of the form ¬E_{G}ψ or ¬C_{G}ψ not being satisfied. This is where the axioms E1 and E2 come into play.

To prove (1), we first need a number of basic facts of epistemic logic and some preliminary observations. The basic facts (which are easily proved using Prop, E3 (or K1 when G = {i}), MP, and EGen (or KGen); see [FHMV95, p. 51, 94]) are that if ψ and ψ′ involve only modal operators in φ, then

K_{G}^{C} ⊢_{φ} E_{G}(ψ ∧ ψ′) ⇔ E_{G}ψ ∧ E_{G}ψ′  (3)

and

if K_{G}^{C} ⊢_{φ} ψ ⇒ ψ′ then K_{G}^{C} ⊢_{φ} E_{G}ψ ⇒ E_{G}ψ′.  (4)

Assume by induction that for all s ∈ S^{1} − S^{j}, we have K_{G}^{C} ⊢_{φ} ¬φ_{s}. We now show that if s ∈ S^{j} does not seem consistent then K_{G}^{C} ⊢_{φ} ¬φ_{s}, by considering in turn each of the two ways s may seem inconsistent.

First suppose that s does not seem consistent because ¬E_{G}ψ ∈ s and there is no state t ∈ S^{j} such that (s, t) ∈ ∪_{i∈G}K_{i} and ¬ψ ∈ t. We show that

K_{G}^{C} ⊢_{φ} φ_{s} ⇒ E_{G}ψ.  (5)

Since ¬E_{G}ψ is a conjunct of φ_{s} (since ¬E_{G}ψ ∈ s, by assumption), (5) shows that φ_{s} is K_{G}^{C}- inconsistent, as desired.

To prove (5), we first show that if G ∈ G_{φ}, then

if (s, t) ∉ ∪_{i∈G}K_{i}, then K_{G}^{C} ⊢_{φ} φ_{s} ⇒ E_{G}¬φ_{t}.  (6)

To prove (6), suppose that (s, t) ∉ ∪_{i∈G}K_{i}. For each i ∈ G there must be some G^{i,t} ∈ G_{φ} and formula E_{G^{i,t}}θ such that i ∈ G^{i,t}, E_{G^{i,t}}θ ∈ s and ¬θ ∈ t. Since E_{G^{i,t}}θ ∈ s and ¬θ ∈ t it is immediate that K_{G}^{C} ⊢_{φ} φ_{s} ⇒ E_{G^{i,t}}θ and K_{G}^{C} ⊢_{φ} θ ⇒ ¬φ_{t}. Now applying (4) and propositional reasoning, we get that K_{G}^{C} ⊢_{φ} φ_{s} ⇒ E_{G^{i,t}}¬φ_{t}. Since we can find such a G^{i,t} for each i ∈ G, we have that G ⊆ ∪_{i∈G}G^{i,t}. Since G is finite, by E2, we have K_{G}^{C} ⊢_{φ} φ_{s} ⇒ E_{G}¬φ_{t}, as desired.

Returning to the proof of (5), note that (since E_{G}ψ ∈ s) if ¬ψ ∈ t then (s, t) ∉ ∪_{i∈G}K_{i}. Thus, from (6) and (3), we have

K_{G}^{C} ⊢_{φ} φ_{s} ⇒ E_{G}(∧_{{t∈S^{j}:¬ψ∈t}}¬φ_{t}).  (7)

By the induction hypothesis, for all states in t ∈ S^{1} − S^{j}, we have that K_{G}^{C} ⊢_{φ} ¬φ_{t}. Thus, using (2), we have

K_{G}^{C} ⊢_{φ} ψ ⇔ ∧_{{t∈S^{j}:¬ψ∈t}}¬φ_{t}.  (8)

(5) now follows from (4), (7), and (8).

Finally, we must show that if ¬C_{G}ψ ∈ s and there is no state t ∈ S^{j} G-reachable from s in S^{j} such that ¬ψ ∈ t, then K_{G}^{C} ⊢_{φ} φ_{s} ⇒ C_{G}ψ, again showing that φ_{s} is K_{G}^{C}-inconsistent. This follows by a relatively straightforward modification of the completeness proof given in [FHMV95, HM92], so we just sketch the details here. Let T_{1} = {t ∈ S^{j} : ¬C_{G}ψ ∈ t and there is no state t′ ∈ S^{j} G-reachable from t in S^{j} such that ¬ψ ∈ t′} and T_{2} = {t ∈ S^{j} : C_{G}ψ ∈ t}. Let T′_{i} consist of those states in T_{i} that also contain ψ, i = 1, 2. Let T = T_{1}∪T_{2} and let T′ = T′_{1}∪T′_{2}. We claim that there is no pair (t, t′) ∈ ∪_{i∈G}K_{i} such that t ∈ T and t′ ∈ S^{j} − T′. It is immediate that if t ∈ T_{2} then (since ψ ∧ C_{G}ψ ∈ t/E_{G} ⊆ t′) t′ ∈ T′_{2}. If t ∈ T_{1} and t′ ∈ S^{j} − T′, then either ¬ψ ∈ t′ or ¬C_{G}ψ ∈ t′ and there is a state t′′ G-reachable from t′ in S^{j} such that ¬ψ ∈ t′′. This means that either t′ or t′′ is a state G-reachable from t in S^{j} containing ¬ψ. This contradicts the fact that t ∈ T_{1}.

It now follows from (6) that for all t ∈ T and t′ ∈ S^{j} − T′, we have

K_{G}^{C} ⊢_{φ} φ_{t} ⇒ E_{G}¬φ_{t′}.  (9)

Let φ_{T} = ∨_{t∈T} φ_{t} and let φ_{T′} = ∨_{t′∈T′}φ_{t′}. By propositional reasoning, we have K_{G}^{C} ⊢_{φ} φ_{T′} ⇔ (φ_{T} ∧ ψ). It easily follows from (3), (4), and (9) that K_{G}^{C} ⊢_{φ} φ_{t} ⇒ E_{G}φ_{T′}. Since this is true for all t ∈ T, we have

K_{G}^{C} ⊢_{φ} φ_{T} ⇒ E_{G}(φ_{T} ∧ ψ).  (10)

By applying RC1 and the fact that s ∈ T, we have K_{G}^{C} ⊢_{φ} φ_{s} ⇒ C_{G}ψ. Since ¬C_{G}ψ ∈ s, it follows that φ_{s} is K_{G}^{C}-inconsistent.

This completes the completeness proof in the case of M_{A}. To deal with M_{A}^{r}, we must just show that if s is eliminated because (s, s) ∉ K_{i} for some i ∈ A, then T_{G}^{C} ⊢_{φ} ¬φ_{s}; all other cases are identical. But if (s, s) ∉ K_{i}, then there must be some G and ψ such that i ∈ G, E_{G}ψ ∈ s, and ¬ψ ∈ s. Since (T_{G}^{C})^{+} includes the axiom E_{G}ψ ⇒ ψ, we have that (T_{G}^{C})^{+} ⊢_{φ} ¬φ_{s}, as desired.

Proof of Theorem 3.1 for M_{A} and M_{A}^{r}: We have already observed that the axioms are sound. For completeness, suppose that φ is valid with respect to M_{A}. By Proposition 4.1, so is φ^{σ_{1}}. By Lemma 4.7, there is a proof of φ^{σ_{1}} in K_{G_{φ}}^{C} that mentions only the modal operators in φ^{σ_{1}}. Given a formula ψ in which the only modal operators that appear are modal operators that appear in φ^{σ_{1}} (and thus have the form E_{σ_{1}(G)}, C_{σ_{1}(G)}, and K_{σ_{1}(i)}, for sets G and {i} in G_{φ}) let ψ^{τ_{1}} be the unique formula all of whose modal operators appear in φ such that (ψ^{τ_{1}})^{σ_{1}} = ψ. Lemma 4.6 assures us that ψ^{τ_{1}} is well defined. We can pull the proof of φ^{σ_{1}} back to a proof of φ, by replacing each occurrence of a formula ψ in the proof by ψ^{τ_{1}}.

The argument for M_{A}^{r} is identical, except that the proof uses instances of the axiom E5. These can be eliminated by using E1 and K2, as we observed earlier (although now the proof of φ may use modal operators K_{i} that do not appear in φ).

4.2 Dealing with M_{A}^{rt}

Proposition 4.1 as it stands does not hold for M_{A}^{rt}. There is no guarantee that the translated formula is satisfiable in M_{A}^{rt}, even if φ is. Indeed, suppose that G ∪ {∅} is closed under intersection and complementation, so that we can use the function σ of Proposition 3.5. Suppose that φ is the formula E_{G}p ∧ ¬E_{G}E_{G}p, where |G| ≥ 2. The formula φ^{σ} looks syntactically identical, except that σ(G) is a single agent in A′. We cannot make the K_{G} relation transitive and still satisfy φ^{σ}. More generally, to deal with M_{A}^{rt}, we must be careful in how we deal with singleton sets.

As a first step, we define mixed structures. Since we also need these to deal with M_{A}^{rst} and M_{A}^{elt}, we define three types of mixed structures at once. We say that a binary relation K is secondarily reflexive [Che80] if (s, t) ∈ K implies (t, t) ∈ K. Let M_{A_{1}+A_{2}}^{rt} (resp., M_{A_{1}+A_{2}}^{rst}; M_{A_{1}+A_{2}}^{elt}) consist of structures M = (S, π, {K_{i} : i ∈ A_{1} ∪ A_{2}}) where the relations K_{i} for i ∈ A_{1} are reflexive and transitive (resp., reflexive, symmetric and transitive; Euclidean, serial and transitive) and the relation K_{i} for i ∈ A_{2} are reflexive (resp., reflexive and symmetric; serial and secondarily reflexive). See Table 2.

Mixed Structures K_{i} for i ∈ A_{1}  K_{i} for i ∈ A_{2}
M_{A_{1}+A_{2}}^{rt} reflexive, transitive reflexive
M_{A_{1}+A_{2}}^{rst}  reflexive, symmetric, transitive reflexive, symmetric
M_{A_{1}+A_{2}}^{elt}  Euclidean, serial, transitive  serial, secondarily reflexive

Table 2: Mixed Structures

We can now define our translation in the case of M_{A}^{rt}. Although we can in fact get an analogue to Proposition 4.1 for M_{A}^{rt}, it turns out to be easier to provide a translation that combines Proposition 4.1 and Lemma 4.4, rather than separating them. As suggested by Proposition 3.3, the translation involves R(G_{φ}^{1}), rather than R(G_{φ}). Given a formula φ, let A^{φ,rt} = {H : ∃G[(G, H) ∈ R(G_{φ}^{1})]}. Let A_{1} = {H : ∃G[(G, H) ∈ R(G_{φ}^{1}), |G − ∪H| = 1]}; let A_{2} = A^{φ,rt} − A_{1}. Define σ_{2} : A → A^{φ,rt} as before: σ_{2}(i) = H if i ∈ A_{H} and σ_{2}(i) is undefined otherwise. Given H ∈ A^{φ,rt}, we define τ_{2}(H) = ∩(G_{φ}^{1} − H). Since it is easy to see that R(G_{φ}^{1}) = R(G_{ψ}) for some appropriate ψ, it is immediate that Lemma 4.4 applies to σ_{2} and τ_{2} with A^{φ,rt} in place of A^{φ} and G_{φ}^{1} in place of G_{φ}.

Proposition 4.8: φ is satisfiable in M_{A}^{rt} iff φ^{σ_{2}} is satisfiable in M_{A_{1}+A_{2}}^{rt}.

Proof: First suppose that (M, s) ⊧ φ, where M ∈ M_{A}^{rt}. We convert M = (S, π, {K_{i} : i ∈ A}) into a structure M′ = (S, π, {K_{H} : H ∈ A^{φ,rt}}) as before, by defining K_{H} = ∪{K_{i} : i ∈ τ_{2}(H)}. Since Lemma 4.4 applies, the proof that (M′, s) ⊧ φ is identical to that in Proposition 4.1. We must only show that M′ ∈ M_{A_{1}+A_{2}}^{rt}. Since the union of reflexive relations is reflexive, it is immediate that K_{H} is reflexive for H ∈ A_{2}. If H ∈ A_{1}, then |A_{H}| = 1. Suppose that A_{H} = {i}. We claim that τ_{2}(H) = {i}. By construction, {i} ∈ G_{φ}^{1}. We cannot have {i} ∈ H, since i ∉ ∪H. Thus {i} ∈ G_{φ}^{1} − H, so τ_{2}(H) = ∩(G_{φ}^{1} − H) ⊆ {i}. Since τ_{2}(H) ≠ ∅ by Lemma 4.4(c), we must have τ_{2}(H) = {i}. Thus, K_{H} = K_{i}, so K_{H} is reflexive and transitive.

For the opposite direction we need to work a little harder than before, because we must ensure that all the K_{i} relations are reflexive and transitive for all i ∈ A. Suppose (M, s) ⊧ φ^{σ_{2}} for some M = (S, π, {K_{H} : H ∈ A^{φ,rt}}) ∈ M_{A_{1}+A_{2}}^{rt}. Let S_{0} and S_{1} be two disjoint copies of S. For a state s ∈ S, let s_{i} be the copy of s in S_{i}, i = 0, 1. Let M′ = (S′, π′, {K_{i} : i ∈ A}) be defined as follows:

• S′ = S_{0} ∪ S_{1}.

• π′(s_{i}) = π(s) for i = 0, 1.

• If σ_{2}(i) ∈ A_{1}, define K_{i} = {(s_{i}, t_{j}) : (s, t) ∈ K_{σ_{2}(i)}, i, j ∈ {0, 1}}. K_{i} is clearly reflexive and transitive in this case, since K_{σ_{2}(i)} is.

• If σ_{2}(i) = H ∈ A_{2}, note that |A_{H}| ≥ 2. It is immediate from the definition that σ_{2}(i) = H for all i ∈ A_{H}. Pick some i_{H} ∈ A_{H}. If i = i_{H}, then define K_{i} = {(s_{0}, t_{1}) : (s, t) ∈ K_{H}} ∪ {(s_{j}, s_{j}) : j ∈ {0, 1}}; if i ≠ i_{H}, define K_{i} = {(s_{1}, t_{0}) : (s, t) ∈ K_{H}} ∪ {(s_{j}, s_{j}) : j ∈ {0, 1}}. Clearly K_{i} is reflexive and transitive.

This construction guarantees that

(s, t) ∈ K_{H} iff (s_{0}, t_{1}), (s_{1}, t_{0}) ∈ ∪_{{i:σ_{2}(i)=H}}K_{i}  (11)

and

(s_{1}, t_{0}) ∈ ∪_{{i:σ_{2}(i)=H}}K_{i} iff (s_{0}, t_{1}) ∈ ∪_{{i:σ_{2}(i)=H}}K_{i}.  (12)

A straightforward argument by induction on structure now shows that if ψ ∈ L_{G_{φ}^{1}}^{C}, then the following are equivalent for all t ∈ S:

• (M, t) ⊧ ψ^{σ_{2}},

• both (M′, t_{0}) ⊧ ψ and (M′, t_{1}) ⊧ ψ,

• (M′, t_{0}) ⊧ ψ or (M′, t_{1}) ⊧ ψ.

Of course, the interesting cases are if ψ is of the form K_{i}ψ′, E_{G}ψ′, or C_{G}ψ′. These follow immediately from observations (11) and (12).

The next step is to get an analogue of Theorem 4.5 for M_{A_{1}+A_{2}}^{rt}. The basic idea of the proof is the same as that of Theorem 4.5. However, in our construction, we need to make the K_{i} relations transitive. To see the difficulty, suppose that φ is K_{1}p ∧ E_{G}q, where G is a set of agents containing 1. Recall that in Theorem 4.5, states are consistent subsets of Sub^{+}(φ). Let s, t, and u be states such that s = {K_{1}p, E_{G}q, p, q}, t = {K_{1}p, ¬E_{G}q, p, q}, and u = {K_{1}p, ¬E_{G}q, p, ¬q}. With our previous construction, we would have both (s, t) ∈ K_{1} and (t, u) ∈ K_{1}. By transitivity, we should also have (s, u) ∈ K_{1}. But since E_{G}q ∈ s and ¬q ∈ u, we have (s, u) ∉ K_{1}. Nevertheless, each of s, t, and u individually seems consistent. Which state should we eliminate in order to preserve transitivity?

To deal with this problem, we need to put more information (i.e., more formulas) into each state. Intuitively, if (s, t) ∈ K_{i}, then we should have K_{i}q ∈ t, because if E_{G}q ∈ s, then K_{i}q should also be in s, as should K_{i}K_{i}q by K4. It would then follow that K_{i}q should be in t. This, in turn, would guarantee that (t, u) ∉ K_{i}, since q ∉ u.

What we would like to do now is to augment Sub(φ) by including all formulas K_{i}ψ such that E_{G}ψ ∈ Sub(φ) and i ∈ G ∩ A_{1}. (We restrict to A_{1} since these are the only relations that are required to be transitive.) While this approach can be used to force the K_{i} relations to be transitive, the resulting set of formulas can have size O(|A_{1}||φ|), which means the resulting state space (the analogue of S^{1}) could then have size 2^{|A_{1}||φ|}. This would not give us the desired complexity bounds. Thus, we must proceed a little more cautiously.

Theorem 4.9: If A = A_{1} ∪ A_{2} is finite and there is an algorithm for deciding if i ∈ G for G ∈ G that runs in time linear in |A|, then there is a constant c > 0 (independent of A) and an algorithm that, given a formula φ of L_{G}^{C}, decides if φ is satisfiable in M_{A_{1}+A_{2}}^{rt} and runs in time O(|A|2^{c|φ|}).

Proof: We assume for ease of exposition that A_{1} ≠ ∅; we leave the straightforward modification in case A_{1} = ∅ to the reader. For each i ∈ A_{1}, let ESub_{i}(φ) be the smallest set containing Sub(φ) such that if E_{G}ψ ∈ Sub(φ) and i ∈ G, then K_{i}ψ ∈ ESub_{i}(φ). It is easy to see that |ESub_{i}(φ)| ≤ 2|Sub(φ)|, since we add at most one formula for each formula in |Sub(φ)|. Let S_{i}^{1} consist of all the subsets of ESub_{i}^{+}(φ) that are maximally consistent, and now let S^{1} = ∪_{i∈A_{1}}S_{i}^{1}. Note that, as modified, |S^{1}| ≤ 2^{2|φ|}. Thus, this modification keeps us safely within the desired exponential time bounds.

We keep the definition of K_{i} unchanged for i ∈ A_{2} (i.e., (s, t) ∈ K_{i} iff s/\overline{K}_{i} ⊆ t), but we need to modify it for i ∈ A_{1}. We redefine K_{i} for i ∈ A_{1} by defining (s, t) ∈ K_{i} iff s/\overline{K_{i}} ∪ \{K_{i}ψ : K_{i}ψ ∈ s\} ⊆ t ∩ (t/\overline{K_{i}} ∪ \{K_{i}ψ : K_{i}ψ ∈ t\}). It is easy to check that this modification forces the K_{i} relations to be transitive. We force all the K_{i} relations to be reflexive just as with M_{A}^{r}, by eliminating s ∈ S^{1} if (s, s) ∉ K_{i} for some i ∈ A_{1} ∪ A_{2}. The remainder of the construction— eliminating the states that do not seem consistent—is unchanged.

We now need to show that the algorithm is correct. First suppose that φ is satisfiable in M_{A_{1}+A_{2}}^{rt}. In that case, (M, s_{0}) ⊧ φ for some structure M = (S, π, {K′_{i} : i ∈ A_{1} ∪ A_{2}}) ∈ M_{A_{1}+A_{2}}^{rt}. We can associate with each state s ∈ S and i ∈ A_{1} the state s_{i}^{∗} in S_{i}^{1} consisting of all the formulas ψ ∈ ESub_{i}(φ) such that (M, s) ⊧ ψ. It is easy to see that if (s, t) ∈ K′_{i} then (s_{j}^{∗}, t_{i}^{∗}) ∈ K_{i} for all j.^{3} Using this observation, a straightforward induction shows that the states s_{i}^{∗} for s ∈ S always seem consistent, and thus are in S^{j} for all j and all i ∈ A_{1}. Moreover, φ ∈ (s_{0})_{i}^{∗} for all i ∈ A_{1}. Thus, the algorithm will declare that φ is satisfiable, as desired.

Conversely, suppose that the algorithm declares that φ is satisfiable. We construct a structure M = (S, π, {K′_{i} : i ∈ A_{1} ∪ A_{2}}) ∈ M_{A_{1}+A_{2}}^{rt} in which φ is satisfied just as Theorem 4.5. Our modified construction guarantees that the K′_{i} relations are all reflexive and the ones in A_{1} are transitive.

We are almost ready to prove Theorem 3.4 for M_{A}^{rt}. However, we first we need to characterize the complexity of translating from φ to φ^{σ_{2}}. In particular, we need a bound on the number of elements in R(G_{φ}^{1}) and the number of oracle calls required to compute them. To do this, we first define two auxiliary sequences of sets D_{i}^{m}(J) and E_{i}^{m}(J), i = 1, 2, 3, . . .. (We omit the parenthetical J when it is clear from context.) Fix m. Let D_{0}^{m} = J and D_{i+1}^{m} = J ∪ {G − ∪H : (G, H) ∈ R(D_{i}^{m}) and |G − ∪H| ≤ m}; let E_{i}^{m} = D_{i}^{m} − D_{0}^{m}. Set D^{m} = ∪_{i}D_{i}^{m} and E^{m} = ∪_{i}E_{i}^{m}. Finally, denote R(D^{m}) by R^{m}(J). It is easy to check, using Lemma 4.3, that D_{0}^{m} ⊆ D_{1}^{m} ⊆ … and that R^{m}(J) = ∪_{i}R(D_{i}^{m}).

For example, if A = {1, 2, 3, …} and J = {{2n, …, 3n} : n = 1, 2, 3, …}, then it is not hard to show that D_{1}^{1} = J ∪ {{6n + 1} : n = 1, 2, 3} (since {6n + 1} = {6n, 9n} − ∪{{4n, 6n}, {6n + 2, 9n + 3}}, and D_{k}^{1} = D_{1}^{1} ∪ {{6n} : n = 1, 2, 3, …}. Similarly, D_{1}^{2} = D_{1}^{1} ∪ {{2n, 2n + 1} : n is not a multiple of 3}, and D_{k}^{2} = D_{2}^{1} ∪ {{2n, 2n + 1} : n is not a multiple of 3}, for k ≥ 1. Finally, D_{k}^{m} = D_{k}^{2} for m ≥ 2. E_{1}^{m} = {{n} : n > 1} = E^{m}.

The next lemma provides partial motivation for these definitions.

Lemma 4.10: R^{m}(J) = R(J^{m}).

3Note that it is not necessarily the case that (s_{j}^{∗}, t_{j′}^{∗}) ∈ K_{i} for j′ ≠ i. For example, suppose φ is the formula E_{G}p, i ∈ G ∩ A_{1}, and M is such that (M, s) ⊧ E_{G}p ∧ p, (M, t) ⊧ ¬E_{G}p ∧ p, and (s, t) ∈ K_{i}. Then for i ≠ j, j′ and j ∉ G, we have s_{j}^{∗} = \{E_{G}p, p\} and t_{j′}^{∗} = \{p, ¬E_{G}p\}. Since p ∈ s_{j}^{∗}/\overline{K_{i}} − t_{j′}^{∗}/\overline{K_{i}}, we have that (s_{j}^{∗}, t_{j′}^{∗}) ∉ K_{i}.

Proof: An easy induction on i shows that D_{i}^{m}(J) ⊆ J_{i}^{m} (as defined in Definition 3.2) for all i, so D^{m} ⊆ J^{m}. We next show that every set in J_{i}^{m} is the union of sets in D^{m}, by induction on i. This is immediate if i = 0, since J_{0}^{m} = D_{0}^{m} = J. Suppose that the result holds for J_{i}^{m}; we show it for J_{i+1}^{m}. Suppose that H ∈ J_{i+1}^{m}. If H ∈ J, then clearly H ∈ D^{m}. Thus, without loss of generality, H ∈ J_{i+1}^{m} − J, which means that |H| ≤ m. Let H′ be the union of all sets in D^{m} contained in H. If H′ = H, then we are done. Suppose by way of contradiction that H − H′ ≠ ∅. We obtain a contradiction to the choice of H′ by showing that H − H′ contains a set in D^{m}.

Since H′ is finite, it can be written as a finite union of sets in D^{m}, say of H_{1} = H_{1}, …, H_{k}. Since H ∈ J_{i+1}^{m}−J, H = G−∪H_{2} for some G ∈ J and H_{2} ⊆ J_{i}^{m}. By the induction hypothesis, there exists some H_{3} ⊆ D^{m} such that ∪H_{2} = ∪H_{3}. There must exist some set H_{4} ⊇ H_{1} ∪ H_{3} such that (G, H_{4}) ∈ R(D^{m}). But then H − H′ ⊇ G − ∪H_{4} ∈ D^{m}, and we obtain the desired contradiction.

It now easily follows that R(J^{m}) = R(D^{m}) = R^{m}(J).

The following result will be used to help compute the elements of R^{m}(J). Recall that J^{∗} is the algebra generated by J.

Lemma 4.11: Let J be a set of subsets of A with |J | = n.

(a) If (G, H) ∈ R(D), where J ⊆ D ⊆ J^{∗}, then G − ∪H is an atom over J.

(b) J ⊆ D_{i}^{m} ⊆ J^{∗} for all i, m.

(c) |{H : ∃G ∈ D^{m}((G, H) ∈ R^{m}(J)}| ≤ 2^{n}.

(d) If (G, H) ∈ R(D_{i}^{m}), then either G ∈ J and E_{i}^{m} ⊆ H or A_{H} ∈ E_{i}^{m} and E_{i}^{m} − {A_{H}} ⊆ H. Moreover, if (G, H) ∈ R^{m}(J), then either G ∈ J and E^{m} ⊆ H or (G − ∪H) ∈ E^{m} and E^{m} − {G − ∪H} ⊆ H.

(e) D^{m} = D_{n}^{m} and E^{m} = E_{n}^{m}.

Proof: For part (a), we know from Lemma 4.3(a) that if (G, H) ∈ R(D), then G − ∪H is an atom over D. Since J ⊆ D ⊆ J^{∗}, it is immediate that it must in fact be an atom over J as well.

Part (b) follows immediately from (a), since an easy induction on i shows that E_{i}^{m} ⊆ J^{∗}. For part (c), by Lemma 4.3(a), it follows that A_{H} is an atom over D^{m}. But since J ⊆

D^{m} = ∪_{i}D_{i}^{m} ⊆ J^{∗} by part (b), it follows that A_{H} is actually at atom over J. Moreover if (G′, H′) ∈ R^{m}(J) and H ≠ H′, then it follows from Lemma 4.3(c) that A_{H} ≠ A_{H′}. Since there are at most 2^{n} atoms over J, part (c) follows.

For part (d), if (G, H) ∈ R(D_{i}^{m}) then, by Lemma 4.3(a), A_{H} = G − ∪H is an atom over D_{i}^{m} and has the form ∩(D_{i}^{m} − H) ∩ ∩\{\overline{H} : H ∈ H\}. By the arguments of part (c), A_{H} is also an atom over J. We say that the sets in D_{i}^{m} − H appear positively in A_{H} and the sets in H appear negatively in A_{H}. If one of the sets G′ ∈ E_{i}^{m} appears positively in A_{H} then clearly A_{H} ⊆ G′. But since the elements of E_{i}^{m} are also atoms over J, it follows that in this case A_{H} = G′ ∈ E_{i}^{m} and, since H is G-maximal, E_{i}^{m} − {A_{H}} ⊆ H. Otherwise, E_{i}^{m} ⊆ H as required; moreover, since D_{i}^{m} = E_{i}^{m} ∪ J and G ∉ H, we must have G ∈ J. The argument for the second half of (d) is identical.

Clearly the two claims in part (e) are equivalent. We prove the second. As observed in the proof of (c), every set in E^{m} is an atom A over J. It is easy to see that there are no atoms in E^{m} where all n sets in J appear negatively, since every set in E^{m} is a nonempty subset of some G ∈ J. (This can be proved by induction on i for each E_{i}^{m}.) We prove by induction on i that if A ∈ E^{m} and n − i sets appear negatively in A for i ≥ 1, then A ∈ E_{i}^{m}.

Clearly if i = 1, then A = G − (H_{1} ∪ … ∪ H_{n−1}) and H = {H_{1}, …, H_{n−1}} is a G-maximal subset of J. Thus, (G, H) ∈ D_{1}^{m} and A ∈ E_{1}^{m}. Suppose that the result is true if i = k and suppose that n − (k + 1) sets appear negatively in A. Since A ∈ E^{m}, there must be some minimal j such that A ∈ E_{j+1}^{m}. By definition, A = A_{H} for some (G, H) ∈ R(D_{j}^{m}). By (d), either A = G − (∪H′ ∪ E_{j}^{m}) and H′ ⊆ J or A ∈ E_{j}^{m}. The latter case contradicts our choice of j, so we may assume that A = G − (∪H′ ∪ E_{j}^{m}) and H′ ⊆ J. It is easy to see that H′ must consist of precisely the sets in J that appear negatively in A. (If H′ did not include all the sets that appear negatively in A then H′ ∪ E_{j}^{m} would not be a G-maximal subset of J ∪ E_{j}^{m}; if H′ included any sets that appear positively in A, then A would be empty.) Let E′ consist of all the atoms A′ in E_{j}^{m} in which the set of sets in J that appear negatively in A′ is a strict superset of H′. It is easy to see that G − (∪H′ ∪ E_{j}^{m}) = G − (∪H′ ∪ E′), since all the sets in E_{j}^{m} − E′ must be disjoint from G − ∪H′. (This is clear for the B ∈ E_{j}^{m} − E′ for which some set appearing negatively in A does not appear negatively in B. On the other hand, if the same sets appear negatively in B as in A, then B = A and we contradict the minimality of j.) By the induction hypothesis, E′ ⊆ E_{n−k}^{m}. Now consider A′ = G − (∪H′ ∪ E_{n−k}^{m}) ∈ E_{n−k+1}^{m}. Since E′ ⊆ E_{n−k}^{m}, it follows that A′ ⊆ A. Moreover, A′ = A_{H′′} for some H′′ such that (G, H′′) ∈ R(D_{n−k}^{m}), since any relevant extension of H′ that would keep the difference with G nonempty would be one for A as well, contradicting the assumption that A ∈ E_{j+1}^{m}. Thus, A′ is an atom over J. As we observed earlier, A is also an atom over J. Thus, A = A′ ∈ E_{n−k+1}^{m}, as desired.

We remark that a simpler proof, just using the fact that there are at most 2^{n} atoms over J, can be used to show that E_{n′}^{m} = E_{2^{n}}^{m} for n′ > 2^{n}. This simpler proof would suffice for the purposes of this subsection. However, we use the added information in part (e) in Section 4.5.

Proof of Theorem 3.4 for M_{A}^{rt}: Again, the lower bound follows from standard results in [HM92].

For the upper bound, suppose that we are given a formula φ such that n = |φ| and H ∈ A^{φ,rt}. By definition, there exists a G such that (G, H) ∈ R(G_{φ}^{1}). By Lemma 4.10, R^{1}(G_{φ}) = R(G_{φ}^{1}). Thus, H ⊆ D^{1}(G_{φ}) = G_{φ} ∪ E_{n}^{1}(G_{φ}). By Lemma 4.11(d), either E_{n}^{1}(G_{φ}) ⊆ H or H contains all but one element of E_{n}^{1}(G_{φ}). Thus, we can uniquely characterize H by a pair (H′, X), where H′ = H ∩ G_{φ} and X = E_{n}^{1}(G_{φ}) − H (so that X is either the empty set or a singleton). It should be clear that we can compute the set E_{n}^{1}(G_{φ}) in time O(n^{2}2^{cn}) and which of these (at most 2^{2n} + 2^{n}) pairs is in A_{1} and A_{2} using at most 2n(2^{2n} + 2^{n}) calls to the oracle O_{1}.

By Lemmas 4.4(a) and 4.11, we can similarly compute the formula φ^{σ_{2}} in time O(2^{cn}) using O(2^{cn}) oracle calls. We now apply Proposition 4.8 and Theorem 4.9, just as we applied Proposition 4.1 and Theorem 4.5 in the case of M_{A}.

We next want to prove Theorem 3.1 for M_{A}^{rt}. Just as with M_{A} and M_{A}^{r}, we want to pull a proof of φ^{σ_{2}} back to a proof of σ. However, it is no longer true that we can necessarily prove φ^{σ_{2}} using only the modal operators that appear in φ^{σ_{2}}. We may also need to use K_{H} for H ∈ A_{1}. Fortunately, this does not cause us problems. The following extension of Lemma 4.6 is immediate.

Lemma 4.12: The mapping σ_{2} (when viewed as a map with domain 2^{A}) is injective on G_{φ}^{1}.

Let (S4_{G}^{C})^{A_{1}+A_{2}} consist of the axioms in (T_{G}^{C})^{+} (so that, in particular, E5 is included), together with every instance of K4 (K_{i}φ ⇒ K_{i}K_{i}φ) for i ∈ A_{1}. We write (S4_{G}^{C})^{A_{1}+A_{2}} ⊢_{φ} ψ if there is a proof of ψ in (S4_{G}^{C})^{A_{1}+A_{2}} using only the modal operators that appear in φ and K_{i} for i ∈ A_{1}.

Lemma 4.13: If A is finite and φ ∈ L_{G}^{C} is valid with respect to M_{A_{1}+A_{2}}^{rt}, then (S4_{G}^{C})^{A_{1}+A_{2}} ⊢_{φ} φ.

Proof: The proof is similar to that of Lemma 4.7 for M_{A}^{r}, except that since the definition of the K_{i} relation is different, we must check that the results still hold with the modified definition.

Suppose that s ∈ S^{j} does not seem consistent because ¬E_{G}ψ ∈ s and there is no state t ∈ S^{j} such that (s, t) ∈ ∪_{i∈G}K_{i} and ¬ψ ∈ t. We want to show that (S4_{G}^{C})^{A_{1}+A_{2}} ⊢_{φ} φ_{s} ⇒ E_{G}ψ. As before this suffices.

For each i ∈ G and, by induction, each j, we have a provable equivalence for ψ similar to the one before: (S4_{G}^{C})^{A_{1}+A_{2}} ⊢_{φ} ψ ⇔ ∧_{{t∈S_{i}^{j}:¬ψ∈t}}¬φ_{t}. So it suffices to find, for each such i and each t ∈ S_{i}^{j} with ¬ψ ∈ t, a G^{i,t} containing i such that (S4_{G}^{C})^{A_{1}+A_{2}} ⊢_{φ} φ_{s} ⇒ E_{G^{i,t}}¬φ_{t}. For i ∈ A_{2}, this follows just as before. For i ∈ A_{1}, we show that (S4_{G}^{C})^{A_{1}+A_{2}} ⊢_{φ} φ_{s} ⇒ K_{i}¬φ_{t}. By our assumption (s, t) ∉ K_{i}. Thus, there exists some formula θ ∈ s/\overline{K_{i}} ∪ \{K_{i}δ : K_{i}δ ∈ s\}−(t∩(t/\overline{K_{i}} ∪\{K_{i}δ : K_{i}δ ∈ t\})). If θ ∈ s/\overline{K_{i}}, then (S4_{G}^{C})^{A_{1}+A_{2}} ⊢_{φ} φ_{s} ⇒ K_{i}θ. If θ = K_{i}θ′ is in s, then (S4_{G}^{C})^{A_{1}+A_{2}} ⊢_{φ} φ_{s} ⇒ K_{i}θ′. By K4, we have that (S4_{G}^{C})^{A_{1}+A_{2}} ⊢_{φ} φ_{s} ⇒ K_{i}K_{i}θ′. Thus, in either case, we have (S4_{G}^{C})^{A_{1}+A_{2}} ⊢_{φ} φ_{s} ⇒ K_{i}θ. Since θ ∈ s/\overline{K_{i}} ∪\{K_{i}δ : K_{i}δ ∈ s\}, it follows that K_{i}θ ∈ ESub_{i}(¬φ). We cannot have K_{i}θ ∈ t, for then (since (t, t) ∈ K_{i}, so t/\overline{K_{i}} ⊆ t) we would have θ ∈ t ∩ t/\overline{K_{i}}, contradicting our choice of θ. Thus we must have that ¬K_{i}θ ∈ t. It follows that (S4_{G}^{C})^{A_{1}+A_{2}} ⊢_{φ} K_{i}θ ⇒ ¬φ_{t}. Using (4), we get that (S4_{G}^{C})^{A_{1}+A_{2}} ⊢_{φ} K_{i}K_{i}θ ⇒ K_{i}¬φ_{t}. Since (S4_{G}^{C})^{A_{1}+A_{2}} ⊢_{φ} K_{i}θ ⇒ K_{i}K_{i}θ and, as shown earlier, (S4_{G}^{C})^{A_{1}+A_{2}} ⊢_{φ} φ_{s} ⇒ K_{i}θ, it follows that (S4_{G}^{C})^{A_{1}+A_{2}} ⊢_{φ} φ_{s} ⇒ K_{i}¬φ_{t}, as desired.

Finally, we must show that if ¬C_{G}ψ ∈ s and there is no state t ∈ S^{j} G-reachable from s in S^{j} such that ¬ψ ∈ t, then S4_{G}^{C} ⊢_{φ} φ_{s} ⇒ C_{G}ψ. This argument is identical to that given in the proof of Lemma 4.7, so we do not repeat it here.

Proof of Theorem 3.1 for M_{A}^{rt}: Again, we have already observed that the axioms are sound. For completeness, suppose that φ is valid with respect to M_{A}. By Proposition 4.8, φ^{σ_{2}} is valid with respect to M_{A_{1}+A_{2}}^{rt}. By Lemma 4.13, there is a proof of φ^{σ_{2}} in K_{G_{φ}}^{C} that mentions only the modal operators in φ^{σ_{2}} and the operators K_{H} for H ∈ A_{1}. Using Lemma 4.12, it follows that we can pull this back to a proof of φ in S4_{G}^{C}.

4.3 Dealing with M_{A}^{rst}

M_{A}^{rst} and M_{A}^{elt} introduce additional complications. The translation used in Proposition 4.8 no longer suffices. We need to deal with the fact that in M_{A}^{rst}, we can test not only that whether a set is a singleton, but whether it has size k for any k. Given a formula φ, suppose that |φ| = n. We want to map A to a finite set of agents and prove an analogue of Propositions 4.8. The obvious analogue of A^{φ,rt} would be to consider the sets H such that (G, H) ∈ R(G_{φ}^{n}). We essentially do this, except that we replace all sets of cardinality ≤ n by the singletons in them.

Given a set J of subsets of A, let J̃^{m} = D^{m}(J) ∪ {{i} : ∃G ∈ D^{m}(J)(|G| ≤ m, i ∈ G)}. Let A^{φ,rst} = {H : ∃G((G, H) ∈ R(G̃_{φ}^{n}))}. Let A_{1} = {H : ∃G[(G, H) ∈ R(G̃_{φ}^{n}), |G − ∪H| = 1]}; let A_{2} = A^{φ,rst} − A_{1}. Define σ_{3} : A → A_{1} ∪ A_{2} as before: σ_{3}(i) = H if i ∈ A_{H} and σ_{3}(i) is undefined otherwise. Much as before, we define τ_{3}(H) = ∩(G̃_{φ}^{n} − H). Since it is easy to see that R(G̃_{φ}^{n}) = R(G_{ψ}) for some appropriately chosen ψ, it is immediate that Lemma 4.4 applies without change to σ_{3} and τ_{3}.

Lemma 4.14: If H ∈ A_{2}, then |A_{H}| ≥ n + 1.

Proof: Suppose, by way of contradiction, that H ∈ A_{2} and 1 ≤ |A_{H}| ≤ n. We must have |A_{H}| > 1, for otherwise H ∈ A_{1}. Since A_{2} ⊆ A^{φ,rst}, there must exist G ∈ D^{n}(G_{φ}) such that H is G-maximal. But if |A_{H}| ≤ n, then every singleton subset of A_{H} is in G̃_{φ}^{n}. This contradicts the fact that H is G-maximal, because if H′ is H together with one of these singleton subsets, we must have G − ∪H′ ≠ ∅.

We have defined A_{1} and A_{2} just above. Recall that M ∈ M_{A_{1}+A_{2}}^{rst} if the relations K_{i} for i ∈ A_{1} are reflexive, symmetric, and transitive while the ones in A_{2} are reflexive and symmetric.

Proposition 4.15: φ is satisfiable in M_{A}^{rst} iff φ^{σ_{3}} is satisfiable in M_{A_{1}+A_{2}}^{rst}.

Proof: First suppose that (M, s) ⊧ φ, where M ∈ M_{A}^{rst}. We convert M = (S, π, {K_{i} : i ∈ A}) into a structure M′ = (S, π, {K_{H} : H ∈ A^{φ,rst}}) as before, by defining K_{H} = ∪{K_{i} : i ∈ τ_{3}(A)}. As the union of symmetric relations is symmetric, the proof that this works is essentially identical to that in Lemma 4.8 for the case of M_{A}^{rt}.

For the opposite direction, suppose that (M, s) ⊧ φ^{σ_{3}} for some M = (S, π, {K_{H} : H ∈ A^{φ,rst}}) ∈ M_{A_{1}+A_{2}}^{rst}. We must construct a structure M′ ∈ M_{A}^{rst} that satisfies φ. The state space for the structure M′ will again consist of copies of S, but two copies no longer suffice to guarantee that the K_{i} relations are equivalence relations. In fact, we use countably many copies.

By Lemma 4.14, for each H ∈ A_{2}, there exist at least n+1 agents in A_{H}. Choose n+1 such agents, and call them i_{H}^{0}, …, i_{H}^{n}. Partition A_{H} into n + 1 disjoint sets G_{H,j} with i_{H}^{j} ∈ G_{H,j}. We build copies of M in a tree-like manner. We index the copies of M with strings of the form ((s_{1}, t_{1}), i_{1}, …, (s_{k}, t_{k}), i_{k}), such that s_{j}, t_{j} ∈ S, i_{j} is i_{H}^{j′} for some H ∈ A_{2} and 0 ≤ j′ ≤ n, (s_{j}, t_{j}) ∈ K_{H}, and i_{j} ≠ i_{j+1}. Roughly speaking, between M_{σ} and M_{σ·((s_{k},t_{k}),i_{k})} we have edges for the K_{i} relations for {i} = A_{H} with H ∈ A_{1} and also edges between s_{k} and t_{k} in K_{i_{k}}; however, there are no edges in K_{j} if {j} ∉ A_{1} and j ≠ i_{k}; moreover, there are no other edges in K_{i_{k}} except those required to assure reflexivity.

Before we can construct M′, we need some preliminary observations. We can suppose that the states in S are well ordered. Thus, for each state s ∈ S, if (M, s) ⊧ ¬C_{G}ψ, there is a lexicographically minimal shortest path (s_{0}, …, s_{k}) such that (s_{i}, s_{i+1}) ∈ K_{H} for some H ∈ G and (M, s_{k}) ⊧ ¬ψ. Note that, for each i ≤ k, (M, s_{i}) ⊧ ¬C_{G}ψ and (s_{i}, …, s_{k}) is also the lexicographically minimal shortest G-path from s_{i} leading to a state that satisfies ¬ψ. For each s ∈ S and B = E or C, let ¬B_{G_{1}}ψ_{1}, …, ¬B_{G_{k}}ψ_{k} be the formulas in Sub^{+}(φ) such that (M, s) ⊧ (¬B_{G_{j}}ψ_{j})^{σ_{3}}. For each state s ∈ S, we can associate a set F (s) of at most n pairs (H, t) such that (s, t) ∈ K_{H} and for every formula B_{G}ψ ∈ Sub(φ), if (M, s) ⊧ (¬B_{G}ψ)^{σ_{3}}, then there exists a pair (H, t) ∈ F (s) such that t is the first state after s on the lexicographically minimal σ_{3}(G_{j})-path from s to a state satisfying ¬ψ.

We can now define a set Σ of strings inductively. Let Σ_{0} be the empty string. Suppose that we have constructed Σ_{k} consisting of strings ((s_{1}, t_{1}), i_{1}, …, (s_{k}, t_{k}), i_{k}) with the properties given above. For each σ = ((s_{1}, t_{1}), i_{1}, …, (s_{k}, t_{k}), i_{k}) ∈ Σ_{k}, s ∈ S, (H, t) ∈ F (s), such that H ∈ A_{2}, there is exactly one string σ · ((s, t), i) ∈ Σ_{k+1}. We choose i ∈ A_{H} in such a way that i ≠ i_{k}, i is one of i_{H}^{0}, …, i_{H}^{n}, and a different i is chosen for each (H, t) ∈ F (s). Since |F (s)| ≤ n and we can choose among n + 1 agents i_{H}^{0}, …, i_{H}^{n}, this can clearly be done. Let Σ = ∪_{k}Σ_{k}.

Let M′ = (S′, π′, {K_{i} : i ∈ A}) be defined as follows:

• S′ = ∪_{σ∈Σ}S_{σ}, where each S_{σ} is a disjoint copy of S. We denote by s_{σ} the copy of state s ∈ S in S_{σ}.

• π′(s_{σ}) = π(s) for s ∈ S, σ ∈ Σ.

• If σ_{3}(i) ∈ A_{1}, define K_{i} = {(s_{σ}, t_{σ′}) : (s, t) ∈ K_{σ_{3}(i)}, σ, σ′ ∈ Σ}. K_{i} is clearly reflexive, symmetric, and transitive in this case, since K_{σ_{3}(i)} is.

• If σ_{3}(i) = H ∈ A_{2} and i ∈ G_{H,j}, then K_{i} = {(s_{σ}, s_{σ}) : s ∈ S, σ ∈ Σ)} ∪ {(s_{σ}, t_{σ′}), (t_{σ′}, s_{σ}) : σ′ = σ · ((s, t), i_{H}^{j}) and (s, t) ∈ K_{σ_{3}(i)}}. Again, it is clear from the construction that K_{i} is reflexive, symmetric, and transitive.

• If σ_{3}(i) is undefined, then K_{i} = {(s_{σ}, s_{σ}) : s ∈ S, σ ∈ Σ)}. Of course, in this case K_{i} is also reflexive, symmetric, and transitive.

We claim that for each formula ψ ∈ Sub^{+}(φ), the following are equivalent:

(a) (M, s) ⊧ ψ^{σ_{3}},

(b) (M′, s_{σ}) ⊧ ψ for all σ ∈ Σ,

(c) (M′, s_{σ}) ⊧ ψ for some σ ∈ Σ.

The argument proceeds by a straightforward induction on the structure of ψ. The argument that (a) implies (b) is easy using the induction hypothesis, and the implication from (b) to (c) is trivial. For the argument that (c) implies (a), the only interesting cases are when ψ is of the form K_{i}ψ′, E_{G}ψ′ or C_{G}ψ′. For K_{i}ψ′, the argument is easy because it is easy to see that {i} = A_{H} with H ∈ A_{1}. For E_{G}ψ′, suppose that (M′, s_{σ}) ⊧ E_{G}ψ′. Then we must have (M, s) ⊧ (E_{G}ψ′)^{σ_{3}}. For suppose not. Then there is some (H, t) ∈ F (s) such that H ∈ σ_{3}(G), (s, t) ∈ K_{H} and (M, t) |̸= (ψ′)^{σ_{3}}. Our construction guarantees that σ′ = σ · ((s, t), i) ∈ Σ for some i ∈ A_{H}. From Lemmas 4.3(a) and 4.4(a), it follows that i ∈ G. Moreover, by our construction, (s_{σ}, t_{σ′}) ∈ K_{i}. The induction hypothesis now guarantees that (M′, t_{σ′}) ⊧ ¬ψ′. But this contradicts the assumption that (M′, s_{σ}) ⊧ (E_{G}ψ′)^{σ_{3}}.

Finally, suppose that (M′, s_{σ}) ⊧ C_{G}ψ′. Again, for a contradiction, suppose that (M, s) ⊧ ¬(C_{G}ψ′)^{σ_{3}}. Now we proceed by a subinduction on the length of the shortest σ_{3}(G)-path in M leading to a state satisfying (¬ψ′)^{σ_{3}} to show that (M′, s_{σ}) ⊧ ¬C_{G}ψ′. We leave the straightforward details to the reader.

Next, we want an analogue of Theorem 4.9 for M_{A}^{rst}. The reader will not be surprised to learn that there are new complications here as well, although the basic result still holds.

Theorem 4.16: If A = A_{1} ∪ A_{2} is finite and there is an algorithm for deciding if i ∈ G for G ∈ G that runs in time linear in |A|, then there is a constant c > 0 and an algorithm that, given a formula φ of L_{G}^{C}, decides if φ is satisfiable in M_{A_{1}+A_{2}}^{rst} and runs in time O(|A|2^{c|φ|})

Proof: We start as in the proof of Theorem 4.9. Again, we assume for ease of exposition that A_{1} ≠ ∅. For i ∈ A_{1}, let S_{i}^{1} consist of all the subsets of ESub_{i}^{+}(φ) that are maximally consistent and let S^{1} = ∪_{i∈A_{1}}S_{i}^{1}. The definitions of the K_{i} relations depend on whether i ∈ A_{1} or i ∈ A_{2}. For i ∈ A_{1}, we define the K_{i} relations on S^{1} so that (s, t) ∈ K_{i} iff s/\overline{K_{i}} ∪ \{K_{i}ψ : K_{i}ψ ∈ s\} ⊆ t and s/\overline{K_{i}}∪\{K_{i}ψ : K_{i}ψ ∈ s\} = t/\overline{K_{i}}∪\{K_{i}ψ : K_{i}ψ ∈ t\}. It is easy to check that this modification forces these K_{i} relations to be Euclidean and transitive. We will need this intermediate result in the next section on M_{A}^{elt}. To make these K_{i} equivalence relations, as needed here, we force them to be reflexive as well using the same technique as with M_{A}^{r}: by eliminating s ∈ S^{1} if (s, s) ∉ K_{i} for some i ∈ A_{1} ∪ A_{2}. For i ∈ A_{2}, we define K_{i} so that (s, t) ∈ K_{i} iff s/\overline{K_{i}} ⊆ t and t/\overline{K_{i}} ⊆ s. Clearly this modification forces these K_{i} relations to be symmetric. We force them to be reflexive just as we did for A_{1}.

We now must also change the definition of s seeming consistent. Define the relations ⪯_{i} on S^{1} × S_{i}^{1} by taking s ⪯_{i} s′ if s′ ∈ S_{i}^{1} and s ∩ ESub_{i}(φ) ⊆ s′. Suppose that we have defined S^{1}, …, S^{m}. S^{m+1} consists of all states s ∈ S^{m} that seem consistent, in that the following three conditions hold (where we assume that all states considered are in S^{m}):

1. For all i ∈ A_{1}, there exists an s′ ∈ S^{m} such that s ⪯_{i} s′.

2. There exist distinct agents i_{1}, …, i_{k} ∈ A_{1} and states s_{1}, …, s_{k} such that s ⪯_{i_{h}} s_{h} for h ∈ {1, …, k} and for every formula of the form ¬E_{G}ψ ∈ s, there is a t such that either

(a) (∃i ∈ G ∩ A_{2})((s, t) ∈ K_{i} ∧ ¬ψ ∈ t) or

(b) (∃h ≤ k)(i_{h} ∈ G ∧ (s_{h}, t) ∈ K_{i_{h}} ∧ ¬ψ ∈ t).

3. If ¬C_{G}ψ ∈ s then there exist states s_{0}, s′_{0}, s_{1}, s′_{1}, …, s_{k′} such that s = s_{0}, ¬ψ ∈ s_{k′}, and there exist j_{0}, …, j_{k′−1} in G such that, for each i ≤ k′, (s′_{i}, s_{i+1}) ∈ K_{j_{i}} and either j_{i} ∈ A_{2} and s_{i} = s′_{i} or j_{i} ∈ A_{1}, s_{i} ⪯_{j_{i}} s′_{i} and s′_{i} is acceptable for s_{i}, where we say that s′ is acceptable for s if there are states t_{h} and agents i_{h}, h = 1, …, k, where these states and agents satisfy the same conditions as the states s_{1}, …, s_{k} and agents i_{1}, …, i_{k} in condition 2 for s, and s′ = t_{i} for some i ≤ k.

Note that the second condition does not simply say that for each formula ¬E_{G}φ in s there is a “witness” t such that (s, t) ∈ K_{i} and ¬ψ ∈ t. For one thing, it is not necessarily (s, t) that is in K_{i}. For i ∈ A_{i}, it is actually (s_{i}, t) that is in K_{i} for some s_{i} such that s ⪯_{i} s_{i}. This leads to a second problem. Suppose that E_{G}ψ and E_{G}ψ′ are both formulas in s. There could be two states s_{i} and s′_{i} such that s ⪯_{i} s_{i}, s ⪯_{i} s′_{i}, and states t and t′ such that (s_{i}, t) ∈ K_{i}, (s_{i}, t′) ∈ K_{i}, ¬ψ ∈ t, and ¬ψ′ ∈ t′. This is not good enough for our purposes. We need to be able to find witnesses for each formula ¬E_{G}ψ ∈ s using at most one state s_{i} corresponding to each agent i ∈ A_{1}. The second consistency condition says that this is possible.

To show that this algorithm is correct, first suppose that φ is satisfiable. In that case, (M, s_{0}) ⊧ φ for some structure M = (S, π, {K′_{i} : i ∈ A}) ∈ M_{A_{1}+A_{2}}^{rst}. As for M^{rt}, we can associate with each state s ∈ S and i ∈ A_{1} the state s_{i}^{∗} in S_{i}^{1} consisting of all the formulas ψ ∈ ESub_{i}^{+}(φ) such that (M, s) ⊧ ψ. It is easy to see that if (s, t) ∈ K′_{i} then (s_{i}^{∗}, t_{i}^{∗}) ∈ K_{i}, while if i ∈ A_{2}, then (s_{j}^{∗}, t_{i}^{∗}) ∈ K_{i} for every j. Using this observation, a straightforward argument shows that the states s_{j}^{∗} for s ∈ S always seem consistent, and thus are in S^{m} for all m and all i ∈ A_{1}: For suppose s_{j}^{∗} ∈ S^{m}. We wish to show that s_{j}^{∗} seems consistent and so is in S^{m+1}. For (1), let s′ = s_{i}^{∗}. For (2), suppose that A_{1} = {i_{1}, …, i_{k}} and set s_{h} = s_{i_{h}}^{∗}, so that s_{j}^{∗} ⪯_{i_{h}} s_{i_{h}}^{∗}. Now if ¬E_{G}ψ ∈ s_{j}^{∗}, (M, s) ⊧ ¬E_{G}ψ. Thus there is a state r and an agent i ∈ G such that (M, r) ⊧ ¬ψ and (s, r) ∈ K′_{i}. If i ∈ G ∩ A_{2} then we satisfy (2a) by taking t = r_{i}^{∗}. If i ∈ A_{1}, say i = i_{h}, we satisfy (2b) by taking t = r_{i_{h}}^{∗}. For (3), if ¬C_{G}ψ ∈ s_{j}^{∗}, then (M, s) ⊧ ¬C_{G}ψ. Thus, there is a sequence of states t_{0}, …, t_{k} in M such that t_{0} = s, (M, t_{k}) ⊧ ¬ψ and (t_{h}, t_{h+1}) ∈ K_{j_{h}} for 0 ≤ h < k with each j_{h} ∈ G. We satisfy (3) by taking s_{h} = (t_{h})_{j_{h−1}}^{∗} and letting s′_{h} be s_{h} if j_{h} ∈ A_{2} and (t_{h})_{j_{h}}^{∗} if j_{h} ∈ A_{1}. Moreover, φ ∈ (s_{0})_{i}^{∗} for all i ∈ A_{1}. Thus, the algorithm will declare that φ is satisfiable, as desired.

For the converse, we need to show that if the algorithm declares that φ is satisfiable, then it is indeed satisfiable in M_{A_{1}+A_{2}}^{rst}. We need to work a little harder than in the previous proofs. Now we can no longer just view the object constructed by our algorithm as the required structure. Rather, it serves as a “blueprint” for building the required structure.

Suppose that the algorithm terminates at stage N with a state u ∈ S_{i_{u}} = S_{i_{u}}^{N} containing φ. Before we go on, we make one observation that will prove useful in the sequel. Notice that if s ⪯_{i} s′, then E_{G}ψ ∈ s iff E_{G}ψ ∈ s′ for G ≠ {i}, and if j ∈ A_{2}, then (s, t) ∈ K_{j} iff (s′, t) ∈ K_{j}. A complete state is a vector s⃗ = (s^{i} : i ∈ A_{1} ∧ s^{i} ∈ S_{i}^{N}) such that

• s^{i} ⪯_{j} s^{j} for all i, j ∈ A_{1} and

• for every formula of the form ¬E_{G}ψ ∈ ∪_{i∈A_{1}}s^{i}, there exists an agent j ∈ G and a state t ∈ S^{N} such that ¬ψ ∈ t and either j ∈ A_{1} ∩ G, ¬K_{j}ψ ∈ s^{j}, and (s^{j}, t) ∈ K_{j} or j ∈ A_{2} and (s^{i}, t) ∈ K_{j} for some i ∈ A_{1} (and hence (s^{i}, t) ∈ K_{j} for all i ∈ A_{1}).

By consistency condition 2, every state s ∈ S^{N} must be a component of some (perhaps many) complete states.

Define a structure M^{∗} = (S^{∗}, π^{∗}, {K_{i}^{∗} : i ∈ A_{1} ∪ A_{2}}) as follows:

• S^{∗} consists of all complete states;

• π^{∗}(s⃗)(p) = true iff p ∈ ∪_{i∈A_{1}}s^{i}; • (s⃗, t⃗) ∈ K_{i}^{∗} for i ∈ A_{1} iff (s^{i}, t^{i}) ∈ K_{i};

• (s⃗, t⃗) ∈ K_{i}^{∗} for i ∈ A_{2} iff (s^{j}, t^{j}) ∈ K_{i} for some j ∈ A_{1} (it is easy to check that if (s^{j}, t^{j}) ∈ K_{i} for some j ∈ A_{1} then (s^{j}, t^{j}) ∈ K_{j} for all j ∈ A_{1}).

It is easy to check that M^{∗} ∈ M_{A_{1}+A_{2}}^{rst}. We now show that for all ψ ∈ ∪_{i∈A_{1}}ESub_{i}^{+}(φ), we have

(M^{∗}, s⃗) ⊧ ψ iff ψ ∈ ∪_{i∈A_{1}}s^{i}.

We proceed, as usual, by induction on the structure of ψ. If ψ is a primitive proposition, a conjunction, or a negation, the argument is easy. Suppose that ψ is of the form E_{G}ψ′. If E_{G}ψ′ ∈ ∪_{i∈A_{1}}s^{i}, then the construction of the K_{j} relations guarantees that ψ′ ∈ ∪_{i∈A_{1}}t^{i} for all t⃗ ∈ S^{∗} such that (s⃗, t⃗) ∈ K_{j}^{∗} for some j ∈ G. Thus, by the induction hypothesis, we have that (M^{∗}, s⃗) ⊧ E_{G}ψ′. For the converse, suppose that ¬E_{G}ψ′ ∈ ∪_{i∈A_{1}}s^{i}. Then from the definition of complete state, there must be some agent j ∈ G and a state t ∈ S^{N} such that ¬ψ ∈ t, and either j ∈ A_{1} ∩ G, ¬K_{j}ψ ∈ s^{j}, and (s^{j}, t) ∈ K_{j} or j ∈ A_{2} ∩ G and (s^{i}, t) ∈ K_{j} for some i ∈ A_{1}. By the second consistency condition, t must be a component of some complete state t⃗. By definition (s⃗, t⃗) ∈ K_{j}^{∗} and ¬ψ′ ∈ ∪_{i∈A_{1}}t^{i}.

Finally, suppose that ψ is of the form C_{G}ψ′. If C_{G}ψ′ ∈ ∪_{i∈A_{1}}s^{i} then, since E_{G}(ψ′ ∧ C_{G}ψ′) must also be in ∪_{i∈A_{1}}s^{i}, an easy induction on the length of the path shows that for every complete state t⃗ G-reachable from s⃗, we must have ψ′ ∈ ∪_{i∈A_{1}}t^{i} so, by the induction hypothesis, we have (M^{∗}, s⃗) ⊧ C_{G}ψ′. For the converse, suppose that ¬C_{G}ψ ∈ ∪_{i∈A_{1}}s^{i}. Then ¬C_{G}ψ ∈ s^{j} for some (in fact, all) j ∈ A_{1}. If G ∩ A_{1} ≠ ∅, choose j ∈ G ∩ A_{1}; otherwise, choose j ∈ G arbitrarily. Thus, there must exist a sequence s_{0}, s′_{0}, s_{1}, s′_{1}, …, s_{k} of states in S^{N} and agents j_{0}, …, j_{k−1} in G, as required by consistency condition 3, where s_{0} = s^{n} and ¬ψ ∈ s_{k}. By the definition of acceptability, it follows that there exist complete states s⃗_{0}, …, s⃗_{k} such that s′_{i} is a component of s⃗_{i}, for i = 0, …, k. (Note that states of the form s′_{i} are needed here to determine the complete state.) By construction, (s⃗_{h}, s⃗_{h+1}) ∈ K_{j_{h}}^{∗} h = 0, …, k − 1, and ¬ψ′ ∈ ∪_{i∈A_{1}}s_{k}^{i}. If j ∈ A_{1}, then (s⃗, s⃗_{0}) ∈ K_{j}^{∗}; if j ∉ A_{1}, then j_{0} ∈ A_{2}, and it follows from our initial observation that (s⃗, s⃗_{1}) ∈ K_{j_{0}}^{∗}. In either case, s⃗_{k} is G-reachable from s⃗, so (M^{∗}, s⃗) ⊧ ¬C_{G}ψ′, as desired.

To see that the algorithm runs in the required time bound, we need to show that we can check whether s seems consistent in time O(|A|2^{c|φ|}). The only difficulty is to determine, for given s and s′, if s′ is acceptable for s. It is clear that k ≤ |φ|, since we need at most one state and agent for each formula of the form ¬E_{G}ψ ∈ s. However, if we simply check each subgroup of states containing s′ and of agents containing j where s′ ∈ S_{j}^{1} that are of size ≤ |φ| in the naive way, this check will take time at least C(2^{|φ|}, |φ|)C(|A|, |φ|) (where C(n, k) is n choose k), which is unacceptable for our desired time bounds. Instead, we proceed as follows.

Suppose that s′ ∈ S_{i_{1}}^{1} and s ⪯_{i_{1}} s′. (If it is not the case that s ⪯_{i_{1}} s′ for some i_{1}, then clearly s′ is not acceptable for s′.) Let F (s, s′) consist of all formulas E_{G}ψ such that

1. ¬E_{G}ψ ∈ s,

2. ¬∃t, i(i ∈ G ∩ A_{2} ∧ (s, t) ∈ K_{i} ∧ ¬ψ ∈ t), and

3. |A(s, s′, E_{G}ψ)| < |φ|, where A(s, s′, E_{G}ψ) = {i ∈ G∩A_{1} : i = i_{1} ∨ ∃t(s ⪯_{i} t ∧ ¬K_{i}ψ ∈ t)}.

Intuitively, F (s, s′) consists of the potentially “problematic” formulas that may prevent s′ from being acceptable for s.

Let T = ∪_{E_{G}ψ∈F (s,s′)}A(s, s′, E_{G}ψ). Note that |T | < |φ|^{2}. Suppose that T = {i_{1}, …, i_{N}}. We construct sets B_{1}, …, B_{N} of subsets of F (s, s′) with the property that X ∈ B_{k} iff X consists of the formulas of the form E_{G}ψ such that there exist states t_{1}, …, t_{k} such that s ⪯_{i_{j}} t_{j} for j = 1, …, k , t_{1} = s′ and, for each formula E_{G}ψ ∈ X, there exists a j such that ¬K_{i_{j}}ψ ∈ t_{j} and i_{j} ∈ G.

Given a state t ∈ S_{i}^{1}, let F_{t}(s, s′) = {E_{G}ψ ∈ F (s, s′) : ¬K_{i}ψ ∈ t, i ∈ G ∩ T }. Intuitively, F_{t}(s, s′) consists of the formulas in F (s, s′) that can be “taken care of” by state t. Let B_{1} = {F_{s′}(s, s′)}. Suppose that we have defined B_{1}, …, B_{k}. Let B_{k+1} = {X ∪ F_{t}(s, s′) : X ∈ B_{k} ∧ s ⪯_{i_{k+1}} t}. It is easy to check that B_{k+1} has the required property. Moreover, we can compute the sets B_{1}, …, B_{N} in time O(2^{cn}). To see this, note that since |F (s, s′)| ≤ |φ|, clearly |B_{j}| ≤ 2^{|φ|}. Thus, given B_{k}, we can clearly compute B_{k+1} in time O(2^{cn}) for some c > 0. Since N < |φ|^{2}, the result follows. Finally, we claim that s′ is acceptable for s iff F (s, s′) ∈ B_{N}.

Clearly if F (s, s′) ∉ B_{N}, then it is almost immediate from the definition that s′ is not acceptable for s. Conversely, if F (s, s′) ∈ B_{N}, then there exist states t_{1}, …, t_{N} such that s′ = t_{1}, s ⪯_{i_{j}} t_{j} and, for each formula in E_{G}ψ ∈ F (s, s′), there exists j such that K_{i_{j}}ψ ∈ t_{j}. We clearly do not need all of these states and agents; we just need at most one for each formula in F (s, s′). That is, there exists a set A′ of agents (contained in {i_{1}, …, i_{N}}) with |A′| ≤ |F (s, s′)| and a state u_{i} corresponding to each agent i ∈ A′ (contained in {t_{1}, …, t_{N}}) such that for each formula E_{G}ψ ∈ F (s, s′), there exists an agent i ∈ A′ such that s ⪯_{i} u_{i} and ¬K_{i}ψ ∈ u_{i}. We now wish to extend A′ to a set showing that s′ is acceptable for s. If we consider any ¬E_{G}ψ ∈ s, either condition 2(a) is satisfied or there is already an i ∈ A′ satisfying 2(b) or |A(s, s′, E_{G}ψ)| ≥ |φ|. In the last case, it is immediate that we can extend A′ to include an agent satisfying 2(b) for E_{G}ψ.

We can now prove Theorem 3.4 for M_{A}^{rst}.

Proof of Theorem 3.4 for M_{A}^{rst}: Again, the lower bound follows from standard results in [HM92].

For the upper bound, suppose that we are given a formula φ such that n = |φ|. We can compute the set E_{n}^{m}(G_{φ}) defined just before Lemma 4.11 in time O(n^{2}2^{cn}), using at most n^{2}2^{n} calls to the oracle O_{m}, just as we computed E^{1}(G_{φ}). Similarly, we can characterize the sets H such that (G, H) is in R(G_{φ}^{n}) = R^{n}(G_{φ}) by a pair (H′, X), where H′ ⊆ G_{φ} and X is either ∅ or an element of E_{n}^{n}(G_{φ}); we can compute which of the pairs (H′, X) actually represent sets H such that (G, H) ∈ R(G_{φ}^{n}) using at most 2n(2^{2n} + 2^{n}) calls to the oracle O_{n}. It is not hard to show that R(G̃_{φ}^{n}) consists of pairs (G, H) such that either |A_{H}| > n + 1 and (G, H) ∈ R(G_{φ}^{n}) or |A_{H}| = 1 and there exists (G, H′) ∈ R(G_{φ}^{n}) such that |A_{H′}| ≤ n and A_{H} ⊆ A_{H′}. Recall that A^{φ,rst} = {H : ∃G((G, H) ∈ R(G̃_{φ}^{n}))}, A_{1} = {H : ∃G[(G, H) ∈ R(G̃_{φ}^{n}), |G − ∪H| = 1]}, and A_{2} = A^{φ,rst} − A_{1}. Thus, we can represent elements H ∈ A_{1} by pairs of the form (H′, X) as above, while elements of H ∈ A_{2} can be represented by triples of the form (H′, X, i), for i = 1, …, |A_{H}|. Thus, although we cannot in general compute the individual elements of the sets A_{H} such that |A_{H}| ≤ m, it does not matter. It suffices that we know the cardinality of these atoms (which our oracle will tell us).

It is now straightforward to compute the formula φ^{σ_{3}} in time O(2^{cn}) using O(2^{cn}) oracle calls. We now apply Proposition 4.15 and Theorem 4.16, just as we applied Proposition 4.1 and Theorem 4.5 in the case of M_{A}.

We now turn our attention to proving Theorem 3.1 for M_{A}^{rst}. Again, the basic structure is the same as for M_{A} and M_{A}^{rt}.

Lemma 4.17: The mapping σ_{3} (when viewed as a map with domain 2^{A}) is injective on G̃_{φ}^{n}.

Let (S5_{G}^{C})^{A_{1}+A_{2}} consist of the axioms in (T_{G}^{C})^{+} (including E5) together with E6 and every instance of K4 and K5 for i ∈ A_{1}. We write (S5_{G}^{C})^{A_{1}+A_{2}} ⊢_{φ} ψ if there is a proof of ψ in (S5_{G}^{C})^{A_{1}+A_{2}} using only the modal operators that appear in φ and K_{i} for i ∈ A_{1}.

Lemma 4.18: If A is finite and φ ∈ L_{G}^{C} is valid with respect to M_{A_{1}+A_{2}}^{rst}, then (S5_{G}^{C})^{A_{1}+A_{2}} ⊢_{φ} φ.

Proof: The proof is similar in spirit to that of Lemma 4.13 for M_{A}^{rt}, except that since we have a different definition of the K_{i} relations and of seeming consistent, we must check that states eliminated under this definition are inconsistent. Again we must consider each of the three ways that a state s can be eliminated.

First, suppose that s ∈ S^{j} and, for some i ∈ A_{1}, there is no s′ such that s ⪯_{i} s′. As before, propositional reasoning shows that (S5_{G}^{C})^{A_{1}+A_{2}} ⊢_{φ} φ_{s} ⇔ ∨_{{s′∈S_{i}^{1}:s⪯_{i}s′}}φ_{s′}. Thus, it easily follows that (S5_{G}^{C})^{A_{1}+A_{2}} ⊢_{φ} ¬φ_{s}.

Next, suppose that s ∈ S^{j} does not satisfy the second condition of seeming consistent. Define an extension of s to be a vector s⃗ = (s^{i} : i ∈ A_{1}) of states, where s ⪯_{i} s^{i}. Let EX(s) be the set of all extensions of s. If s⃗ is an extension of s, let φs⃗ be the conjunction over all i ∈ A_{1} of the formulas in φ_{s^{i}}. By straightforward propositional reasoning, we have (S5_{G}^{C})^{A_{1}+A_{2}} ⊢_{φ} φ_{s} ⇔ ∨_{s⃗∈EX(s)}φs⃗. Thus, to show that (S5_{G}^{C})^{A_{1}+A_{2}} ⊢_{φ} ¬φ_{s} if s is eliminated by the second condition of seeming consistent, it suffices to show that (S5_{G}^{C})^{A_{1}+A_{2}} ⊢_{φ} ¬φs⃗ for each s⃗ ∈ EX(s). This we do by showing that, for each extension s⃗ ∈ EX(s), there is a formula ¬E_{G}ψ ∈ s such (S5_{G}^{C})^{A_{1}+A_{2}} ⊢_{φ} φs⃗ ⇒ E_{G}ψ. Since ¬E_{G}ψ ∈ s, simple propositional reasoning shows that (S5_{G}^{C})^{A_{1}+A_{2}} ⊢_{φ} φs⃗ ⇒ ¬E_{G}ψ. This shows that (S5_{G}^{C})^{A_{1}+A_{2}} ⊢_{φ} ¬φs⃗ as desired.

So suppose that A_{1} = {i_{1}, …, i_{m}} and s⃗ = (s_{1}, …, s_{m}) ∈ EX(s). Since s does not satisfy the second condition of seeming consistent, it follows that there exists some formula ¬E_{G}ψ ∈ s such that for all t ∈ S^{j},

1. for all i ∈ G ∩ A_{2}, if (s, t) ∈ K_{i}, then ψ ∈ t and

2. for all h ∈ {1, …, m} such that i_{h} ∈ G, if (s_{h}, t) ∈ K_{i_{h}}, then ψ ∈ t.

The proof now follows the lines of the analogous argument in the proof of Lemma 4.13. As before, it suffices to find, for each i ∈ G and each t ∈ S_{i}^{j} with ¬ψ ∈ t, a set G^{i,t} of agents containing i such that (S5_{G}^{C})^{A_{1}+A_{2}} ⊢_{φ} φs⃗ ⇒ E_{G^{i,t}}¬φ_{t}. So fix i ∈ G and t ∈ S_{i}^{j} with ¬ψ ∈ t. As before, the proof splits into two cases: i ∈ A_{1} and i ∈ A_{2}.

If i ∈ A_{2}, this follows as before if the reason that (s, t) ∉ K_{i} is that s/\overline{K_{i}} ⊈ t. If instead t/\overline{K_{i}} ⊈ s, then there is some E_{G′}θ ∈ t with i ∈ G′ such that ¬θ ∈ s and so ¬θ ∈ s^{i} for each i. Thus (S5_{G}^{C})^{A_{1}+A_{2}} ⊢_{φ} φs⃗ ⇒ ¬θ and, by E6, (S5_{G}^{C})^{A_{1}+A_{2}} ⊢_{φ} ¬θ ⇒ E_{G′}¬E_{G′}θ. Since E_{G′}θ ∈ t we have that (S5_{G}^{C})^{A_{1}+A_{2}} ⊢_{φ} φs⃗ ⇒ E_{G′}¬φ_{t}. That is, we can take G^{i,t} = G′ in this case.

On the other hand, if i ∈ A_{1}, we show that (S5_{G}^{C})^{A_{1}+A_{2}} ⊢_{φ} φs⃗ ⇒ K_{i}¬φ_{t} (so that we can take G^{i,t} = {i}). By assumption, since ¬ψ ∈ t, (s^{i}, t) ∉ K_{i}. Since t ∈ S_{j}^{i}, there is some formula θ such that either K_{i}θ ∈ s^{i} and ¬K_{i}θ ∈ t or K_{i}θ ∈ t and ¬K_{i}θ ∈ s^{i}. Here we are implicitly using the following facts: (1) if E_{G′}θ ∈ s for some G′ such that i ∈ G′ then K_{i}θ ∈ s^{i}, since s^{i} ∈ S_{i}^{1}, and similarly for t, (2) if K_{i}θ ∉ s, then ¬K_{i}θ ∈ s, since s^{i} ∈ S_{i}^{j}, and similarly for t, and (3) if K_{i}θ ∈ s^{i} then θ ∈ s since (s, s) ∈ K_{i}, and similarly for t. If K_{i}θ ∈ s and ¬K_{i}θ ∈ t, it follows that (S5_{G}^{C})^{A_{1}+A_{2}} ⊢_{φ} φ_{s} ⇒ K_{i}¬φ_{t} just as in the case of (S4_{G}^{C})^{A_{1}+A_{2}}. If K_{i}θ ∈ t and ¬K_{i}θ ∈ s, then by K5 we have (S5_{G}^{C})^{A_{1}+A_{2}} ⊢_{φ} φ_{s} ⇒ K_{i}¬K_{i}θ and (S5_{G}^{C})^{A_{1}+A_{2}} ⊢_{φ} ¬K_{i}θ ⇒ ¬φ_{t}. The desired result now follows by standard arguments.

We have now shown that for all i ∈ G and t ∈ S_{j}^{i} such that ψ ∈ t, there exists some set G^{i,t} with i ∈ G^{i,t} such that (S5_{G}^{C})^{A_{1}+A_{2}} ⊢_{φ} φ_{s} ⇒ E_{G^{i,t}}¬φ_{t}. We can now conclude that (S5_{G}^{C})^{A_{1}+A_{2}} ⊢_{φ} φ_{s} ⇒ ¬E_{G}ψ just as in the case of (S4_{G}^{C})^{A_{1}+A_{2}}, showing that φ_{s} is inconsistent, as desired.

Finally, if s ∈ S^{j} does not satisfy the third condition of seeming consistent, the argument that (S5_{G}^{C})^{A_{1}+A_{2}} ⊢_{φ} ¬φ_{s} is similar to that of Lemma 4.7. We replace G-reachability by the existence of sequences as in condition 3 in the definition of seeming consistent in Theorem 4.16 and note that we have essentially already proved the analogue of (6) from Lemma 4.7. We leave the remaining details to the reader.

Proof of Theorem 3.1 for M_{A}^{rst}: The proof follows as for M_{A}^{rt} using the analogous lemmas proved above for M_{A}^{rst}.

4.4 Dealing with M_{A}^{elt}

For M_{A}^{elt}, we proceed much as for M_{A}^{rst}. There is one new subtlety. Consider the construction in the proof of Proposition 4.15, which uses σ_{3}. Recall that σ_{3}(i) may be undefined for some i. For such i, we defined K_{i} to consist of all pairs (s_{σ}, s_{σ}), making it reflexive. This approach will not work for M_{A}^{elt}. More precisely, the analogue of Proposition 4.15 for M_{A}^{elt} will not hold using this construction (even if we drop the reflexivity requirement). For example, if φ = ¬p∧E_{G_{1}}p∧E_{G_{2}}p and G_{1} ∩ G_{2} ≠ ∅, then φ^{σ_{3}} is satisfiable in M_{A_{1}+A_{2}}^{elt} but φ is not satisfied in the structure M′ constructed in Proposition4.15, since for all i ∈ G_{1} ∩G_{2}, the construction will make K_{i} reflexive. We solve this problem by defining a mapping σ_{4} much like σ_{3}, except that we ensure that σ_{4} is never undefined.

Let B be the set consisting of those maximal subsets T of G_{φ} such that ∩T ≠ ∅ for which the corresponding atom over G^{φ}, A_{T} = (∩T ) ∩ (∩_{G∈G_{φ}−T} \overline{G}) (= ∩T , by the maximality of T ), form A_{H} for some H ∈ A^{φ,rst}. Let A^{φ,elt} = A^{φ,rst} ∪ B, A_{1} = B ∪ {H ∈ A^{φ,rst} : |A_{H}| = 1}, A_{2} = A^{φ,elt} − A_{1}. The definitions of σ_{4} : A → A^{φ,elt} and τ_{4} : A^{φ,elt} → 2^{A} need some care. If i ∈ A_{H} for some H ∈ A^{φ,rst}, let σ_{4}(i) = H as before. Otherwise, choose T ∈ B such that T ⊇ {G ∈ G_{φ} : i ∈ G} and let σ_{4}(i) = T . Note that, by construction, σ_{4} is defined for all i.

For H ∈ A^{φ,rst}, τ_{4}(H) = ∩{G̃_{φ}^{n} − H} as before. For T ∈ B, choose some i_{T} ∈ A_{T} (it does not matter which) and set τ_{4}(T ) = {i_{T} }.

Proposition 4.19: φ is satisfiable in M_{A}^{elt} iff φ^{σ_{4}} is satisfiable in M_{A_{1}+A_{2}}^{elt}.

Proof: First suppose that (M, s) ⊧ φ, where M ∈ M^{elt}. We convert M to M′ ∈ M_{A_{1}+A_{2}}^{elt} as before, by defining K_{I} = ∪{K_{i} : i ∈ τ_{4}(I)} for I ∈ A^{φ,elt}. To apply Proposition 4.1, we need to show that ∪{τ_{4}(I) : I ∈ σ_{4}(G)} = G for all G ∈ G_{φ}. We know from the analysis of the M^{rst} case that ∪{τ_{3}(H) : H ∈ σ_{3}(G)} = G for all G ∈ G_{φ}. Since σ_{4}(G) ⊇ σ_{3}(G) and τ_{4}(H) = τ_{3}(H) for H ∈ A^{φ,rst}, we have that ∪{τ_{4}(I) : I ∈ σ_{4}(G)} = ∪{τ_{3}(H) : H ∈ σ_{3}(G)} ∪ ∪{τ_{4}(I) : I ∈ σ_{4}(G) − σ_{3}(G)}. It is clear from the definitions, however, that if I ∈ σ_{4}(G) − σ_{3}(G), then there exists some i ∈ G such that I = σ_{4}(i) and σ_{3}(i) is undefined. Moreover, I = T for some maximal set T such that (among other things) G ∈ T . Thus, A_{I} ⊆ G, so τ_{4}(I) ∈ G. Thus, ∪{τ_{3}(I) : I ∈ σ_{4}(G) − σ_{3}(G)} ⊆ G, so ∪{τ_{4}(I) : I ∈ σ_{4}(G)} = ∪{τ_{3}(H) : H ∈ σ_{3}(G)} = G, as desired. Applying Proposition 4.1, we get that to see that (M′, s) ⊧ φ^{σ_{4}}.

It remains to verify that M′ ∈ M_{A_{1}+A_{2}}^{elt}. For this, we need to show that the K_{I} relations for I ∈ A_{1} are Euclidean, serial and transitive and that those in A_{2} are serial and secondarily reflexive. For the ones in A_{1}, note that τ_{4}(I) is a singleton and so the desired properties hold since they hold for all agents in M. For the ones in A_{2}, we just note that the union of serial relations is serial and the union of Euclidean relations is secondarily reflexive.

For the other direction, we proceed much as in the proof of Proposition 4.15. In addition to the concerns dealt with there for M^{rst}, our primary new one is to make sure that the K_{i} relations for all agents are serial. The problem arises for those i for which σ_{3}(i) was undefined. The new agents in B are used to deal with this problem.

We proceed much as in Proposition 4.15, with two changes. First, we replace the automatic forcing of reflexivity by forcing secondary reflexivity for σ_{3}(i) ∈ A_{2}. Second, we modify the definition of the K_{i} relation in M′ as follows.

• If σ_{4}(i) ∈ A_{1} ∩ A^{φ,rst} then, as before, K_{i} = {(s_{σ}, t_{σ′}) : (s, t) ∈ K_{σ_{3}(i)}, σ, σ′ ∈ Σ}.

• If σ_{4}(i) ∈ A_{2} and i ∈ G_{H,j}, then K_{i} = {(s_{σ}, t_{σ′}), (t_{σ′}, t_{σ′}) : σ′ = σ · ((s, t), i_{H}^{j})}.

• If σ_{4}(i) = T ∈ B, then K_{i} = {(s_{σ}, t_{σ′}) : (s, t) ∈ K_{σ_{4}(i)}, σ, σ′ ∈ Σ}.

Now note that every relation K_{i} is Euclidean, serial and transitive. For the ones corresponding to agents in A_{1} this is immediate from the fact that the agents in A_{1} have these properties. For those with σ_{4}(i) ∈ A_{2}, seriality follows from the fact that the agents in A_{2} are serial and the construction. Transitivity and the Euclidean property follow from the construction. In particular, if there is a K_{i} edge coming into some t_{σ} then there is none going out by construction except for the one from t_{σ} to itself.

The verification that M′ satisfies φ now proceeds as in Proposition 4.15.

Theorem 4.20: If A = A_{1} + A is finite and there is an an algorithm for deciding if i ∈ G for G ∈ G that runs in time linear in |A|, then there is a constant c > 0 (independent of |A|) and an algorithm that, given a formula φ of L_{G}^{C}, decides if φ is satisfiable in M_{A_{1}+A_{2}}^{elt} and runs in time O(|A|2^{c|φ|}).

Proof: The argument here is like that for the M_{A_{1}+A_{2}}^{rst} case in Theorem 4.16. We keep the definition of K_{i} for i ∈ A_{1} and, as we noted there, this makes these relations Euclidean and transitive. We change the definition of K_{i} for i ∈ A_{2} by putting (s, t) in K_{i} iff s/\overline{K_{i}} ⊆ t and t/\overline{K_{i}} ⊆ t. This latter definition clearly makes the K_{i} secondarily reflexive for i ∈ A_{2}. We ensure seriality by adding a clause to the definition of a state s seeming consistent:

4 For every agent i ∈ A_{2} there is a state t such that (s, t) ∈ K_{i} and for every agent i ∈ A_{1} there are states s′ and t such s ⪯_{i} s′ and (s′, t) ∈ K_{i}.

The proof now proceeds as before.

Proof of Theorem 3.4 for M_{A}^{elt}: The argument here is essentially the same as for M_{A}^{rst}. Just note that using the oracle O′ we can determine the members of B within the appropriate time bound and so compute φ^{σ_{4}} as required.

We now turn our attention to proving Theorem 3.1 for M_{A}^{elt}. The basic structure is the same as for M_{A}^{rst}.

Lemma 4.21: The mapping σ_{4} (when viewed as a map with domain 2^{A}) is injective on G̃_{φ}^{n}.

Let (KD45_{G}^{C})^{A_{1}+A_{2}} consist of the axioms in K_{G}^{C} together with K3, E4, E7, and every instance of K4 and K5 for i ∈ A_{1}. We write (KD45_{G}^{C})^{A_{1}+A_{2}} ⊢_{φ} ψ if there is a proof of ψ in (KD45_{G}^{C})^{A_{1}+A_{2}} using only the modal operators that appear in φ and K_{i} for i ∈ A_{1}.

Lemma 4.22: If A is finite and φ ∈ L_{G}^{C} is valid with respect to M_{A_{1}+A_{2}}^{elt}, then (KD45_{G}^{C})^{A_{1}+A_{2}} ⊢_{φ} φ.

Proof: The proof is similar to that of Lemma 4.18 for M_{A}^{rst}. Again we must check that all states eliminated in the construction are provably inconsistent, but now using the axioms of (KD45_{G}^{C})^{A_{1}+A_{2}} and the modified definition of the K_{i} relations, and dealing with the additional clause in the definition of seeming consistent.

The argument for the first condition for seeming consistent is the same as that for M_{A}^{rst}. Before dealing with the second condition, we prove a fact that will also be useful in dealing

with the fourth condition. Let T_{i} = {t ∈ S_{i}^{j} : (t, t) ∈ K_{i}}. It is easy to see that

if t ∈ S_{i}^{j} − T_{i}, then (KD45_{G}^{C})^{A_{1}+A_{2}} ⊢_{φ} φ_{s} ⇒ E_{G}¬φ_{t} for some G such that i ∈ G.  (13)

For if t ∈ S_{i}^{j} − T_{i}, then there exists E_{G}θ ∈ t such that i ∈ G and ¬θ ∈ t. But then (E_{G}θ ⇒ θ) ⇒ ¬φ_{t} is propositionally valid (and so provable by Prop). Since (KD45_{G}^{C})^{A_{1}+A_{2}} ⊢_{φ} φ_{s} ⇒ E_{G}(E_{G}θ ⇒ θ), we can easily obtain (13) using (4).

Now suppose that s is eliminated because it does not satisfy the second condition for seeming consistent. As in the proof of Lemma 4.18, it suffices to show that for each extension s⃗ ∈ EX(s), there is a formula ¬E_{G}ψ ∈ s such (S5_{G}^{C})^{A_{1}+A_{2}} ⊢_{φ} φs⃗ ⇒ E_{G}ψ. So fix an extension s⃗ = (s^{1}, …, s^{m}) ∈ EX(s) and choose the formula ¬E_{G}ψ ∈ s that causes the violation of the second condition for (s^{1}, …, s^{m}). It again suffices to show that for each i ∈ G and t ∈ S_{i}^{j} such such that ¬ψ ∈ t, there is a set G^{i,t} of agents containing i such that (KD45_{G}^{C})^{A_{1}+A_{2}} ⊢_{φ} φs⃗ ⇒ E_{G^{i,t}}¬φ_{t}. First suppose that i ∈ A_{2}. If (s, t) ∉ K_{i} because s/\overline{K_{i}} ⊈ t then the argument given in Lemma 4.7 works to get a G^{i,t} as desired. If s/\overline{K_{i}} ⊆ t but t/\overline{K_{i}} ⊈ t then the existence of the required G^{i,t} is immediate from (13). Now suppose i ∈ A_{1}. Then, because s does not satisfy the second condition of seeming consistent, we have (s^{i}, t) ∉ K_{i}. If s/K_{i} ⊈ t, then there is some formula θ such that K_{i}θ ∈ s^{i} and ¬θ ∈ t; it easily follows that (KD45_{G}^{C})^{A_{1}+A_{2}} ⊢_{φ} φs⃗ ⇒ K_{i}¬φ_{t}, as required. If {K_{i}θ : K_{i}θ ∈ s} ⊈ t, then there is some θ such that K_{i}θ ∈ s but ¬K_{i}θ ∈ t; the result now easily follows using K4, just as in the argument for (S4_{G}^{C})^{A_{1}+A_{2}}. If both of these conditions hold (but still (s^{i}, t) ∉ K_{i}), then it must be that there is a θ with K_{i}θ ∈ t and K_{i}θ ∉ s. In this case ¬K_{i}θ ∈ s, and the result follows using K5, just as in the argument for (S5_{G}^{C})^{A_{1}+A_{2}}.

The argument in the case that s is eliminated because it does not satisfy the third condition for seeming consistent is the same as in the proof of Lemma 4.18.

Finally, suppose that s does not satisfy the new (fourth) condition of seeming consistent. Then either

• there is an i ∈ A_{2} for which there is no t with (s, t) ∈ K_{i} or

• there is an i ∈ A_{1} for which there is no pair s′, t such that s ⪯_{i} s′ and (s′, t) ∈ K_{i}.

For the first case, for each t ∈ T_{i}, it must be the case that s/\overline{K_{i}} ⊈ t, so that there must be some G^{i,t} with i ∈ G^{i,t} such that (KD45_{G}^{C})^{A_{1}+A_{2}} ⊢ φ_{s} ⇒ E_{G^{i,t}}¬φ_{t}, as usual. By (13), for each t ∈ S_{i}^{j} − T_{i}, there is some G^{i,t} with i ∈ G^{i,t} such that (KD45_{G}^{C})^{A_{1}+A_{2}} ⊢_{φ} φ_{s} ⇒ E_{G^{i,t}}¬φ_{t}. Thus, (KD45_{G}^{C})^{A_{1}+A_{2}} ⊢_{φ} φ_{s} ⇒ ∧_{t∈S^{j}}E_{G^{i,t}}¬φ_{t}. But since (KD45_{G}^{C})^{A_{1}+A_{2}} ⊢_{φ} ¬(∧_{t∈S^{j}}¬φ_{t}) by induction and propositional reasoning, it follows from E7 that (KD45_{G}^{C})^{A_{1}+A_{2}} ⊢_{φ} ¬(∧_{t∈S^{j}}E_{G^{i,t}}¬φ_{t}). Thus we get (KD45_{G}^{C})^{A_{1}+A_{2}} ⊢_{φ} ¬φ_{s}, as desired.

For the second case, we know as in the proof of Lemma 4.18 that φ_{s} is provably equivalent to the disjunction of φ_{s′} for those s′ such that s ⪯_{i} s′ and similarly for any t. Thus to prove (KD45_{G}^{C})^{A_{1}+A_{2}} ⊢_{φ} ¬φ_{s} it suffices to prove (KD45_{G}^{C})^{A_{1}+A_{2}} ⊢_{φ} ¬φ_{s′} for every s′ ∈ S_{i}^{j} such that s ⪯_{i} s′. For each such s′ we know that there is no t′ ∈ S_{i}^{j} such that (s′, t′) ∈ K_{i}. Given s′, if t′ ∈ S_{i}^{j} and (s′, t′) ∉ K_{i}, then the same argument as in the proof of Lemma 4.18 shows that (KD45_{G}^{C})^{A_{1}+A_{2}} ⊢_{φ} φ_{s′} ⇒ K_{i}¬φ_{t′}, since the K_{i} relations are defined the same way for agents in A_{1} in both the M_{A}^{elt} and M_{A}^{rst} cases, and the proof in Lemma 4.18 used only axioms K4 and K5 (as well as Prop, K1, and MP), and these axioms are in both (S5_{G}^{C})^{A_{1}+A_{2}} and (KD45_{G}^{C})^{A_{1}+A_{2}}.

By (3), we have that (KD45_{G}^{C})^{A_{1}+A_{2}} ⊢ φ_{s′} ⇒ K_{i}(∧_{t′∈S_{i}^{j}}¬φ_{t′}). Since (KD45_{G}^{C})^{A_{1}+A_{2}} ⊢_{φ}

(∧_{t′∈S_{i}^{j}}¬φ_{t′}) ⇒ false by induction and propositional reasoning, we conclude that (KD45_{G}^{C})^{A_{1}+A_{2}}

⊢_{φ} φ_{s′} ⇒ K_{i}false. Now using K3, we get (KD45_{G}^{C})^{A_{1}+A_{2}} ⊢_{φ} ¬φ_{s′}, as desired.

Proof of Theorem 3.1 for M_{A}^{elt}: The proof follows as for M_{A}^{rt} using the analogous lemmas proved above for M_{A}^{elt}. We must just show that E7 is derivable from the other axioms in KD45_{G}^{C}. Suppose that i ∈ G_{1} ∩ … ∩ G_{k}. Then, using E1, KD45_{G}^{C} ⊢ E_{G_{1}}φ_{1} ∧ … ∧ E_{G_{k}}φ_{k} ⇒ K_{i}φ_{1} ∧ … ∧ K_{i}φ_{k}. By (3), we have KD45_{G}^{C} ⊢ K_{i}φ_{1} ∧ … ∧ K_{i}φ_{k} ⇒ K_{i}(φ_{1} ∧ … ∧ φ_{k}). Thus, KD45_{G}^{C} ⊢ ¬K_{i}(φ_{1} ∧…∧φ_{k}) ⇒ ¬(E_{G_{1}}φ_{1} ∧…∧E_{G_{k}}φ_{k}). It thus suffices to show that in KD45_{G}^{C}, from ¬(φ_{1} ∧ … ∧ φ_{k}) we can infer ¬K_{i}(φ_{∧} … ∧ φ_{k}). But since ¬(φ_{1} ∧ … ∧ φ_{k}) is equivalent to (φ_{1} ∧ … φ_{k}) ⇒ false, this follows easily using (4) and K3.

4.5 The complexity of querying the oracles

Up to now we have assumed that we are charged one for each query to an oracle. In this section, we reconsider our results, trying to take into account more explicitly the cost of the oracle queries.

Let f(m, k) be the worst-case time complexity of deciding whether a set with description G ∈ Ĝ_{A}^{m} such that l(G) ≤ k has cardinality greater than m′ for each m′ ≤ m (where we take the worst case over all G ∈ Ĝ_{A}^{m} such that l(G) ≤ k and over all m′ ≤ m). Let g(k) to be the worst-case complexity of deciding if G_{1} ∩ … ∩ G_{k} = ∅ for G_{1}, …, G_{k} ∈ G_{A}. We take f(m, k) (resp., g(k)) to be ∞ if these questions are undecidable. We can think of f(m, k) (resp., g(k)) as the worst-case cost of querying the oracle O_{m} (resp., O′) on a set with a description of length ≤ k.

Using these definitions, we can sharpen Theorem 3.4 as follows.

Theorem 4.23: There is a constant c > 0 and an algorithm that decides if a formula φ ∈ L_{G}^{C} is satisfiable in M_{A} (resp., M_{A}^{r}, M_{A}^{rt}, M_{A}^{rst}, M_{A}^{elt}) and runs in time 2^{c|φ|}f(0, |φ|) (resp., 2^{c|φ|}f(0, |φ|), 2^{c|φ|}f(1, 2^{c|φ|^{2}}), 2^{c|φ|}f(|φ|, 2^{c|φ|^{2}}), 2^{c|φ|}(f(|φ|, 2^{c|φ|^{2}}) + g(|φ|))) Moreover, if G contains a subset with at least two elements, then there exists a constant d > 0 such that every algorithm for deciding the satisfiability of formulas in M_{A} (resp., M_{A}^{r}, M_{A}^{rt}, M_{A}^{rst}, M_{A}^{elt}) runs in time at least max(2^{d|φ|}, f(0, d|φ|)) (resp., (max(2^{d|φ|}, f(0, d|φ|)), max(2^{d|φ|}, f(1, d|φ|)), max(2^{d|φ|}, f(d|φ|, d|φ|)), max(2^{d|φ|}, f(d|φ|, d|φ|), g(d|φ|))) for infinitely many formulas φ.

Proof: The upper bound is almost immediate from the proof of Theorem 3.4. The only point that needs discussion is the second argument—2^{c|φ|^{2}}—of f in the cases M_{A}^{rt}, M_{A}^{rst}, and M_{A}^{elt}. This follows from Lemma 4.11. An easy induction on i shows that the sets in the set E_{i}^{|φ|} constructed just before Lemma 4.11 have description length at most ≤ 2^{2i|φ|} (using the fact that |E_{i}^{|φ|}| ≤ 2^{|φ|} for all i). Thus, all the sets that we need to deal with have description length ≤ 2^{2|φ|^{2}}, since they are all in E_{|φ|}^{|φ|}, by Lemma 4.11(e).

The lower bound is immediate from the results of [HM92] and Proposition 3.3.

Note that if f_{0}(k) = f(0, k) is well behaved, in that there exist c′, k_{0} such that f_{0}(k) ≤ 2^{c′k} for all k ≥ k_{0} or f_{0}(k) ≥ 2^{c′k} for all k ≥ k_{0}, then it is easy to see that there is some c′′ > 0 such that 2^{c|φ|}f(0, |φ|) ≤ max(2^{c′′|φ|}, c′′f(0, |φ|)). Thus, if f_{0} is well behaved, then the lower and upper bounds of Theorem 3.4 match, and we have tight bounds in the case of M_{A} and M_{A}^{r}. This is not the case for M_{A}^{rt}, M_{A}^{rst}, and M_{A}^{elt}, because the sets that arise have exponential-length descriptions.

Do we really have to answer queries about such complicated formulas if we are to deal with M_{A}^{rt}, M_{A}^{rst}, and M_{A}^{elt}? To some extent, this is an artifact of our insistence that the sets be described using union and set difference. In fact, all the sets that we need to consult the oracle about in our algorithm are atoms, and so have very simple descriptions (O(|φ|)) if we are allowed to used intersections and complementation. Indeed, suppose that we define an ordering ≺ on atoms such that A_{H} ≺ A_{H′} if H ⊃ H′. It follows easily from Lemma 4.3 and Lemma 4.4 that in order to compute σ_{2}(G) (resp., σ_{3}(G), σ_{4}(G)), we start by considering all atoms A_{H} such that G appears positively in A_{H} and all other sets in G_{φ} appear negatively; we then need to check whether |A_{H}| > 0 and |A_{H}| > 1 (resp., |A_{H}| > 0, …, and |A_{H}| > |φ|) only for those atoms A_{H} such that for all H′ ≺ H, we have |A_{H′}| ≤ 1 (resp., |A_{H′}| ≤ |φ|). (In addition, in the case of σ_{4}, we have also have to check whether G_{1} ∩ … ∩ G_{k} = ∅, but again, these are sets with simple descriptions if we allow intersection.) Thus, as long as we can check the required properties of sets described in terms of intersection and complementation relatively efficiently, then the queries to the oracle pose no problem. Unfortunately, the bounds in Proposition 3.3 depend on the descriptions involving only set difference and union, so we cannot get tight bounds for Theorem 3.4 (at least, with our current techniques) using descriptions that involve intersection and complementation. It remains an open question whether we can get tight bounds in all cases taking into account the cost of querying the oracle.

5 Conclusions

We have characterized the complexity of satisfiability for epistemic logics when the set of agents is infinite. Our results emphasize the importance of how the sets of agents are described and provide new information even in the case where the sets involved are finite.

In this paper we have focused on a language that has operators E_{G} and C_{G}. There are two interesting directions to consider extending our results.

• We could restrict the language so that it has only E_{G} operators. If the set of agents is finite (and all sets G are presented in such a way that it is easy to check if i ∈ G), then there are well-known results that show the complexity of the decision problem in this case is PSPACE complete [HM92]. However, again, this result counts E_{G} as having length |G|. Although we have not checked details, it seems relatively straightforward to combine the techniques of [HM92] with those presented here to get PSPACE completeness for L_{G}^{E}, taking E_{G} to have length 1, using the same types of oracle calls as in Theorem 3.4. (Note that Proposition 3.3 applies to the language L_{G}^{E}; we did not use the C_{G} operators in this proof.)

• We could add the distributed knowledge operator D_{G} to the language [FHMV95, FHV92, HM92]. Roughly speaking, φ is distributed knowledge if the agents could figure out that φ is true by pooling their knowledge together. Formally, we have

(M, s) ⊧ D_{G}φ if (M, t) ⊧ φ for all t ∈ ∩_{i∈G}K_{i}(s).

It is known that if A is finite (and there is no difficulty in telling if i ∈ G), then adding D_{G} to the language poses no essential new difficulties [FHMV95, HM92]. We can get a complete axiomatization, the satisfiability problem for the language with D_{G} and E_{G} operators is PSPACE complete, and once we add common knowledge, the satisfiability problem becomes exponential-time complete. Once we allow infinitely many agents, adding D_{G} introduces new subtleties. For example, even if we place no assumptions on the K_{i} relations, once we have both E_{G} and D_{G} in the language, we need to be able to distinguish between sets of cardinality one and those with larger cardinality since E_{G}p ⇔ D_{G}p is valid if and only if G is a singleton. New issues also arise once we make further assumptions about the K_{i} relations because different properties are preserved for the new agents, say K_{A^{D}} and K_{A^{E}}, which are to be added on as in Proposition 3.5 to represent D_{A} and E_{A}, respectively. Intuitively, K_{A^{E}} corresponds to the union of the relations K_{i} for i ∈ G while K_{A^{D}} corresponds to their intersection. Thus, while both K_{A^{D}} and K_{A^{E}} inherit reflexivity and symmetry from the K_{i} relations, K_{A^{D}} inherits transitivity and the Euclidean property while K_{A^{E}} does not. There are also additional relations between these agents that must be taken into account. Examples in S4 and S5 include K_{A^{E}}φ ⇒ K_{A^{D}}φ, K_{A^{E}}K_{A^{D}}φ ⇒ K_{A^{E}}φ and K_{A^{D}}K_{A^{E}}φ ⇒ K_{A^{E}}φ. These are issues for future work.

Acknowledgment: We thank an anonymous referee for his/her many detailed and useful comments on a previous version of this paper.

References

[Aum76] R. J. Aumann. Agreeing to disagree. Annals of Statistics, 4(6):1236–1239, 1976.

[Che80] B. F. Chellas. Modal Logic. Cambridge University Press, Cambridge, U.K., 1980.

[FHMV95] R. Fagin, J. Y. Halpern, Y. Moses, and M. Y. Vardi. Reasoning about Knowledge. MIT Press, Cambridge, Mass., 1995.

[FHV92] R. Fagin, J. Y. Halpern, and M. Y. Vardi. What can machines know? On the properties of knowledge in distributed systems. Journal of the ACM, 39(2):328– 376, 1992.

[FL79] M. J. Fischer and R. E. Ladner. Propositional dynamic logic of regular programs. Journal of Computer and System Sciences, 18(2):194–211, 1979.

[Gea94] J. Geanakoplos. Common knowledge. In R. Aumann and S. Hart, editors, Handbook of Game Theory, Vol. 2. Elsevier Science, 1994.

[Hal95] J. Y. Halpern. The effect of bounding the number of primitive propositions and the depth of nesting on the complexity of modal logic. Artificial Intelligence, 75(2):361– 372, 1995.

[HM92] J. Y. Halpern and Y. Moses. A guide to completeness and complexity for modal logics of knowledge and belief. Artificial Intelligence, 54:319–379, 1992.

[HvdM99] J. Y. Halpern and R. van der Meyden. A logic for SDSI’s linked local name spaces. Journal of Computer Security, 9(1,2):47–74, 2001.

[HvdMS99] J.Y. Halpern, R. van der Meyden, and F. Schneider. A logical framework for trust management. manuscript, 1999.

[RL96] R.L. Rivest and B. Lampson. SDSI — a simple distributed security infrastructure.

          at http://theory.lcs.mit.edu/∼cis/sdsi.html, 1996.