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

[Part 10] A Propositional Logic approach to Raymond Smullyan's Knights and Knaves puzzles Automating puzzle proofs with Mace4

Earlier in this series, we solved the following Knights and Knaves puzzle in a variety of ways:

A makes the following statement, "At least one of us is a knave."  

What are A and B?

First, we solved it informally.

Second, we solved it using a rather linear, direct formal proof. 

Third, we solved it using a hierarchical, natural deduction-style proof.

Fourth, we solved it using a truth table.

Fifth, we solved it using a proof by contradiction.

Sixth, in the previous post, we solved it using automated theorem proving in Prover9.

The way we used Prover9 in the previous post was to input both the statement of the puzzle and its solution. This use case would correspond to a scenario where:

1. we are able to solve the puzzle informally, but 
2. we want to check our solution formally without having to write a formal proof ourselves.

In other words, we were able to automate step 2.

But can we automate step 1 as well?

In other words, could we simply feed the puzzle statement, but not its solution, to an automated theorem prover that would then discover a provably correct solution?

The answer is yes; but Prover9 will not do for this.

Recall, from the previous post, that the app I used, namely Prover9-Mace4, is described as a "front end to the programs Prover9 (which searches for proofs) and Mace4 (which searches for finite models and counterexamples)." 

It turns out that Mace4 will allow us to automate step 2 above.

Mace4 takes, as input, a set of formulas and returns one or more models for it.

In the context of propositional logic, a model for a given set of formulas is an interpretation that makes all formulas in the set true, where an interpretation is an assignment of truth values (i.e., True or False) to all propositions in the set of formulas. 

When solving Knights and Knaves puzzles, the input to Mace4 is a set of one or more formulas that encode the puzzle statement. Mace4 will then return the truth values that all propositions in the formulas must take on to make the puzzle statement true, that is, to solve the puzzle.

And since the propositions, for us, will be \(A\), \(B\), etc., that is, the propositions that represent, "A is a knight, "B is a knight", etc., the output of Mace4 will be a solution to the puzzle!

Let's then use Mace4 to solve the puzzle above.

Here again is what the GUI for the Prover9-Mace4 app looks like:

It is the same GUI as before; but we will use it differently:

1. We will use the top-left input box (as before) to specify the input to Mace4 
2. but this time, we will leave the bottom left input box empty: note that, under our current use case, we do not yet know the solution to the puzzle; and we do not need it since we are not looking for a proof by contradiction
3. we will use the Mace4 panel in the bottom-right corner instead of the Prover9 panel in the top-right corner.

Here is the same GUI with the input formula typed in:

Before we run Mace4, we want to override one of its default options. To do this, we click on the "Mace4 Options" tab toward the top of the window...

... and set the maximum number of models to 4 (circled in red above). 

Since our puzzle statement involves exactly two propositions (\(A\) and \(B\)) and each one of them can be either True or False, the total number of distinct interpretations is equal to 4.

We are using Mace4 to find out which one(s) of these four interpretations is a (are) solution(s) to the puzzle. 

Now, if we set this option to 1, Mace4 would return the first solution it finds. But then we may miss alternative solutions (for puzzles that have more than one solution). 

If we set this option to a number larger than 4, we may make Mace4 work harder than it needs to, since there cannot possibly be more than 4 distinct solutions.

Having set this option to a reasonable value (and left the other options to their default values), we click on the "Formulas" tab to return to the main window and we launch Mace4 by clicking on the "Start" button in the bottom-right pane.

Mace4 returns an answer almost instantaneously (given the tiny size of our problem), namely:

This output lists four models, that is, four interpretations (numbered 1 through 4) that make the puzzle statement true.

Each interpretation associates (i.e., establishes a relation between) a truth value
(1 for True and 0 for False) to the propositions \(A\) and \(B\).

In the first model, we see that \(A\) is True and \(B\) is False, which is the expected solution to this puzzle. In other words, A must be a knight and B must be a knave.

