Multi-Agent Subset Space Logic

1 Introduction

The study of subset space logic (SSL) was initiated in [Moss and Parikh, 1992]. One of the main motivations of this logic is to characterize epistemic effort in a reasonably simple framework which, for various reasons, has been chosen to be a topological one. In SSL's subset models an agent is assumed to have an associated epistemic range, a set of points. The epistemic range is not fixed: it can shrink as the result of an effort by the agent. Knowledge of ϕ is interpreted as ϕ being true at all points in the current epistemic range, and thus an effort can change the agent's knowledge or ignorance. The set of possible epistemic ranges is called a subset space.

Consider the following example from [Parikh et al., 2007]. A policeman holds a radar gun to test speeding on a motorway. The accuracy of the radar gun is ±3 km/h, and the speed limit of the motorway is 120 km/h. Now a car is coming, and the radar gun shows it is running at 122 km/h. Is the car speeding or not? The policeman is not certain. However, if he used a different radar gun with accuracy ±1 km/h and read 122 km/h, he would be certain. This is captured by the SSL formula ¬K(Speeding)∧¬✷¬K(Speeding). The first conjunct says that the policeman does not know, the second that it is possible for him to know. The language of SSL is simply propositional logic extended with the modalities K and ✷.

Further investigations of SSL consider, e.g., restrictions on subset spaces [Georgatos, 1994; Dabrowski et al., 1996;

Thomas ˚Agotnes

Dept. of Information Science and Media Studies University of Bergen, Norway thomas.agotnes@infomedia.uib.no

Georgatos, 1997], or add names for points and sets to the language, making it a hybrid logic [Heinemann, 2003; 2004; 2008b; 2008a; Wang, 2009].

Despite the simplicity and flexibility of SSL, other dynamic epistemic approaches, such as public announcement logic [Plaza, 1989] and action model logic [Baltag and Moss, 2004], have received more attention in recent years. One reason might be that no satisfactory multi-agent version of SSL have existed. In this paper we aim to improve this situation.

Some attempts at multi-agent versions of SSL have been made [Bas¸kent, 2007; Heinemann, 2008b; 2010; Wen et al., 2011]. However, [Bas¸kent, 2007] and [Wen et al., 2011] both, first, have problems with the semantics of nested epistemic formulas (see Sections 3 and 6), and, second, have no known meta-logical results like completeness. [Heinemann, 2008b; 2010], on the other hand, have completeness results for logics that take multiple agents into account, but it can be argued that these approaches are not multi-agent extensions of SSL in the way standard multi-agent epistemic logic [Fagin et al., 1995] extends single-agent epistemic logic, neither syntactically nor semantically. Syntactically, these approaches add additional operators (hybrid-like, in the case of [Heinemann, 2008b]) instead of just replacing the K-operator with a Kioperator for each agent i as in standard epistemic logic (and possibly similarly for ✷). Semantically, the Ki-operators do not have the S5 properties of knowledge.

Our motivation in this paper is to study the natural and conservative extension of the original SSL language obtained by "agentizing" the K and ✷ modalities, without adding hybrid operators or other additional modalities, under the assumption that agents have S5 knowledge (as in the original SSL). Similarly to (single-agent) SSL, the language of our multi-agent SSL extends propositional logic with modalities Ki and ✷i for each agent i. This language is also used in, e.g., [Bas¸kent, 2007]. We define a semantics for multi-agent SSL, and give an axiomatization that we prove is sound and complete.

We also observe and formally show that (multi-agent) SSL has a relational aspect in the sense that every subset model corresponds to a certain multi-dimensional relational model. This observation brings SSL closer to the tradition of classical modal logic based on relational semantics. As a result, we are able to make use of well-known model theory of classical modal logic, which is helpful for further research in this field.

