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

For our third puzzle, we will use the \(44^{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". This puzzle takes place 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. [...]

We first consider a married couple, Mr. and Mrs. A. They make the following statements:

Mr. A: My wife is not normal.

Mrs. A: My husband is not normal.  

What are Mr. and Mrs. A?

This puzzle turns out to be rather easy. But it is interesting to solve it in this series because it will allow us to use a new binary (i.e., two-place) predicate: to represent the fact that two inhabitants A and B are married, we will use the formula:

Mar(A,B).

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

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

Finally, we represent the marriage restrictions based on types with the axiom:

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

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

Turning to our specific puzzle, we represent the fact that Mrs. and Mr. A are two distinct islanders who are married to each other with the formulas:

Mar(MrA,MrsA).

MrA != MrsA.

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

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

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

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: both Mrs. and Mr. A must be normals.