Surprisingly, the last three interpretations are identical to the first one. This simply means that there is only one solution to this puzzle.

The reason for the duplication is that internally, these interpretations are represented in such a way that Mace4 cannot immediately tell that they are actually identical to each other.

In fact, they are identical to us (technically, they are isomorphic to each other). What we really want is only one such solution, called a canonical form.

To ask Mace4 to remove all isomorphic solutions and only display what we consider to be distinct solutions, we can:

1. click on the "Isofilter..." button at the top of the output window,
2. select the "Canonical Forms" algorithm in the pop-up window, and
3. click the "Start" button in this same pop-up window.

Mace4 will then output:

which is the unique solution to this puzzle.

[Part 9] A Propositional Logic approach to Raymond Smullyan's Knights and Knaves puzzles Automating puzzle proofs with Prover9

Earlier in this series, we solved the following Knights and Knaves puzzle in a variety of ways:

A makes the following statement, "At least one of us is a knave."  

What are A and B?

First, we solved it informally.

Second, we solved it using a rather linear, direct formal proof. 

Third, we solved it using a hierarchical, natural deduction-style proof.

Fourth, we solved it using a truth table.

Fifth, in the previous post, we solved it using a proof by contradiction.

In this post, we'll describe how a software program can solve this type of puzzle using automated theorem proving.

When searching for relevant tools, I came across the Prover9-Mace4 app that, according to its documentation, is a "front end to the programs Prover9 (which searches for proofs) and Mace4 (which searches for finite models and counterexamples)." 

I played a little bit with Prover9 for this post and will give a brief demo of it here. In the next post, I will turn to Mace4.

Here is what the GUI for the Prover9-Mace4 app looks like:

For this demo, I'll use Prover9 to complete a proof by contradiction of the puzzle's solution.

For this use case, I first entered the logical formula that makes up the puzzle into the top (larger) input box labeled "Assumptions:".

As discussed in previous posts, the statement of this puzzle translates to a single formula, namely:

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

which, in Prover9, can be typed up as:

A <-> (-A | -B).

Note the period that must end each formula in Prover9.

Then, I entered the logical formula that makes up the puzzle's solution into the bottom (smaller) input box labeled "Goals:".

As discussed in previous posts, the statement of this solution translates to a single formula, namely:

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

which, in Prover9, can be typed up as:

A & -B.

Again, note the period at the end of the formula.

Before running the theorem prover, I clicked on the "Show Current Input" button in the top-right corner of the GUI. This popped up a window containing the input that is put together into a text file made up of what I typed into the GUI and that will be fed to the command-line tool that this app is a front end for.

This window looks like this:

This automatically generated input file contains Prover9 options (e.g., limits on the running time; many other options are available) followed by the two groups of input formulas: assumptions and goals.

Everything looked good to me. So I closed this window. Then, back in the main window, I clicked on the "Start" button in the Prover9 section (the top one, above the Mace4 section).

For such a simple example, Prover9 finds a proof almost instantaneously.

Here is its output:

The numbered lines at the bottom of the output window show the proof's steps.

Since the proof is abbreviated (when compared to the level of detail that was used in the proofs of previous posts), I will go through it step by step.

The first two lines show the two input formulas, that is, the assumption and the goal.

The "non_clause" annotation on each one of these lines means that these two formulas are not in the format that Prover9 expects: they are not clauses.

A clause is a formula that has a special form: it must be a disjunction of literals, where a literal is a single proposition, optionally negated. Here is an example of a clause:

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

with three literals, two of which are negated.

As a pre-processing step, Prover9 first converts all input formulas, including assumptions and goals (the latter is first negated, as we discuss below), to clauses. This algorithm is called "clausify".

This is a general yet simple algorithm that converts any input formula \(\varphi\) in propositional logic into a conjunction of clauses that is logically equivalent to \(\varphi\).

