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

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

Table of contents for the series on Knights, Knaves, and Normals puzzles

1. Limitations of propositional logic
   • In which we discuss why propositional logic is far from ideal when it comes to represent these puzzles formally
2. Predicates and quantifiers to the rescue
   • In which we discuss how to use first-order predicate calculus to represent succinctly the type constraints on all inhabitants
3. Representing statements made by islanders
   • In which we discuss how to use first-order predicate calculus to represent the fact a specific islander made a given statement
4. First puzzle, solved with Mace4
   • In which we discuss how to represent a full puzzle statement in first-order predicate logic and use Mace4 to automatically discover/prove the correct solution to this puzzle
5. First puzzle, solved with Prover9
   • In which we discuss how to represent our first puzzle correctly for input to Prover9 and then exhibit a formal proof of the correctness of our solution to this puzzle
6. Second puzzle, solved with Prover9
   • In which we discuss how to solve our second puzzle which asks for a proof of a given result and is thus a perfect fit for Prover9
7. Third puzzle, on the island of Bahava
   • In which we discuss how to solve our third puzzle, which takes place on the island of Bahava, where normals can only marry normals and knights can only marry knaves (and vice-versa)
8. Fourth puzzle, on the island of Bahava
   • In which we discuss how to solve our last puzzle, which takes place again on the island of Bahava, and involves two couples