[Part 1] Raymond Smullyan's Certified Knights and Knaves puzzles Puzzle #1

In two earlier series, we had some fun with basic knights and knaves puzzles and then with knights, knaves, and normals puzzles.

In this series, we will solve puzzles from Chapter V of Raymond Smullyan's 2013 book entitled "The Gödelian Puzzle Book - Puzzles, Paradoxes & Proofs". 

These puzzles take place on another island with only knights and knaves who have the opportunity to have their type certified. So, those knights (respectively, knaves) who have been proven to be knights (respectively, knaves) are certified. The other knights and knaves, who did not take advantage of this opportunity, are said to be uncertified.

For our first puzzle, we will solve Problem 1 on page 41 of the 2013 Dover edition [ISBN: 978-0486497051], which reads:

I once came across a native of the island who said, "I am not a certified knight." Was he a knight or a knave? Was he certified?

This puzzle is not a hard one. It is thus a good choice to demonstrate the basic principles for how to use formal logic to solve such puzzles.

I trust that you can solve it informally. Smullyan's answer is a simple case analysis given on page 44.

In this post, we will give three different proofs of the solution. All of them require that we first translate the puzzle statement into formal logic.

As we did when dealing with basic knights and knaves puzzles, we will use propositional logic. First-order predicate logic would also work, but seems a little bit like overkill in this case.

All we need here are:

• One proposition, say \(A\), to represent the fact that islander A (say) is a knight (therefore, the formula \(-A\) represents the fact that A is a knave).
• One proposition, say \(Acert\), to represent the fact that A is certified.
• A scheme for representing in logic the statements made by islanders. Here, we will reuse the representation principle described in this post, namely:

---

 Representation principle for Knights and Knaves puzzles

For any person P living on this island and any statement S
(where S is represented by the formula \(\varphi\))
the fact that P said S
will be represented by the formula:

\(P \leftrightarrow \varphi\)

---

First, let's give a name, say A, to the islander in our puzzle.

A's statement is S = "I am not a certified knight." 

After getting rid of the initial pronoun, S becomes:

"A is not a certified knight."

This statement is equivalent to the sentence:

"It is not the case that A is both certified and a knight."

which can be represented in propositional logic with the formula \(\varphi\) equal to:

\(-(A\ \&\ Acert)\)

Applying our representation principle to A and its statement, we get the formula:

\(A \leftrightarrow  -(A\ \&\ Acert)\)

This is the entire logical representation of our puzzle!

First formal proof

For our first formal proof, we will use the Mace4 tool, which we described in an earlier post.

The input to Mace4 is thus the single formula:

A <-> -(A & Acert).

And its output is:

This output tells us that \(A\) must be true (1) and \(Acert\) must be false (0).

In other words, the solution of our puzzle is that A is an uncertified knight.

Second formal proof

For our second proof, we will use the automated theorem prover Prover9, which we described earlier.

Prover9 searches for proofs by contradiction. So, we must feed it our puzzle statement (like with Mace4) as well as the formula representing our solution, namely:

A & -Acert.

Prover9 calls this formula its goal, since it must find a proof for it. It does so by negating the goal and deriving a contradiction.

Here is the input to Prover9:

and here is its output:

This proof is quite short and easy to follow, at least if you have read posts in the two previous series.

Third formal proof

Finally, we'll solve this puzzle using a truth table (see this post for a description of this approach).

\(A\)	\(Acert\)	\(A\ \&\ Acert\)	\(-(A\ \&\ Acert)\)	\(A \leftrightarrow -(A\ \&\ Acert)\)
\(F\)	\(F\)	\(F\)	\(T\)	\(F\)
\(F\)	\(T\)	\(F\)	\(T\)	\(F\)
\(T\)	\(F\)	\(F\)	\(T\)	\(T\)
\(T\)	\(T\)	\(T\)	\(F\)	\(F\)

Note that the only row in which the last value is \(T\) (which makes our puzzle formula true) is the next-to-last one. On this row, \(A\) is True and \(Acert\) is False, which, of course, is the same solution as before.