# only_knowing_meets_common_knowledge__a5b5c78d.pdf Only Knowing Meets Common Knowledge Vaishak Belle Dept. of Computer Science KU Leuven Belgium vaishak@cs.kuleuven.be Gerhard Lakemeyer: Dept. of Computer Science RWTH Aachen University Germany gerhard@cs.rwth-aachen.de Only knowing captures the intuitive notion that the beliefs of an agent are precisely those that follow from its knowledge base. While only knowing has a simple possible-world semantics in a single agent setting, the many agent case has turned out to be much more challenging. In a recent paper, we proposed an account which arguably extends only knowing to multiple agents in a natural way. However, the approach was limited in that the semantics cannot deal with infinitary notions such as common knowledge. In this work, we lift that serious limitation to obtain a first-order language with only knowing and common knowledge, allowing us to study the interaction between these notions for the very first time. By adding a simple form of public announcement, we then demonstrate how the muddy children puzzle can be cast in terms of logical implications given what is only known initially. 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 different from classical epistemic logic where Kp does not rule out Kpp qq. Similarly, from Op Ppaq _ Ppbqq we get Kp Dxr Ppxq 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 affiliated with the University of Toronto. 1In this paper, we do not distinguish between knowledge and belief and freely use the terms interchangeably. 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 affairs as epistemic states, where each element consists of a world in the sense of Levesque together with sets of states of affairs 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 2It 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]. Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence (IJCAI 2015) identified in [Halpern and Lakemeyer, 2001], and when restricted to the propositional case, the relationship to many related efforts, including [Halpern and Lakemeyer, 2001], was also established in our previous paper. 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 differences, 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 t D, , Ą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 Ep Ekα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 Ek as follows: Ek 2WŚ n Ek 1 for k ą 1. An element of Ek is referred to as a k-structure, denoted ek. (When the context is clear, the superscript is dropped.) As noted, e P E1 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 E2 is of the form pw1, e1 1, . . . , e1 nq, pw2, e2 1, . . . , e2 nq, . . . ( , which says that at w1, i s beliefs about (say) agent n is given by e1 n but at w2, i believes that e2 n 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 Ñ Ť8 k 1Ek such that for any i and k ě 1, fpi, kq P Ek. 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 differs; 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 Ek and e1 P Ek 1 as i-compatible inductively as follows: for k 1: e tw | pw, e1, . . . , ei, . . . , enq P e1u and ei e; tw | pw, e1, . . . , ei, . . . , enq P eu tw | pw, e1 1, . . . , e1 i, . . . , e1 nq P e1u and e1 i e; for every pw, e1 1, . . . , e1 i, . . . , e1 nq P e1 there is a pw, e1, . . . , ei, . . . , enq P e such that e1 j 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, fpi, kq and fpi, 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: fp1, 1q twu fp1, 2q tpw, fp1, 1q, tw1uq, pw, fp1, 1q, tw2uqu fp1, 3q tpw, fp1, 2q, t pw1, tw u , tw1uq uq, pw, fp1, 2q, t pw2, tw u , tw2uq uqu 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 affairs 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: f w i tproper f 1 | for all k ą 0: if f 1p1, kq e1, . . . , f 1pn, kq en, then pw, e1, . . . , enq P fpi, k 1qu. Example 7: Using Example 5, and considering only the first level, suppose f 1p1, 1q fp1, 1q and f 1p2, 1q tw1u. Since pw, fp1, 1q, tw1uq P fp1, 2q, f 1 would belong in f w 1 . Considering only the first and second levels, let f 1p1, 1q and f 1p2, 1q be as above, f 1p1, 2q fp1, 2q and f 1p2, 2q tpw1, tw u , tw1uqu. Since pw, fp1, 2q, tpw1, tw u , tw1uquq P fp1, 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 pf, wq, where f is a (proper) epistemic state and w is a world. The semantic rules are given inductively as follows: f, w |ù p iffp P w; f, w |ù pm1 m2q iffm1 and m2 are the same names; f, w |ù α ifff, w |ù α; f, w |ù α β ifff, w |ù α and f, w |ù β; f, w |ù @x. α ifff, w |ù αx m for every standard name m; f, w |ù Kiα ifffor all w1 P fpi, 1q, for all f 1 P f w1 i , f 1, w1 |ù α; f, w |ù Cα ifff, w |ù Ekα for all k ě 1; f, w |ù Oiα ifffor all w1 and f 1, w1 P fpi, 1q and f 1 P f w1 i ifff 1, w1 |ù α. A formula α P COLn is said to be satisfiable iffthere 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α Ą Ki Kiα |ù 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 fpi, 1q and all f 1 P f w1 i , f 1, w1 |ù α. Suppose f, w |ù Ki Kiα. Then there is some w1 P fpi, 1q and some f 1 P f w1 i such that f 1, w1 |ù Kiα, that is, some w2 P f 1pi, 1q and some f 2 P f 1w2 i such that f 2, w2 |ù α. However, by definition, fpi, 1q f 1pi, 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: |ù @x Kiα Ą Kip@xαq |ù Dx Kiα Ą Ki Dxα Proof: We show the case for @, the other being analogous. Suppose f, w |ù @x Kiα. By definition, f, w |ù Kiαx m for all names m. By definition, again, for all w1 P fpi, 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α |ù @x Cα Ą 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 |ù CCα. That is, f, w |ù Ekp Elαq for k, l ě 1, and so, f, w |ù 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 |ù Epα Cαq. Clearly, f, w |ù Eα is a contradiction, and so f, w |ù ECα. From the definition of E and C it follows that f, w |ù Ki Ekα for some i and some k ě 1 and hence f, w |ù 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: |ù Kiα Ą α |ù Cα Ą α Proof: Let f be any epistemic state such that every world w P fpi, 1q is such that p P w for some proposition p. Let w be a world such that p < w . Clearly, f, w |ù Kip Ą p showing that |ù Kiα Ą α, and so Cα Ą α cannot be valid. A weaker version in the context of knowledge, however, can be shown: |ù Kip Cα Ą αq Proof: Suppose f, w |ù Kip Cα Ą αq. Then for some w1 P fpi, 1q and f 1 P f w1 i , f 1, w1 |ù p Cα Ą α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 iff instead of the if for Ki to test that the pairs pf 1, w1q, where w1 P fpi, 1q and f 1 P f w1 i , are models of α. So Oiα implies Kiα. This does not extend to common knowledge, because Oip, where p is a proposition, means that i knows nothing about the beliefs of other agents: |ù Oip Ą Cp Proof: Suppose f, w |ù Oip Cp. It is easy to see that f, w |ù Oip Ą Ki K jp for j , i that contradicts the truth of Cp at pf, wq. In general, however, |ù 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 Oip is impossible: |ù COip Proof: Suppose f, w |ù COip. Then, f, w |ù Ki K j Kip, letting j , i. By definition of Oi, it is easy to show that Oip Ą Ki K j Kip is valid. Because f, w |ù COip, we have f, w |ù Ki Oip, and so, f, w |ù Ki Ki K j Kip, which is a contradiction. Of course, then, common knowledge that p is not the only thing known is satisfiable: C Oip is satisfiable Proof: Let w any world such that p < w. Let U1 twu, and inductively, Uk 1 pw, Uk, . . . , Ukq ( . Let f be a proper epistemic structure such that fpj, 1q U1 and fpj, kq Uk for all j. Then, f, w1 |ù C Oip for any w1. A knowledge base can believe p and also believe that p is common knowledge: Oipp Cpq is satisfiable Proof: Let U1 tw | p P w, w P Wu, and inductively, let Uk 1 pw, Uk, . . . , Ukq | w P U1( . Then, let fpi, kq Uk 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: |ù Oi Cp Proof: Suppose f, w |ù Oi Cp. By definition, w1 P fpi, 1q and f 1 P f w1 i ifff 1, w1 |ù Cp. Since the truth of Cp does not depend on the actual world, fpi, 1q W. This means that f, w |ù Kip, which is a contradiction. In fact, the following also holds (as observed for the single agent case in [Levesque and Lakemeyer, 2001]): |ù Oi Kip Intuitively, saying that all that is known about the world is Kip 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 Ek and w P W as defined here. So a formula α of depth k is said to be satisfiable iffthere is such a tuple. If α is true wrt every pe1 a, e1 b, wq, where e1 i 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 fpi, kq ei. Then: f, w |ù α iffea, eb, w |ù1 α. By means of an induction on α, one can argue that formulas of depth k are true wrt pf, wq iffthey 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 Ek: Proposition 9: For every pair pea, ebq, where ei P Ek for any k, there is a f such that fpi, 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: |ù α iff|ù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 Ek, 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 iffEkα 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 pf, wq is called a knowledge model ifffor all i, we have w P fpi, 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: As is needed, knowledge models will be assumed for the developments in subsequent sections. 3For a language with quantification, OLn differs 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 fpi, 1q and w P f 1pi, 1qu for k ą 1, f pi, kq tpw, e1, . . . , enq | pw, e1, . . . , enq P fpi, kq and pw, e1, . . . , enq P f 1pi, 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 |ù K jα and f 1, w |ù K jβ then f X f 1, w |ù K jpα βq; if f, w |ù p Kjβ K j βq and f 1 is as before, then f X f 1, w |ù K jβ. We define the meaning of α P COL n inductively as before, with the following new rule: f, w |ù rφsα ifff, 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φs Kiα 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 ifff, w |ù φ implies f|φ, w |ù p. We claim f, w |ù φ implies f|φ, w |ù p ifff, w |ù φ Ą p. Suppose f, w |ù φ, then the LHS is vacuously true but then so is the RHS. Conversely, suppose f, w |ù φ. Then f|φ, w |ù p iff(by definition) p P w ifff, w |ù p because the epistemic state is irrelevant iff(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 All Muddy is true, where: All Muddy m1 . . . mn 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 All Muddy and the knowledge bases for every i: Oip Others Muddy p Xmi _ X miq Cp At Least Oneqq where, Others Muddy Ź j,i mj captures (a); Xα Ź j,i K jα abbreviates they know for (b); At Least One Ž 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: No K1m1 . . . Knmn. The puzzle, then, is: Theorem 17: |ù Σ Ą n 1 times hkkkkkkikkkkkkj r Nos . . . r Nosp K1m1 . . . Knmnq. After pn 1q occurrences of No,4 the children know that they have muddy foreheads. To better see the knowledge bases 4More 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 At Least One 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. in action, we give the argument for n 2; that is, suppose I ta, bu, and we are to prove: |ù Σ Ą r Nosp Kama Kbmbq. Proof: Let pf, wq be a knowledge model for Σ and let f 1 be the epistemic state where Oap No Cp Noqq Obp No Cp Noqq 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, p Kbpma _ mbq Kb maq Ą Kbmb is valid. (In contrast, p Kbpma _mbq Kbmaq Ą Kbmb is falsifiable.) Let α denote Kbpma_mbq, β denote Kb ma, γ denote Kbmb 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 At Least One is common knowledge in Σ, f, w |ù Ka Kb At Least One, 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 |ù Kap Kbma _ 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 |ù Ka Kbma. When knowledge is true the sentence Kbψ Ą ψ is valid, and so f X f 1, w |ù Kama. 7 Related Work 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 differ 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 offthe 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 different levels. While at level 1 our concepts match (that is, just worlds), a level 2 structure of theirs is already different 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 differs 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. [Baltag et al., 1998] A. Baltag, L. S. Moss, and S. Solecki. The logic of public announcements, common knowledge, and private suspicions. In Proc. TARK, pages 43 56, 1998. [Barwise, 1981] J. Barwise. Scenes and other situations. Journal of Philosophy, 78(7):369 397, 1981. [Belle and Lakemeyer, 2010] V. Belle and G. Lakemeyer. Multiagent only-knowing revisited. In Proc. KR, pages 49 60, 2010. [Belle and Lakemeyer, 2015] V. Belle and G. Lakemeyer. Semantical considerations on multiagent only knowing. Artif. Intell., 223:1 26, 2015. [Elgot-Drapkin, 1991] J. J. Elgot-Drapkin. Step-logic and the threewise-men problem. In Proc. AAAI, pages 412 417, 1991. [Fagin et al., 1991] R. Fagin, J. Y. Halpern, and M. Y. Vardi. A model-theoretic analysis of knowledge. J. ACM, 38(2):382 428, 1991. [Fagin et al., 1995] R. Fagin, J. Y. Halpern, Y. Moses, and M. Y. Vardi. Reasoning About Knowledge. MIT Press, 1995. [Gamow and Stern, 1958] G. Gamow and M. Stern. Puzzle Math. New York: Viking Press, 1958. [Gerbrandy and Groeneveld, 1997] J. Gerbrandy and W. Groeneveld. Reasoning about information change. J. of Logic, Lang. and Inf., 6(2):147 169, April 1997. [Halpern and Lakemeyer, 1995] J. Y. Halpern and G. Lakemeyer. Levesque s axiomatization of only knowing is incomplete. Artif. Intell., 74(2):381 387, 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. [Hintikka, 1962] J. Hintikka. Knowledge and belief: an introduction to the logic of the two notions. Cornell University Press, 1962. [Hughes and Cresswell, 1972] G. E. Hughes and M. J. Cresswell. An introduction to modal logic. Methuen London, 1972. [Kraus and Lehmann, 1988] S. Kraus and D. J. Lehmann. Knowledge, belief and time. Theor. Comput. Sci., 58:155 174, 1988. [Kripke, 1963] S. Kripke. Semantical considerations on modal logic. Acta Philosophica Fennica, 16:83 94, 1963. [Lakemeyer, 1993] Gerhard 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. [Levesque, 1990] H. J. Levesque. All I know: a study in autoepistemic logic. Artif. Intell., 42(2-3):263 309, 1990. [Lutz, 2006] C. Lutz. Complexity and succinctness of public announcement logic. In Proc. AAMAS, 2006. [Moses et al., 1986] Y. Moses, D. Dolev, and J. Y. Halpern. Cheating husbands and other stories: A case study of knowledge, action, and communication. Distributed Computing, 1(3), 1986. [Pratt-Hartmann, 2000] I. Pratt-Hartmann. Total knowledge. In Proc. AAAI, pages 423 428, 2000. [van Der 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. [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., 2007] H. van Ditmarsch, W. van der Hoek, and B. Kooi. Dynamic Epistemic Logic. Springer, 2007. [Waaler and Solhaug, 2005] A. Waaler and B. Solhaug. Semantics for multi-agent only knowing: extended abstract. In Proc. TARK, pages 109 125, 2005. [Waaler, 2004] A. Waaler. Consistency proofs for systems of multiagent only knowing. In Advances in Modal Logic, pages 347 366. College Publications, 2004.