# multiagent_only_knowing_on_planet_kripke__f372b894.pdf

Multi-Agent Only Knowing on Planet Kripke

Guillaume Aucher University of Rennes 1 INRIA Rennes, France guillaume.aucher@irisa.fr

Vaishak Belle

Dept. of Computer Science KU Leuven Leuven, Belgium vaishak@cs.kuleuven.be

The idea of only knowing is a natural and intuitive notion to precisely capture the beliefs of a knowledge base. However, an extension to the many agent case, as would be needed in many applications, has been shown to be far from straightforward. For example, previous Kripke frame-based accounts appeal to proof-theoretic constructions like canonical models, while more recent works in the area abandoned Kripke semantics entirely. We propose a new account based on Moss characteristic formulas, formulated for the usual Kripke semantics. This is shown to come with other benefits: the logic admits a group version of only knowing, and an operator for assessing the epistemic entrenchment of what an agent or a group only knows is definable. Finally, the multi-agent only knowing operator is shown to be expressible with the cover modality of classical modal logic, which then allows us to obtain a completeness result for a fragment of the logic.

1 Introduction

Suppose a modeler were to provide a collection of logical sentences Σ as a knowledge base to characterize an agent. One would expect that the beliefs of the agent would be exactly those that follow from Σ.1 However, in classical epistemic logic [Fagin et al., 1995], Kα does not preclude K(α β) from holding in general. So unless Σ carefully includes both the beliefs and non-beliefs of the agent, it is not the case the KΣ can succinctly characterize all the beliefs of the agent. In this regard, the idea of only knowing is a natural and intuitive notion to precisely capture the beliefs of a knowledge base. First introduced by Levesque [1990], it enriches classical epistemic logic with a new operator O, the idea being Op holds precisely when the worlds considered possible by the agent are all and only those where p holds. So, Op Kp and more interestingly, Op Kq. For knowledge-based agents,

Partially funded by the FWO project on Data Cleaning and KU Leuven s GOA on Declarative Modeling for Mining and Learning. 1In this work, we do not differentiate between knowledge and belief , and use these terms interchangeably.

in particular, this seems like the right kind of modality to include in our language. And indeed, it is very closely related to important concepts such as minimal knowledge [Halpern and Moses, 1984]. The main difference being that the logic of only knowing includes the O modality in the language, whereas in [Halpern and Moses, 1984], knowledge minimization is purely a meta-theoretic concept; so, only knowing has some advantages. Somewhat surprisingly, extending only knowing s simple semantics to the many agent case has been far from straightforward. Independently, Halpern [1993] and Lakemeyer [1993] attempted extensions, but these were shown to exhibit unintuitive properties [Halpern and Lakemeyer, 2001]. In later work, Halpern and Lakemeyer [2001] do manage to capture only knowing, but by appealing to prooftheoretic constructs such as canonical models in the semantics. (Canonical models, moreover, which are based on sets of maximally consistent sets of formulas, are also perhaps not realizable in practice.) The approach of Waaler and Solhaug [2005] was based on model-theoretic constraints, which as the authors admit, is complex and hard to penetrate . Finally, in more recent work, Belle and Lakemeyer [2010] show how the proof-theoretic construction of [Halpern and Lakemeyer, 2001] can be avoided to naturally capture multi-agent only knowing, but at the cost of introducing a semantics that significantly deviates from the classical (that is, Kripke) account. The purpose of this paper is to revisit the notion of multiagent only knowing, but to phrase the truth conditions in terms of the usual Kripke framework in a natural way, that is, by avoiding canonical models and other proof-theoretic machinery. There are several reasons why this is being attempted. Formulating the account in a more familiar truth theory has the advantage that deep results known in other areas of modal logic can finally be put in the context of only knowing. Indeed, as one would observe, the basis for our reconstruction is Moss investigation into normal forms [Moss, 2007], which itself is inspired by and builds on the seminal work of Fine [1975]. Second, we show how the multi-agent only knowing modality developed here can be expressed in terms of the cover modality [D Agostino and Lenzi, 2005], which is intimately connected to co-algebras and their role in central results on modal logic, such as interpolation and Beth definability. In the longer term, a multi-agent only know-

Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence (IJCAI 2015)