The idea of treating a subset model as a multi-dimensional relational model is not new: a similar approach is used in the single-agent case in [Dabrowski et al., 1996]. However, their result is weaker (not a one-to-one correspondence) and the technique used in this paper (for the multi-agent case) is fundamentally different. Dabrowski et al. [1996] also give a completeness proof for single-agent SSL, but it uses a proof technique that seems difficult to apply directly to the multiagent case or other extensions of the logic. In this paper we present a new and detailed completeness proof for the multiagent case, which is based on its relational aspect and standard modal logic techniques (the step-by-step method).

The paper is organized as follows. In the next section we briefly recall basic subset space logic. In Section 3 we propose a language and semantics for multi-agent SSL and present a sound axiomatization. In Section 4 we introduce relational semantics for multi-agent SSL, and show its correspondence to multi-agent subset semantics. The completeness proof is found in Section 5. We discuss related and future work and conclude in Section 6.

2 Background: Single-Agent SSL

We briefly recall the main concepts of (single-agent) SSL, see [Moss and Parikh, 1992; Dabrowski et al., 1996] for details. Let PROP be a countable set of propositional variables.

Definition 1 (Single-agent language) The language L is given by the following grammar rule, where p ∈ PROP:

Kϕ is intended to mean that "ϕ is known", and ✸ϕ that "there is a refinement of knowledge (e.g., new evidence) under which ϕ is true". Formally the semantics is defined as follows.

Definition 2 (Subset structures) A pair (X,O) is called a subset space, if X is a non-empty set and O ⊆ ℘(X). A subset model is a tuple X = (X,O, V ) where (X,O) is a subset space and V : PROP → ℘(X) is an valuation function. Elements of O are called open sets.

An epistemic scenario of a subset model X = (X,O, V ) is a pair (x,O) where x ∈ X is the factual state, O ∈ O is the epistemic range or evidence, and where x ∈ O.

Definition 3 Let X = (X,O, V ) be a subset model, and (x,O) an epistemic scenario of X. The satisfaction relation |= is given as follows:

SSL, an (equivalent variant of a) sound and complete axiomatization [Moss and Parikh, 1992] of subset space logic is given in Figure 1.

3 Multi-Agent Subset Space Logic

Things become more interesting and more complicated when more agents are involved. Consider the following example:

Example 1 Alice is driving a car on a motorway with a speed limit of 120km/h. The speedometer displays the speed to an accuracy of ±5 and it reads 120km/h at the moment. She knows that the police use a radar gun with accuracy ±1 km/h. Now she is stopped by a policeman with a radar gun which reads 122 km/h (which Alice does not see). The car was running at 121.5km/h. The following questions are of interest: (i) Does the policeman know that Alice was speeding? (ii) Does Alice know that the policeman knows that she was speeding? (iii) Does Alice know that the policeman knows that she knows she was speeding? (iv) Alice can replace her speedometer with a new one with an accuracy of 0 ∼ 5% (the reading is never lower than the actual speed). Is there anything Alice can do to make sure she knows she was speeding whenever the policeman knows she was speeding (so that she will never get into trouble)?

The first question is a simple statement of the type that was mentioned in the introduction, which single-agent SSL can be used to reason about. The other questions, however, are multi-agent ones. The fourth question relates to knowledge update by effort. In multi-agent SSL, we must be able to reason about nested knowledge, like in questions 2-4.

A natural modeling attempt is to define a multi-agent subset model as a structure X = (X,O0, . . . , On-1, V ) which differs from a single-agent subset model only in that it includes a set of open sets for each agent. An epistemic scenario becomes (x, O0, . . . , On-1) such that x ∈ O0 ∩ · · · ∩ On-1. Then, the definition of satisfaction can be extended in the natural way. This attempt appears in [Wen et al., 2011, Section 4.2]. However, there is a problem: the truth value of a nested formula of the form KiKjϕ is in fact not well defined. For consider in the above example that Alice knows that the policeman knows that she was speeding, denoted by K0K1(Speeding). To verify X, x,O0, . . . ,On-1 |= K0K1(Speeding), we need to check whether X, y, O0, . . . , On-1 |= K1(Speeding) for all y ∈ O0. Now, observe that y ∈ O0 does not necessarily mean that y ∈ O1, which means that (y,O0, . . . ,On-1) is not necessarily an epistemic scenario as defined above. But we do need the condition y ∈ O1, to interpret K1(Speeding) (it makes no sense in SSL to have a factual state outside an epistemic range).

