[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 5] Raymond Smullyan's Certified Knights and Knaves puzzles Puzzle #5 - With two natives and a two-step solution

For our fifth puzzle, we will solve Problem 7 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". 

[Note that we skipped Problem 5 in the book because it is very similar to the two previous problems in this series. We also skipped Problem 6 because it is quite a bit harder; we will devote the next couple of posts to that problem.]

Now, Problem 7 reads:

On another occasion I came across two natives A and B. I was curious to know of each one whether he was a knight or a knave and whether or not he was certified. They made the following statements:

A: "B is an uncertified knight." 

B: "A is a certified knave." 

I thought awhile and could solve part of the problem, but not all of it, because I had no way of knowing whether B was a knight or a knave. I later found out whether B was a knight or a knave, and then could solve the entire problem! What is the solution?

This problem involves two natives. We will 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 a certified.

Then we represent A's statement with the formula:

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

and B's statement with the formula:

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

Therefore, the entire puzzle is represented by the formula \(\varphi\):

\((A \leftrightarrow (B\ \&\ {-Bc}))\ \&\ (B \leftrightarrow ({-A}\ \&\ Ac))\)

which represents the fact that each native made one of the statements.

We now build the truth table for \(\varphi\) as follows:

\(A\)	\(Ac\)	\(B\)	\(Bc\)	\(B\ \&\ {-Bc}\)	\(A \leftrightarrow (B\ \&\ {-Bc})\)	\({-A}\ \&\ Ac\)	\(B \leftrightarrow ({-A}\ \&\ Ac)\)	\(\varphi\)
\(F\)	\(F\)	\(F\)	\(F\)	\(F\)	\(T\)	\(F\)	\(T\)	\(T\)
\(F\)	\(F\)	\(F\)	\(T\)	\(F\)	\(T\)	\(F\)	\(T\)	\(T\)
\(F\)	\(F\)	\(T\)	\(F\)	\(T\)	\(F\)	\(F\)	\(F\)	\(F\)
\(F\)	\(F\)	\(T\)	\(T\)	\(F\)	\(T\)	\(F\)	\(F\)	\(F\)
\(F\)	\(T\)	\(F\)	\(F\)	\(F\)	\(T\)	\(T\)	\(F\)	\(F\)
\(F\)	\(T\)	\(F\)	\(T\)	\(F\)	\(T\)	\(T\)	\(F\)	\(F\)
\(F\)	\(T\)	\(T\)	\(F\)	\(T\)	\(F\)	\(T\)	\(T\)	\(F\)
\(F\)	\(T\)	\(T\)	\(T\)	\(F\)	\(T\)	\(T\)	\(T\)	\(T\)
\(T\)	\(F\)	\(F\)	\(F\)	\(F\)	\(F\)	\(F\)	\(T\)	\(F\)
\(T\)	\(F\)	\(F\)	\(T\)	\(F\)	\(F\)	\(F\)	\(T\)	\(F\)
\(T\)	\(F\)	\(T\)	\(F\)	\(T\)	\(T\)	\(F\)	\(F\)	\(F\)
\(T\)	\(F\)	\(T\)	\(T\)	\(F\)	\(F\)	\(F\)	\(F\)	\(F\)
\(T\)	\(T\)	\(F\)	\(F\)	\(F\)	\(F\)	\(F\)	\(T\)	\(F\)
\(T\)	\(T\)	\(F\)	\(T\)	\(F\)	\(F\)	\(F\)	\(T\)	\(F\)
\(T\)	\(T\)	\(T\)	\(F\)	\(T\)	\(T\)	\(F\)	\(F\)	\(F\)
\(T\)	\(T\)	\(T\)	\(T\)	\(F\)	\(F\)	\(F\)	\(F\)	\(F\)

The only three rows in which \(\varphi\) is True are highlighted. 
In all three rows, A is a knave. So this part of the puzzle is solved.
However, B is a knave in the two blue rows and a knight in the green row. This is the part of the puzzle that Smullyan needed more info about.
If this new info were that B is a knave, then the two blue rows would be compatible with the puzzle statement and we could not narrow down the answer to a single solution.
Therefore, to meet the requirement of the puzzle that finding out the type of B would allow us to solve the entire puzzle, the new info must be that B is a knight.
This leaves us with a single row, namely the green one, according to which:

• A is a certified knave.
• B is a certified knight.

And that is the unique solution to this puzzle.

Of course, Smullyan's solution (given on pages 45-46) is the same as ours, but his informal reasoning is wordier than our truth table!

[Part 4] Raymond Smullyan's Certified Knights and Knaves puzzles Puzzle #4 - Going backwards again

For our fourth puzzle, we will solve Problem 4 on pages 41-42 of the 2013 Dover edition [ISBN: 978-0486497051] of Raymond Smullyan's 2013 book entitled "The Gödelian Puzzle Book - Puzzles, Paradoxes & Proofs". 

This puzzle reads:

I once came across a native who made a statement such that I could deduce that he must be certified (either a certified knight or a certified knave), but there was no possible way to tell whether he was a knight or a knave. 

What statement would work?

Just like in the previous post, we build a truth table in which the last column contains the value True in the only two rows that correspond to the scenarios allowed by the puzzle statement:

\(A\)	\(Acert\)	\(\varphi\) = ?	\(A \leftrightarrow \varphi\)
\(F\)	\(F\)		\(F\)
\(F\)	\(T\)		\(T\)
\(T\)	\(F\)		\(F\)
\(T\)	\(T\)		\(T\)

Solving the puzzle now means finding a formula \(\varphi\) that correctly completes this table.

Since the main connective in \(A \leftrightarrow \varphi\) is a biconditional, \(\varphi\) must have the same truth value as \(A\) in the second and fourth rows (where the biconditional is true) and a different truth value from \(A\) in the first and third rows (where the biconditional is false).

Therefore, the almost-full table must look like:

\(A\)	\(Acert\)	\(\varphi\) = ?	\(A \leftrightarrow \varphi\)
\(F\)	\(F\)	\(T\)	\(F\)
\(F\)	\(T\)	\(F\)	\(T\)
\(T\)	\(F\)	\(F\)	\(F\)
\(T\)	\(T\)	\(T\)	\(T\)

Finally, the table will be complete (and the puzzle solved!) once we have found a formula \(\varphi\) that works:

\(A\)	\(Acert\)	\(\varphi\) = ?	\(A \leftrightarrow \varphi\)
\(F\)	\(F\)	\(T\)	\(F\)
\(F\)	\(T\)	\(F\)	\(T\)
\(T\)	\(F\)	\(F\)	\(F\)
\(T\)	\(T\)	\(T\)	\(T\)

In the most general case, we can assume that \(\varphi\) will depend on the two propositions in this puzzle, namely \(A\) and \(Acert\).
By inspection of the table above, we see that \(\varphi\) is true exactly when \(A\) and \(Acert\) have the same truth value.
Therefore, \(\varphi\) can simply be chosen to be:
\(A \leftrightarrow Acert\)
which could have come from the English statement: 

 "I am a knight if and only if I am certified."

And this statement is indeed logically equivalent to the answer given by Smullyan on page 44 of his book:

"I am either a certified knight or an uncertified knave."

[Part 3] Raymond Smullyan's Certified Knights and Knaves puzzles Puzzle #3 - Going backwards

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

This puzzle reads:

I once came across a native who made a statement from which I could deduce that he must be a[n] uncertified knave. What statement would work?

In the previous puzzles, we were given a statement S and were asked to determine the type and certified status of the speaker.

In such puzzles (with a native called A, say), we converted S to a logical formula \(\varphi\) and then built a truth table for the formula \(A \leftrightarrow \varphi\) to figure out which row(s) of the table contained the value True. 

This puzzle introduces a new twist: we are given the type and certified status of a native and must find a statement that the native could have made to allow us to make those deductions.

We must therefore find a formula \(\varphi\), corresponding to a statement S, that makes the native both uncertified and a knave.

More precisely, since only one native is involved, we call him A and build our table based on the usual two propositions \(A\) and \(Acert\).

The first two columns of the table list all of the possible combinations of truth values for these two propositions, while the last column contains the expected truth value of the formula representing the native's statement, yielding the table:

\(A\)	\(Acert\)	\(\varphi\) = ?	\(A \leftrightarrow \varphi\)
\(F\)	\(F\)		\(T\)
\(F\)	\(T\)		\(F\)
\(T\)	\(F\)		\(F\)
\(T\)	\(T\)		\(F\)