ing framework in classical modal logic would be more accessible for dynamic epistemic logic based knowledge representation languages [Demolombe, 2003; Herzig et al., 2000; van Ditmarsch et al., 2011]. In sum, only knowing is arguably an essential companion to the classical knowledge operator in AI applications, and the work considered here would allow modal logicians to use it more readily.

The paper is organized as follows. In Section 2, we recall the essentials of epistemic logic and characteristic formulas, as introduced by Moss, together with some related results used in the sequel. Then, in Section 3, we define our logic with our specific truth conditions for the multi-agent only knowing connectives which use the characteristic formulas. In Section 4, we compare and relate formally our logic and our definition of multi-agent only knowing with the recent approach proposed by Belle and Lakemeyer [2010]. In Section 5, we present the cover modality and establish formally its connection with our multi-agent only knowing modality. This allows us in Section 6 to axiomatize the validities of our logic once it is extended with the cover modality. We discuss other related efforts in Section 7 before concluding.

2 Preliminaries In this section, we first recall the basics of epistemic logic. Then, we introduce the characteristic formulas for modal logic as defined by Moss and recall a number of results about these formulas that will be used in the rest of the article.

2.1 Epistemic Logic In the rest of the paper, P is a set of propositional letters called atomic facts and A is a finite set whose elements are called agents. Definition 1 (Language L). We define the language L inductively as follows.

ϕ ::= p | ϕ | (ϕ ϕ) | K jϕ | CGϕ

where G A, j A and p P. In the sequel, we use the following abbreviations:

Kjϕ; b Kjϕ Kj ϕ; c CGϕ CG ϕ

Let ϕ L. The modal depth of ϕ, denoted d(ϕ), is defined inductively as follows: d(p) = 0, d(ϕ ψ) = max{d(ϕ), d(ψ)}, d( ϕ) = d(ϕ), d(Kjϕ) = d(ϕ) + 1 and d(CGϕ) = d(ϕ) + 1. The set of propositional letters appearing in ϕ is denoted P(ϕ).

The formula Kjϕ reads as agent j Knows ϕ . Dually, the formula b Kjϕ reads as agent j considers it possible that ϕ holds . The formula EGϕ reads as everybody in group G knows that ϕ holds . Common knowledge of ϕ means that everybody knows that ϕ but also that everybody knows that everybody knows ϕ, that everybody knows that everybody knows that everybody knows ϕ, and so on ad infinitum. Formally, this corresponds to the following formula CGϕ := EGϕ EGEGϕ EGEGEGϕ . . . , and is infinitary in nature. But as we do not allow infinite conjunction, the common knowledge operator is introduced as a primitive connective in our language.

PL Axioms and Inference Rules of Prop. Logic Dist Kj(ϕ ψ) (Kjϕ Kjψ) E EAϕ

Mix CAϕ EA(ϕ CAϕ) Ind if ϕ EA(ψ ϕ) then ϕ CAψ

Figure 1: Proof System L for L

A (pointed) epistemic model (M, w) represents how the actual world represented by w is perceived by the agents. Atomic facts are used to state properties of this actual world.

Definition 2 (Epistemic model). An epistemic model is a tuple M = (W, R, V) where:

W is a non-empty set of possible worlds,

R : G 2W W is a function assigning to each agent

j G an accessibility relation on W,

V : Φ 2W is a function assigning to each proposi-

tional letter of Φ a subset of W. V is called a valuation.

We write w M for w W, and (M, w) is called a pointed epistemic model (w often represents the actual world). If w, v W, we write w Rjv for R(j)(w, v). Finally, we write

Intuitively, in the definition above, v R j(w) means that at w, the agent j believes that v might be the real world.

The truth conditions of Kjϕ are defined in such a way that Kjϕ holds in a possible world when ϕ holds in all the worlds agent j considers possible.

Definition 3 (Truth conditions). Let M be an epistemic model, w M and ϕ L. Then, M, w |= ϕ is defined inductively as follows:

M, w |= p iff w V(p) M, w |= ϕ iff M, w |= ϕ M, w |= ϕ ψ iff M, w |= ϕ and M, w |= ψ M, w |= K jϕ iff for all v R j(w), we have M, v |= ϕ M, w |= CGϕ iff for all v RG(w), we have M, v |= ϕ

