Did you know ... Search Documentation:
Pack logicmoo_nars -- ImportantDocs/jmc/puzzles.md

FORMALIZATION OF TWO PUZZLES

INVOLVING KNOWLEDGE

John McCarthy

Computer Science Department

Stanford University

Stanford, CA 94305

jmc@cs.stanford.edu

http://www-formal.stanford.edu/jmc/

1978-1981

This paper describes a formal system and uses it to express the puzzle of

the three wise men and the puzzle of Mr. S and Mr. P. Four innovations in

the axiomatization of knowledge were required: the ability to express joint

knowledge of several people, the ability to express the initial non-knowledge,

the ability to describe knowing what rather than merely knowing that, and the

ability to express the change which occurs when someone learns something.

Our axioms are written in first order logic and use Kripke-style possible

worlds directly rather than modal operators or imitations thereof. We intend

to use functions imitating modal operators and taking “propositions” and

“individual concepts” as operands, but we haven’t yet solved the problem of

how to treat learning in such a formalism.1

11997: The puzzle of the three wise men is old and well known. I have not been able to

trace Mr. S and Mr. P back beyond its alleged appearance on a bulletin board at Xerox

PARC. 2005 note: The puzzle has been recently traced to the Dutch mathematician Hans

Freudenthal. Freudenthal didn’t publish it and didn’t give a reference. The consensus

opinion is that Freudenthal invented it.

![139647661408464](images/139647661408464)

1 THE PUZZLES

The three wise men puzzle is as follows:

A certain king wishes to test his three wise men. He arranges them in a

circle so that they can see and hear each other and tells them that he will put

a white or black spot on each of their foreheads but that at least one spot will

be white. In fact all three spots are white. He then repeatedly asks them, “Do

you know the color of your spot?” What do they answer?

The solution is that they answer, “No,” the first two times the question

is asked and answer “Yes” thereafter.

This is a variant form of the puzzle. The traditional form is:

A certain king wishes to determine which of his three wise men is the

wisest. He arranges them in a circle so that they can see and hear each other

and tells them that he will put a white or black spot on each of their foreheads

but that at least one spot will be white. In fact all three spots are white. He

then offers his favor to the one who will first tell him the color of his spot.

After a while, the wisest announces that his spot his white. How does he

know?

The intended solution is that the wisest reasons that if his spot were

black, the second would see a black and a white and would reason that if his

spot were black, the third would have seen two black spots and reasoned from

the king’s announcement that his spot was white. This traditional version

requires the wise men to reason about how fast their colleagues reason, and

we don’t wish to try to formalize this.

Here is the Mr. S and Mr. P puzzle:

Two numbers m and n are chosen such that 2 ≤ m ≤ n ≤ 99.

Mr. S is told their sum and Mr. P is told their product. The following

dialogue ensues: Mr. P: I don’t know the numbers.

Mr. S: I knew you didn’t know. I don’t know either.

Mr. P: Now I know the numbers.

Mr S: Now I know them too.

In view of the above dialogue, what are the numbers?

2007 note: At the time I wrote this article, I was unable to discover the

author. It was Hans Freudenthal, Nieuw Archief Voor Wiskunde, Series 3,

Volume 17, 1969, page 152).

2 AXIOMATIZATION OF THE WISE MEN

The axioms are given in a form acceptable to FOL, the proof checker com-

