AXIOMATIZATION OF THE WISE MEN

The axioms are given in a form acceptable to FOL, the proof checker computer program for an extended first order logic developed by Richard Weyhrauch at the Stanford Artificial Intelligence Laboratory (Weyhrauch, 1977). FOL uses a sorted logic. Constants and variables are declared to have given sorts, and quantifiers on these variables are interpreted as ranging over the sorts corresponding to the variables.

The axiomatization has the following features:

1. It is entirely in first order logic rather than in a modal logic.

2. The Kripke accessibility relation is axiomatized. No knowledge operator or function is used. We hope to present a second axiomatization using a knowledge function, but we haven't yet decided how to handle time and learning in such an axiomatization.

3. We are essentially treating ``knowing what'' rather than ``knowing that''. We say that $p$ knows the color of his spot in world $w$ by saying that in all worlds accessible from $w$, the color of the spot is the same as in $w$.

4. We treat learning by giving the accessibility relation a time parameter. To say that someone learns something is done by saying that the worlds accessible to him at time $n+1$ are the subset of those accessible at time $n$ in which the something is true.

5. The problems treated are complicated by the need to treat joint knowledge and joint learning. This is done by introducing fictitious persons who know what a group of people know jointly. (When people know something jointly, not only do they all know it, but they jointly know that they jointly know it).

This isn't the place for a description of the FOL interactive theorem prover. However a few remarks will make it easier to read the axioms.

Since FOL uses a sorted logic, it must be told the sorts of the variables and constants, so it can determine whether a substitution is legitimate. This is done by declare statements resembling declarations in programming languages. The notation for formulas in as is usual in logic, so there shouldn't be difficulty reading it. Writing it so that the computer will accept it is a more finicky task.

$declare INDCONST RW \in WORLD;$

$declare INDVAR w w1 w2 w3 w4 w5 \in WORLD;$

$RW$ denotes the real world, and $w, w1, \ldots , w5$ are variables ranging over worlds.

$declare INDVAR m n m1 m2 m3 n1 n2 n3 \in NATNUM;$

We use natural numbers for times.

$declare INDCONST S1 S2 S3 S123 \in PERSON;$

$declare INDVAR p p0 p1 p2 \in PERSON;$

$S1$, $S2$ and $S3$ are the three wisemen. $S123$ is a fictitious person who knows whatever $S1$, $S2$ and $S3$ know jointly. The joint knowledge of several people is typified by events that occur in their joint presence. Not only do they all know it, but $S1$ knows that $S2$ knows that $S1$ knows that $S3$ knows etc. Instead of introducing $S123$, we could introduce prefixes of like ``$S1$ knows that $S2$ knows'' as objects and quantify over prefixes.

$declare PREDCONST A(WORLD,WORLD,PERSON,NATNUM);$

This Kripke-style accessibility relation has two more arguments than is usual in modal logic -- a person and a time.

$declare INDVAR c c1 c2 c3 c4 \in COLORS;$

$declare INDCONST W B \in COLORS;$

There are two colors - white and black.

$declare OPCONST color(PERSON,WORLD) = COLORS;$

A person has a color in a world. A previous axiomatization was simpler. We merely had three propositions WISE1, WISE2 and WISE3 asserting that the respective wise men had white spots. We now need the colors, because we want to quantify over colors.

$axiom reflex: \forall w p m.A(w,w,p,m);;$

The accessibility relation is reflexive as is usual in the Kripke semantics of M. It is equivalent to asserting that what is known is true.

$axiom transitive:$

$\qquad \forall w1 w2 w3 p m.(A(w1,w2,p,m) \land A(w2,w3,p,m) \supset A(w1,w3,p,m));;$

Making the accessibility relation transitive gives an S4 like system. We use transitivity in the proof, but we aren't sure it is necessary.

$axiom who: \forall p.(p=S1 \lor p=S2 \lor p=S3 \lor p=S123);;$

We need to delimit the set of wise men.

$axiom w123:$

$\quad\quad\quad\quad \forall w1 w2 m.(A(w1,w2,S1,m) \lor A(w1,w2,S2,m) \lor A(w1,w2,S3,m)$

$\quad\quad\quad\quad\quad\quad\quad\quad \supset A(w1,w2,S123,m));;$

This says that anything the wise men know jointly, they know individually.

$axiom foolspot: \forall w.(color(S123,w)=W);;$

This ad hoc axiom is the penalty for introducing $S123$ as an ordinary individual whose spot must therefore have a color. It would have been better to distinguish between real persons with spots and the fictitious person(s) who only know things. Anyway, we give $S123$ a white spot and make it generally known, e.g. true in all possible worlds. I must confess that we do it this way here in order to repair a proof that the computer didn't accept on account of people not knowing the color of $S123$'s spot.

$axiom color: \lnot (W=B);\quad \forall c.(c=W \lor c=B);;$

Both of these axioms about the colors are used in the proof.