Note that the only True value in the last column represents the fact that A must be a knave (so \(A\) is False) and uncertified (so \(Acert\) is False).

Solving the puzzle now means finding a formula \(\varphi\) that correctly completes this table.

Since the main connective in \(A \leftrightarrow \varphi\) is a biconditional, \(\varphi\) must have the same truth value as \(A\) in the first row (where the biconditional is true) and a different truth value from \(A\) in the last three rows (where the biconditional is false).

Therefore, the almost-full table must look like:

\(A\)	\(Acert\)	\(\varphi\) = ?	\(A \leftrightarrow \varphi\)
\(F\)	\(F\)	\(F\)	\(T\)
\(F\)	\(T\)	\(T\)	\(F\)
\(T\)	\(F\)	\(F\)	\(F\)
\(T\)	\(T\)	\(F\)	\(F\)

Finally, the table will be complete (and the puzzle solved!) once we have found a formula \(\varphi\) that works:

\(A\)	\(Acert\)	\(\varphi\) = ?	\(A \leftrightarrow \varphi\)
\(F\)	\(F\)	\(F\)	\(T\)
\(F\)	\(T\)	\(T\)	\(F\)
\(T\)	\(F\)	\(F\)	\(F\)
\(T\)	\(T\)	\(F\)	\(F\)

In the most general case, we can assume that \(\varphi\) will depend on the two propositions in this puzzle, namely \(A\) and \(Acert\).
Since these two propositions can be combined into a single formula using conjunction, disjunction, conditional, biconditional, etc., we need to pick one of these logical connectives. This choice will determine the type of statement made by the native A.
Since Smullyan's answer is a conjunction, we will pick a different kind of statement, say, a conditional.
Finally, we consider possible ways to combine \(A\) and \(Acert\) with a conditional and optional negations, to get the table:

\(A\)	\(Acert\)	\({A} \rightarrow {Acert}\)	\({-A} \rightarrow {Acert}\)	\({A} \rightarrow {-Acert}\)	\({-A} \rightarrow {-Acert}\)	Target
\(F\)	\(F\)	\(T\)	\(F\)	\(T\)	\(T\)	\(F\)
\(F\)	\(T\)	\(T\)	\(T\)	\(T\)	\(F\)	\(T\)
\(T\)	\(F\)	\(F\)	\(T\)	\(T\)	\(T\)	\(F\)
\(T\)	\(T\)	\(T\)	\(T\)	\(F\)	\(T\)	\(F\)

We observe that none of the conditionals match the target column.

However, the next-to-last column contains, on each row, the negation of the value in the target column:

\(A\)	\(Acert\)	\({A} \rightarrow {Acert}\)	\({-A} \rightarrow {Acert}\)	\({A} \rightarrow {-Acert}\)	\({-A} \rightarrow {-Acert}\)	Target
\(F\)	\(F\)	\(T\)	\(F\)	\(T\)	\(T\)	\(F\)
\(F\)	\(T\)	\(T\)	\(T\)	\(T\)	\(F\)	\(T\)
\(T\)	\(F\)	\(F\)	\(T\)	\(T\)	\(T\)	\(F\)
\(T\)	\(T\)	\(T\)	\(T\)	\(F\)	\(T\)	\(F\)

Therefore, a possible statement by native A could he encoded with the formula:

\({-({-A} \rightarrow {-Acert})}\)
which could have come from the English statement: 

 "Do not believe anyone who says that, if I am a knave, then I must be uncertified."

This formulation being a bit heavy, we could use the fact that the formula:

\({-({-A} \rightarrow {-Acert})}\)

is logically equivalent to the disjunction:

\({-(A\ |\ {-Acert})}\)

which in turn could have come from the English statement:

"Anyone who says that I am a knight or uncertified is a liar."
Note that the solution given by Smullyan on page 44 of his book is a more concise conjunction that is equivalent to both formulas above.

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

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

This puzzle reads:

On another occasion I came across a native who said, "I am an uncertified knight." Is this the same situation as the last problem? Is it now possible to tell whether or not he is a knight? Can one tell whether or not he is certified?

Recall the "last puzzle", that is, our puzzle #1:

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?

Neither one of these puzzles is hard but, to answer the first question:

Is this the same situation as the last problem?

no, this is not the same as the first puzzle. In fact, these puzzles highlight why we need to be careful with the meaning of negation in English statements.

