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