Only Knowing Meets Common Knowledge

1 Introduction

When considering knowledge-based agents, it seems natural that the beliefs of the agent are those that follow from the assumption that its knowledge base is all that is known. 1 Levesque [1990] was among the first to capture this idea in the logic of only knowing, where a modality O is introduced in addition to the classical epistemic operator K. For example, from Op it follows that Kq, which is di�erent from classical epistemic logic where Kp does not rule out Kpp ^ qq. Similarly, from OpPpaq _ Ppbqq we get KpDxrPpxq ^ KPpxqsq, which says that "if all I know is Ppaq or Ppbq then I know that there is an instance of P but not what." So, one of the advantages here is that a precise characterization of the beliefs and the non-beliefs can be given.

While single-agent only knowing has a particularly simple possible-world semantics, the many agent case, where agents may have beliefs about what other agents believe, has turned out to be much more challenging. Early approaches such as [Halpern, 1993; Lakemeyer, 1993; Halpern and Lakemeyer, 2001; Waaler, 2004; Waaler and Solhaug, 2005] either

�Partially funded by the FWO project on Data Cleaning and KU Leuven's GOA on Declarative Modeling for Mining and Learning.

:Also a�liated with the University of Toronto.

1 In this paper, we do not distinguish between "knowledge" and "belief" and freely use the terms interchangeably.

Gerhard Lakemeyer:

Dept. of Computer Science RWTH Aachen University Germany

gerhard@cs.rwth-aachen.de

had undesirable properties or had to resort to proof-theoretic concepts such as canonical models built into the semantics. In a recent paper, we [Belle and Lakemeyer, 2010] came up with an account which arguably extends the semantics of only knowing to multiple agents in a natural way. Most significantly, this scheme is for a first-order language with equality and quantification, as in Levesque's proposal, but in stark contrast to approaches such as [Halpern and Lakemeyer, 2001], based on canonical models, that are propositional. 2

In Levesque's single agent semantics of only knowing, a model, or an epistemic state, is simply a set of worlds e, which satisfies only knowing a sentence � just in case e is maximal, that is, adding any other world to e would lead to not believing � any more. (Worlds are simply truth assignments to atoms of a first-order language and believing is interpreted in the usual way as truth in all worlds in e.)

For many agents, in [Belle and Lakemeyer, 2010], we introduced sets of states of a�airs as epistemic states, where each element consists of a world in the sense of Levesque together with sets of states of a�airs for every other agent, representing their beliefs at this particular world. In order to avoid circularity, each model is limited to a finite depth, where depth refers to the maximal number of alternating nested beliefs considered at this model. The idea is roughly as follows. Suppose there are n agents. At level 1, an agent's epistemic state, called a 1-structure (or k-structure more generally), is simply a set of worlds; a pk � 1q-structure is a set of tuples pw; e1; e2; : : : ; enq, where each ei is a k-structure. In order to interpret a formula, one then picks a model consisting of a world and k-structures, one for each agent, such that k is at least as big as the depth of the formula in question. Since k-structures are sets, knowing and only knowing can be defined in a way similar to the single agent case except that interpreting a belief of another agent leads to "popping up" the k-structures of the respective agent. Of course, despite the depth limitation of each model, validity and satisfiability are well defined for all formulas (of arbitrary depth), since each formula has finite depth, and there are enough models of this (or greater) depth. Most significantly, this approach was shown to generalize the features of Levesque's logic as identified in [Halpern and Lakemeyer, 2001], and when restricted to the propositional case, the relationship to many related e�orts, including [Halpern and Lakemeyer, 2001], was also established in our previous paper.

2 It is also not clear how such a proof-theory based semantics can be extended to the first-order case mainly because there cannot be a complete first-order axiomatization of only knowing even for a single agent [Halpern and Lakemeyer, 1995].