Bas¸kent [2007] proposes two different semantics for the language of multi-agent SSL based on the above defined multi-agent subset models, which avoid the problem mentioned above. In the first of these, knowledge is interpreted in the following way: X, x,O0, . . . ,On-1 |= Kiϕ iff ∀y ∈ O0 ∩ · · · ∩ On-1. X , y, O0, . . . , On-1 |= ϕ. This does avoid the problem that the factual state falls outside of an epistemic range, however, with the cost that any formula of the form KiKjϕ ↔ KjKiϕ is valid, which is unlike in standard epistemic logic and arguably gives a much less intuitive and interesting logic. The second approach in [Bas¸kent, 2007] has a similar problem.

A natural solution to these problems is to increase the order: to define a multi-agent subset space as a tuple (X,O) for each agent, where O ⊆ ℘(℘(X)) (instead of O ⊆ ℘(X) as for single-agent subset space), such that O forms a set of partitions of X. An update of an individual's knowledge can then be modeled as refinement of a partition for that agent. This setting will be referred to as partition semantics. As we shall see, partition semantics allows us to model multiagent nested S5 knowledge in the correct way. In the singleagent case, the relationship between partition semantics and the classical SSL semantics is just like the relationship between using equivalence classes and using universal relations in a relational model for interpreting the modal logic S5; see [Hughes and Cresswell, 1996, p. 61]. It is not hard to see that single-agent SSL is equivalently interpreted in either semantics, for in the partition semantics: i) since each agent has a set of partitions there can be multiple open sets available to model different epistemic scenarios, and ii) all the equivalence classes other than the current one in every partition are redundant. To sum up, our proposed partition semantics is equivalent to the standard SSL subset semantics for singleagent SSL but is suitable for multi-agent SSL as well.

We now formally define the language, semantics and axiomatization of multi-agent SSL. They are very natural extensions of single-agent SSL. After that, we introduce an equivalent relational semantics for multi-agent SSL, which we use to prove completeness.

Language and Semantics

We still let PROP be a countable set of propositional variables. Let N be the set of all agents. We assume that N is a finite nonempty set, and abuse notation by both treating it as a natural number N ≥ 1 and a set N = {0, . . . , N - 1}.

Definition 4 (Multi-agent language) The language Lm is given by the following rule, where p ∈ PROP and i ∈ N:

As usual, we write ˆKiϕ for ¬Ki¬ϕ, and ✸iϕ for ¬✷i¬ϕ.

We now propose a semantics for this language in terms of multi-agent subset models, based on partition semantics.

Definition 5 (Multi-agent subset models) A multi-agent subset model is a tuple (X, O, V ) where

• X is a non-empty set;
• O : N → ℘(℘(℘(X))) assigns to every agent a set of partitions of X; we write Oi for O(i);
• V : PROP →℘(X) is an valuation function.

The set of all multi-agent subset models is denoted by Sub.

Given a multi-agent subset model X = (X,O, V ), a profile of X is a function O : N → ℘(℘(X)) such that O(i) ∈ Oi. We write Oi for O(i). Here, an epistemic scenario is a pair (x, O) such that x ∈ X and O is a profile. We introduce the following notation when O and U are profiles:

The notation [x]Oi will be used in a more general form: [x]P , where P is any partition. Moreover, the relation ⪯ is a partial order as the notation already suggests.

Definition 6 (Multi-agent subset semantics) Let X be a multi-agent subset model, and (x,O) an epistemic scenario of X :

