Table of contents for the series of posts on Knights and Knaves puzzles

1. Review of propositional logic
   • In which we discuss propositional variables, logical connectives, and a couple of logical equivalences
2. Representation principle for Knights and Knaves puzzles
   • In which we discuss a general principle for representing, in propositional logic, statements made by the island's inhabitants
3. First example - Informal solution
   • In which we discuss a typical puzzle with two inhabitants and solve it informally. A typical puzzle asks questions of the type: What is A?
4. First example - Formal proof
   • In which we discuss a complete, formal proof of the solution to our first puzzle
5. First example - A natural-deduction proof
   • In which we discuss what a natural-deduction-style proof looks like and provide such a formal proof by cases for our first example
6. First example - Truth table approach
   • In which we discuss how to solve a typical puzzle by building a truth table
7. First example - Proof by contradiction
   • In which we discuss an indirect proof of the puzzle's solution that contrasts with the direct proofs we gave earlier
8. Second example
   • In which we discuss both an informal solution and a formal, truth-table-based approach to a second typical puzzle with 3 inhabitants
9. Automating puzzle proofs with Prover9
   • In which we discuss an automatic theorem prover and use it to automatically generate a proof by contradiction of the solution to our first puzzle
10. Automating puzzle proofs with Mace4
    • In which we discuss how to automatically solve the first puzzle using another theorem prover that does not need the solution of the puzzle to generate the proof
11. Third example
    • In which we discuss how to solve a typical puzzle with more than one solution using both Prover9 and Mace4.
12. Fourth example
    • In which we discuss how to solve another typical problem that involves statements of the form "such and such inhabitants are (not) of the same type"
13. Fifth example
    • In which we discuss how to solve yet another type of puzzle that does not ask to determine the type of inhabitants but rather the answer that they will give to some question
14. Sixth example
    • In which we discuss how to solve yet another type of puzzle in which we have to use additional information given by the author, that is not part of the puzzle's storyline
15. Seventh example
    • In which we discuss how to solve yet another type of puzzle in which we must determine if the answers to two questions posed to two inhabitants are the same
16. Creating our own puzzle
    • In which we discuss how to reverse the truth-table approach to create new Knights and Knaves puzzles that are provably correct

[Part 16] A Propositional Logic approach to Raymond Smullyan's Knights and Knaves puzzles Creating our own puzzles

So far in this series, we have discussed how to solve Knights and Knaves puzzles both informally and (mostly) formally. We have illustrated a few types of formal proofs, such as direct proofs, proofs by contradiction, and proofs based on truth tables.

When using truth tables, we followed this process:

1. Represent the puzzle statement using a formula \(\varphi\) that is a conjunction of one or more formulas in propositional logic using, \(\varphi\) contains \(n\) distinct propositional variables, where \(n\) is the number of island inhabitants involved in the puzzle statement.
2. Build a truth table with \(2^n\) rows in which each row corresponds to one unique assignment of truth values to the propositions in \(\varphi\).
3. Read out of the truth table the answer to the puzzle based on which row(s) of the table make \(\varphi\) true.

In this post, we will reverse this process to create a new puzzle as follows:

1. Pick \(n\) (the number of inhabitants in our new puzzle) and build a truth table with \(2^n\) rows for an unknown conjunction \(\varphi\). In this table, we will assign the value False for\(\varphi\) in all rows but one in order to make sure that the puzzle has a unique solution. This table will only contain one column for each proposition and one column for the unknown \(\varphi\).
2. We will fill in the table with intermediate columns corresponding to carefully chosen formulas to be combined together in a conjunction that will make up \(\varphi\).
3. We will convert each sub-formula (i.e., each conjunct) in \(\varphi\) into an English statement. The concatenation of these English statements, with added text for context, will make up the statement of the new puzzle.

Step 1

We pick \(n\) to be 3 and choose the names A, B, and C for these inhabitants.

We then build a truth table with \(2^3=8\) rows. As shown below, we arbitrarily chose \(\varphi\) to be true only when all three inhabitants are knights (last row):

\(A\)	\(B\)	\(C\)	\(\varphi\)
\(F\)	\(F\)	\(F\)	\(F\)
\(F\)	\(F\)	\(T\)	\(F\)
\(F\)	\(T\)	\(F\)	\(F\)
\(F\)	\(T\)	\(T\)	\(F\)
\(T\)	\(F\)	\(F\)	\(F\)
\(T\)	\(F\)	\(T\)	\(F\)
\(T\)	\(T\)	\(F\)	\(F\)
\(T\)	\(T\)	\(T\)	\(T\)

Step 2

We pick a formula to become the first conjunct in \(\varphi\). Since we'd like our puzzle to be made of statements by the inhabitants, we choose a bi-conditional with a single proposition on its left, namely:

\(B \leftrightarrow A\)

This formula will become a statement made by B.

Here is the new truth table with a column inserted for this sub-formula of \(\varphi\):

\(A\)	\(B\)	\(C\)	\(B \leftrightarrow A\)	\(\varphi\)	done
\(F\)	\(F\)	\(F\)	\(T\)	\(F\)
\(F\)	\(F\)	\(T\)	\(T\)	\(F\)
\(F\)	\(T\)	\(F\)	\(F\)	\(F\)	✔
\(F\)	\(T\)	\(T\)	\(F\)	\(F\)	✔
\(T\)	\(F\)	\(F\)	\(F\)	\(F\)	✔
\(T\)	\(F\)	\(T\)	\(F\)	\(F\)	✔
\(T\)	\(T\)	\(F\)	\(T\)	\(F\)
\(T\)	\(T\)	\(T\)	\(T\)	\(T\)