puter program for an extended first order logic developed by Richard Weyhrauchat 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 oper- ator 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 knowl- edge 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 lan-

    guages. 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 IN DCON ST RW ∈ W ORLD;

    declare IN DV AR w w1 w2 w3 w4 w5 ∈ W ORLD;

    RW denotes the real world, and w, w1,

    . . .

    , w5 are variables ranging

    over worlds.

    declare IN DV AR m n m1 m2 m3 n1 n2 n3 ∈ N AT N U M;

    We use natural numbers for times.

    declare IN DCON ST S1 S2 S3 S123 ∈ P ERSON;

    declare IN DV AR p p0 p1 p2 ∈ P ERSON;

    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 P REDCON ST A(W ORLD, W ORLD, P ERSON, N AT N U M );

    This Kripke-style accessibility relation has two more arguments than is

    usual in modal logic — a person and a time.

    declare IN DV AR c c1 c2 c3 c4 ∈ COLORS;

    declare IN DCON ST W B ∈ COLORS;

    There are two colors - white and black.

    declare OP CON ST color(P ERSON, W ORLD) = 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 ref lex : ∀ 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 :

    ∀w1 w2 w3 p m.(A(w1, w2, p, m)∧A(w2, w3, p, m) ⊃ 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 : ∀p.(p = S1 ∨ p = S2 ∨ p = S3 ∨ p = S123); ;

    We need to delimit the set of wise men.

    axiom w123 :

    ∀w1 w2 m.(A(w1, w2, S1, m)∨A(w1, w2, S2, m)∨A(w1, w2, S3, m)⊃ A(w1, w2, S123, m)); ;

    This says that anything the wise men know jointly, they know individu-

    ally.

    axiom f oolspot : ∀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 : ¬(W = B);

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

    axiom rw : color(S1, RW ) = W ∧color(S2, RW ) = W ∧color(S3, RW ) =

    ∀c.(c = W ∨ c = B); ;

    W ; ;

    In fact all spots are white.

    axiom king : ∀w.(A(RW, w, S123, 0) ⊃ color(S1, w) = W ∨color(S2, w) =W ∨ 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 :

    ∀c w.(A(RW, w, S123, 0) ⊃

    (c = W ∨ color(S2, w) = W ∨ color(S3, w) = W

    ⊃ ∃w1.(A(w, w1, S1, 0) ∧ color(S1, w1) = c))∧

    (c = W ∨ color(S1, w) = W ∨ color(S3, w) = W

    ⊃ ∃w1.(A(w, w1, S2, 0) ∧ color(S2, w1) = c))∧

    (c = W ∨ color(S1, w) = W ∨ color(S2, w) = W

    ⊃ ∃w1.(A(w, w1, S3, 0) ∧ color(S3, w1) = c)));

    ∀w w1.(A(RW, w, S123, 0) ∧ A(w, w1, S1, 0)

    color(S2, w1) = color(S2, w)color(S3, w1) = color(S3, w));

    ∀ww1.(A(RW, w, S123, 0) ∧ A(w, w1, S2, 0)

    color(S1, w1) = color(S1, w)color(S3, w1) = color(S3, w));

    ∀w w1.(A(RW, w, S123, 0) ∧ A(w, w1, S3, 0)

    color(S1, w1) = color(S1, w)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 :

    ∀w.(A(RW, w, S123, 1) ≡ A(RW, w, S123, 0)

    ∧∀p.(∀w1.(A(w, w1, p, 0) ⊃ color(p, w1) = color(p, w))

    ≡ ∀w1.(A(RW, w1, p, 0) ⊃ color(p, w1) = color(p, RW ))));

    ∀w1w2.(A(w1, w2, S1, 1) ≡ A(w1, w2, S1, 0) ∧ A(w1, w2, S123, 1));

    ∀w1w2.(A(w1, w2, S2, 1) ≡ A(w1, w2, S2, 0) ∧ A(w1, w2, S123, 1));

    ∀w1w2.(A(w1, w2, S3, 1) ≡ A(w1, w2, S3, 0) ∧ 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 ∀p in this axiom covers S123 also and

    forced us to say that they jointly know the color of S123’s spot.

    axiom elwek2 :

    ∀w.(A(RW, w, S123, 2) ≡ A(RW, w, S123, 1)

    ∧∀p.(∀w1.(A(w, w1, p, 1) ⊃ color(p, w1) = color(p, w))

    ≡ ∀w1.(A(RW, w1, p, 1) ⊃ color(p, w1) = color(p, RW ))));

    ∀w1w2.(A(w1, w2, S1, 2) ≡ A(w1, w2, S1, 1) ∧ A(w1, w2, S123, 1));

    ∀w1w2.(A(w1, w2, S2, 2) ≡ A(w1, w2, S2, 1) ∧ A(w1, w2, S123, 1));

    ∀w1w2.(A(w1, w2, S3, 2) ≡ A(w1, w2, S3, 1) ∧ A(w1, w2, S123, 1)); ;

    The file WISEMA.PRF[S78,JMC] at the Stanford AI Lab contains a com-

    puter checked proof from these axioms of

    ∀w.(A(RW, w, S3, 2) ⊃ 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.

    3 AXIOMATIZATION OF MR. S AND MR. PThese axioms involve the same ideas as the wise man axiomatization. They

    are a debugged version of the axioms by Ma Xiwen of Peking University,

    which, in turn, were a variant of my earlier axiomatization.

    This formalization separates the knowledge part of the problem from the

    arithmetic part in a neat way. Ma Xiwen verified, using FOL, that his axioms

    imply a certain purely arithmetic condition on the pair of numbers. It can

    be then shown that the only pair satisfying that condition is 4, 13.

    declare indvar t ∈ natnum;

    declare indconst k0 ∈ pair;

    declare indvar k

    k1 k2 k3 ∈ pair;

    declare indconst RW ∈ world;

    declare indvar w w1 w2 w3 ∈ world;

    declare indconst S P SP ∈ person;

    declare indvar r ∈ person;

    declare opconst K(world) = pair;

    declare opconst s(pair) = natnum;

    declare opconst p(pair) = natnum;

    declare predconst A(world, world, person, natnum);

    The predicates Qs, Qp, Q1, Q2, R1, R2 and R3 are represent arithmetic

    conditions on the pair of numbers that are used to express the arithmetic

    conditions on the pair that replace the knowledge conditions given in the

    problem statement.

    declare predconst Qs(pair) Qp(pair) Q1(pair) Q2(pair) Q3(pair);

    declare predconst Bs(world) Bp(world) B1(world) B2(world);

    declare predconst R1(pair) R2(pair) R3(pair);

    declare predconst C1(world) C2(world);

    The first two axioms state that the accessibility relation is reflexive and

    transitive. They assert that what is known is true and one knows that one

    knows what one knows. Got that?

    axiom ar : ∀w r t.A(w, w, r, t); ;

    axiom at : ∀w1 w2 w3 r t.(A(w1, w2, r, t)∧A(w2, w3, r, t) ⊃ A(w1, w3, r, t)); ;This axiom says that the joint person knows what Mr. S and Mr. P both

    know. At first sight it seems too weak, but transitivity tells us that what

    they jointly know, they jointly know they jointly know.

    axiom sp : ∀w1 w2 t.(A(w1, w2, S, t)∨A(w1, w2, P, t) ⊃ A(w1, w2, SP, t)); ;This next axiom is just a definition for the purposes of abbreviation. RW

    is the real world, so k0 is just the real pair.

    axiom rw : k0 = K(RW ); ;

    In the initial situation they jointly know that Mr. S knows the sum and

    Mr. P the product. They also jointly know that this is all that Mr. S and

    Mr. P know about the numbers. This is asserted by saying that given any

    pair of numbers with the right sum, there is a world possible for Mr. S in

    which this is the pair of numbers.

    axiom init :

    ∀w w1.(A(RW, w, SP, 0) ∧ A(w, w1, S, 0) ⊃ s(K(w)) = s(K(w1)));

    ∀w w1.(A(RW, w, SP, 0) ∧ A(w, w1, P, 0) ⊃ p(K(w)) = p(K(w1)));

    ∀w k.(A(RW, w, SP, 0) ∧ s(K(w)) = s(k) ⊃ ∃w1.(A(w, w1, S, 0) ∧ k =

    ∀w k.(A(RW, w, SP, 0) ∧ p(K(w)) = p(k) ⊃ ∃w1.(A(w, w1, P, 0) ∧ k =

    K(w1)));

    K(w1))); ;

    These axioms on the pair will be used to translate knowledge assertions.

    For example, Qs(k) asserts that there is another pair that has the same sum

    as k and is used in the assertion that Mr. S, knowing the sum, does not know

    the pair, i.e. does not know the numbers. As we proceed through the dialog

    the arithmetic conditions become more complex.

    axiom qs : ∀k.(Qs(k) ≡ ∃k1.(s(k) = s(k1) ∧ ¬(k = k1))); ;

    axiom qp : ∀k.(Qp(k) ≡ ∃k1.(p(k) = p(k1) ∧ ¬(k = k1))); ;

    axiom q :

    ∀k.(Q1(k) ≡ ∀k1.(s(k) = s(k1) ⊃ Qp(k1)));

    ∀k.(Q2(k) ≡ ∀k1.(R1(k1) ∧ p(k) = p(k1) ⊃ k = k1));

    ∀k.(Q3(k) ≡ ∀k1.(R2(k1) ∧ s(k) = s(k1) ⊃ k = k1)); ;

    axiom r :

    ∀k.(R1(k) ≡ Qs(k) ∧ Q1(k));

    ∀k.(R2(k) ≡ R1(k) ∧ Q2(k));

    ∀k.(R3(k) ≡ R2(k) ∧ Q3(k)); ;

    Bs(w) asserts that in the possible world w, Mr. S doesn’t know the num-

    bers.

    axiom bs : ∀w.(Bs(w) ≡ ∃w1.(A(w, w1, S, 0) ∧ ¬(K(w) = K(w1)))); ;

    axiom bp : ∀w.(Bp(w) ≡ ∃w1.(A(w, w1, P, 0) ∧ ¬(K(w) = K(w1)))); ;

    axiom b :

    ∀w.(B1(w) ≡ ∀w1.(A(w, w1, S, 0) ⊃ Bp(w1)));

    ∀w.(B2(w) ≡ ∀w1.(A(w, w1, P, 1) ⊃ K(w) = K(w1))); ;

    axiom c :

    ∀w.(C1(w) ≡ Bs(w) ∧ B1(w));

    ∀w.(C2(w) ≡ C1(w) ∧ B2(w)); ;

    The previous axioms were just definitions. Now we have the information

    coming from the dialog. SKNPK stands for “S Knows that P does Not

    Know” and the axiom asserts this about the real world at time 0.

    axiom sknpk : B1(RW ); ;

    NSK stands for “S doesn’t know”, and the axiom asserts this about the

    real world.

    axiom nsk : Bs(RW ); ;

    PK stands for “P knows the numbers”, and the axiom asserts this about

    the real world at time 1.

    axiom pk : B2(RW ); ;

    SK tells us that at time 2, Mr. S knows the numbers.

    axiom sk : ∀w.(A(RW, w, S, 2) ⊃ K(RW ) = K(w)); ;

    The last two axioms are the learning axioms. LS tells us that everyone

    learns by time 1 that Mr. S knew at time 0 that Mr. P didn’t know the

    numbers, and he didn’t know them either. LP tells us that everyone learns

    by time 2 that Mr. P knew the numbers by time 1.

    axiom lp :

    ∀ww1.(A(RW, w, SP, 1) ⊃ (A(w, w1, P, 1) ≡ A(w, w1, P, 0) ∧ C1(w1))); ;

    axiom ls :

    ∀ww1.(A(RW, w, SP, 2) ⊃ (A(w, w1, S, 2) ≡ A(w, w1, S, 1) ∧ C2(w1))); ;

    Ma Xiwen’s proof was carried out using a sequence of lemmas. The first

    lemma shows the essential equivalence of a condition on possible worlds with

    a condition on pairs.

    Lemma 1. ∀wk.(A(RW, w, SP, 0) ∧ k = K(w) ⊃ (Qs(k) ≡ Bs(w))).

    Lemma 2. ∀wk.(A(RW, w, SP, 0) ∧ k = K(w) ⊃ (Qp(k) ≡ Bp(w))).

    Lemma 3. ∀wk.(A(RW.w.SP, 0) ∧ k = K(w) ⊃ (Q1(k) ≡ B1(w))).

    Lemma 4. ∀wk.(A(RW, w, SP, 0) ∧ k = K(w) ⊃ (R1(k) ≡ C1(w))).

    Lemma 5. R2(k0).

    Lemma 6. ∀wk.(A(RW, w, SP, 0) ∧ k = K(w) ⊃ (R2(k) ⊃ C2(w))).

    Lemma 7. Q3(k0).

    Main Theorem. R3(k0).

    R3(k0) is a purely arithmetic condition on the pair of numbers. From

    an axiom asserting that k0 is a pair of numbers in the interval 2 ≤ x ≤ 99

    and Peano’s axioms for arithmetic, the numbers can be proved to be 4 and

    13. Alternatively, R3(k0) can be translated into a computer program for

    computing the numbers. Most people who solve the problem write such a

    program.

    4 References

    Weyhrauch, Richard W. (1977). FOL: A proof checker for first-order logic

    (Stanford Artificial Intelligence Laboratory Memo AIM–235.1). Stanford

    University, Stanford.

    /@steam.stanford.edu:/u/ftp/jmc/puzzles.tex: begun 1996 May 14, latexed 2007 Nov 19 at 12:45 p.m.