We write X |= ϕ, if X, (x,O) |= ϕ holds for all epistemic scenarios (x,O). In a similar fashion, we can define the validity of ϕ in a multi-agent subset space (X,O) (notation: X, O |= ϕ), and so on.

As we have already argued, when N = 1, the multi-agent subset semantics is equivalent to the original subset semantics.

Let us formalize Example 1. Let 0 and 1 be Alice and the policeman respectively. Let X = (R+,O, V ), with O0 = {O0, U0} and O1 = {O1}, where O0 = {(114, 126), R+ \ (114, 126)}, O1 = {(121, 123), R+ \ (121, 123)}, and U0 = {(114, 120), [120, 126), R+ \ (114, 126)}; and V such that V (Speeding) = (120, +∞). The current epistemic scenario is (121.5, {〈0,O0〉, 〈1,O1〉}). Whether the formulas K1(Speeding), K0K1(Speeding), K0K1K0(Speeding) and ✸0(K1(Speeding) → K0(Speeding)) are true in this situation represents the questions in Example 1. It is an easy exercise to check that these are true, false, false, and true, respectively. For the truth of the last formula, U0 represents the result of an effort (replacing the speedometer) by which K0(Speeding) becomes true.

Axiomatization

The axiomatization SSLm for multi-agent subset space logic is given in Figure 2. SSLm contains multi-agent versions of all axioms and rules of SSL, in addition to three axiom schemata for characterizing (non-)interaction between dimensions. They are in two groups: COM for commutativity, and ChR for Church-Rosser. We do not need ChR·◦ , i.e. ˆKi✷jϕ → ✷j ˆKiϕ where j ̸= i, as an axiom, because it can be derived in SSLm. It is clear that SSLm coincides with SSL when restricted to a single agent.

Theorem 1 (Soundness) Every SSLm-theorem is valid in the class of all multi-agent subset models.

4 Relational Correspondence

We now define an equivalent relational semantics for multiagent SSL. We first define a class of relational models called R-models and their interpretation of Lm, define a strict subset of them called R+-models, and then show that R+-models one-to-one correspond to multi-agent subset models. Thus, we are capable of investigating subset space logic in terms of relational structures, and by doing so, conditions lying in the "point-set" structure become frame conditions over relational structures. The correspondence result will be fundamental in the completeness proof of SSLm in Section 5.

The idea of treating SSL relationally can be traced back to [Dabrowski et al., 1996]. Section 2.3 of [Dabrowski et al., 1996] introduces the notion of a "cross axiom model", which is based on the relational semantics. But this notion is defined only for the purpose of achieving decidability. Technically, every subset model can be truth-preservingly translated into a cross axiom model, but not necessarily vice versa, the direction which we are more interested in, for the sake of the completeness proof. With a one-to-one correspondence, we will get an alternative, relational, semantics for SSL.

Definition 7 (R-structures) An R-frame is a tuple (M, ∼, ▷ ) where

• M = Y × U0 × · · · × UN-1 is an (N + 1)-dimensional non-empty domain such that Y is an arbitrary non-empty set and every Ui (0 ≤ i ≤ N - 1) is a set of partitions of Y ; an element of M is called a state and is denoted by a pair (x, O) where x ∈ Y and O ∈ U0 × · · · × UN-1; we write Oi for the projection of O on Ui.
• ∼: N → ℘(M 2 ) assigns to every agent i an equivalence relation, ∼i, on M such that {{(y, O) | y ∈ [x]Oi } | (x, O) ∈ M} is the set of all ∼i-equivalence classes, or in other words, (x, O) ∼i (y, U) iff O = U and y ∈ [x]Oi ;
• ▷: N → ℘(M 2 ) assigns to every agent i a reflexive transitive relation, ▷i, on M such that:
• ▷i links only states variant in Ui; i.e., (x,O) ▷i (y,U) implies x = y and ∀j.(j ̸= i ⇒ Oj = Uj);
• ▷i is indifferent along Y ; i.e., for all x, y, O, U, (x, O) ▷i (x,U) implies (y,O) ▷i (y,U);
• ▷i is indifferent along Uj (j ̸= i); i.e., for all x, y,O, U, j, if (x, (Oj,-)) ▷i (y, (Oj,-′ )) then (x, (Uj,-)) ▷i (y, (Uj , -′ )), where the symbols - and -′ stand for other

