[Part 11] A Propositional Logic approach to Raymond Smullyan's Knights and Knaves puzzles Third example

In this post, we will solve our third Knights and Knaves puzzle, both informally and formally.

For our third example, we will use the seventh puzzle in Chapter 3 (or the \(32^{nd}\) puzzle overall) 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 page 22 of the 2011, paperback Dover Recreational Math edition [ISBN: 9780486481982], the puzzle reads:

[Again we have three people, A, B, C] Suppose [...] A and B say the following:

A: All of us are knaves.
B: Exactly one of us is a knave. 

Can it be determined what B is? Can it be determined what C is?

As was the case for our first two puzzles, we will first solve this one informally.

In the second part of this post, we will check our solution with two different, automatically generated proofs.

Informal solution

First, A must be a knave. Otherwise, as a knight who never lies, A could never state that all three of them (including A) are knaves.

Next, if B is a knight, then C must also be a knight. This is because B's statement is true and we already know that A is the knave.

Finally, if B is knave, then her statement is false, which means that there must be either two or three knaves (recall, A is definitely a knave). Since A and B are knaves, C can be either a knight or a knave, according to B's statement. But if C were a knave, all three would be knaves, which contradicts A's statement's being false.

In conclusion, there are two possible solutions to this puzzle:

1. A is a knave, whereas B and C are knights.
2. A and B are knaves, whereas C is a knight.

More precisely, to answer the puzzle's two questions:

• Can it be determined what B is?
  • No, B can be either a knave or a knight.
• Can it be determined what C is?
  • Yes, C must be a knight.

We will now prove that these answers are correct using two different formal methods.

Since the first step in formalizing a puzzle is to translate its statement into propositional logic, we do this first.

Using the representation scheme described earlier in this series, A's statement becomes the formula:

\(A \leftrightarrow (-A\ \&\ {-B}\ \&\ {-C})\)

Similarly, B's statement becomes the formula:

\(B \leftrightarrow (({-A}\ \&\ {B}\ \&\ {C})\ |\ ({A}\ \&\ {-B}\ \&\ {C})\ |\ ({A}\ \&\ {B}\ \&\ {-C}))\)

Now we can use this logical formulation of the puzzle in two different ways.

Formal solution #1

In this first formal approach, we will feed the puzzle statement to Mace4 and compare its output to our solution.

Given the input:

Mace4 produces the following output:

As was discussed in a previous post, to get this output, I set Mace4's "max models" parameter to 8 (since the puzzle uses three propositions, each of which can be True or False in a model, and \(2^3 = 8\)). I also used the "Isofilter..." post-processing step described in the same earlier post to eliminate duplicate models.

Mace4's output above gives us the two solutions we found by reasoning informally, thereby formally proving the correctness of our reasoning.

Alternatively, we could have manually built a truth table for the conjunction of the two puzzle formulas; however, that would have been much more tedious than running Mace4!

Formal solution #2

In this second formal approach, we will feed the puzzle statement and its solution to Prover9 to let it find a contradiction.

Since there are two possible solutions, at least one of them must hold, which yields the following disjunction:

\( (-A\ \&\ {-B}\ \&\ C )\ |\ (-A\ \&\ {B}\ \&\ C)\)

which simplifies to:

\( -A\ \&\ C \)

since the truth value of \(B\) does not matter, but \(A\) and \(C\) must be False and True, respectively.

We are now ready to feed both the puzzle statement and this solution formula to Prover9.

Now, given the input:

Prover9 outputs the following proof:

Again, we were able to use Prover9 to confirm, using a proof by contradiction, the correctness of our solution to the puzzle.