However, as we acknowledged in that work, there is a price to pay when using depth-limited models, since there is no single model which works for all formulas. While this is often not a problem, as knowledge bases are usually assumed to be finite collections of sentences, there is one important exception: common knowledge. This notion has been found useful in distributed systems [Moses et al., 1986] as well as in artificial intelligence, game theory and philosophy [Fagin et al., 1995]. A formula � is common knowledge if everybody believes � and everybody believes that everybody believes �, and so on, ad infinitum. Thus, given the depth limitation of the our account, it is not possible to give meaning to such (useful) infinitary notions.

In this paper, we show how this limitation can be overcome. The idea is, roughly, to move from fixed k-structures to infinite sequences of k-structures for all k and all agents, where each member of a sequence for a particular agent is compatible with the beliefs of its predecessor and extends it to account for one additional level of nested beliefs. This construction is shown to be fully compatible with depth-limited models in terms of validity, and so it inherits the reasonableness of the previous account. The treatment is inspired by Fagin et al. [1991] and their idea of using infinite sequences of epistemic states for many agents and common knowledge. There are significant technical di�erences, however, which we will discuss in more detail later. Moreover, Fagin et al. do not consider only knowing and limit themselves to the propositional case. Thus, for the very first time, we are able to study the interaction between the notions of only knowing and common knowledge. Interestingly, by adding a simple form of public announcement to the logic, we are also able to demonstrate how the muddy children puzzle [Fagin et al., 1995] can be cast in terms of logical implications given what is only known initially.

We structure the work by beginning with the new logic, discussing some of its properties and extensions before turning to the puzzle. We conclude after discussing related work.

2 The Logic COLn

Syntax

The non-modal fragment of COLn consists of standard firstorder logic with � (that is, connectives t^; @; u, syntactic abbreviations tD; �; �u, parentheses, period) and a countably infinite set of standard names N: As we shall see, these standard names will serve as a fixed domain of discourse, permitting a substitutional interpretation for quantifiers. To keep matters simple, function symbols are not considered in this language. We call a predicate other than �, applied to firstorder variables and standard names, an atomic formula. We write � x m to mean that the variable x is substituted in � by a standard name m. If all the variables in a formula � are substituted by standard names, then we call it a ground formula.

We let I � t1; : : : ; nu be a set of agents, and let i range over this set. COLn has three epistemic operators: Ki� is to be read as "i knows �," Oi� is to be read as "all that i knows is �," and C� is to be read as "� is common knowledge among the agents in I:" For convenience, we also use E�, to be read as "everybody knows �," as an abbreviation for K1� ^ : : : ^Kn�. Letting E1 � mean E�, Ek�1 � for k ¥ 1 is used as an abbreviation for EpEk �q: A formula not mentioning modalities is called objective, and a formula where all predicate symbols appear within the scope of a modal operator is called subjective.

Semantics

The semantics is given in terms of possible worlds. Here, a world is simply a set of ground atoms, and let W denote the set of all possible worlds.

Epistemic states, which are used to define the meaning of subjective formulas, are described in two steps. First, we describe the beliefs of an agent using the notion of a k-structure.

Definition 1: Let k ¡ 0. Then define E k as follows:

• � E 1 � 2 W ;
• � E k � 2 W�n E k�1 for k ¡ 1.

An element of E k is referred to as a k-structure, denoted e k . (When the context is clear, the superscript is dropped.)

As noted, e P E 1 for agent i, written ei for clarity, is of the form tw1 ; w2 ; : : :u and determines what i believes about the world, but has nothing interesting to say about i's views of other agents. By extension, ei P E 2 is of the form pw1 ; e11 ; : : : ; e1n q; pw2 ; e21 ; : : : ; e2n q; : : :(, which says that at w1 , i's beliefs about (say) agent n is given by e1n but at w2 , i believes that e2n captures n's beliefs.

An epistemic state, roughly speaking, is used to determine the beliefs of all agents and at all levels.

Definition 2: An epistemic state f is a function of the form I �N� �8k�1 E k such that for any i and k ¥ 1, f pi; kq P E k .