components of the vectors;

M = (F, V ) is called an R-model (based on F) if F is an R-frame and V : PROP →℘(M) is an evaluation function.

By the definition of ▷, it makes sense to use the notation O ▷i U where O and U are elements of U0 × · · · × UN-1.

Definition 8 (R+-models) An R+-model (M, ∼, ▷, V ) is an R-model that is first-component evaluated (1CE) and fully designated (FD), as defined below:

(1CE) Evaluation is determined by the first component of a state, i.e, (x, O) ∈ V (p) ⇔ (x, U) ∈ V (p);

The set of all R+-models is denoted by R+.

An example of an R+-model can be found in Figure 3.

Definition 9 (R+-Sub-translation) We define a translation ρ : R+ → Sub as follows. Let M = (Y × U0 × · · · × UN-1,∼,▷, V ) be an R+-model. Its translation ρ(M) is a multi-agent subset model (X,O, ν) such that X = Y , Oi = Ui for all i ∈ N, and ν(p) = {x | (x, O) ∈ V (p) & O ∈ U0 × · · · × UN-1} for all p ∈ PROP.

Definition 10 (Sub-R+-translation) We define a translation σ : Sub → R+ as follows. Let X = (X,O, V ) be a multi-agent subset model. Its translation σ(X) is an R+- model (M, ∼, ▷, µ) defined below:

• M = X ×O0 × · · · ×ON-1;
• ∀i ∈ N, ∼i= {((x, O), (y, O)) ∈ M ×M | {x, y} ⊆ Oi};
• ∀i ∈ N, ▷i= {((x, O), (x, U)) ∈ M ×M | O ⪰i U}, i.e., for any profiles O and U, O ▷i U iff O ⪰i U;
• ∀p ∈ PROP, µ(p) = {(x, O) | x ∈ V (p) & O is a profile}.

Definitions 9 and 10 are well defined. Namely, given M an R+-model, ρ(M) is a multi-agent subset model; and given X a multi-agent subset model, σ(X) is an R+-model. It is easy to see that a state of an R+-model is itself an epistemic scenario in a corresponding multi-agent subset model.

Theorem 2 (R+-Sub-correspondence) For any multiagent subset model X and any R+-model M:

Thus, ρ and σ are both bijective functions, and they are the inverse functions of each other. An illustration of the R+- Sub-correspondence is given in Figure 3.

Definition 11 (R-satisfaction) Let M = (M,∼,▷, V ) be an R-model and a be a state of M.

M, a ⊩ p iff a ∈ V (p) M, a ⊩ ¬ϕ iff M, a ⊮ ϕ M, a ⊩ ϕ∧ψ iff M, a ⊩ ϕ & M, a ⊩ ψ M, a ⊩ Kiϕ iff ∀b ∈M.(a ∼i b ⇒M, b ⊩ ϕ)

Theorem 3 (Semantic correspondence) Let M be an R+- model and X be a multi-agent subset model. Then, for any formula ϕ,

1. For any state (x, O), M, (x, O) ⊩ ϕ iff ρ(M), x, O |= ϕ;
2. For any epistemic scenario (x,O) of X, X, x,O |= ϕ iff σ(X ), (x, O) ⊩ ϕ.

Corollary 1 If a set of formulas is satisfiable in an R+- model, then it is also satisfiable in a multi-agent subset model.

5 Completeness

