Introduction

The need to represent Information about who knows what in intelligence computer programs was the original motivation for this work. For example, a program that plans trips must know that travel agents know who knows the availability of rooms in hotels. An early problem Is how to represent what people know about other people's knowledge of facts, and even the knowledge of propositions treated In this paper presented some problems that were not treated in previous literature.

We started with the following well known puzzle of the three wise men: A king wishing to know which of his three wise men is the wisest, paints a white spot on each of their foreheads, tells them at least one spot is white, and asks each to determine the color of his spot. After a while the smartest announces that his spot is white reasoning as follows: ``Suppose my spot were black. The second wisest of us would then see a black and a white and would reason that if his spot were black, the dumbest would see two black spots and would conclude that his spot is white on the basis of the king's assurance. He would have announced it by now, so my spot must be white."

In formalizing the puzzle, we don't wish to try to formalize the reasoning about how fast other people reason. Therefore, we will imagine that either the king asks the wise men in sequence whether they know the colors of their spots or that he asks synchronously, ``Do you know the color of your spot" getting a chorus of noes. He asks it again with the same result, but on the third asking, they answer that their spots are white. Needless to say, we are also not formalizing any notion of relative wisdom.

We start with a general set of axioms for knowledge based on the notation, axioms, and inference rules of propositional calculus supplemented by the notation S*p standing for, ``Person S knows proposition p." Thus can stand for, ``The third wise man knows that the second wise man knows that the first wise man does not know that the first wise man's spot is white''.

We use axiom schemata with subscripted S's as person variables, subscripted p's and q's as propositional variables, and a special person constant called ``any fool" and denoted by 0. It is convenient to Introduce ``any fool" because whatever he knows, everyone knows that everyone else knows. ``Any fool" is especially useful when an event occurs in front of all the knowers, and we need sentences like, `` knows that knows that knows etc.". Here are the schemata:

K0: ; What a person knows is true.

K1: ; Any fool knows that what a person knows is true.

K2: ; What any fool knows, any fool knows everyone knows, and any fool knows that.

K3: ; Any fool knows everyone can do modus ponens.

There are two optional schemata K4 and K5:

K4: ; Any fool knows that what someone knows, he knows he knows.

K5: ; Any fool knows that what some doesn't know he knows he doesn't know.

If there is only one person S, the system is equivalent to a system of modal logic. Axioms K1-K3 give a system equivalent to what Hughes and Cresswell[1] called T, and K4 and K5 give the modal systems S4 and S5 respectively. We call K4 and K5 the introspective schemata.

It is convenient to write as an abbreviation for ; it may be read ``S knows whether p".

On the basis of these schemata we may axiomatize the wise man problem as follows:

C0:

C1:

C2:

C2:

C3:

C4:

C5:

From K0-K3 and C1-C5 it is possible to prove . C0 is not used in the proof. In some sense C4 and C5 should not be required. Looking at the problem sequentially, it should follow that does not know initially, and that even knowing that, doesn't know .

In order to proceed further with the problem, model theoretic semantics is necessary. In what follows, however, we will deal with the puzzle of unfaithful wives (cf. Section 4) rather than that of three wise men, because the latter may be considered as a simplified version of the former. To do so we must extend the system K5 to KT5 in which one can treat the notion of time as well. We will use slightly different notations in the following sections since they are convenient to denote time and have similarity to those used in ordinary modal logics.

We briefly describe the Hilbert-type formulation of the system KT5 in Section 2, and its model theory in Section 3. Finally, we will sketch the outline of the solution to the puzzle of unfaithful wives in this formalism in Section 4. The reader is referred to Sato[2] for details.