We write M |= ϕ when M, w |= ϕ for all w M, and |= ϕ when for all epistemic models M, M |= ϕ. In that latter case, we say that ϕ is L-valid.

The following theorem shows that the set of validities of L can be axiomatized by the proof system L.

Theorem 1. The proof system L for L defined in Figure 1 is sound and strongly complete for L w.r.t. the class of epistemic models.

2.2 Characteristic Formulas

We will resort in our definitions and proofs to particular kinds of modal formulas which capture the structure of epistemic models (modulo bisimulation) up to a given modal depth. These formulas were defined by Moss [2007] and are very similar to the normal forms for modal logic as introduced by Fine [1975].2

In what follows, we use S and E, possibly decorated with superscripts and subscripts, to denote sets of formulas. The subscripts refer to constructions using inductive definitions. When the superscript is an agent index j or the group G, it means that the formulas in the set are in the context of Kj and CG respectively.

Definition 4. [Moss, 2007] Let P P be finite. We inductively define the sets EP n as follows:

p P S 0 p S 0 P

EP n+1 = ( δ0

δ0 EP 0 and S j n, S G n EP n

An element δ of EP n with n > 0 will often be written as follows (note that the S j n are replaced by Rj(δ) and the S G n are replaced by RG(δ)):

δj Rj(δ) b Kjδj K j _

δj R j(δ) δ j

δG RG(δ) c CGδG CG _

δG RG(δ) δG

Basically, a characteristic formula δn+1 provides a complete syntactic representation of a pointed epistemic model up to modal depth n + 1. So, intuitively, if we view a characteristic formula δn+1 of EP n+1 as the syntactic representation up to modal depth n + 1 of a possible world w where it holds, a formula δn of S j n can also be viewed as a syntactic representation up to modal depth n of a possible world accessible by R j from w. The following proposition not only tells us that a formula δn completely characterizes the structure up to modal depth n of any pointed epistemic model where it holds (first item), but also that the structure of any epistemic model up to modal depth n can be characterized by such a δn (second item).

Proposition 1. [Moss, 2007] Let P P be finite, let n N and let δ EP n . Let ϕ L such that d(ϕ) n and P(ϕ) P.

2Halpern and Lakemeyer [2001] discuss a similar normal form in the context of only knowing.

Then, the following hold:

Either |= δ ϕ or |= δ ϕ.

The following corollary is also used in the sequel. It states that any formula can be reduced to a disjunction of δs. (Thus, they are referred to as normal forms.) The decomposition of a formula ϕ into δs syntactically (and precisely) captures the relevant structure of the set of pointed epistemic models which make ϕ true. Put differently, each δ can be seen as a syntactic description of the modal structure (up to depth n and modulo bisimulation) of a pointed epistemic model which makes ϕ true.

Corollary 1. Let ϕ L and let k N. Let P := P(ϕ) and let n = d(ϕ) + k. Then, there is S ϕ n = {δ1 n, . . . , δm n } EP n such that

Moreover, for each n, this set S ϕ n is unique.

3 Defining Multi-Agent Only Knowing

We define our logic for multi-agent only knowing in two steps. First, we define a language where we cannot nest the multi-agent only knowing connectives. Then, we generalize it to allow for an arbitrary nesting of these connectives.

3.1 A Constrained Logic

The class of models for our first logic is the class of epistemic models. Only the syntax of the logical language and the truth conditions change, because the language is extended with only knowing operators. Our first language is in fact an extension of the language ONL n of Belle and Lakemeyer [2010], in the sense that no connector Ok j or Ok G may occur in the scope of a Kj, a Ok j or a Ok G.

Definition 5 (Language LO G ). We define the languages LO G inductively as follows.

ϕ ::= p | ϕ | (ϕ ϕ) | K jϕ | Ok jψ | CGϕ | Ok Gψ

where ψ L, k N, G Agt, j A, and p P. The formulas Ojϕ and OGϕ are abbreviations for O0 jϕ and O0 Gϕ respectively.

The formula Ok jψ reads the agent j only believes (knows) ψ up to degree k and the formula Ok Gψ reads the group of agents G only believes (knows) ψ up to degree k .

Definition 6 (Truth conditions for LO G ). The satisfaction relation |= between pointed epistemic models and formulas of LO G is defined inductively as follows. The basic case as well as the cases for the connectives , , Kj and CG are defined like in Definition 3. We only define the cases for Ok j and Ok G. Let M be an epistemic model, w M and let ψ L. Let

n = k + d(ψ) and let X A 2A. Then,

M, w |= Ok Xψ iff for all v RX(w) there is δ S ψ n such that M, v |= δ, and for all δ S ψ n there is v RX(w) such that M, v |= δ

We recall that the finite set S ψ n = {δ1, . . . , δm} EP n (where P = P(ψ)) is such that |= ψ _

Let ϕ LO G . We write M |= ϕ when M, w |= ϕ for all w M, and |= ϕ when for all epistemic models M, M |= ϕ.

The intuition underlying our definition of the truth condition for our multi-agent only knowing operator can be explained as follows. As noted in the previous section, each δ of S ψ n can be seen as a syntactic description of the modal structure (up to depth n and modulo bisimulation) of a pointed epistemic model which makes ψ true. So, the agent (or the group of agents) only knows ψ if she considers possible all and only the possible worlds that make ψ true, disregarding the structure of these worlds after a certain depth k: the bigger k is, the more entrenched this knowledge will be. Note that if we restrict our setting to the propositional case with a single agent, then we recover the original definition of only knowing as defined by Levesque [1990]. Importantly, note that we do not need to resort to an operator Njϕ like in the usual definitions of multi-agent only knowing. Instead, we refer in the semantics to characteristic formulas and our only knowing operator is introduced here as a primitive connective.

Example 1. One would think that this constrained language is little more than the single agent version, that is, formulas such as Oip Kiq are the only interesting valid sentences in this logic. In fact, this language can be used to capture multiagent autoepistemic defaults [Lakemeyer, 1993].3 Suppose p denotes a secret, and consider the default assumption that if i has no knowledge of j knowing the secret, then it is the case that j does not know it. Let δ = Ki Kjp Kjp. It can now be shown that if δ is the only formula that i only knows, then, Oiδ Ki Kjp is a valid sentence. That is, i actually believes that j does not know p. Note, for example, adding objective knowledge to i s knowledge does not change his conclusion, that is, |= Oi(p δ) Ki Kjp. Of course, if i where to believe that j indeed knows p, this conclusion is now retracted: |= Oi(p δ Kjp) Ki Kjp.

3.2 A Logic of Multi-Agent Only Knowing As in the logic of the previous section, the class of models is again the class of (pointed) epistemic models. Only the syntax of the logical language changes, the satisfaction relation and the class of models remains the same as before. The syntax of this full language is, in fact, an extension of the language ONLn of Belle and Lakemeyer [2010]. Like for ONLn, we also allow an arbitrary nesting of the connectors Kj, Ok j and Ok G.

3Levesque [1990] had previously shown that only knowing a subjective formula can capture such defaults in the single agent case.

Definition 7 (Languages LO G and LO). The language LO G is defined inductively as follows.

ϕ ::= p | ϕ | (ϕ ϕ) | K jϕ | Ok jϕ | CGϕ | Ok Gϕ

where k N, G Agt, j A and p P. The formulas Ojϕ and OGϕ are abbreviations for O0 jϕ and O0 Gϕ respectively. We define the language LO as the language LO G without the group connectives CG and Ok G. Proposition 2. Let k N and ψ L. Let P := P(ψ) and n = d(ψ)+k. Then by Corollary 1, there is S n = {δ1 n, . . . , δm n } EP n such that |= ψ _

δn S n δn. Then, we have that the following

δ S n b Kjδ Kj

δ S n c CGδ CG

Proof. It follows straightforwardly from the truth conditions for Ok j and Ok G. qed

Corollary 2. Let k N and ϕ LO G. Let P := P(ϕ) and n = d(ϕ) + k. Then, there is S ϕ n = {δ1 n, . . . , δm n } EP n such that

Moreover, for each n, this set S ϕ n is unique.

Proof. The proof is by induction on the nesting depth n of operators Ok j and Ok G. The base case n = 0 holds trivially by definition. The induction step is proved by applying Proposition 2: the right-hand sides of Expressions (1) and (2) do not contain operators Ok j and Ok G. qed

Definition 8 (Truth conditions for LO G). The truth conditions are exactly the same as in Definition 6. When |= ϕ holds for some ϕ LO G, we say that ϕ is LO-valid. Example 2. With the enriched language, we can handle entailments of the sort:

|= Ki(p Ojq) Ki Kjq Ki Kjp

That is, if i believes p and also believes j to only know q, he not only knows that j knows q (as in classical epistemic logic) but also knows that j does not know p (a property of only knowing). As an extension to our previous example, suppose ξ says that if i does not believe p is the only thing that j knows then it is the case that j knows more. That is,

ξ = Ki Ojp Ojp

We can then show that Oiξ Ki Ojp is a valid sentence, that is, i believes that j knows more than p.

Given the reading of our graded multi-agent only knowing operator, we have the following expected result, which is the counterpart of [Belle and Lakemeyer, 2010, Theorem 5]: if an agent (or a group of agents) only knows that ϕ holds up to a certain degree, then she also only knows it up to a lower degree. Proposition 3. Let m, n N such that n m and let ϕ LO G. Let j A and G A. Then, the following holds:

On jϕ Om j ϕ On Gϕ Om Gϕ

Proof. The proof follows the same lines as the proof of [Belle and Lakemeyer, 2010, Theorem 5]. Let (M, v) be a pointed epistemic model. First, one should observe that for all δm EP m, there is δn S δm n such that M, v |= δn if, and only if, M, v |= δm (this δn depends on the structure of (M, v) beyond modal depth m). Vice versa, for all δn EP n , there is δm EP m such that M, v |= δn if, and only if, M, v |= δm (this δn does not depend on the structure of (M, v) beyond modal depth m). From this observation and by examining the truth conditions of Definition 6, we conclude easily that our two implications hold. qed

However, the reverse implications in Proposition 3 do not hold necessarily, because of the dependence on the structure of (M, v) in the first case. We now explore the relation to the Belle and Lakemeyer scheme in more detail in the next section.

4 Relation to Belle and Lakemeyer First, we recall the essentials of the approach of Belle and Lakemeyer [2010]. They do not consider only knowing operators dealing with groups of agents and do not consider degrees of only knowing as we do. Moreover, and without loss of generality, we assume that there are only two agents: A := {a, b}, as in [Belle and Lakemeyer, 2010]. Then, we consider the fragment ONLO n of the language LO G defined as follows: Definition 9 (Languages ONLn and ONLO n ). The language ONLn is defined inductively as follows:

ϕ ::= p | ϕ | (ϕ ϕ) | K jϕ | Njϕ

where p P and j A. The formula Ojϕ is an abbreviation for Kjϕ Nj ϕ. The language with the connectives , , Kj and Oj (instead of Nj) is denoted ONLO n . The semantics of Belle and Lakemeyer [2010] is based on the notion of k-structures. We consider a non-empty set of possible worlds W which simply consists of all the propositional valuations for the propositional letters in P. A kstructure (k 1), say ek, for an agent is defined inductively as follows: e1 W {{}}, ek W Ek 1, where Em is the set of all m-structures. A e1 for a, denoted as e1 a, is intended to represent a set of worlds {(w, {}), . . .}. A e2 is of the form {(w, e1 b), (w , e 1 b ), . . .}, and it is to be read as at w, a believes b considers worlds from e1 b possible but at w , a believes b to consider worlds from

e 1 b possible . This conveys the idea that a has only partial information about b, and so at different worlds, a believes different things about b. We define a ek for a, a e j for b and a world w W as a (k, j)-model (ek a, ej b, w). Only formulas of a maximal a-depth of k, and a maximal b-depth of j are interpreted w.r.t. a (k, j)- model. (See [Belle and Lakemeyer, 2010] for more details on these notions; definitions are not reproduced here.) The truth conditions are defined as follows:

ek a, ej b, w |= p iff p w ek a, ej b, w |= ϕ iff it is not the case that ek a, ej b, w |= ϕ ek a, ej b, w |= ϕ ψ iff ek a, e j b, w |= ϕ and ek a, e j b, w |= ψ ek a, ej b, w |= Kaϕ iff for all (w , ek 1 b ) ek a, we have that ek a, ek 1 b , w |= ϕ ek a, ej b, w |= Naϕ iff for all (w , ek 1 b ) < ek a, we have that ek a, ek 1 b , w |= ϕ

With these definitions and our abbreviations, we have that

ek a, e j b, w |= Oaϕ iff for all worlds w , for all ek 1 for b, (w , ek 1 b ) ek a iffek a, ek 1 b , w |= ϕ

We say that a formula ϕ ONLO n is BL-valid when it is valid in the sense of Belle and Lakemeyer [2010], that is when it is true in all (k, j)-models, if ϕ is of a-depth k and b-depth j. We now show that the set of BL-validities for the language ONLO n is the same as the set of validities in our logic LO.

Lemma 1. Let ϕ ONLO n be a formula of a-depth k and of b-depth j. Then, for all (k, j)-models (ek a, ej b, w), there is a pointed epistemic model (M, w) such that ek a, e j b, w |= ϕ if, and only if, M, w |= ϕ. Vice versa, for all pointed epistemic models (M, w), there is a (k, j)-model (ek a, e j b, w) such that ek a, ej b, w |= ϕ if, and only if, M, w |= ϕ.

Proof. For the first part, the worlds of M are w and all the k structures and the j structures present in ek a and ej b. The valuations and the accessibility relations for these worlds are defined canonically. For the second part, we unravel the pointed epistemic model (M, w) up to modal depth k for the worlds accessible from w by a and up to modal depth j for the worlds accessible from w by b (see [Blackburn et al., 2001]). qed

Theorem 2. A formula ϕ ONLO n is LO-valid if, and only if, it is BL-valid.

Proof. It follows from the previous Lemma 1. qed

Note that, unlike the approach of Belle and Lakemeyer [2010], we can simultaneously satisfy an infinite set of sentences of unbounded modal depth.

5 The Cover Modality

The cover modality has been used as a syntactic primitive in modal logics [D Agostino and Lenzi, 2005]. It has recently been axiomatized [Bılkov a et al., 2008]. Here, we define a multi-modal version of this cover logic.

Definition 10 (Language L ). The language L is defined inductively as follows.

ϕ ::= p | ϕ | (ϕ ϕ) | j{ϕ, . . . , ϕ}

where j A and p P. Moreover, we use the following abbreviations: Kjϕ := j j{ϕ}.

Definition 11 (Truth conditions for L ). The satisfaction relation |= is defined like in Definition 6 for the base case and for the connectives and . For the cover modalities, the truth conditions are defined as follows:

M, w |= j{ϕ1, . . . , ϕm} iff

for all v Rj(w) there is i {1, . . . , m} such that M, v |= ϕi, and for all i {1, . . . , m} there is v Rj(w) such that M, v |= ϕi.

Note that |= b Kjϕ j{ , ϕ}. Likewise, we can define our multi-agent only knowing modalities Ok

j with the cover modality as follows.

Proposition 4 (Expressiveness of the cover modality). Let ϕ LO

G and k N. Let P := P(ϕ) and n = d(ϕ) + k. Then for all pointed epistemic model (M, w), we have that the following holds: for any j A,

jϕ iff M, w |= j{δ1, . . . , δm}

where {δ1, . . . , δm} EP

n is such that |= ϕ δ1 . . . δm.

Proof. It follows straightforwardly from the truth conditions of the multi-agent only knowing operators Ok

G given in Definition 6. qed

The above proposition shows that L is at least as expressive as LO on the class of epistemic models. Therefore:

Theorem 3 (Decidability of LO). Let ϕ LO. The problem of determining whether ϕ is LO-valid is decidable.

Proof. The proof follows from the fact that L is at least as expressive as LO on the class of epistemic models by Proposition 4 and the fact that the validity problem of L is decidable, as shown by Bılkov a et al. [2008]. qed

6 Proof System

To define the proof system for L , we need to introduce some further notations. Typically, formulas of L are denoted ϕ, ψ, . . ., finite sets of formulas are denoted α, β, . . . and sets of sets of formulas are denoted A, B, . . .

We define the (power set) lifting of the relation L 2L

as the relation 2L 22L given by α A if, and only if, for all ϕ α, there is β A such that ϕ β, and for all β A, there is ϕ α such that ϕ β.

Let E be a non-empty set. An object A 22E is a redistribution of a set B 22E if α A for all α B (hence in particular

A). We call such a redistribution slim if

A. The set of all slim redistributions of A is denoted by S RD(A).

( 0) Axioms and Inference Rules of Prop. Logic ( 1) If ϕ α, ψ β such that ϕ ψ, and ψ β, ϕ α such that ϕ ψ then jα jβ

) B S RD(A)