Completeness proofs for subset space logics turn out to be non-trivial [Dabrowski et al., 1996]. In short, the canonical model method fails (already in the single-agent case it turns out to be difficult to define the set of open sets in the canonical subset model). A well known general technique for such cases is the step-by-step method (see, e.g., [Blackburn et al., 2001, Chapter 4]). Compared with the completeness proof in [Dabrowski et al., 1996] for single-agent SSL, which seems difficult to extend directly, we here instead show a completeness result with respect to R+, which is equivalent to the completeness of SSLm with respect to Sub by the correspondence results in Section 4. The proof makes use of the standard step-by-step method for the relational semantics, which makes it clearer and more adaptable than a more ad-hoc proof. The method constructs a "canonical" model via a "network" construction, which is not a proper canonical model but shares some similarities.

We say Φ is consistent if Φ ⊬ ⊥, and inconsistent otherwise. Furthermore, Φ is maximal consistent if Φ is consistent and there is no consistent Ψ such that Φ ⊂ Ψ. The set of all maximal consistent sets of formulas is denoted by MCS, and if Φ ∈ MCS, then we also say Φ is an MCS. For any agent i, we define ∼ci as a binary relation on MCS such that Φ ∼ci Ψ iff ∀ϕ ∈ Lm.(Kiϕ ∈ Φ ⇒ ϕ ∈ Ψ). Similarly, ▷ci is defined to be a binary relation on MCS such that Φ ▷ci Ψ iff ∀ϕ ∈ Lm.(✷iϕ ∈ Φ ⇒ ϕ ∈ Ψ). These two relations will serve as "canonical relations" for our "canonical" R+-model.

Proposition 1 Given i ∈ N and Φ, Ψ ∈ MCS:

1. ∼ci is an equivalence relation, and ▷ci is a reflexive transitive relation;
2. Φ ▷ci Ψ implies ∀p ∈ PROP.(p ∈ Φ ⇔ p ∈ Ψ).

What normally follows now is to show an existence lemma. However, in our multi-dimensional setting with extra conditions on the frames, we need a quite sophisticated existence lemma. Intuitively, a "canonical" R+-model is like a hypercube whose vertices are labeled by MCSs and edges by canonical relations. The question is whether we are able to label all the vertices and edges coherently. While there are general methods in the literature which are of help, we face the new problem of labeling the last vertex of the hypercube. To handle this problem, we now define the concepts of MCS-s-cubes and completing vertices before stating the existence lemma. The vertices and edges of an s-dimensional hypercube will be called an s-cube.

Definition 12 (MCS-s-cubes) For an s ∈ N with s ≥ 2, an MCS-s-cube is an s-cube that forms an R+-frame such that:

1. Each of its vertices is an MCS;
2. (Undirected) edges in the first dimension are labeled by a set of agents and reflect ∼ci -relations for all agents i;
3. (Directed) edges in the j-th dimension, with 2 ≤ j ≤ s, are all labeled by j and reflect the ▷cj-2 -relation;
4. The property FD is satisfied;
5. All the ▷cx -relations indeed link related vertices.

In the above definition we choose to say that a vertex is an MCS instead of that an MCS labels a vertex. This is not an essential difference. An MCS-s-cube is an R+-frame in the usual sense, and it is of a special type where all edges are indeed connected by a ∼cA- or ▷ci -relation. We mention here that the "canonical" R+-model that we will build meets this requirement.

Definition 13 (Completing vertices) A completing vertex of an MCS-s-cube is a vertex such that:

1. If it is a part of a face 1 with two ∼ci -lines and two ▷ci - arrows as edges, then it has an outgoing ▷ci -arrow; and
2. If it is a part of a face with two ▷ci - and two ▷cj -arrows as edges, then it is not the input, i.e., the vertex where both arrows are outgoing.

Completing vertices always exist in a cube.

Lemma 1 (Existence) Let i, j ∈ N such that i ̸= j, and Φ,Ψ, Ξ ∈ MCS, then

