Logician Raymond Smullyan has written several books (e.g. What is the Name of this Book?, Prentice Hall, 1978), in which many word problems are stated and proved. We show off the use of equational logic with one of his problems, which was brought to our attention and solved by Michael Barnett.

A group of three people, each of which is a knight (tells the truth
all the time) or a knave (lies all the time) are talking. *B*
says that *C* and *D* are the same type (both knaves or
both knights). Someone then asks *D*, ``Are *B* and
*C* the same type?'' What does *D* answer?

Here's our solution. Let *b* stand for "*B*" is a
knight", and similarly for *c* and *d*. The statement
``*C* and *D* are the same type'' is formalized as
*c* == *d*. Since *B* said it, we have
*b* == (*c* == *d*). *D*'s answer can be
formalized as *b* ? *c*, where ? is either ==
if *D* answers ``yes'' or /== if *D* answers ``no'', and
we have to determine which it is. Since *D* answers, we write
this as *d* == (*b* ? *c*).

We manipulate *d* == *b* ? *c* under the
assumption *b* == *c* == *d*. In the
manipulation, we omit all parentheses because == is associative and ==
and /== are mutually associative.

By inference rule Equanimity, the last line is a theorem. But the last line is a theorem only if ? is ==. Therefore, we conclude thatd==b?c--Fact

= < Factb==c==d>

b==c==b?c

Lest the reader thinks that the answer is obvious because of our simple proof, we give Smullyan's answer, an answer that many people might give if they did not think about formalizing and then manipulating. It is filled with confusing case analysis:

Return to table of contentsI'm afraid we can solve this problem only by analysis into cases.

Case One:Bis a knight. ThenC,Dreally are of the same type. IfDis a knight, thenCis also a knight, hence is of the same type asB, soDbeing truthful answers ``yes''. IfDis a knave, thenCis also a knave (since he is the same type asD), hence is of a different type thanB. SoD, being a knave, lies and answers ``yes''.

Case Two:Bis a knave. ThenC,Dare of different types. IfDis a knight, thenCis a knave, hence he is of the same type asB. SoD, being a knight, answers ``yes''. IfDis a knave, thenC, being of different type thanD, is a knight, hence of a different type thanB. ThenD, being a knave, lies aboutBandCbeing of different types and answer ``yes''.