Such an epistemic state is reasonable only when an agent's beliefs are consistent across all levels. That is, each level extends the previous level by adding another layer of (nested) beliefs about other agents' beliefs, while keeping the set of worlds an agent considers the same. (This latter set is possibly duplicated to allow for situations where at a world, an agent's beliefs about what another knows di�ers; see the example below.) To formalize this idea we need the following notion of i-compatibility for subsequent k-structures.

Definition 3: We define e P E k and e1 P E k�1 as i-compatible inductively as follows:

• � for k � 1:

• � for k ¡ 1:

• for every pw; e11 ; : : : ; e1i ; : : : ; e1n q P e1 there is a pw; e1; : : : ; ei; : : : ; enq P e such that e1j and ej are j-compatible for all j , i.

Definition 4: We say an epistemic state f is proper if for all i; for all k ¡ 0; f pi; kq and f pi; k � 1q are i-compatible.

Henceforth, epistemic states are implicitly assumed to be proper.

Example 5: Here is a simple illustration using three levels and two agents, from the first agent's perspective:

At level 1, the first agent only considers w possible. At level 2, the second agent is believed to consider the worlds w1 and w2 possible. (At this level, the first agent's view of himself is precisely given by w, and so is fully compatible with the first level.) At level 3, at the world w1 ; the second agent believes that the first agent's knowledge is characterized by the world w� : In other words, the first agent believes that the second agent considers the first agent's knowledge to be given by w� : Analogously, at w2 ; the second agent's beliefs about what the first agent knows is given by w�� : (Here too, the agents' view of themselves is fully compatible with the previous level.)

We will also be interested in the progression of an epistemic state wrt some i and w, by means of which we can refer to the state of a�airs as considered possible by i at w:

Definition 6: Given an epistemic state f; we define its progression wrt an agent index i and a world w as follows:

Example 7: Using Example 5, and considering only the first level, suppose f 1 p1; 1q � f p1; 1q and f 1 p2; 1q � tw1 u. Since pw; f p1; 1q; tw1 uq P f p1; 2q, f 1 would belong in f w 1 :

Considering only the first and second levels, let f 1 p1; 1q and f 1 p2; 1q be as above, f 1 p1; 2q � f p1; 2q and f 1 p2; 2q � tpw1 ; tw� u ; tw1 uqu. Since pw; f p1; 2q; tpw1 ; tw� u ; tw1 uquq P f p1; 3q, f 1 would belong in f w 1 :

(This can be seen to be analogous to the notion of an accessibility relation in Kripke structures [Fagin et al., 1995].)

We now provide a semantics. By a model, we mean a pair p f; wq, where f is a (proper) epistemic state and w is a world. The semantic rules are given inductively as follows:

• � f; w |ø p i� p P w;
• � f; w |ø pm1 � m2q i� m1 and m2 are the same names;
• � f; w |ø � i� f; w6|ø �;
• � f; w |ø �^� i� f; w |ø � and f; w |ø �;
• � f; w |ø @x: � i� f; w |ø � x m for every standard name m;
• � f; w |ø Ki� i� for all w1 P f pi; 1q, for all f 1 P f w1 i , f 1 ; w1 |ø �;
• � f; w |øC� i� f; w |ø Ek � for all k ¥ 1;
• � f; w |øOi� i� for all w1 and f 1 , w1 P f pi; 1q and f 1 P f w1 i i� f 1 ; w1 |ø �:

A formula � P COLn is said to be satisfiable i� there is a proper epistemic state f and a world w such that f; w |ø �: Given any set � of sentences, we write � |ø � (read: "� entails �") if for all proper f and w, if f; w |ø � for every � P �, then f; w |ø �. We write |ø � (read: "� is valid") to mean tu |ø �:

3 Properties

Knowledge and Introspection

As we model knowledge as a set of possible worlds [Kripke, 1963; Hintikka, 1962], it is perhaps not surprising that we obtain the usual properties of K45n [Fagin et al., 1995]:

• � |øKi�^Kip� � �q �Ki�
• � |øKi� �KiKi�
• � |ø Ki� �Ki Ki�

The first property says that knowledge is closed under modus ponens. The second and third say that the agent knows its beliefs and non-beliefs.

Proof: We prove the case for positive introspection, and the others are analogous. Suppose f; w |ø Ki�. By definition, for all w1 P f pi; 1q and all f 1 P f w1 i , f 1 ; w1 |ø �. Suppose f; w |ø KiKi�. Then there is some w1 P f pi; 1q and some f 1 P f w1 i such that f 1 ; w1 |ø Ki�, that is, some w2 P f 1 pi; 1q and some f 2 P f 1w2 i such that f 2 ; w2 6|ø �. However, by definition, f pi; 1q � f 1 pi; 1q, and so this is a contradiction.

Knowledge and Validity

As a simple property of the semantics, valid sentences are always believed:

• � If |ø � then |øKi�

This property, however, should be distinguished from the knowledge of true sentences:

• � � �Ki� is falsifiable

These are analogous to the single agent case [Levesque and Lakemeyer, 2001, Section 4.2].

Knowledge and Barcan Formula

Owing to the fixed domain of discourse, we obtain the Barcan formula for knowledge, including its existential version:

• � |ø @xKi� �Kip@x�q
• � |ø DxKi� �KiDx�

Proof: We show the case for @, the other being analogous. Suppose f; w |ø @xKi�. By definition, f; w |ø Ki� x m for all names m. By definition, again, for all w1 P f pi; 1q and all f 1 P f w1 i , f 1 ; w1 |ø � x m . Then, f 1 ; w1 |ø @x�. So, f; w |øKi@x�.

Common Knowledge

Since C is interpreted in terms of Ki, it follows that all of the introspection properties also hold for C [Fagin et al., 1995; 1991], as well as a version of the Barcan Formula:

• � |øC�^Cp� � �q �C�
• � |øC� �CC�
• � |ø C� �C C�
• � |ø @xC� �Cp@x�q

Proof: We show the case for positive introspection, and the others are analogous in relation to the proofs for Ki: Suppose

• f; w |ø C�. By definition, f; w |ø Ek � for k ¥ 1. Suppose
• f; w 6|ø CC�. That is, f; w 6|ø Ek pEl �q for k; l ¥ 1, and so,
• f ; w 6|ø Ek�l �, which is a contradiction.

An inductive definition of C in terms of E also holds:

• � |øC� �Ep�^C�q

Proof: Suppose f; w |ø C� but f; w 6|ø Ep� ^ C�q. Clearly, f; w 6|ø E� is a contradiction, and so f; w 6|ø EC�. From the definition of E and C it follows that f ; w 6|ø KiEk � for some i and some k ¥ 1 and hence f ; w 6|ø Ek�1 �, which is also a contradiction.

Let us reiterate that since knowledge need not be true, by extension, common knowledge need not be true:

• � 6|ø Ki� � �
• � 6|ø C� � �

Proof: Let f be any epistemic state such that every world w P f pi; 1q is such that p P w for some proposition p. Let w� be a world such that p < w� : Clearly, f; w� 6|ø Ki p � p showing that 6|ø Ki� � �, and so C� � � cannot be valid.

A weaker version in the context of knowledge, however, can be shown:

• � |øKipC� � �q

Proof: Suppose f; w |ø KipC� � �q. Then for some w1 P f pi; 1q and f 1 P f w1 i , f 1 ; w1 |ø pC� � �q, that is, f 1 ; w1 |ø C�^ �. So, f 1 ; w1 |ø Ki�^ �: However note that, then, f; w |ø Ki� and so f; w |ø Ki Ki�. This means that f 1 ; w1 |ø Ki� as well, an inconsistency.

Only Knowing and Common Knowledge

Here we discuss a few properties on the interaction between only knowing and common knowledge.

Let us begin by noting that, as in the single agent setting [Levesque, 1990], only knowing implies knowing:

• � |øOi� �Ki�

Proof: The semantic rule for Oi uses "i�" instead of the "if" for Ki to test that the pairs p f 1 ; w1 q, where w1 P f pi; 1q and f 1 P f w1 i , are models of �: So Oi� implies Ki�.

This does not extend to common knowledge, because Oi p, where p is a proposition, means that i knows nothing about the beliefs of other agents:

Proof: Suppose f; w |ø Oi p ^Cp. It is easy to see that f; w |ø Oi p � KiKj p for j , i that contradicts the truth of Cp at p f ; wq.

In general, however, 6|ø Oi� � C�. For example, suppose � is p ^ Cp: As we shall see, Oi� is satisfiable, and suppose f; w |ø Oi�. Clearly, then, f; w |ø Cp and so f; w |øCpp^Cpq. Thus, f; w |øOi�^C�:

Since common knowledge implies having knowledge about what other agents believe, common knowledge about Oi p is impossible:

• � |ø COi p

Proof: Suppose f; w |ø COi p. Then, f; w |ø KiKjKi p, letting j , i. By definition of Oi, it is easy to show that Oi p � KiKjKi p is valid. Because f; w |ø COi p, we have f; w |ø KiOi p, and so, f; w |ø Ki KiKjKi p, which is a contradiction.

Of course, then, common knowledge that p is not the only thing known is satisfiable:

• � C Oi p is satisfiable

Proof: Let w any world such that p < w. Let U 1 � twu, and inductively, U k�1 � pw;U k ; : : : ;U k q(. Let f be a proper epistemic structure such that f p j; 1q � U 1 and f p j; kq � U k for all j. Then, f; w1 |øC Oi p for any w1 .

A knowledge base can believe p and also believe that p is common knowledge:

• � Oipp^Cpq is satisfiable

Proof: Let U 1 � tw | p P w; w PWu, and inductively, let U k�1 � pw;U k ; : : : ;U k q | w P U 1(. Then, let f pi; kq � U k for every k. It is easy to see f; w |øOipp^Cpq for any w.

It is worth remarking that one cannot be made to only know Cp without actually knowing p:

• � |ø OiCp

Proof: Suppose f; w |ø OiCp. By definition, w1 P f pi; 1q and f 1 P f w1 i i� f 1 ; w1 |ø Cp. Since the truth of Cp does not depend on the actual world, f pi; 1q � W. This means that f; w |ø Ki p, which is a contradiction.

In fact, the following also holds (as observed for the single agent case in [Levesque and Lakemeyer, 2001]):

Intuitively, saying that all that is known about the world is Ki p says nothing about the world leading to this property.

4 Relation to Existing Logics

The Logic OLn

This work not only extends our previous account in the sense of capturing common knowledge, but it is also compatible with it for the language OLn. (That is, OLn � COLn �C:) We recall some essentials: the prior account was limited to two agents, say ta; bu; a model of a formula � of depth k (definition not reproduced here) is a tuple of the form pea; eb; wq, where ei P E k and w P W as defined here. So a formula � of depth k is said to be satisfiable i� there is such a tuple. If � is true wrt every pe1a ; e1b ; wq, where e1i is a k1 -structure with k1 ¥ k, it is said to be valid.

As noted, our prior work was shown to be reasonable in terms of salient features of Levesque's logic [Halpern and Lakemeyer, 2001]. Thus, by establishing compatibility, we inherit the reasonableness of only knowing in the many agent case. The proof is not hard but tedious. Here we only go over the main ideas. Suppose |ø1 denotes the satisfaction relation in [Belle and Lakemeyer, 2010]. Then:

Lemma 8: Suppose I � ta; bu and � P OLn is of depth k: Given any f and w; suppose f pi; kq � ei. Then:

By means of an induction on �, one can argue that formulas of depth k are true wrt p f; wq i� they hold at pea; eb; wq. Intuitively, satisfaction wrt |ø implies satisfaction wrt |ø1 :

Next, we need a simple property that proper epistemic states can be constructed for any ei P E k :

Proposition 9: For every pair pea; ebq, where ei P E k for any k; there is a f such that f pi; kq � ei.

Owing to the definition of proper epistemic states (that is, consistent beliefs across all levels) and the above proposition, satisfaction wrt |ø1 can be seen to imply satisfaction wrt |ø, leading to the following result:

Theorem 10: Suppose � P OLn. Then: |ø � i� |ø1 �:

The Logic KC45n

For a propositional language, 3 OLn was also related to K45n:

Lemma 11: [Belle and Lakemeyer, 2010, Lemma 16] Suppose OLn is propositional. For any � P OLn not mentioning Oi, if � is consistent wrt K45n then � is satisfiable wrt |ø1 :

The proof rests on the property that every K45n-consistent formula is satisfiable wrt the canonical model for K45n axioms [Hughes and Cresswell, 1972; Fagin et al., 1995]. A tuple pea; eb; wq, where ei P E k ; can then be constructed to correspond precisely to the canonical model for formulas of depth k: Of course, by means of Theorem 10, we obtain:

Corollary 12: Suppose OLn is propositional. For any � P OLn not mentioning Oi, if � is consistent wrt K45n then � is satisfiable wrt |ø :

From this, letting KC45n denote K45n with the common knowledge operator [Fagin et al., 1995], we finally get:

Theorem 13: Suppose COLn is propositional. For any � P COLn not mentioning Oi, if � is consistent wrt KC45n then � is satisfiable wrt |ø :

Proof (sketch): The proof uses Lemma 11 and Corollary 12 to argue that if Ek � for any k ¡ 0 is satisfiable in KC45n, then it is satisfiable wrt |ø : Since C� is true i� Ek � is true for every k ¡ 0; the argument follows.

5 Extensions

Truthful Knowledge

As noted, knowledge need not be true, but we can require it, using a straightforward definition:

Definition 14: Given any proper f and any w; the pair p f; wq is called a knowledge model i� for all i; we have w P f pi; 1q:

(By the definition of proper, w will be considered possible by all agents at all levels.) Logical consequence, then, can be extended in an obvious way; � |ø � means that in every knowledge model where � is true, so is �. And indeed, as required of knowledge that is true [Fagin et al., 1995], the following properties are shown to hold:

• � |øKi� � �
• � |øC� � �

As is needed, knowledge models will be assumed for the developments in subsequent sections.

3 For a language with quantification, OLn di�ers from the usual treatments of first-order epistemic logic [Fagin et al., 1995, Chapter 3] in assuming a fixed domain of discourse called standard names as in [Levesque and Lakemeyer, 2001].

Public Announcements

In this paper, we are also interested in showing how the logical system can be used for a puzzle in a dynamical context that involves announcements. Perhaps the simplest way to capture this is to consider the addition of an announcement modality [Baltag et al., 1998] to COLn: So let COL�n be the addition of the modality r�s to COLn; where � P COLn: To give a semantics for this modality, we first define the intersection operator for epistemic states:

Definition 15: Given any f and f 1 , we define f � � f X f 1 inductively as follows. For every i:

• � f � pi; 1q � tw | w P f pi; 1q and w P f 1 pi; 1qu
• � for k ¡ 1, f � pi; kq � tpw; e1; : : : ; enq | pw; e1; : : : ; enq P f pi; kq and pw; e1; : : : ; enq P f 1 pi; kqu

For this definition, it is easy to show the following property:

Proposition 16: Suppose �; � P COLn are Boolean combinations of objective formulas and formulas of the form Ki� and Oi�, where � P COLn: Suppose f and f 1 are epistemic states, and w is any world. For j , i; if f; w |ø Kj� and f 1 ; w |ø Kj� then f X f 1 ; w |ø Kjp� ^ �q; if f; w |ø p Kj�^ Kj �q and f 1 is as before, then f X f 1 ; w |ø Kj�:

We define themeaning of � P COL�n inductively as before, with the following new rule:

• � f; w |ø r�s� i� f; w |ø � implies f |�; w |ø �:

Here f |� � f X f 1 , where f 1 is any proper epistemic state such that f 1 ; w |ø � Oip�^C�q. So, the announcement of � is defined simply in terms of an epistemic state where � and common knowledge about � is all that is believed. (Preconditions for announcements are omitted for simplicity [Baltag et al., 1998].) Intuitively, the only knowing modality ensures that the epistemic state considered is the "maximal" one where � holds at all levels. On intersecting such an epistemic state with the current one f; all structures where � is not believed are discarded.

The operator can be shown to have the following reasonable properties [Lutz, 2006]:

• � |ø r�sp � p� � pq
• � |ø r�s � � p� � r�s�q
• � |ø r�s�^� � pr�s�^ r�s�q
• � |ø r�sKi� � p� �Kip� � r�s�qq
• � |ø r�s@x� � @xpr�s�q

Proof: We prove the first item only, and the others can be proved by induction using the first item as the base case. By definition, f; w |ø r�sp i� f; w |ø � implies f |�; w |ø p. We claim f; w |ø � implies f |�; w |ø p i� f; w |ø � � p. Suppose f ; w 6|ø �, then the LHS is vacuously true but then so is the RHS. Conversely, suppose f; w |ø �. Then f |�; w |ø p i� (by definition) p P w i� f; w |ø p because the epistemic state is irrelevant i� (by assumption) f ; w |ø � � p:

6 The Muddy Children Puzzle

The muddy children puzzle [Barwise, 1981; Moses et al., 1986], which is a variant of the cheating wives puzzle [Gamow and Stern, 1958], brings out subtle changes to the knowledge states of a group of logical agents. The situation is as follows. Imagine n children playing together, leading some of them to get mud on their foreheads. Each child can see the foreheads of all other children, but not its own. Along comes the father, who says, "At least one of you has mud on your forehead," thus expressing a fact known to each of them before he spoke. The father then asks the question, "Do any of you know whether your forehead is dirty?," over and over. If two children have muddy foreheads, for example, every child announces "no" the first time the question is asked; but the next time, the dirty ones declares that their forehead is muddy.

Here, a purely deductive account of the puzzle is developed as logical consequences of what is only known initially, thereby complementing the usual approach with model constructions [Fagin et al., 1995].

Formally, assume mi says that child i has a muddy forehead. Initially, let us suppose that every child has a muddy forehead, that is, the real world w is any world where AllMuddy is true, where:

Next, we take note of three properties of the puzzle to characterize the knowledge bases of the children: (a) first, i sees that every other child has a muddy forehead; (b) second, i knows that others see its forehead; and (c) third, the father announces initially that at least one child has a muddy forehead, which is the only thing assumed to be common knowledge because every child has heard the father's announcement. Putting this together, the initial theory � is the conjunction of AllMuddy and the knowledge bases for every i:

OipOthersMuddy ^ pXmi _X miq ^CpAtLeastOneqq where,

• � OthersMuddy � � j,i mj captures (a);
• � X� � � j,i Kj� abbreviates "they know" for (b);
• � AtLeastOne � � mi is the father's message in (c).

Finally, every time the father asks the question of whether the children know their foreheads are muddy, their announcements are lumped together as:

The puzzle, then, is:

hkkkkkkikkkkkkj

After pn�1q occurrences of No, 4 the children know that they have muddy foreheads. To better see the knowledge bases in action, we give the argument for n � 2; that is, suppose I � ta; bu, and we are to prove:

4 More generally, if k / n children have mud on their foreheads, k�1 announcements of No need to be made [Fagin et al., 1995]. For example, if k � 1, owing to AtLeastOne being common knowledge, the child with the muddy forehead notices that others have clean ones, and concludes immediately that he must be the muddy one.

Proof: Let p f; wq be a knowledge model for � and let f 1 be the epistemic state where OapNo ^ CpNoqq ^ ObpNo ^ CpNoqq holds. We prove the case for a concluding that its own forehead is muddy, the other being analogous.

Owing to the closure of knowledge under modus ponens, pKbpma _ mbq ^Kb maq � Kbmb is valid. (In contrast, pKbpma_mbq^Kbmaq � Kbmb is falsifiable.) Let � denote Kbpma_mbq, � denoteKb ma, � denoteKbmb and � denote Kbma. So p� ^ �q � � is valid. Owing to the knowledge of valid sentences, the validity of p� ^ �q � � means Kapp�^ �q � �q is valid, and so is true at f and f 1 :

Since AtLeastOne is common knowledge in �, f; w |ø KaKbAtLeastOne, that is, f; w |ø Ka�: By construction, f; w |ø Ka� ^ Ka � because of only knowing. (That is, in the absence of only knowing, there are epistemic states where, say, Ka� is believed.) By construction, f 1 ; w |ø Ka � because of only knowing. Using Proposition 16, f X f 1 ; w |øKa �:

On expanding X in � ; we get f; w |ø KapKbma _ Kb maq, that is, f; w |øKap�_�q: By construction, f 1 ; w |ø p Kap�_�q^ Ka p�_�qq because of only knowing. By Proposition 16, f X f 1 ; w |ø Kap� _ �q:

Putting it together, we get f X f 1 ; w |ø Ka�, that is, f X f 1 ; w |ø KaKbma. When knowledge is true the sentence Kb � is valid, and so f X f 1 ; w |ø Kama.

7 RelatedWork

As noted, there have been some prominent proposals for multiagent only knowing such as [Halpern, 1993; Lakemeyer, 1993; Halpern and Lakemeyer, 2001; Waaler, 2004; Waaler and Solhaug, 2005]. Besides being propositional, they have problematic features, as discussed at length in [Belle and Lakemeyer, 2010]. See that work on how these problems are avoided using k-structures.

The underlying notion of only knowing is due to Levesque [1990]. Incidentally, there are some related notions, such as total knowledge [Pratt-Hartmann, 2000] and minimal knowledge [Halpern and Moses, 1984], the latter of which has also received recent multiagent treatments [van Der Hoek and Thijsse, 2002]. However, these notions di�er significantly from Levesque's only knowing [Levesque and Lakemeyer, 2001]. Although not the focus of this paper, we note that when the knowledge base itself refers to the agent's beliefs, only knowing also exhibits a form of nonmonotonic reasoning; see [Levesque and Lakemeyer, 2001] and [Belle and Lakemeyer, 2015] for discussions and references in the single and multiagent cases respectively.

Let us also remark that multiagent logics of knowledge are an active focus in artificial intelligence [van der Hoek and Wooldridge, 2012], with a number of extensions for reasoning about time, actions, desires, and intentions, among others. (For an account using sets of possibilities, see [Gerbrandy and Groeneveld, 1997].) Investigations in the area on common knowledge and muddy children variants are also fairly prevalent; for example, see [Fagin et al., 1995; van Ditmarsch et al., 2007]. The analysis of the puzzle here is mostly by means of model constructions, with approaches such as [Kraus and Lehmann, 1988; Elgot-Drapkin, 1991] being notable exceptions. In particular, one would observe in this latter work that the muddy children puzzle requires an explicit enumeration of the non-beliefs of the agents. In contrast, we can get o� the ground simply in terms of what is believed initially (with help from only knowing), which (to the best of our knowledge) has not been obtained before.

Finally, the inspiration for the infinite sequence of structures is the work in [Fagin et al., 1991]. They introduce what they call knowledge structures, also for di�erent levels. While at level 1 our concepts match (that is, just worlds), a level 2 structure of theirs is already di�erent from a 2structure. Most significantly, they are propositional, do not treat only knowing and require knowledge to always be true. The way that the infinite sequences work in the semantics of the two proposals di�ers as well: in our case, the C modality causes the epistemic states to repeatedly progress, whereas in theirs there are structures for every nesting of this modality which requires structures corresponding to many ordinal numbers. Nonetheless, they do establish a connection to the logic KC45n [Fagin et al., 1991, Corollary 5.9], as do we, and so we would agree on formulas of this language.

8 Conclusions

A first-order logic of only knowing and common knowledge was introduced that allows us to investigate the interaction between these notions, and provide a solution to the muddy children puzzle in terms of what is only known initially. Among other things, this logic is shown to be fully compatible with (and extend) previous accounts, and thus is a very general first-order proposal of only knowing in the many agent case.

Beginning with OLn [Belle and Lakemeyer, 2010], exploring issues related to axiomatization and nonmonotonic reasoning in the presence of common knowledge would make for interesting future work.