1. ˆKiϕ ∈ Φ⇒ ∃Ψ.(ϕ ∈ Ψ&Φ ∼ci Ψ);
2. ✸iϕ ∈ Φ implies ∃Ψ.(ϕ ∈ Ψ & Φ ▷ci Ψ);
3. ∃Γ.(Φ ▷ci Γ ∼ci Ψ) implies ∃∆.(Φ ∼ci ∆▷ci Ψ);
4. ∃Γ.(Φ ∼ci Γ ▷cj Ψ) iff ∃∆.(Φ ▷cj ∆∼ci Ψ);
5. ∃Γ.(Φ ▷ci Γ ▷cj Ψ) iff ∃∆.(Φ ▷cj ∆▷ci Ψ);
6. Φ ∼ci Ψ&Φ ▷cj Ξ implies ∃Γ.(Ψ ▷cj Γ &Ξ ∼ci Γ);
7. Φ ▷ci Ψ&Φ ▷cj Ξ implies ∃Γ.(Ψ ▷cj Γ &Ξ ▷ci Γ);
8. If there is a possible MCS-s-cube with only one completing vertex unfinished, then there exists an MCS which can be filled in as the last vertex so as to form an MCS-s-cube.

We now define the notion of a perfect network for a given consistent set Φ of formulas. It is then used to induce a satisfying "canonical" model for Φ, by the use of the existence lemma, which gives us completeness.

1 A face (a.k.a. a 2-dimensional face) of a hypercube is a standard concept in elementary geometry. It is different from a 2-cube, in the sense that a 2-cube is restricted to a single agent whereas a face of a hypercube can have relations for multiple agents.

Definition 14 (Network) A network for multi-agent SSL is a tuple (M,∼,▷, l), where (M,∼,▷) is an R-frame, and l : M → MCS a labeling function.

A network (M,∼,▷, l) is called coherent, if satisfies:

• (C1) For all a, b ∈ M, a ∼i b ⇒ l(a) ∼ci l(b) and a ▷i b ⇒ l(a) ▷ci l(b);
• (C2) The R-frame (M,∼,▷) satisfies FD (see Def. 8);
• (C3) For any x and i, the structure ({(x, (Oi,-)) | oi ∈ Mi+2},▷i) is a weakly-connected directed graph, i.e., it becomes a connected undirected graph when all of its ▷i-edges are replaced with undirected edges.

A network (M,∼,▷, l) is called saturated, if for all a ∈ M and all ϕ ∈ Lm:

• (S1) ˆKiϕ ∈ l(a) implies ∃b ∈M. (a ∼i b&ϕ ∈ l(b)), and (S2) ✸iϕ ∈ l(a) implies ∃b ∈ M. (a ▷i b & ϕ ∈ l(b)).

A network is called perfect, if it is coherent and saturated. µ = (M,∼,▷, l) is called a perfect network for a set Φ of formulas, if it is perfect and there is an a ∈ M with Φ ⊆ l(a).

Definition 15 (Defects) Let µ = (M,∼,▷, l) be a network. An S1-defect of µ consists of a designated point a ∈ M and a formula ˆKiϕ ∈ l(a) such that ¬∃b.(a ∼i b & ϕ ∈ l(b)). An S2-defect of µ consists of a designated point a ∈ M and a formula ✸iϕ ∈ l(a) such that ¬∃b.(a ▷i b & ϕ ∈ l(b)).

Let µ = (M,∼,▷, l) be a network. The R-model Mµ = (M,∼,▷, Vµ) with Vµ(p) = {a ∈ M | p ∈ l(a)} for all p ∈ PROP, is called the µ-induced R-model. The following lemma states the key steps of the step-by-step method. In particular, it defines our "canonical" R+-model.

Lemma 2 (Step-by-step method) Let µ be a network and M the µ-induced R-model. Let Φ be a set of formulas.