$axiom rw: color(S1,RW) = W \land color(S2,RW) = W \land color(S3,RW) = W;;$

In fact all spots are white.

$axiom king:$ $\;\forall w.(A(RW,w,S123,0) \supset color(S1,w)=W \lor color(S2,w)=W\lor color(S3,w)=W);;$

They jointly know that at least one spot is white, since the king stated it in their mutual presence. We use the consequence that $S3$ knows that $S2$ knows that $S1$ knows this fact.

$axiom initial:$

$\forall c w.(A(RW,w,S123,0) \supset$

$\quad\quad\quad\quad (c=W \lor color(S2,w)=W \lor color(S3,w)=W$

$\quad\quad\quad\quad\quad\quad\quad\quad \supset \exists w1.(A(w,w1,S1,0) \land color(S1,w1) = c)) \land$

$\quad\quad\quad\quad (c=W \lor color(S1,w)=W \lor color(S3,w)=W$

$\quad\quad\quad\quad\quad\quad\quad\quad \supset \exists w1.(A(w,w1,S2,0) \land color(S2,w1) = c)) \land$

$\quad\quad\quad\quad (c=W \lor color(S1,w)=W \lor color(S2,w)=W$

$\quad\quad\quad\quad\quad\quad\quad\quad \supset \exists w1.(A(w,w1,S3,0) \land color(S3,w1) = c)));$

$\forall w w1.(A(RW,w,S123,0) \land A(w,w1,S1,0)$

$\quad\quad\quad\quad \supset color(S2,w1) = color(S2,w) \land color(S3,w1) = color(S3,w));$

$\forall w w1.(A(RW,w,S123,0) \land A(w,w1,S2,0)$

$\quad\quad\quad\quad \supset color(S1,w1) = color(S1,w) \land color(S3,w1) = color(S3,w));$

$\forall w w1.(A(RW,w,S123,0) \land A(w,w1,S3,0)$

$\quad\quad\quad\quad \supset color(S1,w1) = color(S1,w) \land color(S2,w1) = color(S2,w));;$

These are actually four axioms. The last three say that every one knows that each knows the colors of the other men's spots. The first part says that they all know that no-one knows anything more than what he can see and what the king told them. We establish non-knowledge by asserting the existence of enough possible worlds. The ability to quantify over colors is convenient for expressing this axiom in a natural way. In the S and P problem it is essential, because we would otherwise need a conjunction of 4753 terms.

$axiom elwek1:$

$\forall w.(A(RW,w,S123,1) \equiv A(RW,w,S123,0)$

$\quad\quad\quad\quad \land \forall p.(\forall w1.(A(w,w1,p,0) \supset color(p,w1)=color(p,w))$

$\qquad\quad\quad\quad\quad \equiv \forall w1.(A(RW,w1,p,0) \supset color(p,w1)=color(p,RW))));$

$\forall w1 w2.(A(w1,w2,S1,1) \equiv A(w1,w2,S1,0) \land A(w1,w2,S123,1));$

$\forall w1 w2.(A(w1,w2,S2,1) \equiv A(w1,w2,S2,0) \land A(w1,w2,S123,1));$

$\forall w1 w2.(A(w1,w2,S3,1) \equiv A(w1,w2,S3,0) \land A(w1,w2,S123,1));;$

This axiom and the next one are the same except that one deals with the transition from time $0$ to time $1$ and the other deals with the transition from time $1$ to time $2$. Each says that they jointly learn who (if anyone) knows the color of his spot. The quantifier $\forall p$ in this axiom covers $S123$ also and forced us to say that they jointly know the color of $S123$'s spot.

$axiom elwek2:$

$\forall w.(A(RW,w,S123,2) \equiv A(RW,w,S123,1)$

$\quad\quad\quad\quad \land \forall p.(\forall w1.(A(w,w1,p,1) \supset color(p,w1)=color(p,w))$

$\qquad\quad\quad\quad\quad \equiv \forall w1.(A(RW,w1,p,1) \supset color(p,w1)=color(p,RW))));$

$\forall w1 w2.(A(w1,w2,S1,2) \equiv A(w1,w2,S1,1) \land A(w1,w2,S123,1));$

$\forall w1 w2.(A(w1,w2,S2,2) \equiv A(w1,w2,S2,1) \land A(w1,w2,S123,1));$

$\forall w1 w2.(A(w1,w2,S3,2) \equiv A(w1,w2,S3,1) \land A(w1,w2,S123,1));;$

The file WISEMA.PRF[S78,JMC] at the Stanford AI Lab contains a computer checked proof from these axioms of

$$\forall w.(A(RW,w,S3,2) \supset color(S3,w) = color(S3,RW))$$

which is the assertion that at time $2$, the third wise man knows the color of his spot. As intermediate results we had to prove that previous to time $2$, the other wise men did not know the colors of their spots. In this symmetrical axiomatization, we could have proved the theorem with a variable wise man instead of the constant $S3$.