[Part 4] Raymond Smullyan's Knights, Knaves, and Normals puzzles First puzzle, solved with Mace4

Being comfortable with predicate logic and our new representation principle, we are now ready to automate the solution of our first puzzle.

For our first example, we will use the \(39^{th}\) puzzle in Chapter 3 of Raymond Smullyan's 1978 book entitled "What Is the Name of This Book?: The Riddle of Dracula and Other Logical Puzzles". As stated on pages 23 and 24 of the 2011, paperback Dover Recreational Math edition [ISBN: 9780486481982], the puzzle reads:

We are given three people, A, B, C, one of whom is a knight, one a knave, and one normal (but not necessarily in that order). They make the following statements:

A: I am normal.

B: That is true. 

C: I am not normal. 

What are A, B, and C?

The informal answer given by Smullyan in the book (on page 32) is a proof by cases. I will not spoil the fun of your coming up with a solution on your own. 

Once you have solved this puzzle, come back here to check your solution and read about how to obtain a formal proof of the solution.

First, we represent the constraint shared by all puzzles that take place on this island: everybody is a knight, a knave, or (a) normal, but cannot be of more than one type. As we discussed earlier in this series, one formal representation of this constraint is the following set of four axioms:

\(∀x\ (Kni(x)\ |\ Kna(x)\ |\ Nor(x))\)

\(∀x\ (Kni(x) \rightarrow (-Kna(x)\ \&\ {-Nor(x)}))\)

\(∀x\ (Kna(x) \rightarrow (-Kni(x)\ \&\ {-Nor(x)}))\)

\(∀x\ (Nor(x) \rightarrow (-Kni(x)\ \&\ {-Kna(x)}))\)

Second, we need to represent the fact that we are dealing with 3 distinct inhabitants. We will refer to them by the constants \(A\), \(B\), and \(C\). 

However, to a theorem prover, having three different names (i.e., constants) does not prevent two (or more) of these names to refer to the same individual (like, e.g., the names "Clark Kent" and "Superman").

Therefore, we must make it explicit that these three constants do refer to three distinct islanders. We can do so using the equality predicate as follows:

\(-Equal(A,B)\ \&\ {-Equal(A,C)}\ \&\ {-Equal(B,C)}\)

Now, Mace4,  the theorem prover we chose, uses the infix notation \( x\ !\!=\ y\) instead of the (prefix) predicate notation \(-Equal(x,y)\). 

Therefore, we will use this notation as well to rewrite the formula above as:

\(A\ !\!=\ B\quad \&\quad A\ !\!=\ C\quad \&\quad B\ !\!=\ C\)

Third, we need to represent the fact, specific to this puzzle, that among the three inhabitants, there is one of each type. This becomes:

\(∃x\ Kni(x)\)
\(∃x\ Kna(x)\)
\(∃x\ Nor(x)\)

Finally, we must represent the three islanders' statements.

A's statement, "I am normal", becomes the formula \(\varphi_A\):

\(Nor(A)\)

B's statement, "That is true" (interpreted as "A is normal"), becomes the formula \(\varphi_B\):

\(Nor(A)\)

Note that B's agreeing with A means that A and B's statements are identical.

C's statement, "I am not normal", becomes the formula \(\varphi_C\):

\(-Nor(C)\)

Of course, we do not know the truth value of these three statements. We just know that one of the inhabitants uttered one of them, respectively.

We will apply our representation principle to reflect this last component of the puzzle, namely:

---

 Representation principle for Knights, Knaves, and Normals puzzles

For any person P living on this island and any statement S
(with P represented by constant \(P\) 
and S represented by formula \(\varphi\)),
the fact that P said S
will be represented by the formula:

\((Kni(P)\ \&\ \varphi)\ |\ (Kna(P)\ \&\ {-\varphi})\ |\ Nor(P)\)

---

The application of this principle to the three puzzle statements, yields the three formulas:

\((Kni(A)\ \&\ Nor(A))\ |\ (Kna(A)\ \&\ {-Nor(A)}\ |\ Nor(A)\)
\((Kni(B)\ \&\ Nor(A))\ |\ (Kna(B)\ \&\ {-Nor(A)})\ |\ Nor(B)\)
\((Kni(C)\ \&\ {-Nor(C)})\ |\ (Kna(C)\ \&\ {Nor(C)})\ |\ Nor(C)\)

Now, these three formulas simplify to:

\(Kna(A)\ |\ Nor(A)\)
\((Kni(B)\ \&\ Nor(A))\ |\ (Kna(B)\ \&\ {-Nor(A)})\ |\ Nor(B)\)
\(Kni(C)\ |\ Nor(C)\)

because:

1. The sub-formula \((Kni(A)\ \&\ Nor(A))\) in the first formula is always false, and can thus be deleted (as one disjunct of the whole formula).
2. The sub-formula \((Kna(A)\ \&\ {-Nor(A)})\) in the first formula reduces to \(Kna(A)\), since being a knave implies (see axiom above) not being normal.
3. The sub-formula \((Kni(C)\ \&\ {-Nor(C)})\) in the third formula reduces to \(Kni(C)\), since being a knight implies (see axiom above) not being normal.
4. The sub-formula \((Kna(C)\ \&\ {Nor(C)})\) in the third formula is always false, and can thus be deleted (as a disjunct of the whole formula).

Collecting all of the formulas we need according to the discussion above, we get the following input to Mace4:

Two comments on this input:

• We need to remember to add the period at the end of each formula.
• The quantifiers are handled like this in Mace4:
• \(∃ x\ \varphi\), for any formula \(\varphi\), becomes \((exists\ x\ \varphi)\)
• \(∀ x\ \varphi\), for any formula \(\varphi\), becomes \(all\ x\ \varphi\), or simply, \(\varphi\), since all variables (e.g., \(x\), \(y\), \(z\)) are universally quantified in Mace4 by default.

As explained in a previous post, we run Mace4 on this input. In this case, we set the following options for Mace4:

• domain_size is set to 3, since we have exactly three islanders in our domain for this specific puzzle.
• max_models is set to 6, in case there happens to be more than one solution (or model) for this puzzle. 

The output generated by Mace4 is the following:

which we interpret as follows:

1. The first line indicates that there is only one model (or puzzle solution) found and that it contains three inhabitants.
2. The three middle lines show that Mace4 created its own three names for our inhabitants (namely, c1, c2, and c3), which are internally represented by the integers 2, 0, and 1, respectively. These three integers will be used below to reference our islanders by indices in three-element arrays.
3. The first three lines show that our islander A is associated with the index 0, our islander B is associated with the index 1, and our islander C is associated with the index 2.
4. The last three lines indicate that only the islander with index 0 (that is, A) is a knave, only the islander with index 2 (that is, C) is a knight, and only the islander with index 1 (that is, B) is normal.

So Mace4 determined (i.e., proved) on its own that the only solution to the puzzle is:

• A is a knave
• B is normal
• C is a knight

Did you solve this puzzle correctly?