1. If µ is coherent, thenM is an R+-model;
2. If µ is perfect, then ∀ϕ∀a.(M, a ⊩ ϕ⇔ϕ ∈ l(a));
3. If there is a perfect network for Φ, then Φ is satisfiable in an R+-model;
4. (Repair lemma) If µ is finite and coherent, and let D be a defect of it, then there is a finite coherent network µ′ extending µ, such that D is not a defect of µ′ .
5. Φ is consistent iff there is a perfect network for Φ;
6. SSLm is strongly complete wrt. the class of all R+-models. We get the following from Lemma 2(6) and Corollary 1.

Theorem 4 (Completeness) SSLm is strongly complete with respect to the class of all multi-agent subset models.

6 Discussion

In this paper we have proposed a multi-agent version of subset space logic (SSL), which is a natural extension of singleagent SSL. As discussed earlier, the few existing attempts at multi-agent SSL are, in our view, unsatisfactory solutions to the problem we solve. In [Bas¸kent, 2007] any formula of the form KiKjϕ ↔ KjKiϕ is valid, unlike in standard epistemic logic. In [Wen et al., 2011], the truth value of a formula of the form KiKjϕ is in fact not even defined. The semantics we have proposed in this paper is well defined, it gives the standard meaning to nested knowledge, and its singleagent restriction is equivalent to the original SSL. Heinemann [2008b; 2010] obtain completeness results by extending the language with other operators (unlike in this paper), where agents do not have S5 knowledge, which are conceptually significant differences compared to the original SSL. We also introduced a relational semantics, which we used to show a correspondence between (multi-agent) SSL and a classical multi-dimensional modal logic. This brings SSL closer to classical modal logic, so that many existing techniques are now at hand. In particular, we are able to use the step-by-step method to show completeness.

There are several recent works on the relationship between public announcement logic (PAL) [Plaza, 1989] and SSL. W´ang and ˚Agotnes [2013] give a completeness proof for (single-agent) PAL interpreted in (single-agent) subset models. They make use of a corresponding relational semantics, but only for the single-agent case, which does not seem to be easily extended to the multi-agent case. The (single-agent) completeness result and technique in [W´ang and ˚Agotnes, 2013] share some similarities but is fundamentally different from the ones in the current paper. Balbiani et al. [2013] add public announcement operators to a (non-standard) variant of SSL, and completeness of an axiomatization is shown, but again only in the single-agent case. There is no clear direct relationship to the results or the techniques in the current paper. However, there is an interesting conceptual relationship here, as follows. The logic we have studied in this paper uses multi-agent versions of operators both for knowledge and for refinement, i.e., Ki and ✷i. An agent-independent operator for refinement would also be interesting. For example, instead of talking about "agent 1 can come up with evidence so that agent 2 gets to know p" (✸1K2p), it also makes sense to talk about "there is new evidence so that agent 2 gets to know p", which we can denote by ✸K2p. This ✸ operator is more-or-less related to the ✸ operator in arbitrary public announcement logic [Balbiani et al., 2008] which can be read as "there is a public announcement such that ...". Balbiani et al. [2013] study such operators in their subset space setting. We consider using the framework developed in this paper to extend the work on public announcements in the SSL setting in [W´ang and ˚Agotnes, 2013; Balbiani et al., 2013] to the multi-agent case a very interesting direction for future work. Also interesting for future work is incorporating group notions of knowledge into multi-agent SSL, and we believe the framework developed in this paper will help doing that. Another direction is to further extend other variants of SSL, e.g., with restrictions on subset spaces [Georgatos, 1994; Dabrowski et al., 1996; Georgatos, 1997], to the multi-agent case.

Acknowledgments

Y`ı W´ang gratefully acknowledges funding support from the Major Project of National Social Science Foundation of China (No. 11&ZD088). Thomas ˚Agotnes is also affiliated with Southwest University, China, and Bergen University College, Norway.