



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 calculational 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" isformalized 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 "n"', 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. d
== b ? c Fact 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. His answer is filled with confusing case analysis: I'm afraid we can solve this problem only by analysis into cases. 