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!