Here is a (reconstructed) trace of this algorithm when applied to \(\varphi = A \leftrightarrow (-A\ |\ {-B})\). It simply uses a series of logical equivalences to rewrite \(\varphi\) as follows:

1.  \(A \leftrightarrow (-A\ |\ {-B})\)  [initial formula]
2.  \((A \rightarrow (-A\ |\ {-B}))\ \&\ ((-A\ |\ {-B})\ \rightarrow A)\) [a. + equivalence of a bi-conditional to a conjunction of conditionals]
3. \(A \rightarrow (-A\ |\ {-B})\) [first half of conjunction elimination on b.]
4. \((-A\ |\ {-B}) \rightarrow A\) [second half of conjunction elimination on b.]

At this point, \(\varphi\) is equivalent to the conjunction of the two formulas above (c. and d.), each one of which must be "clausified".

5. \(-A\ |\ (-A\ |\ {-B})\) [c.+ conditional to disjunction equivalence] 
6. \(-A\ |\ {-B}\) [e.+ idempotence of disjunction]

This last step works because \(-A\ |\ {-A}\) is logically equivalent to \(-A\). 

This is how Prover9 infers the clause on line 3 in the output image above, that is, as (partial) output of the clausify algorithm applied to the formula on line 1.

Now, continuing the trace of the clausify algorithm, we get:

