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 knows the color of his spot in world by saying that in all worlds accessible from , the color of the spot is the same as in .

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 are the subset of those accessible at time 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.

denotes the real world, and are variables ranging over worlds.

We use natural numbers for times.

, and are the three wisemen. is a fictitious person who knows whatever , and 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 knows that knows that knows that knows etc. Instead of introducing , we could introduce prefixes of like `` knows that knows'' as objects and quantify over prefixes.

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

There are two colors - white and black.

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.

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.

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

We need to delimit the set of wise men.

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

This ad hoc axiom is the penalty for introducing 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 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 's spot.

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

In fact all spots are white.

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

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.

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

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

which is the assertion that at time , the third wise man knows the color of his spot. As intermediate results we had to prove that previous to time , 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 .

2007-11-19