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

In this post, we will solve our fifth Knights and Knaves puzzle. In this puzzle, instead of having to determine the type of one or more inhabitants, we have to figure out the answer that one inhabitant (whose type is unknown) will give to a question.

For our fifth example, we will use the tenth puzzle in Chapter 3 (or the \(35^{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:

Again three people A, B, and C (sic). A says "B and C are of the same type." Someone then asks C, "Are A and B of the same type?"

What does C answer?

The most direct, informal analysis of this puzzle uses two main cases and four sub-cases. Since it is longer than the previous informal solutions and it is not too exciting, let's just jump right into the formal approaches.

Recall that the first step in formalizing a puzzle is to translate its statement into propositional logic. This step is where this puzzle differs from the previous ones and what justifies our presentation of it.

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

\(A \leftrightarrow (B \leftrightarrow C)\)

For the second part of the puzzle, we start by representing the question that is posed to C, as follows:

\(A \leftrightarrow B\) ?

Of course, the question mark is not part of our formal logical language but is added here to indicate that this is not a stated fact nor even a statement by one of the protagonists.

Recall that we are interested in C's answer to this question. C's answer, and thus the solution of this puzzle, will be either Yes or No.

Now, if C' s answer is Yes, it will be equivalent to C saying: "Yes, A and B are of the same type." 

By the same token, if C' s answer is No, it will be equivalent to C saying: "No, A and B are not of the same type." 

In other words, we can represent C's answer with the formula:

\(C \leftrightarrow (A\ \leftrightarrow\ B)\) \(\qquad(*)\)

This completes our translation of the puzzle statement into propositional logic.

Formal solution #1

Note that, in this puzzle, and unlike all of our previous puzzles, we are not interested in the truth value assigned to the individual propositions (\(A\), \(B\), \(C\)). Instead, we are interested in the truth value of the formula labeled \((*)\) above.

Since Mace4 outputs models, that is, interpretations that make the puzzle statement true, it will produce one or more assignments of truth values to the individual propositions. 

In order for Mace4 to tell us the truth value of the \((*)\) formula, we will introduce a new proposition \(R\) to represent C's reply to the question.

Now, to represent the fact that \(R\) has the same truth value as \((*)\), we can use this logical formula:

\(R \leftrightarrow (C \leftrightarrow (A\ \leftrightarrow\ B))\)

which we add to A's statement to make up the logical translation of the puzzle.

So, 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 16 (since the puzzle uses four propositions, each of which can be True or False in a model, and \(2^4 = 16\)). I also used the "Isofilter..." post-processing step described in the same earlier post to eliminate duplicate models.

Mace4's output above gives us four distinct models. In other words, there are four combinations of truth values for \(A\), \(B\), \(C\), and \(R\) that make the puzzle statement true.

However, in all four models, the value of \(R\) is True, which is the answer to the puzzle's question.

In the end, this puzzle has a unique solution: C will answer Yes to the question "Are A and B of the same type?"

Interestingly, the pair of inhabitants A and B could be any combination of knights and/or knaves as shown by the truth values assigned to \(A\) and \(B\) in the four models above.

But in all cases, C's answer to the question is always the same due to C's type changing from knight to knave and then to knight again when going through the four models.

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.

Of course, the puzzle is still encoded by the same two formulas as above.

However, the goal we are trying to prove is that the proposition \(R\) is true, since \(R\) represents the reply given by C to the puzzle's question.

So, 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 previous solution to the puzzle.

One more observation: since we knew the answer to the question (namely, that C would reply Yes), we did not need to use the proposition \(R\) when using Prover9.

We could have found a proof by contradiction using A's statement as the only assumption and the \((*)\) formula as the goal to be proven.

The output of Prover9 with this smaller input is:

This second proof is shorter than the first one, but only by 6 steps. Frankly, I don't feel bad about making Prover9 work a bit harder than necessary. 

In any case, both proofs are tiny compared to what Prover9 is designed to handle (in first-order predicate logic, which is much more expressive than propositional logic)!