7. \(-(-A\ |\ {-B})\ |\ A\) [d.+ conditional to disjunction equivalence] 
8. \((A\ \&\ B)\ |\ A\) [g.+ De Morgan's law + double negation elimination] 
9. \((A\ |\ A)\ \&\ (B\ |\ A)\) [h.+ distributivity of disjunction over conjunction] 
10. \(A\ |\ A\) [first half of conjunction elimination on i.] 
11. \(A\) [j.+ idempotence of disjunction]

And this is how Prover9 infers the clause on line 4 in the output image above, that is, as (partial) output of the clausify algorithm applied to the formula on line 1.

This step also marks the completion of the clausify algorithm.

Now, recall that Prover9 is searching for a proof by contradiction, which requires negating the goal formula.

So, line 5 of Prover9's output is simply the negation of the conjunction of the two clauses on line 2.  Note that the negation of the goal formula is already a clause, and therefore does not need to be clausified in this sample proof.

As the next-to-last step, Prover9 infers, on line 6,  the clause \(B\) by applying the resolution inference rule to the clauses on lines 4 and 5.

Note that Prover9 uses the phrase unit deletion here (instead of resolution) because one of the premises, namely the clause \(A\) on line 4, is a unit clause (that is, a clause made up of a single literal). This clause is combined with the premise \(-A\ |\ B\) on line 5 to cancel its literal \(-A\), yielding \(B\) on line 6.

Finally, Prover9 infers \(\$F\) on line 7, which is its symbol for \(\perp\).

Note that Prover9 uses the phrase back unit deletion here because the newly inferred formula \(B\) on line 6 is used to cancel out the \(-B\) (hence the unit deletion) in the previously inferred formula on line 3 (that is, an inference step that goes back and modifies a previously inferred formula).

This back unit deletion step yields the clause \(-A\) which, in this same step (i.e., on line 7) is cancelled out with the clause \(A\) on line 4 (another unit deletion operation) to yield the contradiction.

This last step concludes the proof, since a contradiction was inferred. 

The (non-negated) goal formula is therefore a logical consequence of the assumption. 

In other words, Prover9 has formally proved our solution to the Knights and Knaves puzzle.

In the next post, we will use Mace4 to solve this same puzzle using another application of automated theorem proving.

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

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

For our second example, we will use the sixth puzzle in Chapter 3 (or the \(31^{st}\) 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 21 of the 2011, paperback Dover Recreational Math edition [ISBN: 9780486481982], the puzzle reads:

[...] we have three people, A, B, C, each of whom is either a knight or a knave. A and B make the following statements:

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

What are A, B, C?

As was the case for our first puzzle, our informal, yet systematic approach to solving it is to reason by cases. Since each inhabitant is either a knight or a knave, there are only two possible cases for each inhabitant.

Since this puzzle involves three inhabitants, we must pick one of them as a starting point. We'll start with A. [Exercise for the reader: Solve this puzzle with a case analysis based on B instead. It would be hard to start with C, since we do not have a statement from C on which to base our analysis.]

Case 1: A is a knight

If A were a knight, her statement would be true, which means that A (as well as B and C) would have to be a knave. Therefore, this case is impossible. 

Case 2: A is a knave [This case must hold] 

Since A lied, we know that at least one of the three inhabitants is a knight. Since A is a knave, it must be the case that one of B and C is a knight, or both B and C are knights.

To decide which, we turn to B's statement. 

Again, we consider two cases for B (as sub-cases of Case 2).

Case 2a: B is a knave (and A is still a knave)

In this case, B's statement must be false. Since it does not hold that "exactly one of us is a knight" and both A and B are knaves, it must be the case that C is also a knave (otherwise, C would be the only knight).

But then all three of them would be knaves, which would make A's statement true, which in turn would make A a knight. 

This sub-case is thus impossible.  

Case 2b: B is a knight (and A is still a knave)

In this case, B's statement must be true.

Since B is a knight, B must be the only knight. 

Therefore, C is a knave.

This fact does not contradict either of the statements.

Finally, only Case 2b is possible, which leads us to the only conclusion:

Solution to the puzzle: A and C are knaves, whereas B is a knight.

We will now formally prove that this solution is correct using the truth table approach that we described and applied (in Part 6) to the first puzzle.

We must start by translating the puzzle statement into propositional logic as follows.

First, A's statement becomes:

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

Since this formula will become part of a longer formula, we will refer to it with the symbol \(A_{statement}\).

Now, the fact that A made this statement becomes:

\(A \leftrightarrow A_{statement}\)

Second, B's statement becomes:

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

Since this formula is quite long, we will refer to it with the symbol \(B_{statement}\).

Now, the fact that B made this statement becomes:

\(B\leftrightarrow B_{statement} \)

Therefore, the complete, formal representation of the puzzle statement is the conjunction of the two statements, namely the formula \(\varphi\) defined as:

\(\varphi = (A \leftrightarrow A_{statement})\ \&\ (B\leftrightarrow B_{statement})\)

Finally, we build a truth table for this formula:

\(A\)	\(B\)	\(C\)	\(A_{statement}\)	\(A\leftrightarrow A_{statement}\)	\(B_{statement}\)	\(B\leftrightarrow B_{statement}\)	\(\varphi\)
\(F\)	\(F\)	\(F\)	\(T\)	\(F\)	\(F\)	\(T\)	\(F\)
\(F\)	\(F\)	\(T\)	\(F\)	\(T\)	\(T\)	\(F\)	\(F\)
\(F\)	\(T\)	\(F\)	\(F\)	\(T\)	\(T\)	\(T\)	\(T\)
\(F\)	\(T\)	\(T\)	\(F\)	\(T\)	\(F\)	\(F\)	\(F\)
\(T\)	\(F\)	\(F\)	\(F\)	\(F\)	\(T\)	\(F\)	\(F\)
\(T\)	\(F\)	\(T\)	\(F\)	\(F\)	\(F\)	\(T\)	\(F\)
\(T\)	\(T\)	\(F\)	\(F\)	\(F\)	\(F\)	\(F\)	\(F\)
\(T\)	\(T\)	\(T\)	\(F\)	\(F\)	\(F\)	\(F\)	\(F\)

The third row in this table (highlighted above) proves that the only way to make \(\varphi\) True is to have the propositions \(A\), \(B\), and \(C\) assigned the truth values, \(F\), \(T\), and \(F\), respectively.

This confirms the correctness of our informal solution: A and C must be knaves, whereas B is a knight.