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

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

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

In the previous post, we used Mace4 to solve the following puzzle:

We are given three people, A, B, C, one of whom is a knight, one a knave, and one normal (but not necessarily in that order). They make the following statements:

A: I am normal.

B: That is true. 

C: I am not normal. 

What are A, B, and C?

In this post, we use Prover9 to build a proof by contradiction of this puzzle's solution.

Here is the input that we fed to Mace4 to represent this puzzle:

in which:

• the first group of formulas represent the fact that each islander has EXACTLY (i.e., at least and at most) one of three types (knight, knave, or normal),
• the second group of formulas represent (to some extent; see below for details) the fact that the three islanders all have different types,
• the third group (of one formula) represents the fact that the three constants \(A\), \(B\), and \(C\) refer to three different islanders, and
• the last group of formulas represent the three statements made by the islanders.

Now, in addition to these formulas, we need to feed to Prover9 the goal that we are trying to prove, namely the solution of the puzzle:

\(Kna(A)\ \&\ Nor(B)\ \&\ Kni(C)\).

Unfortunately, given this input, Prover9 returns:

which means that Prover9 was not able to find a proof.

Why is Prover9 failing to find a proof for a solution that Mace4 found?

Was Mace4 wrong? Or is Prover9 less powerful than Mace4?

No! In this case, the problem lies somewhere else: Mace4 is using a piece of information that Prover9 does not have, namely the number of islanders that are relevant to this puzzle.

When using Mace4, recall that I set its domain_size parameter to 3. This is because the "domain" of a model in this case is the set of islanders involved in the puzzle.

This piece of information is important to the puzzle but is not encoded in the input we fed to Prover9.

The input we fed to Mace4 was augmented by the domain size parameter, which was NOT part of the input formulas. This extra parameter (or option) is not available to Prover9, which does not have an explicit domain (recall that it finds proofs instead of models).

Note that the formulas that form the second group we fed as input to Mace4, namely:

(exists x Kni(x)).
(exists x Kna(x)).
(exists x Nor(x)).

represent the fact that there exists at least one inhabitant of each type. But, while we know those to be A, B, and, C, the formulas do not imply that. That is because there could be additional inhabitants (other than A, B, and C) in the domain of discourse (i.e., the puzzle). 

What we need to do is to encode this information explicitly in the input we feed to Prover9.

This is actually easy; and there are several ways to do it. I chose to add the following formula to our puzzle description:

\(∀x\ (x\ =\ A\ |\ x\ =\ B\ |\ x\ =\ C)\)

which represents the fact that, if you randomly pick any islander, it will always end up being one element of the set {A, B, C}. 

In other words, the puzzle only involves these three inhabitants. Recall that we already encoded the fact that these three constants identify three distinct inhabitants.

The Prover9 syntax for this formula is:

forall x (x = A | x = B | x = C).

or simply:

x = A | x = B | x = C.

since each variable (e.g., x) is implicitly universally quantified.

Now, before we test Prover9 again, let me simplify our input a bit.

Look back at the first group of formulas  (in the image above, right below the puzzle statement) we fed to Mace4.

The last three formulas in this group represent the fact that no islander can have more than one type. For example, the formula:

Kni(x) -> (-Kna(x) & -Nor(x)).

means that any knight cannot be a knave nor a normal. Together, the three formulas in this group cover all possibilities.

However, this constraint can also be conveyed with the statement: 

"No inhabitant can be 

both a knight and a knave, 

nor both a knight and a normal, 

nor both a knave and a normal." 

which, in Prover9 notation, becomes:

-(Kni(x) & Kna(x)).

-(Kni(x) & Nor(x)).

-(Kna(x) & Nor(x)).

Since Prover9 will convert these three formulas to clauses, we might as well do it ourselves, yielding:

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

by De Morgan's law for distributing negation over conjunction.

So, here is our final input for Prover9:

And here is Prover9's output:

============================== PROOF =================================
1 (exists x Kni(x)) # label(non_clause).  [assumption].
2 (exists x Kna(x)) # label(non_clause).  [assumption].
3 (exists x Nor(x)) # label(non_clause).  [assumption].
4 Kni(B) & Nor(A) | Kna(B) & -Nor(A) | Nor(B) # label(non_clause).  [assumption].
5 Kna(A) & Nor(B) & Kni(C) # label(non_clause) # label(goal).  [goal].
7 -Kni(x) | -Kna(x).  [assumption].
8 -Kni(x) | -Nor(x).  [assumption].
9 -Kna(x) | -Nor(x).  [assumption].
10 x = A | x = B | x = C.  [assumption].
11 A = x | B = x | C = x.  [copy(10),flip(a),flip(b),flip(c)].
17 Kni(c1).  [clausify(1)].
18 Kna(c2).  [clausify(2)].
19 Nor(c3).  [clausify(3)].
20 Kna(A) | Nor(A).  [assumption].
21 Kni(B) | -Nor(A) | Nor(B).  [clausify(4)].
22 Nor(A) | Kna(B) | Nor(B).  [clausify(4)].
23 Kni(C) | Nor(C).  [assumption].
24 -Kna(A) | -Nor(B) | -Kni(C).  [deny(5)].
26 -Nor(c1).  [resolve(17,a,8,a)].
27 -Kna(c1).  [resolve(17,a,7,a)].
28 c1 = A | c1 = B | Kni(C).  [para(11(c,2),17(a,1)),flip(a),flip(b)].
29 -Nor(c2).  [resolve(18,a,9,a)].
30 -Kni(c2).  [ur(7,b,18,a)].
31 c2 = A | c2 = B | Kna(C).  [para(11(c,2),18(a,1)),flip(a),flip(b)].
34 c3 = A | c3 = B | Nor(C).  [para(11(c,2),19(a,1)),flip(a),flip(b)].
35 -Nor(A) | Nor(B) | -Kna(B).  [resolve(21,a,7,a)].
36 Nor(C) | -Kna(C).  [resolve(23,a,7,a)].
66 c2 = A | c2 = B | -Nor(C).  [para(11(c,2),29(a,1)),flip(a),flip(b)].
76 c1 = A | c1 = B | -Kna(A) | -Nor(B).  [resolve(28,c,24,c)].
83 c2 = A | c2 = B | Nor(C).  [resolve(31,c,36,b)].
86 c1 = A | c1 = B | c3 = A | c3 = B.  [hyper(8,a,28,c,b,34,c)].
89 c2 = A | c2 = B.  [resolve(83,c,66,c),merge(c),merge(d)].
90 c2 = B | Kna(A).  [para(89(a,1),18(a,1))].
93 c2 = B | -Nor(A).  [para(89(a,1),29(a,1))].
104 c1 = A | c1 = B | -Nor(B) | c2 = B.  [resolve(76,c,90,b)].
109 c1 = A | c1 = B | c3 = B | Nor(A).  [para(86(c,1),19(a,1))].
120 c1 = A | c1 = B | c3 = B | c2 = B.  [resolve(109,d,93,b)].
129 c1 = A | c1 = B | c2 = B | Nor(B).  [para(120(c,1),19(a,1))].
133 c1 = A | c1 = B | c2 = B.  [resolve(129,d,104,c),merge(d),merge(e),merge(f)].
134 c1 = A | c1 = B | Kna(B).  [para(133(c,1),18(a,1))].
135 c1 = A | c1 = B | -Nor(B).  [para(133(c,1),29(a,1))].
138 Nor(B) | c1 = A | c1 = B | c3 = B.  [hyper(35,a,109,d,c,134,c),merge(e),merge(f)].
149 c1 = A | c1 = B | c3 = B.  [resolve(138,a,135,c),merge(d),merge(e)].
150 c1 = A | c1 = B | Nor(B).  [para(149(c,1),19(a,1))].
152 c1 = A | c1 = B.  [resolve(150,c,135,c),merge(c),merge(d)].
153 c1 = B | Kni(A).  [para(152(a,1),17(a,1))].
156 c1 = B | -Nor(A).  [para(152(a,1),26(a,1))].
160 c1 = B | Nor(A).  [hyper(7,a,153,b,b,20,a)].
168 c1 = B.  [resolve(160,b,156,b),merge(b)].
169 -Kna(B).  [back_rewrite(27),rewrite([168(1)])].
170 -Nor(B).  [back_rewrite(26),rewrite([168(1)])].
171 Kni(B).  [back_rewrite(17),rewrite([168(1)])].
172 Nor(A).  [back_unit_del(22),unit_del(b,169),unit_del(c,170)].
173 c2 = B.  [back_unit_del(93),unit_del(b,172)].
174 $F.  [back_rewrite(30),rewrite([173(1)]),unit_del(a,171)].
============================== end of proof ==========================

