[Part 6] Raymond Smullyan's Certified Knights and Knaves puzzles Puzzle #6 - Analysis

For our sixth puzzle, we will solve Problem 6 on page 42 of the 2013 Dover edition [ISBN: 978-0486497051] of Raymond Smullyan's 2013 book entitled "The Gödelian Puzzle Book - Puzzles, Paradoxes & Proofs", which reads:

On another particularly interesting occasion I came across two natives A and B each of whom made a statement such that I could infer that at least one of them must be an uncertified knight, but there was no way to tell which one it was. From neither statement alone could one have deduced this.

What two statements would work? [This problem is not easy!]

One reason this puzzle is tricky is because it involves two natives and requires us to "go backwards" from the inferred fact back to the statements.

Another reason why it is not easy is that the inferred fact is a bit hard to interpret. 

When Smullyan writes:

"at least one of them must be an uncertified knight, but there was no way to tell which one it was."

the initial adverbial phrase "at least" implies that we need to consider three possibilities:

1. Only A is an uncertified knight.
2. Only B is an uncertified knight.
3. Both A and B are uncertified knights.

However, if exactly one of these possibilities is the case, then there IS a way to tell which native is a certified knight.

Therefore, the second half of the inferred fact above (namely, "but there was no way to tell...") implies that more than one of these possibilities must be SIMULTANEOUSLY compatible with the two statements made by the native.

The possible combinations of these possibilities are (shown as sets):

• {1,2}
• {1,3}
• {2,3}
• {1,2,3}

But are all combinations compatible with the puzzle statement?

This is where the puzzle may be open to several interpretations.

In my interpretation, the first and last bullet points are compatible with the puzzle statement:

• With {1,2}, exactly one of the two natives is an uncertified knight but there is no way to tell which one.
• With {1,2,3}, either one or both of the natives could be an uncertified knight but there is no way to tell whether A is an uncertified knight nor whether B is an uncertified knight.

In contrast (again, in my interpretation), the second and third bullet points above are NOT compatible with the puzzle statement:

• With {1,3}, B may or may not be an uncertified knight but it is certain that A is one.
• With {2,3}, A may or may not be an uncertified knight but it is certain that B is one.

To me, knowing for sure that one of the natives is an uncertified knight contradicts the requirement that "there was no way to tell which one it was."

Therefore, in my analysis of the puzzle, the two statements made by the natives allow us to infer that:

• either: exactly one of A and B is an uncertified knight, but there is no way to tell which one is
• or: at least one of A and B is an uncertified knight, but there is no way to tell which one is or if both are

This analysis led me to reason as follows.

First, since this problem involves two natives, we will again use the proposition \(A\) (respectively, \(B\)) to represent the fact that A (respectively, B) is a knight. And we will use the proposition \(Ac\) (respectively, \(Bc\)) to represent the fact that A (respectively, B) is certified.

Second, we are looking for two statements \(S_A\) and \(S_B\), encoded as formulas \(\varphi_A\) and \(\varphi_B\), respectively, such that the formula:

\(\varphi = (A \leftrightarrow \varphi_A)\ \&\ (B \leftrightarrow \varphi_B)\)

represents the puzzle correctly.

Third, the formulas \(\varphi_A\) and \(\varphi_B\) must satisfy the requirements represented by the following truth table:

\(A\)	\(Ac\)	\(B\)	\(Bc\)	\(\varphi = (A \leftrightarrow \varphi_A)\ \&\ (B \leftrightarrow \varphi_B)\)
\(F\)	\(F\)	\(F\)	\(F\)	\(F\)
\(F\)	\(F\)	\(F\)	\(T\)	\(F\)
\(F\)	\(F\)	\(T\)	\(F\)	\(T\)	only B
\(F\)	\(F\)	\(T\)	\(T\)	\(F\)
\(F\)	\(T\)	\(F\)	\(F\)	\(F\)
\(F\)	\(T\)	\(F\)	\(T\)	\(F\)
\(F\)	\(T\)	\(T\)	\(F\)	\(T\)	only B
\(F\)	\(T\)	\(T\)	\(T\)	\(F\)
\(T\)	\(F\)	\(F\)	\(F\)	\(T\)	only A
\(T\)	\(F\)	\(F\)	\(T\)	\(T\)	only A
\(T\)	\(F\)	\(T\)	\(F\)	\(T\)	both A and B
\(T\)	\(F\)	\(T\)	\(T\)	\(T\)	only A
\(T\)	\(T\)	\(F\)	\(F\)	\(F\)
\(T\)	\(T\)	\(F\)	\(T\)	\(F\)
\(T\)	\(T\)	\(T\)	\(F\)	\(T\)	only B
\(T\)	\(T\)	\(T\)	\(T\)	\(F\)

In the table above:

• the green rows correspond to the possibility "Only A is an uncertified knight",
• the red rows correspond to the possibility "Only B is an uncertified knight", and 
• the blue row corresponds to the possibility "Both A and B are uncertified knights".

In the next few posts, we'll describe a JavaScript program that will find an answer to this puzzle, that is, formulas \(\varphi_A\) and \(\varphi_B\) such that the formula \(\varphi\) is:

• always False in the white rows
  AND
  • EITHER [case {1,2}]:
    • True in one or more green rows
      AND
    • True in one or more red rows
  • OR [case {1,2,3}]:
    • True in one or more green rows
      AND
    • True in one or more red rows
      AND
    • True in the blue row

Phew!

Now you see why I split my discussion of this puzzle into several posts:

1. this post to specify my interpretation of the puzzle and pin down its requirements, and
2. the next posts describing how I solved the puzzle (according to this interpretation) using a JavaScript program.

Before moving on to the code though, we make the following observation.

Since the requirements in the {1,2} case are a strict subset of the requirements in the {1,2,3} case, the extra requirement (numbered 3) is really optional.  In other words, we simply need to find statements that meet the requirements of case {1,2}.

So, as a simplification, we will be looking for formulas \(\varphi_A\) and \(\varphi_B\) such that the formula \(\varphi\) is:

• always False in the white rows
  AND
• True in one or more green rows 
  AND
• True in one or more red rows

[Part 6] Raymond Smullyan's Knights, Knaves, and Normals puzzles Second puzzle, solved with Prover9

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

Here is an unusual one: Two people, A and B, each of whom is either a knight, or knave, or a normal, make the following statements:

A: B is a knight.

B: A is not a knight.  

Prove that at least one of them is telling the truth, but is not a knight.

One reason this puzzle is unusual is because the author gives us its solution and asks us to prove it.

This is a perfect fit for this series!

The author's proof appears on page 33. But we will use Prover9 to find one for us.

First, we represent our island's world in which each inhabitant has exactly one of three types, using our usual formulas:

Kni(x) | Kna(x) | Nor(x).
-Kni(x) | -Kna(x).
-Kni(x) | -Nor(x).
-Kna(x) | -Nor(x).

Second, we apply our representation principle to reflect the islanders' statements, namely:

---

 Representation principle for Knights, Knaves, and Normals puzzles

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

\((Kni(P)\ \&\ \varphi)\ |\ (Kna(P)\ \&\ {-\varphi})\ |\ Nor(P)\)

---

Collecting all of the formulas we need according to the discussion above, we get the following input to feed to Mace4:

The output generated by Mace4 is the following:

Even though I tried to translate this proof back into English, to be compared with my own proof, or Smullyan's, I was not really successful. 

I think that one difficulty is that informal proofs do not use anything like big disjunctions. But that is what Prover9 does, since it converts all formulas to clauses.

Maybe we'll have a chance to get back to this issue later on.