The cells highlighted in green above indicate that this sub-formula matches the expected truth value of \(\varphi\) in five of the eight rows. In particular, the rows ending in a checkmark are considered final since adding any new conjuncts to \(\varphi\) (as we do below) cannot make them True again. 

We can thus simplify our table as follows:

\(A\)	\(B\)	\(C\)	\(B \leftrightarrow A\)	\(\varphi\)	done
\(F\)	\(F\)	\(F\)		\(F\)
\(F\)	\(F\)	\(T\)		\(F\)
\(F\)	\(T\)	\(F\)			✔
\(F\)	\(T\)	\(T\)			✔
\(T\)	\(F\)	\(F\)			✔
\(T\)	\(F\)	\(T\)			✔
\(T\)	\(T\)	\(F\)		\(F\)
\(T\)	\(T\)	\(T\)		\(T\)

Next, we pick a second sub-formula in order to handle as many of the remaining rows as possible. 

More precisely, we want to find another conjunct that will be added to \(\varphi\) to make it still True in the last row but False in the remaining rows (i.e., rows 1, 2 and 7).

This step requires a bit of thinking. After some trial and error, I found the following candidate formula:

\(C \leftrightarrow ({-A} \rightarrow {-C})\)

Next, I insert a column in our truth table for this new sub-formula:

\(A\)	\(B\)	\(C\)	\(B \leftrightarrow A\)	\(C \leftrightarrow ({-A} \rightarrow {-C})\)	\(\varphi\)	done
\(F\)	\(F\)	\(F\)		\(F\)	\(F\)	✔
\(F\)	\(F\)	\(T\)		\(F\)	\(F\)	✔
\(F\)	\(T\)	\(F\)				✔
\(F\)	\(T\)	\(T\)				✔
\(T\)	\(F\)	\(F\)				✔
\(T\)	\(F\)	\(T\)				✔
\(T\)	\(T\)	\(F\)		\(F\)	\(F\)	✔
\(T\)	\(T\)	\(T\)		\(T\)	\(T\)	✔

As shown in green above, this new formula does take care of all remaining rows. 

Therefore, we do not need additional formulas. These two sub-formulas appear sufficient to make \(\varphi\) True in exactly one case (i.e., the last row, in which all three inhabitants are knights).

If our truth table is correct (and we will prove it formally in two ways below), then our puzzle, as it stands, is encoded in the following two propositional logic formulas:

\(B \leftrightarrow A\)

\(C \leftrightarrow ({-A} \rightarrow {-C})\)

Step 3

Finally, we translate these formulas into English to yield a Smullyan-style puzzle. 

Of course, there are many possibilities. Let's go with this one:

On your next visit to the island of knights and knaves, you meet three inhabitants. When you ask the first one if he is a knight or a knave, he (i.e., A) refuses to answer. 

Then, the second one (i.e., B) tells you: "Too bad he is in a bad mood today because, whenever he talks, A cannot lie.". 

Finally, C, who is in a great mood adds: "Let me tell you, if A is a knave, then so am I." 

What are A, B, and C? 

And, voila!

But is this puzzle correct? Does it have a solution? As importantly, does it have a unique solution?

As has been our habit in this series, we now look for formal proofs of the correctness of our new puzzle.

Formal proof #1

First, we use Mace4. Given the input:

Mace4 outputs only one model, as expected:

in which all three inhabitants are knights.

Formal proof #2

Now, we use Prover9 which, given the input:

outputs a formal proof (by contradiction) of the correctness of our puzzle:

Well, I think this is as good a place as any to end both this post and the whole series.

I hope you enjoyed it!

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

In this post, we will solve our last example in this series. In this seventh Knights and Knaves puzzle, we must determine if the answers to two questions posed to two inhabitants are the same.

For our seventh example, we will use the twelfth puzzle in Chapter 3 (or the \(37^{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 23 of the 2011, paperback Dover Recreational Math edition [ISBN: 9780486481982], the puzzle reads:

Suppose you visit the island of knights and knaves. You come across two of its inhabitants lazily lying in the sun. You ask one of them whether the other one is a knight, and you get a (yes-or-no) answer. Then you ask the second one whether the first one is a knight. You get a (yes-or-no) answer.

Are the two answers necessarily the same?

The informal answer given by Smullyan in the book (on page 32) is again a proof by cases.

However, this is an example where the formal approach is much quicker!

Recall that the first step in a formal approach is to couch the puzzle statement in a formal language. Propositional logic is the language we have been using in this series.

As it turns out, once this puzzle is translated into propositional logic, the answer will be obvious. Therefore, there will be no need to use Mace4 nor Prover9. All of the work fun is in the representation step.

As we have done several times already, we will call the two inhabitants A and B. Then, the question posed to A becomes:

\(A \leftrightarrow B\) ?

Recall that the question mark is not part of the formula; it is added here to indicate that this is a question whose answer we do not know. If this translation is not obvious to you, refer back to this post for an explanation.

Similarly, the question posed to the other inhabitant becomes:

\(B \leftrightarrow A\) ?

Recall that the proposition on the left of the bi-conditional represents the person who gives the answer while the formula on the right is the question being asked.

Now, we are asked to determine whether the two answers are necessarily the same. 

The answer is clearly Yes, because the two logical formulas are equivalent. This is due to the fact that the bi-conditional connective is a commutative logical operator. 

In other words, for any formulas \(\varphi_1\) and \(\varphi_2\):

\(\varphi_1 \leftrightarrow \varphi_2\)

and 

\(\varphi_2 \leftrightarrow \varphi_1\)

always have the same value.

This is similar to the addition operator being commutative in the context of arithmetic. Whatever the integer or real values of \(x\) and \(y\):

\(x + y\)

and 

\(y + x\)

always have the same value, because \(+\) is a commutative operator.

[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.

[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)!

[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. 

[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.