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

In this post, we will solve our fourth Knights and Knaves puzzle, both informally and formally. This puzzle is the first one to use the phrase "of the same type".

For our fourth example, we will use the ninth puzzle in Chapter 3 (or the \(34^{th}\) 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:

We again have three inhabitants, A, B, and C, each of whom is a knight or a knave. Two people are said to be of the same type if they are both knights or both knaves. A and B make the following statements:

A: B is a knave.
B: A and C are of the same type. 

What is C?

As was the case for our first three 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

If B is a knight, then A lied and must be a knave. In this case, B's statement is true and C must be of the same type as A, that is, a knave.

If B is a knave, then A told the truth and is a knight. In this case, B's statement is false and C must be of a different type from A. Therefore, C is a knave.

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

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

More precisely, to answer the puzzle's question:

• What is C?
  • C must be a knave, since that fact holds in both solutions above.

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 is straightforward now and becomes the formula:

\(A \leftrightarrow {-B}\)

B's statement, however, is not one we have seen before, since it uses the new "same type" concept.

If A and C are of the same type, then the associated \(A\) and \(C\) propositions must always have the same truth value. In other words, it must hold that:

\(A \leftrightarrow C\)

Since B made this statement, the second part of the puzzle becomes:

\(B \leftrightarrow (A\ \leftrightarrow\ 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 a bit 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 the solution to the puzzle is that C is a knave, the goal formula is:

\( -C\)

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.