Figure 2: Proof System L for L

Theorem 4. [Bılkov a et al., 2008] The proof system L defined in Figure 2 is sound and strongly complete for L w.r.t. the class of epistemic models.

We are going to extend the language of L in order to include explicitly the only knowing operator that we introduced in Section 3. Since this modality is definable in terms of the cover modality by Proposition 4, we straightforwardly obtain an axiomatization of this extended language. Definition 12 (Language LO

). The language LO

is defined inductively as follows.

ϕ ::= p | ϕ | (ϕ ϕ) | j{ϕ, . . . , ϕ} | Ok

where ψ LO, k N, j A and p P. Moreover, we use the following abbreviation: Kjϕ := j j{ϕ}.

The truth conditions are defined like in Definition 3 for the base case and for the connectives and . For the cover modalities, the truth conditions are defined like in Definition 11, and for the multi-agent only knowing modality the truth conditions are defined like in Definition 6. Theorem 5. The proof system LO

is the proof system L of Figure 2 to which we add the following inference rule: for all

j A, for all ϕ LO, for all k N,

j) If ϕ δ1 . . . δm with {δ1, . . . , δm} EP

j(ϕ) j{δ1, . . . , δm}

where n := d(ϕ) + k and P := P(ϕ).

Then, the proof system LO