The old statement, "I am not a certified knight.", means that it is not the case that I am both a knight and certified.

In contrast, the new statement, "I am an uncertified knight.", means that I am definitely both a knight and not certified.

The logic formulas are therefore different, namely:

-(A & Acert) [Puzzle #1]

versus

A & -Acert [Puzzle #2]

assuming again that the native in the puzzle is referred to as A and that the propositions A and Acert mean "A is a knight" and "A is certified", respectively.

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

We can solve it formally, by building a truth table, as follows:

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

Note that the formula in the last column is the representation of the native's statement, according to our usual representation principle.

Since the top three rows contain True, this puzzle has three solutions:

1. A is an uncertified knave (row 1)
2. A is a certified knave (row 2)
3. A is an uncertified knight (row 3)

So the answers to the puzzle's questions:

• Is it now possible to tell whether or not he is a knight? 
• Can one tell whether or not he is certified?

are both negative!

If we did not want to build the truth table manually, we could have used Mace4 with the following input:

Mace4's output, namely:

proves that the three solutions we identified earlier are correct.

Finally, we could have used Prover9 to prove that our solution is correct.

The solution to the puzzle could be represented as:

(-A & -Acert) | (-A & Acert) | (A & -Acert)

as the disjunction of the three possible scenarios.

However, it would be more concise to state, equivalently, that the last scenario is NOT possible, namely:

-(A & Acert)

or equivalently:

-A | -Acert

(by one of De Morgan's laws), which we feed as a goal to Prover9:

to get the following proof by contradiction:

This is a short proof indeed!

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

[Part 8] Raymond Smullyan's Knights, Knaves, and Normals puzzles Fourth puzzle, on the island of Bahava

For our fourth puzzle, we will use the \(46^{th}\) (and last) 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". This puzzle takes place again on the island of Bahava, on which marriage is highly regulated. As stated on pages 25-26 of the 2011, paperback Dover Recreational Math edition [ISBN: 9780486481982], the puzzle reads:

[...] Thus, given any married couple, either they are both normal, or one of them is a knight and the other a knave. [...]

This problem concerns two married couples on the island of Bahava, Mr. and Mrs. A, and Mr. and Mrs. B. They are being interviewed, and three of the four people give the following testimony:

Mr. A: Mr B. is a knight.

Mrs. A: My husband is right; Mr. B is a knight.  

Mrs. B: That's right. My husband is indeed a knight.  

What are each of the four people, and which of the three statements are true?

As always in this series, the following axioms represent the possible types for all inhabitants:

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

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

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

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

Like in the previous post, we represent the fact that two inhabitants A and B are married with the formula:

Mar(A,B).

 Since the "married" relationship is symmetrical, we add the following axiom:

Mar(x,y) -> Mar(y,x).

Then we represent the marriage restrictions based on types with the axiom:

Mar(x,y) -> ((Nor(x) & Nor(y)) | (Kni(x) & Kna(y))).

Finally, we encode the fact that polygamy is not allowed with the axiom:

(Mar(x,y) & Mar(x,z)) -> y = z.

This concludes our representation of the island of Bahava's general conditions.

Turning to our specific puzzle, we represent the fact that we have two couples made of four distinct islanders, and that there are no other islanders in this puzzle, as follows:

Mar(MrA,MrsA).

Mar(MrB,MrsB).

MrA != MrsA & MrA != MrB & ...  [formula continued on the next line]

... MrA != MrsB & MrsA != MrB & MrsA != MrsB | MrB != MrsB.

x = MrA | x = MrsA | x = MrB | x = MrsB.

Finally, we represent the three statements using our usual representation principle for the knights/knaves/normals puzzle, yielding the three formulas:

(Kni(MrA) & Kni(MrB)) | (Kna(MrA) & -Kni(MrB)) | Nor(MrA). 

(Kni(MrsA) & Kni(MrB)) | (Kna(MrsA) & -Kni(MrB)) | Nor(MrsA). 

(Kni(MrsB) & Kni(MrB)) | (Kna(MrsB) & -Kni(MrB)) | Nor(MrsB).

The entire input given to Mace4 is thus:

and its output is:

The only model in this output demonstrates that there is only one solution to this puzzle: all four islanders are normals; therefore all three statements are false.