--- title: "W-JS: A Modal Logic of Knowledge" authors: - "Xiwen Ma" - "Weide Guo" doi: "" url: "https://ijcai.org/proceedings/1983/96" pdf: "https://ijcai.org/proceedings/1983/0096.pdf" venue: "Proceedings of the Eighth International Joint Conference on Artificial Intelligence" year: 1983 pages: "398-400" track: "Knowledge Representation" keywords: --- # W-JS: A Modal Logic of Knowledge Xiwen Ma, Weide Guo *Proceedings of the Eighth International Joint Conference on Artificial Intelligence*, pages 398-400. ## Abstract W-JS is a first-order predic ate ca lculus on the modal theory of knowledge. It is based on natural deduction rules and accompanied by possible-worldaccessibility semantics . As an example, the famous "Mr. S and Mr. P" puz7.le is solved in W-JS. ## Full text ## W-JS: A MODAL LOGIC OF KNOWLEDGE Ma Xiwen Guo Weide Computer Science Institute, Peking University, Beijing ## ABSTRACT W-JS is a first-order predicate calculus on the modal theory of knowledge. It is based on natural deduction rules and accompanied by possible-world­ accessibility semantics. As an example, the famous "Mr. S and Mr. P" puz7.le is solved in W-JS. ## I INTRODUCTION Reasoning about knowledge is one of the areas which has received the most attenti<m from researchers in AI. J. McCarthy and others (McCarthy, et al., 1978) have given a propositional modal logic of knowledge and some examples solved in it. But it is obvious that the famous Mr. Sand Mr. P puzzle (see Appendix) can­ not be effectively formulated in a propositional modal logic. And, in a personal communication, J. McCarthy let us know that he had challenged the modal logicians to solve this puzzle. What we presellt here is a solu­ tion, we believe. This is a brief version of our paper (Ma and Guo, 1982). ## II W-LANGUAGES W-languages are extensions of the usual first-order languages. To express the statements about knowledge, we distinguish three cases: S: p (S knows that p) S! p (S knows whether p) S * c (S knows what c is) where pis a wff, cis a term, and Sis a subject symbol. In addition, we use S%p to denote "S accepts p" or "S doesn't know that ·p". Here is a short description of the syntax of W­ languages. Symbols: A symbol is one of the following: Subject symbols; Constant symbols; Concept symbols; Variable symbols; Function symbols; Predicate symbols; Terms: A term is one of the following: A constant symbol; A concept symbol; A variable symbol; f(tl, ... , tn) where f is an n-ary function symbol, and t1, ... , tn are n terms. Subject-terms: A subject-term is a finite string of subject symbols. Formulas: A formula is one of the following: t1 = t2 where t11 t2 are terms; P(tt, ... , tn) where P is an n-ary predicate symbol, and t1, ... , tn are n terms; ·p where p is a formula; p ~ q where p and q are formulas; Vx p where p is a formula and x is a variable sym­ bol; S: p where p is a formula and S is a subject-term. We will use the conventional abbreviations p 1\ q, p V q, p +--+ q, and 3x p. In addition, the following abbreviations are new: S ! p for S : p V S : ·p We also use the conventional terminology for bound/free variables and closed formulas. In addition, the substitution p[tja] will be used for arbitrary closed formula p, term t, and constant symbol a. The deduction rules are (in the following rules, S, S1 are subject-terms, p, Pl, . .. , Pn, q, r are closed formulas, and G, G1 are finite sets of closed formulas): - (1) G 1- p provided p E G - (2) G 1- p provided G 1- G1, G1 1- p - (3) G i- p provided G, ·p 1- q, ·q - (4) p, p ----+ q 1- q - (5) G 1- p ----+ q provided G, p 1- q - (6) 1- t = t provided t is a variable-free term - (7) G 1- \fx p[ x /a] provided G 1- p and x is not f1-ee in any members of G - (8) p[tl/a], t1 = t2 1- p[t2/a] where t1, t2 are variable-free terms and p is a closed formula which is both concept-free and subject-free or where t11 t2 are terms which are both variable-free and concept-free and p is any for­ mula - (9) \fxp[x/a]l- p[tja] where tis a variable-free term and p is a formula which is both concept-free and subject-free or where tis a term which is both variable-free and concept-free and p is any formula Be careful with the rules (8) and (9). - (10) S:pl-p - (11) S:p1, ... , S:pn, G 1- S:q provided Pl> ... , Pn, G 1q where all formulas in G arc both concept-free and subject-free - (12) r- S: S1: p V S: ·S1 : p where all subject symbols in s occur in sl ## Ill JS-SEMANTICS OF W-LANGUAGES JS-semantics is a possible-world-accessibility semantics of W-languages. The details will not be presented here. Within JS-semantics, the deduction rules are sound. But the completeness problem is still open. ## IV EXAMPLE We will solve the Mr. Sand Mr. P puzzle as below. Let the subject symbols So, S1, S2, Po, P1, P2 denote Mr. S and Mr. Pat different times, the concept symbol c denotes the pair of the selected numbers and the function symbols s, p denote the sum and product. Thus, we have: So* s(c) (At time 0, Mr. S knows what the sum is.) Po * p(c) (At time 0, Mr. P knows what the product is.) Let K0 be the conjunction of the above four for­ mulas. Then we have SoPo:Ko (at time 0, Mr. Sand Mr. P jointly know that Ko.) When Mr. S said: I know you don't· know what c is, but I don't know either. It is just said that which we will denote by D0 . Thus there is a distinction between Po's knowledge and P1 's, and it is just Do: We will use K 1 to denote the conjunction of the above formula and Thus we have Similarly, we will use Dt to denote and K 2 to denote the conjunction of Thus we have Finally, we denote by D2. We will solve the puzzle by deducing a suitable first-order formula from First of all, we can prove From these we easily obtain and We define Eo(z) as 3yo (p(yo) = p(z) 1\ ·Yo = z), then Proceeding as in (SPl) - (SP3), we can obtain On the other hand, we can prove Thus, the ordinary first-order calculus will give Then we have Further, at time 1, we obtain and we can prove Then we have Using (SP9), we have which will deduce thus, Then we can prove and finally where E 3 (c) is an abbreviation of This is what we wanted. ## APPENDIX Mr. S and Mr. P puzzle: Two numbers m and n are chosen such that Mr. Sis told their sum and Mr. Pis told their product. The following dialogue ensues: - Mr. S: I know you don't know the numbers. I don't know them either. Mr. P: Now I know the numbers. Mr. S: Now I know them too. In view of the above dialogue, what are the num­ bers? ## References 1. John McCarthy, et al., "On the Model Theory of Knowledge," Memo AIM 312, Stanford University, 1978. 2. Ma Xiwen, Guo Weide, "W-JS: A Modal Logic about 'Knowing'," Computer R esearch and Development, No. 12, Vol. 19, Beijing, 1982.