is sound and strongly complete for LO

w.r.t. the class of epistemic models. Proof. The proof of soundness is standard. Completeness is obtained by observing that Theorem 4 gives us completeness for the language L without the multi-agent only knowing modality. Then, we obtain completeness for the full language LO

because the multi-agent only knowing modality is definable in terms of the cover modality by Proposition 4 and this definition corresponds in fact to our inference rule (Ok

The language LO

is an extension of the language LO of Section 3 with the cover modality. From Theorem 5, we obtain a soundness and completeness result for this restricted language LO: Corollary 3. Let ϕ LO. Then, ϕ is derivable in the proof system LO

if, and only if, ϕ is LO-valid.

7 Other Related Work

Besides the immediately relevant work already discussed above, let us note the following related efforts. Minimal knowledge approaches have also enjoyed multiagent extensions [Hoek and Thijsse, 2002]. While minimal knowledge is related to only knowing, it differs in the sort of conclusions one can draw. We refer readers to [Levesque and Lakemeyer, 2001] for discussions. A related proposal is that of total knowledge [Pratt-Hartmann, 2000], where knowledge is required to be true. So defaults, for example, would lead to an inconsistency. Although defaults are not the focus of this paper, there are also proposals that study the interaction between knowledge and defaults in a multi-agent setting, such as [Morgenstern, 1990]. In terms of proof theory, Bonatti and Olivetti [2002], among others, have developed proof systems for such defaults. The relation between concepts like only knowing and this work, however, remains to be explored. Finally, there are numerous modal logics for multi-agent systems for concepts such as beliefs, dynamics, and desires, which we do not review here. See [van der Hoek and Wooldridge, 2012; Fagin et al., 1995] and references therein. Only knowing is not considered by these, however.

8 Conclusion

We investigated a new version of multi-agent only knowing in the classical Kripke setting, while putting it in context of existing proposals on this topic. This comes with a number of benefits for example, the definability with the cover modality, a group version of multi-agent only knowing, and an operator for assessing the epistemic entrenchment of what an agent or a group only knows while avoiding proof-theoretic constructions. At this point, the development of this paper could lead to dynamic logic based representation formalisms such as [van Ditmarsch et al., 2011] finally embracing the only knowing modality in a multi-agent and dynamic setting. These formalisms are also based on a Kripke semantics.

References [Belle and Lakemeyer, 2010] V. Belle and G. Lakemeyer. Multi-agent only-knowing revisited. In Fangzhen Lin, Ulrike Sattler, and Miroslaw Truszczynski, editors, KR. AAAI Press, 2010. [Bılkov a et al., 2008] M. Bılkov a, A. Palmigiano, and Y. Venema. Proof systems for the coalgebraic cover modality. Advances in Modal Logic, 7:1 21, 2008. [Blackburn et al., 2001] P. Blackburn, M. de Rijke, and Y. Venema. Modal Logic, volume 53 of Cambridge Tracts in Computer Science. Cambridge University Press, 2001. [D Agostino and Lenzi, 2005] G. D Agostino and G. Lenzi. An axiomatization of bisimulation quantifiers via the µcalculus. Theoretical Computer Science, 338(1):64 95, 2005. [Fine, 1975] K. Fine. Normal forms in modal logic. Notre Dame Journal of Formal Logic, 16:229 237, 1975.

[Levesque, 1990] H. J Levesque. All I know: a study in autoepistemic logic. Artificial intelligence, 42(2):263 309, 1990. [Moss, 2007] L. S. Moss. Finite models constructed from canonical formulas. Journal of Philosophical Logic, 36(6):605 640, 2007. [Belle and Lakemeyer, 2010] V. Belle and G. Lakemeyer. Multi-agent only-knowing revisited. In Proc. KR, pages 49 60, 2010. [Bonatti and Olivetti, 2002] P. A. Bonatti and N. Olivetti. Sequent calculi for propositional nonmonotonic logics. ACM Trans. Comput. Log., 3(2):226 278, 2002. [Demolombe, 2003] R. Demolombe. Belief change: from situation calculus to modal logic. In Proc. Nonmonotonic Reasoning, Action, and Change (NRAC), 2003. [Fagin et al., 1995] R. Fagin, J. Y. Halpern, Y. Moses, and M. Y. Vardi. Reasoning About Knowledge. MIT Press, 1995. [Halpern and Lakemeyer, 2001] J.Y. Halpern and G. Lakemeyer. Multi-agent only knowing. Journal of Logic and Computation, 11(1):251 265, 2001. [Halpern and Moses, 1984] J. Y. Halpern and Y. Moses. Towards a theory of knowledge and ignorance: Preliminary report. In Proc. NMR, pages 125 143, 1984. [Halpern, 1993] J. Y. Halpern. Reasoning about only knowing with many agents. In Proc. AAAI, pages 655 661, 1993. [Herzig et al., 2000] A. Herzig, J. Lang, D. Longin, and T. Polacsek. A logic for planning under partial observability. In Proc. AAAI / IAAI, pages 768 773, 2000. [Hoek and Thijsse, 2002] W. van Der Hoek and E. Thijsse. A general approach to multi-agent minimal knowledge: With tools and samples. Studia Logica, 72(1):61 84, 2002. [Lakemeyer, 1993] G. Lakemeyer. All they know: A study in multi-agent autoepistemic reasoning. In Proc. IJCAI, pages 376 381, 1993. [Levesque and Lakemeyer, 2001] H.J. Levesque and G. Lakemeyer. The logic of knowledge bases. The MIT Press, 2001. [Morgenstern, 1990] L. Morgenstern. A formal theory of multiple agent nonmonotonic reasoning. In Proc. AAAI, pages 538 544, 1990. [Pratt-Hartmann, 2000] I. Pratt-Hartmann. Total knowledge. In Proc. AAAI, pages 423 428, 2000. [van der Hoek and Wooldridge, 2012] W. van der Hoek and M. Wooldridge. Logics for multiagent systems. AI Magazine, 33(3):92 105, 2012. [van Ditmarsch et al., 2011] H. P. van Ditmarsch, A. Herzig, and T. De Lima. From situation calculus to dynamic epistemic logic. J. Log. Comput., 21(2):179 204, 2011. [Waaler and Solhaug, 2005] A. Waaler and B. Solhaug. Semantics for multi-agent only knowing: extended abstract. In Proc. TARK, pages 109 125, 2005.