It is the longest proof we have seen so far, no doubt!

But it was easy to produce (just one click!) once we had the correct logical formulation.

Can you make sense of (parts of) it? 

Can you relate (parts of) it to your informal proof? 

Or to the one that Raymond Smullyan provides on page 32 of the 2011 paperback Dover Recreational Math edition [ISBN: 9780486481982] of his 1978 book entitled "What Is the Name of This Book?: The Riddle of Dracula and Other Logical Puzzles"?

[Part 4] Raymond Smullyan's Knights, Knaves, and Normals puzzles First puzzle, solved with Mace4

Being comfortable with predicate logic and our new representation principle, we are now ready to automate the solution of our first puzzle.

For our first example, we will use the \(39^{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 pages 23 and 24 of the 2011, paperback Dover Recreational Math edition [ISBN: 9780486481982], the puzzle reads:

We are given three people, A, B, C, one of whom is a knight, one a knave, and one normal (but not necessarily in that order). They make the following statements:

A: I am normal.

B: That is true. 

C: I am not normal. 

What are A, B, and C?

The informal answer given by Smullyan in the book (on page 32) is a proof by cases. I will not spoil the fun of your coming up with a solution on your own. 

Once you have solved this puzzle, come back here to check your solution and read about how to obtain a formal proof of the solution.

First, we represent the constraint shared by all puzzles that take place on this island: everybody is a knight, a knave, or (a) normal, but cannot be of more than one type. As we discussed earlier in this series, one formal representation of this constraint is the following set of four axioms:

\(∀x\ (Kni(x)\ |\ Kna(x)\ |\ Nor(x))\)

\(∀x\ (Kni(x) \rightarrow (-Kna(x)\ \&\ {-Nor(x)}))\)

\(∀x\ (Kna(x) \rightarrow (-Kni(x)\ \&\ {-Nor(x)}))\)

\(∀x\ (Nor(x) \rightarrow (-Kni(x)\ \&\ {-Kna(x)}))\)

Second, we need to represent the fact that we are dealing with 3 distinct inhabitants. We will refer to them by the constants \(A\), \(B\), and \(C\). 

However, to a theorem prover, having three different names (i.e., constants) does not prevent two (or more) of these names to refer to the same individual (like, e.g., the names "Clark Kent" and "Superman").

Therefore, we must make it explicit that these three constants do refer to three distinct islanders. We can do so using the equality predicate as follows:

\(-Equal(A,B)\ \&\ {-Equal(A,C)}\ \&\ {-Equal(B,C)}\)

Now, Mace4,  the theorem prover we chose, uses the infix notation \( x\ !\!=\ y\) instead of the (prefix) predicate notation \(-Equal(x,y)\). 

Therefore, we will use this notation as well to rewrite the formula above as:

\(A\ !\!=\ B\quad \&\quad A\ !\!=\ C\quad \&\quad B\ !\!=\ C\)

Third, we need to represent the fact, specific to this puzzle, that among the three inhabitants, there is one of each type. This becomes:

\(∃x\ Kni(x)\)
\(∃x\ Kna(x)\)
\(∃x\ Nor(x)\)

Finally, we must represent the three islanders' statements.

A's statement, "I am normal", becomes the formula \(\varphi_A\):

\(Nor(A)\)

B's statement, "That is true" (interpreted as "A is normal"), becomes the formula \(\varphi_B\):

\(Nor(A)\)

Note that B's agreeing with A means that A and B's statements are identical.

C's statement, "I am not normal", becomes the formula \(\varphi_C\):

\(-Nor(C)\)

Of course, we do not know the truth value of these three statements. We just know that one of the inhabitants uttered one of them, respectively.

We will apply our representation principle to reflect this last component of the puzzle, 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)\)

---

The application of this principle to the three puzzle statements, yields the three formulas:

\((Kni(A)\ \&\ Nor(A))\ |\ (Kna(A)\ \&\ {-Nor(A)}\ |\ Nor(A)\)
\((Kni(B)\ \&\ Nor(A))\ |\ (Kna(B)\ \&\ {-Nor(A)})\ |\ Nor(B)\)
\((Kni(C)\ \&\ {-Nor(C)})\ |\ (Kna(C)\ \&\ {Nor(C)})\ |\ Nor(C)\)

Now, these three formulas simplify to:

\(Kna(A)\ |\ Nor(A)\)
\((Kni(B)\ \&\ Nor(A))\ |\ (Kna(B)\ \&\ {-Nor(A)})\ |\ Nor(B)\)
\(Kni(C)\ |\ Nor(C)\)

because:

1. The sub-formula \((Kni(A)\ \&\ Nor(A))\) in the first formula is always false, and can thus be deleted (as one disjunct of the whole formula).
2. The sub-formula \((Kna(A)\ \&\ {-Nor(A)})\) in the first formula reduces to \(Kna(A)\), since being a knave implies (see axiom above) not being normal.
3. The sub-formula \((Kni(C)\ \&\ {-Nor(C)})\) in the third formula reduces to \(Kni(C)\), since being a knight implies (see axiom above) not being normal.
4. The sub-formula \((Kna(C)\ \&\ {Nor(C)})\) in the third formula is always false, and can thus be deleted (as a disjunct of the whole formula).

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

Two comments on this input:

• We need to remember to add the period at the end of each formula.
• The quantifiers are handled like this in Mace4:
• \(∃ x\ \varphi\), for any formula \(\varphi\), becomes \((exists\ x\ \varphi)\)
• \(∀ x\ \varphi\), for any formula \(\varphi\), becomes \(all\ x\ \varphi\), or simply, \(\varphi\), since all variables (e.g., \(x\), \(y\), \(z\)) are universally quantified in Mace4 by default.

As explained in a previous post, we run Mace4 on this input. In this case, we set the following options for Mace4:

• domain_size is set to 3, since we have exactly three islanders in our domain for this specific puzzle.
• max_models is set to 6, in case there happens to be more than one solution (or model) for this puzzle. 

The output generated by Mace4 is the following:

which we interpret as follows:

1. The first line indicates that there is only one model (or puzzle solution) found and that it contains three inhabitants.
2. The three middle lines show that Mace4 created its own three names for our inhabitants (namely, c1, c2, and c3), which are internally represented by the integers 2, 0, and 1, respectively. These three integers will be used below to reference our islanders by indices in three-element arrays.
3. The first three lines show that our islander A is associated with the index 0, our islander B is associated with the index 1, and our islander C is associated with the index 2.
4. The last three lines indicate that only the islander with index 0 (that is, A) is a knave, only the islander with index 2 (that is, C) is a knight, and only the islander with index 1 (that is, B) is normal.

So Mace4 determined (i.e., proved) on its own that the only solution to the puzzle is:

• A is a knave
• B is normal
• C is a knight

Did you solve this puzzle correctly?

[Part 3] Raymond Smullyan's Knights, Knaves, and Normals puzzles Representing statements made by islanders

Now that we understand the advantages of using predicates and quantifiers, we can represent the fact that each and every inhabitant of this island must have exactly one type using the following axioms:

\(∀x\ (Kni(x)\ |\ Kna(x)\ |\ Nor(x))\)

\(∀x\ (Kni(x) \rightarrow (-Kna(x)\ \&\ {-Nor(x)}))\)

\(∀x\ (Kna(x) \rightarrow (-Kni(x)\ \&\ {-Nor(x)}))\)

\(∀x\ (Nor(x) \rightarrow (-Kni(x)\ \&\ {-Kna(x)}))\)

While this is knowledge about the island world itself that is shared by all puzzles, we now turn our attention to the statements that islanders make as part of each specific puzzle.

First, the contents of each statement can also be represented with the same predicates and constants. For example, the statement "If A is a knave, then B is normal", is represented by the following formula of our first-order predicate calculus:

\(Kna(A) \rightarrow Nor(B)\)

In general, we will represent any such statement using some formula \(\varphi\). 

Second, how do we represent the fact that a specific inhabitant made that statement?

Back on the other island, when propositional logic was adequate, we used the following representation principle for statements.

---

 Representation principle for Knights and Knaves puzzles

For any person P living on this island and any statement S,
the fact that P said S
will be represented by the formula:

\(P \leftrightarrow S\)

---

Refer back to this earlier post for a discussion of this principle. Briefly: back then, we saw that \(P\) (representing the fact that P is a knight) has the same truth value as \(S\) because:

• If \(P\) is true, then P is a knight and all of its statements, including S, are true.
• If \(P\) is false, then P is a knave and all of its statements, including S, are false.

If two formulas \(P\) and \(S\) always have the same truth value, we say that they are equivalent, which can be represented in propositional logic using the formula:

\(P \leftrightarrow S\)

This approach will not work in our predicate calculus because:

• each islander is now represented by a constant, not a true/false proposition, and
• there is now a third type (i.e., normal) to consider.

However, we can get around these two issues and extend the applicability of our representation principle to predicate logic using a case-by-case reasoning similar to the two-type scenario of the previous island. 

Note that the formula:

\(P \leftrightarrow S\)

is equivalent to:

\((P\ \&\ S)\ |\ ({-P}\ \&\ {-S})\)

reflecting the two cases discussed above, that is, P being either a knight or a knave.

To extend this approach to our new island with three types, we simply need to add the third case.

Assume that person P made statement S. 

First, we will represent statement S with a predicate logic formula \(\varphi\).

Second, we will consider three cases:

• If P is a knight, then each one of P's statements, including S, is true; this is represented by the formula: \(Kni(P)\ \&\ \varphi\)
• If P is a knave, then each one of P's statements, including S, is false; this is represented by the formula: \(Kna(P)\ \&\ {-\varphi}\)
• If P is normal, then each one of P's statements, including S, is either true or false; since we have no information on the truth value of S, this case is represented by the formula: \(Nor(P)\).

In conclusion, when using predicate calculus to represent statements made by inhabitants of our new island, we will apply the following principle.

---

 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)\)

