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

In this post, we will solve our sixth Knights and Knaves puzzle. In this puzzle, we again have to determine the type of two inhabitants; but this time, we have to use additional information given by the author, that is not part of the puzzle's storyline.

For our sixth example, we will use the eleventh puzzle in Chapter 3 (or the \(36^{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 pages 22-23 of the 2011, paperback Dover Recreational Math edition [ISBN: 9780486481982], the puzzle, entitled "An adventure of mine", reads:

[...] Once when I visited the island of knights and knaves, I came across two of the inhabitants resting under a tree. I asked one of them, "Is either one of you a knight?" He responded, and I knew the answer to my question.

What is the person to whom I addressed the question-is he a knight or a knave; and what is the other one? I can assure you, I have given you enough information to solve the problem.

The most direct, informal analysis of this puzzle uses a case-by-case analysis. Instead, we will first develop a semi-formal approach to this puzzle, using Mace4, to eliminate most cases, and then use Mace4's output to informally deduce the solution.

In the second part of this post, we will formally prove this solution using Prover9.

Based on the second half of the puzzle statement, it appears that both answers (Yes and No) to the question are possible, but only one of them narrows down to a single answer the possible types of both inhabitants.

We will test this hypothesis by using Mace4 to list all cases consistent with both answers. The hypothesis will be confirmed if one of the answers to the question leads to only one possible type for each inhabitant. 

We will then know that this is the answer that was given to the visitor. As a result, we will be able to directly read out the answer to the puzzle in the truth values of the corresponding model output by Mace4.

Recall that the first step in formalizing a puzzle is to translate its statement into propositional logic.

Let's call A the inhabitant to whom the question was (A)dressed, while B will be the other inhabitant.

Using the representation scheme described earlier in this series, the question asked is straightforward and becomes the formula:

\(A\ |\ 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.

Since the question is posed to A, his answer, as before, will be represented by the formula:

\(A \leftrightarrow (A\ |\ B)\) 

since, if A' s answer is Yes, it will be equivalent to A saying: "Yes, one of us is a knight.", and if A's answer is No, it will be equivalent to A saying: "No, neither one of us is a knight." 

Finally, like for our fifth example, we will use \(R\) to refer to the truth value of A's reply, yielding the formula:

\(R \leftrightarrow (A \leftrightarrow (A\ |\ B))\) 

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

Semi-formal 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 four 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 four distinct models. In other words, there are four combinations of truth values for \(A\), \(B\), and \(R\) that make the puzzle statement true.

Three of these models assign True to \(R\). In other words, when the answer to the question is Yes, there are three possible combinations of types for A and B, and it is not possible to ascertain their type.

However, our hypothesis is confirmed by the fact that there is only one model in which the answer is No (i.e., \(R\) is assigned the value 0 for False). This is the second model in Mace4's output.

In this model, \(A\) is assigned the value 0 (False), while \(B\) is assigned the value 1 (True).

Since this is the only answer that provides enough information, as per the puzzle statement, the answer to the question must be No, and the solution to the puzzle must be:

• A ("the person to whom I addressed the question") is a knave, while
• B ("the other one") is a knight.

Alternatively, we could have manually built a truth table; however, that would have been a bit more tedious than running Mace4!

Formal solution

Now that we have discovered the solution to the puzzle, we can prove that it is correct with a formal proof by contradiction.

First, recall that A's answer to the question was represented with the formula:

\(A \leftrightarrow (A\ |\ B)\)

Since we inferred that the answer to this question is No, we can represent this knowledge by negating the formula above to yield:

\(-(A \leftrightarrow (A\ |\ B))\)

which is equivalent to:

\(A \leftrightarrow -(A\ |\ B)\)

Now, the goal we are trying to prove is that A is a knave while B is a knight, that is:

\( -A\ \&\ B\)

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.