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

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 with 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.

1 Introduction

Reasoning about knowledge and common knowledge has been shown to be widely applicable in distributed computing, AI, and game theory. (See [2] 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. And in some applications in game theory and economics (where reasoning about knowledge and common knowledge is quite standard; see, for example, [1, 4]) economies are often modeled as consisting of infinitely many (even uncountably many) agents. 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.

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):

1. In the statement of the complexity result in [2], 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.

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

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

2. In the earlier proofs, it is implicitly presumed 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 need 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 may also need 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 the full paper, we 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 [8], 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 [5, 6]) 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 some of the details of the proofs of the main results (the remainder can be found in the full paper).

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}(Φ). We read K_{i}φ as “agent i knows φ”, E_{G}φ as “everyone in group G knows φ”, and C_{G}φ as “φ is common knowledge among the agents in G”. 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 [2, 7], A is taken to be the set {1, …, n}; in [7], 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 [2], G is taken to consist of all nonempty subsets of A.

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 [2].

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, serial, and transitive).^{1} 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}(Φ).

Axioms: The following are the standard axioms and rules that have been considered for knowledge.

Prop. All substitution instances of tautologies of propositional calculus.

K1. (K_{i}φ ∧ K_{i}(φ ⇒ ψ)) ⇒ K_{i}ψ, i ∈ A.

K2. K_{i}φ ⇒ φ, i ∈ A.

K3. ¬K_{i}false, i ∈ A.

K4. K_{i}φ ⇒ K_{i}K_{i}φ, i ∈ A.

K5. ¬K_{i}φ ⇒ K_{i}¬K_{i}φ, i ∈ A.

MP. From φ and φ ⇒ ψ infer ψ.

KGen. From φ infer K_{i}φ, i ∈ A.

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:

E1. E_{G}φ ⇒ K_{i}φ if i ∈ G, G ∈ 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}φ.

EGen. From φ infer E_{G}φ.

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 [2, 7]. 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.

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.

Axiom E6 (with E_{G} replaced by K_{i}) is the standard axiom used to characterize symmetric K_{i} relations [2]. 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}.

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

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 [2, 7]—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 G just consists of the singleton A. In that case, E2 becomes vacuous. Thus, while the axioms force E_{A}φ to imply that each agent in A knows φ, we have no way of expressing the converse. Indeed, as we show in the full paper, 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.

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.

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 we have defined J_{0}^{m}, …, J_{k}^{m}. Then J_{k+1}^{m} = J ∪ {G − ∪H :

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}.

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 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 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 iff |G| > 0.

• If (M, s) ⊧ φ_{G,p}, then (M, s) ⊧ ¬K_{j}p for some

j ∈ G.

• ψ_{G} is satisfiable 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 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 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.

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. In the full paper, we show that φ_{G,p} and ψ_{G} have the required properties. This clearly suffices to prove (b).

The proof of part (c) is similar in spirit to that of (b); we leave the details to the full paper.

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 the full paper. 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 and an algorithm that decides if a formula φ ∈ L_{G}^{C} is satisfiable in a structure in M_{A} (resp., M_{A}^{r}, M_{A}^{rt}, M_{A}^{rst}, M_{A}^{elt}) that runs in time 2^{c|φ|} for some constant c > 0 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 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 whether 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 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}}.) Note that |G_{φ}| ≤ |φ|.

Suppose 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 nonempty 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}. 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 (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 an algorithm that decides whether a formula φ ∈ L_{G}^{C} is satisfiable in M_{A} that runs in time 2^{c2^{|φ|}} for some c > 0.

Proof: Clearly, to check if φ is satisfiable, it suffices to check if φ^{σ} is satisfiable. In [7], 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 doubleexponential 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 φ 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, it is also 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. For K1 and MP it is just 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 doubleexponential 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 sketch the proof of Theorems 3.1 and 3.4 for M_{A}, M_{A}^{r}, and M_{A}^{rt}; we leave the proof in the case of M_{A}^{rst} and M_{A}^{elt} to the full paper. 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.

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 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: Left to the full paper.

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.

Lemma 4.3 : Suppose (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: Left to the full paper.

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 when it is clear from the context which set 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 : ∃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: Left to the full paper.

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 will 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 procedure that, given a formula φ of L_{G}^{C}, decides whether φ is satisfiable with respect to M_{A} (resp., M_{A}^{r}) and runs in time O(|A|2^{c|φ|}) for some c > 0.

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 [2, 7]. (Far more serious modifications are needed to prove the analogous result for the M_{A}^{rt}, M_{A}^{rst}, and M_{A}^{elt}; see Theorem 4.9.)

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 maximal, i.e., (a) for each formula ψ ∈ Sub(φ), either ψ ∈ s or ¬ψ ∈ s, (b) propositionally consistent (in that, for example, we cannot have all of ψ ∧ ψ′, ¬ψ, and ¬ψ′ in s), and (c) 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 we have defined S^{1}, …, S^{j}. S^{j+1} consists of all states 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. The ideas are relatively straightforward and left to the full paper.

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 [7, Theorem 6.19] using techniques developed by Fischer and Ladner [3] 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 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 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 [2, 7], 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 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}. This suffices to prove the lemma, since, by C1 and RC1, nothing is lost by our assumption that C_{G}ψ ∈ s iff E_{G}(ψ ∧ C_{G}ψ), standard propositional reasoning (using Prop and MP) shows that, for any formula ψ ∈ Sub(¬φ),

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

Negating both sides of ⇔, we get

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

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. We leave details to the full paper.

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 oberved 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 a structure 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. Let M_{A_{1}+A_{2}}^{rt} 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 and the relation K_{i} for i ∈ A_{2} are reflexive.

We can now define our translation in the case of 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}.

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

Proof: First suppose (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}(A)}. 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, τ_{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. Supppose (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} (1)

and

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

(2)

A straightforward argument by induction on structure now shows that if ψ ∈ L_{G_{φ}}^{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 (1) and (2).

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}. But 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 doing this will allow us to force the K_{i}’s 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 procedure that, given a formula φ of L_{G}^{C}, decides whether φ is satisfiable with respect to M_{A_{1}+A_{2}}^{rt} and runs in time O(|A|2^{c|φ|}) for some c > 0.

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 least 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 maximal, 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}, 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 leave the proof of correctness of the algorithm to the full paper.

Modulo the changes required because we are dealing with mixed structures, the proofs of Theorems 3.4 and 3.1 in the case of M_{A}^{rt} now proceed in much the same spirit as those for M_{A}. The details can be found in the full paper. Dealing with M_{A}^{rst} and M_{A}^{elt} introduces yet new subtleties; these too can be found in the full paper.

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. We have focused here on a logic with a common knowledge operator. What happens if we have only the E_{G} operators? Although we have not checked details, it seems relatively straightforward to combine the techniques of [7] with those presented here to get PSPACE completeness for L_{G}^{E} (even with infinitely many agents) using the same types of oracle calls as in Theorem 3.4. We are currently exploring what happens if we add the distributed knowledge operator D_{G} to the language [2, 7]. The interaction between E_{G} and D_{G} seems to add new subtleties.

References

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

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

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

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

[5] J. Y. Halpern and R. van der Meyden. A logic for SDSI’s linked local name spaces. In 12th IEEE Computer Security Foundations Workshop, 1999.

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

[7] 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.

[8] R. Rivest and B. Lampson. SDSI—a simple distributed security infrastructure. http://theory.lcs.mit.edu/∼cis/sdsi.html,