---

Coming back to our earlier example, the fact that inhabitant C made the statement "If A is a knave, then B is normal" would be represented by the following formula of first-order predicate calculus:

\((Kni(C)\ \&\ (Kna(A) \rightarrow Nor(B)))\ |\ (Kna(P)\ \&\ {-(Kna(A) \rightarrow Nor(B))})\ |\ Nor(P)\)

[Part 2] Raymond Smullyan's Knights, Knaves, and Normals puzzles Predicates and quantifiers to the rescue

In the previous post, we identified some limitations of propositional logic as a formal language for representing knights, knaves, and normals puzzles. 

The main issue was that too many propositions were needed. For example, in the scheme we described, we used the propositions \(AKni\) and \(BNor\) to represent the facts that A is a knight and B is normal, respectively.

More precisely, we needed three propositions for each inhabitant of the island, say,  \(BKni\), \(BKna\), and \(BNor\) for inhabitant B.

Furthermore, we needed four axioms for each inhabitant, say:

\(BKni\ |\ BKna\ |\ BNor\)
\(BKni \rightarrow (-BKna\ \&\ {-BNor})\)
\(BKna \rightarrow (-BKni\ \&\ {-BNor})\)

\(BNor \rightarrow (-BKni\ \&\ {-BKna})\)

for inhabitant B.

In conclusion, if there were \(n\) inhabitants on the island, we needed:

• \(3n\) propositions, and
• \(4n\) axioms,

just to represent the fact that each inhabitant has exactly one type (knight, knave, or normal). And that is not yet taking into account the representation of the statements that are made by the inhabitants in a specific puzzle.

Can we reduce the number of propositions and axioms needed to represent this world?

We can, if we realize that our propositions, as defined in propositional logic, have  a major drawback: they conflate two pieces of information that should be separated.

Consider the propositions \(AKni\) and \(BNor\) again. Each one of them both identifies one inhabitant and characterizes the type of this inhabitant. 

This does not seem to be a problem, until we realize that the propositions \(AKni\) and \(ANor\) identify the same person and thus cannot be true simultaneously. Similarly, \(ANor\) and \(BNor\) assign the same type to two different inhabitants. 

In each case, both propositions in the pair encode share information: shared identity or shared type. Therefore, the truth value of one proposition in a pair is likely to constrain the possible truth values of the other proposition in the pair.

Yet these constraints are not apparent from the propositions themselves. Recall that the propositions in a pair could have been called \(P\) and \(Q\) with no loss of information. The name/label of propositional variables do not affect how they get used within the logical system. 

Each propositional variable represents an atomic proposition that encodes a single statement, such as "Inhabitant I is of type T", whose internal structure is not accessible. It is not possible to extract "I" or "T" from such a proposition. 

To solve this problem, we would like to break down each proposition into two components, namely the identity of the inhabitant and the type of the inhabitant. 

If we can expose this internal structure, we can use the same "identifier" for the same person (or the same type) in two different statements, and thus automatically impose constraints on the truth values of related statements, instead of having to encode these constraints in many axioms, as we did above.

Instead of using a proposition to represent a statement (or sentence), we are going to break it into two parts:

• the subject of the sentence, and
• the part of the sentence that contains the verb and states something about the subject.

We will use constants like \(A\) and \(B\) to identify subjects.

We will use predicates to represent phrases like "is a knight" and "is normal".

Note that constants here represent individuals on our island. Therefore, these constants, unlike our earlier propositions, do NOT have a truth value. \(A\) now represents one inhabitant and can thus be neither true nor false. It is not a statement.

A predicate is also not a full statement, since it is missing a subject. We can represent the predicate "is a knight" with the expression \(Knight(.)\), with the dot as a placeholder for a subject that we do not yet know. 

Since we only have three types, and their three initial letters are sufficient to distinguish them, we will use \(Kni(.)\) as a somewhat more concise version. We will do so as well for the predicates \(Kna(.)\) and \(Nor(.)\). 

Finally, we can represent the statement "A is a knight" by applying the corresponding predicate to the previously defined constant for A, yielding the expression:

\(Kni(A)\)

Now, this expression is a valid formula that is either true or false.

This new type of logical language we are building is called a predicate calculus, with which inferences can be made, once we add inference rules to it (which we will not discuss at this point).

In this post, we will extend the expressive power of our predicate calculus by adding variables to it.

First, we define our domain (or universe of discourse) as the set of all inhabitants of our island.

Second, we define variables that range over our domain. For example, the variable \(x\) stands for an unknown inhabitant.

Third, we introduce the two quantifiers "for all" (denoted ∀) and "there exists" (denoted ∃) that allow us to build new formulas, such as:

\(∀x\ (Kni(x)\ |\ Kna(x)\ |\ Nor(x))\)

and

\(∃x\ Kni(x)\)

to represent the statements:

"Every inhabitant is a knight, a knave, or a normal."

and

"(At least) one inhabitant is a knight.",

respectively.

Now, we are able to represent the fact that each and every inhabitant of the island has exactly one type, using the following axioms:

\(∀x\ (Kni(x)\ |\ Kna(x)\ |\ Nor(x))\)

\(∀x\ (Kni(x) \rightarrow (-Kna(x)\ \&\ {-Nor(x)}))\)

\(∀x\ (Kna(x) \rightarrow (-Kni(x)\ \&\ {-Nor(x)}))\)

\(∀x\ (Nor(x) \rightarrow (-Kni(x)\ \&\ {-Kna(x)}))\)

Whatever the number \(n\) of inhabitants, these four axioms are sufficient to represent the same constraint over all of them, whereas we needed \(4n\) axioms in our earlier, propositional representation scheme.

Hence, we replaced a representation whose length is proportional to (i.e., linear in) the number \(n\) of inhabitants with one whose length is constant (i.e., independent of \(n\)).

In future proofs, we will add one constant for each inhabitant in a puzzle (e.g., \(A\), \(B\), etc.), so we can instantiate the four axioms above to represent, for example, the fact that inhabitant A has exactly one type, yielding:

\(Kni(A)\ |\ Kna(A)\ |\ Nor(A)\)

\(Kni(A) \rightarrow (-Kna(A)\ \&\ {-Nor(A)})\)

\(Kna(A) \rightarrow (-Kni(A)\ \&\ {-Nor(A)})\)

\(Nor(A) \rightarrow (-Kni(A)\ \&\ {-Kna(A)})\)

However, these axiom instances will be generated automatically by the theorem prover (if needed during a proof) whose input will be limited to the four general axioms and the individual constants.

So, when it comes to the formulas that WE have to work out if there are \(n\) inhabitants on the island, we went from:

• \(3n\) propositions and
• \(4n\) axioms

to:

• \(n\) constants and
• \(4\) axioms.

Now that we have our island world encoded in logic, we need to be able to represent statements made by inhabitants as part of a puzzle statement.

But this is a task we will tackle in the next post.

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

[Part 1] Raymond Smullyan's Knights, Knaves, and Normals puzzles Limitations of propositional logic

Raymond Smullyan introduced the Knights and Knaves puzzles in chapter 3 of his 1978 book entitled "What Is the Name of This Book?: The Riddle of Dracula and Other Logical Puzzles".

We discussed these puzzles at length in an earlier series.

In this series, we discuss  the second kind of puzzle that Smullyan introduced later in that same chapter, called the "Knights, Knaves, and Normals" puzzles, starting on page 23 of the 2011, paperback Dover Recreational Math edition [ISBN: 9780486481982].

On this new island, there are three types of inhabitants: "knights, who always tell the truth; knaves, who always lie; and normal people, who sometimes lie and sometimes tell the truth."

The existence of "normals" makes the puzzle a bit more complex and thus more rewarding to solve. It also illustrates weaknesses of propositional logic, as we used it in our previous series.

Back then, when solving the knights and knaves puzzles (without normals), we used a single proposition for each inhabitant involved in the puzzle. For example, the proposition \(A\) represented the fact that the inhabitant whose name is A was a knight.

It was very convenient that each inhabitant on that island always was of one type and that there were exactly two possible types: knight or knave. In this scenario, proving that someone is not a knight was the same as proving that this person was a knave, and vice versa.

In logical terms, a single proposition was enough to represent the type an inhabitant: 

• if \(A\) is true, then person A is a knight;
• otherwise (that is, when \(A\) is false, or equivalently, \(-A\) is true), person A is a knave.

Things are not so neat on the new island because of the third possible type (normal). In this scenario, proving that someone is not a knight is NOT the same as proving that this person is a knave. Instead, it proves that this person is a knave or a normal.

More generally, disproving one type is not enough to establish a person's type.

This difficulty also has consequences for the way that puzzles are represented in formal logic. 

First difficulty

On the old island, there was no need to include, as axioms, formulas of the form:

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

to represent the fact that A must be a knight or a knave, since this formula is a tautology (i.e., it is always true) in any logic that follows the law of excluded middle, one of the three laws of thought.

On the new island, this law still applies. So, if we know that \(A\) is false, we can infer that \(-A\) is true. However, \(-A\) now means that "A is not a knight", which is not the same as "A is a knave" any longer.

Instead, \(-A\) means that "A is a knave or a normal."

But then, we cannot use the proposition \(A\) (nor its negation) to represent "A is knave" or "A is (a) normal".

We are forced to introduce new propositions to represent the separate facts that "A is knave" or "A is normal".

Let's assume we use the three propositions \(AKni\), \(AKna\), and \(ANor\) to represent the facts that "A is a knight", "A is a knave", and "A is normal", respectively.

Now, to accurately represent the facts of life on the new island, we must add axioms of the form:

\(AKni \rightarrow (-AKna\ \&\ {-ANor})\)

\(AKna \rightarrow (-AKni\ \&\ {-ANor})\)

\(ANor \rightarrow (-AKni\ \&\ {-AKna})\)

Second difficulty

The three previous axioms are needed to represent the fact that A has (at most) one type, and cannot be, for example, both a knight and a knave (which follows from the first axiom above).

To be clear, the law of excluded middle still applies: it is still true that either A is a knight or A is not a knight. Unfortunately, knowing that A is not a knight does not give us any information about whether A is a knave or a normal.

Worse, since we use three distinct propositions for the three possible types of A, there is no connection at all among these three variables in propositional logic.

On the old island, the two types (i.e., Knight and Knave) were automatically connected (as opposites), since one being true automatically meant that the other one was false (and vice versa). It was a given that exactly one of them had to be true (again, by the law of excluded middle).

On the new island, the connection among the three types is lost in the representation. The propositions \(AKni\) and \(AKna\) are no more (semantically) related than if they were named \(P\) and \( Q\), respectively, which is to say that they are NOT semantically related at all.

For this reason, we must now explicitly represent this semantic relationship with the new axiom:

\(AKni\ |\ AKna\ |\ ANor\)

which encodes the fact that person A's type must be one of the three possible types.

More precisely, this axiom states that A must be of at least one of these types, whereas the three axioms introduced earlier together state that A must be of at most one of these types.

To recap, we need three propositions and four axioms to represent the possible types for person A.

What about the other inhabitants of the island?

Third difficulty

All of the propositions and axioms described so far pertain to person A only. If the puzzle involves other inhabitants of the new island, we are going to need a new set of three propositions and four axioms to represent the possible types of each one of them.

For example, for person B, we would need the propositions \(BKni\), \(BKna\), and \(BNor\) and the axioms:

\(BKni\ |\ BKna\ |\ BNor\)

\(BKni \rightarrow (-BKna\ \&\ {-BNor})\)
\(BKna \rightarrow (-BKni\ \&\ {-BNor})\)

\(BNor \rightarrow (-BKni\ \&\ {-BKna})\)

This representation scheme may quickly get out of hand.

In the next post, we will use these limitations of propositional logic to motivate the use of first-order logic that involves predicates and quantifiers.