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

Table of contents for the series of posts on Knights and Knaves puzzles

1. Review of propositional logic
   • In which we discuss propositional variables, logical connectives, and a couple of logical equivalences
2. Representation principle for Knights and Knaves puzzles
   • In which we discuss a general principle for representing, in propositional logic, statements made by the island's inhabitants
3. First example - Informal solution
   • In which we discuss a typical puzzle with two inhabitants and solve it informally. A typical puzzle asks questions of the type: What is A?
4. First example - Formal proof
   • In which we discuss a complete, formal proof of the solution to our first puzzle
5. First example - A natural-deduction proof
   • In which we discuss what a natural-deduction-style proof looks like and provide such a formal proof by cases for our first example
6. First example - Truth table approach
   • In which we discuss how to solve a typical puzzle by building a truth table
7. First example - Proof by contradiction
   • In which we discuss an indirect proof of the puzzle's solution that contrasts with the direct proofs we gave earlier
8. Second example
   • In which we discuss both an informal solution and a formal, truth-table-based approach to a second typical puzzle with 3 inhabitants
9. Automating puzzle proofs with Prover9
   • In which we discuss an automatic theorem prover and use it to automatically generate a proof by contradiction of the solution to our first puzzle
10. Automating puzzle proofs with Mace4
    • In which we discuss how to automatically solve the first puzzle using another theorem prover that does not need the solution of the puzzle to generate the proof
11. Third example
    • In which we discuss how to solve a typical puzzle with more than one solution using both Prover9 and Mace4.
12. Fourth example
    • In which we discuss how to solve another typical problem that involves statements of the form "such and such inhabitants are (not) of the same type"
13. Fifth example
    • In which we discuss how to solve yet another type of puzzle that does not ask to determine the type of inhabitants but rather the answer that they will give to some question
14. Sixth example
    • In which we discuss how to solve yet another type of puzzle in which we have to use additional information given by the author, that is not part of the puzzle's storyline
15. Seventh example
    • In which we discuss how to solve yet another type of puzzle in which we must determine if the answers to two questions posed to two inhabitants are the same
16. Creating our own puzzle
    • In which we discuss how to reverse the truth-table approach to create new Knights and Knaves puzzles that are provably correct

[Part 16] A Propositional Logic approach to Raymond Smullyan's Knights and Knaves puzzles Creating our own puzzles

So far in this series, we have discussed how to solve Knights and Knaves puzzles both informally and (mostly) formally. We have illustrated a few types of formal proofs, such as direct proofs, proofs by contradiction, and proofs based on truth tables.

When using truth tables, we followed this process:

1. Represent the puzzle statement using a formula \(\varphi\) that is a conjunction of one or more formulas in propositional logic using, \(\varphi\) contains \(n\) distinct propositional variables, where \(n\) is the number of island inhabitants involved in the puzzle statement.
2. Build a truth table with \(2^n\) rows in which each row corresponds to one unique assignment of truth values to the propositions in \(\varphi\).
3. Read out of the truth table the answer to the puzzle based on which row(s) of the table make \(\varphi\) true.

In this post, we will reverse this process to create a new puzzle as follows:

1. Pick \(n\) (the number of inhabitants in our new puzzle) and build a truth table with \(2^n\) rows for an unknown conjunction \(\varphi\). In this table, we will assign the value False for\(\varphi\) in all rows but one in order to make sure that the puzzle has a unique solution. This table will only contain one column for each proposition and one column for the unknown \(\varphi\).
2. We will fill in the table with intermediate columns corresponding to carefully chosen formulas to be combined together in a conjunction that will make up \(\varphi\).
3. We will convert each sub-formula (i.e., each conjunct) in \(\varphi\) into an English statement. The concatenation of these English statements, with added text for context, will make up the statement of the new puzzle.

Step 1

We pick \(n\) to be 3 and choose the names A, B, and C for these inhabitants.

We then build a truth table with \(2^3=8\) rows. As shown below, we arbitrarily chose \(\varphi\) to be true only when all three inhabitants are knights (last row):

\(A\)	\(B\)	\(C\)	\(\varphi\)
\(F\)	\(F\)	\(F\)	\(F\)
\(F\)	\(F\)	\(T\)	\(F\)
\(F\)	\(T\)	\(F\)	\(F\)
\(F\)	\(T\)	\(T\)	\(F\)
\(T\)	\(F\)	\(F\)	\(F\)
\(T\)	\(F\)	\(T\)	\(F\)
\(T\)	\(T\)	\(F\)	\(F\)
\(T\)	\(T\)	\(T\)	\(T\)

Step 2

We pick a formula to become the first conjunct in \(\varphi\). Since we'd like our puzzle to be made of statements by the inhabitants, we choose a bi-conditional with a single proposition on its left, namely:

\(B \leftrightarrow A\)

This formula will become a statement made by B.

Here is the new truth table with a column inserted for this sub-formula of \(\varphi\):

\(A\)	\(B\)	\(C\)	\(B \leftrightarrow A\)	\(\varphi\)	done
\(F\)	\(F\)	\(F\)	\(T\)	\(F\)
\(F\)	\(F\)	\(T\)	\(T\)	\(F\)
\(F\)	\(T\)	\(F\)	\(F\)	\(F\)	✔
\(F\)	\(T\)	\(T\)	\(F\)	\(F\)	✔
\(T\)	\(F\)	\(F\)	\(F\)	\(F\)	✔
\(T\)	\(F\)	\(T\)	\(F\)	\(F\)	✔
\(T\)	\(T\)	\(F\)	\(T\)	\(F\)
\(T\)	\(T\)	\(T\)	\(T\)	\(T\)

The cells highlighted in green above indicate that this sub-formula matches the expected truth value of \(\varphi\) in five of the eight rows. In particular, the rows ending in a checkmark are considered final since adding any new conjuncts to \(\varphi\) (as we do below) cannot make them True again. 

We can thus simplify our table as follows:

\(A\)	\(B\)	\(C\)	\(B \leftrightarrow A\)	\(\varphi\)	done
\(F\)	\(F\)	\(F\)		\(F\)
\(F\)	\(F\)	\(T\)		\(F\)
\(F\)	\(T\)	\(F\)			✔
\(F\)	\(T\)	\(T\)			✔
\(T\)	\(F\)	\(F\)			✔
\(T\)	\(F\)	\(T\)			✔
\(T\)	\(T\)	\(F\)		\(F\)
\(T\)	\(T\)	\(T\)		\(T\)

Next, we pick a second sub-formula in order to handle as many of the remaining rows as possible. 

More precisely, we want to find another conjunct that will be added to \(\varphi\) to make it still True in the last row but False in the remaining rows (i.e., rows 1, 2 and 7).

This step requires a bit of thinking. After some trial and error, I found the following candidate formula:

\(C \leftrightarrow ({-A} \rightarrow {-C})\)

Next, I insert a column in our truth table for this new sub-formula:

\(A\)	\(B\)	\(C\)	\(B \leftrightarrow A\)	\(C \leftrightarrow ({-A} \rightarrow {-C})\)	\(\varphi\)	done
\(F\)	\(F\)	\(F\)		\(F\)	\(F\)	✔
\(F\)	\(F\)	\(T\)		\(F\)	\(F\)	✔
\(F\)	\(T\)	\(F\)				✔
\(F\)	\(T\)	\(T\)				✔
\(T\)	\(F\)	\(F\)				✔
\(T\)	\(F\)	\(T\)				✔
\(T\)	\(T\)	\(F\)		\(F\)	\(F\)	✔
\(T\)	\(T\)	\(T\)		\(T\)	\(T\)	✔

As shown in green above, this new formula does take care of all remaining rows. 

Therefore, we do not need additional formulas. These two sub-formulas appear sufficient to make \(\varphi\) True in exactly one case (i.e., the last row, in which all three inhabitants are knights).

If our truth table is correct (and we will prove it formally in two ways below), then our puzzle, as it stands, is encoded in the following two propositional logic formulas:

\(B \leftrightarrow A\)

\(C \leftrightarrow ({-A} \rightarrow {-C})\)

Step 3

Finally, we translate these formulas into English to yield a Smullyan-style puzzle. 

Of course, there are many possibilities. Let's go with this one:

On your next visit to the island of knights and knaves, you meet three inhabitants. When you ask the first one if he is a knight or a knave, he (i.e., A) refuses to answer. 

Then, the second one (i.e., B) tells you: "Too bad he is in a bad mood today because, whenever he talks, A cannot lie.". 

Finally, C, who is in a great mood adds: "Let me tell you, if A is a knave, then so am I." 

What are A, B, and C? 

And, voila!

But is this puzzle correct? Does it have a solution? As importantly, does it have a unique solution?

As has been our habit in this series, we now look for formal proofs of the correctness of our new puzzle.

Formal proof #1

First, we use Mace4. Given the input:

Mace4 outputs only one model, as expected:

in which all three inhabitants are knights.

Formal proof #2

Now, we use Prover9 which, given the input:

outputs a formal proof (by contradiction) of the correctness of our puzzle:

Well, I think this is as good a place as any to end both this post and the whole series.

I hope you enjoyed it!

[Part 15] A Propositional Logic approach to Raymond Smullyan's Knights and Knaves puzzles Seventh example

In this post, we will solve our last example in this series. In this seventh Knights and Knaves puzzle, we must determine if the answers to two questions posed to two inhabitants are the same.

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

Suppose you visit the island of knights and knaves. You come across two of its inhabitants lazily lying in the sun. You ask one of them whether the other one is a knight, and you get a (yes-or-no) answer. Then you ask the second one whether the first one is a knight. You get a (yes-or-no) answer.

Are the two answers necessarily the same?

The informal answer given by Smullyan in the book (on page 32) is again a proof by cases.

However, this is an example where the formal approach is much quicker!

Recall that the first step in a formal approach is to couch the puzzle statement in a formal language. Propositional logic is the language we have been using in this series.

As it turns out, once this puzzle is translated into propositional logic, the answer will be obvious. Therefore, there will be no need to use Mace4 nor Prover9. All of the work fun is in the representation step.

As we have done several times already, we will call the two inhabitants A and B. Then, the question posed to A becomes:

\(A \leftrightarrow B\) ?

Recall that the question mark is not part of the formula; it is added here to indicate that this is a question whose answer we do not know. If this translation is not obvious to you, refer back to this post for an explanation.

Similarly, the question posed to the other inhabitant becomes:

\(B \leftrightarrow A\) ?

Recall that the proposition on the left of the bi-conditional represents the person who gives the answer while the formula on the right is the question being asked.

Now, we are asked to determine whether the two answers are necessarily the same. 

The answer is clearly Yes, because the two logical formulas are equivalent. This is due to the fact that the bi-conditional connective is a commutative logical operator. 

In other words, for any formulas \(\varphi_1\) and \(\varphi_2\):

\(\varphi_1 \leftrightarrow \varphi_2\)

and 

\(\varphi_2 \leftrightarrow \varphi_1\)

always have the same value.

This is similar to the addition operator being commutative in the context of arithmetic. Whatever the integer or real values of \(x\) and \(y\):

\(x + y\)

and 

\(y + x\)

always have the same value, because \(+\) is a commutative operator.

[Part 14] A Propositional Logic approach to Raymond Smullyan's Knights and Knaves puzzles Sixth example

In this post, we will solve our sixth Knights and Knaves puzzle. In this puzzle, we again have to determine the type of two inhabitants; but this time, we have to use additional information given by the author, that is not part of the puzzle's storyline.

For our sixth example, we will use the eleventh puzzle in Chapter 3 (or the \(36^{th}\) puzzle overall) 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 22-23 of the 2011, paperback Dover Recreational Math edition [ISBN: 9780486481982], the puzzle, entitled "An adventure of mine", reads:

[...] Once when I visited the island of knights and knaves, I came across two of the inhabitants resting under a tree. I asked one of them, "Is either one of you a knight?" He responded, and I knew the answer to my question.

What is the person to whom I addressed the question-is he a knight or a knave; and what is the other one? I can assure you, I have given you enough information to solve the problem.

The most direct, informal analysis of this puzzle uses a case-by-case analysis. Instead, we will first develop a semi-formal approach to this puzzle, using Mace4, to eliminate most cases, and then use Mace4's output to informally deduce the solution.

In the second part of this post, we will formally prove this solution using Prover9.

Based on the second half of the puzzle statement, it appears that both answers (Yes and No) to the question are possible, but only one of them narrows down to a single answer the possible types of both inhabitants.

We will test this hypothesis by using Mace4 to list all cases consistent with both answers. The hypothesis will be confirmed if one of the answers to the question leads to only one possible type for each inhabitant. 

We will then know that this is the answer that was given to the visitor. As a result, we will be able to directly read out the answer to the puzzle in the truth values of the corresponding model output by Mace4.

Recall that the first step in formalizing a puzzle is to translate its statement into propositional logic.

Let's call A the inhabitant to whom the question was (A)dressed, while B will be the other inhabitant.

Using the representation scheme described earlier in this series, the question asked is straightforward and becomes the formula:

\(A\ |\ B\) ?

Of course, the question mark is not part of our formal logical language but is added here to indicate that this is not a stated fact nor even a statement by one of the protagonists.

Since the question is posed to A, his answer, as before, will be represented by the formula:

\(A \leftrightarrow (A\ |\ B)\) 

since, if A' s answer is Yes, it will be equivalent to A saying: "Yes, one of us is a knight.", and if A's answer is No, it will be equivalent to A saying: "No, neither one of us is a knight." 

Finally, like for our fifth example, we will use \(R\) to refer to the truth value of A's reply, yielding the formula:

\(R \leftrightarrow (A \leftrightarrow (A\ |\ B))\) 

This completes our translation of the puzzle statement into propositional logic.

Semi-formal solution

Given the input:

Mace4 produces the following output:

As was discussed in a previous post, to get this output, I set Mace4's "max models" parameter to 8 (since the puzzle uses four propositions, each of which can be True or False in a model, and \(2^3 = 8\)). I also used the "Isofilter..." post-processing step described in the same earlier post to eliminate duplicate models.

Mace4's output above gives us four distinct models. In other words, there are four combinations of truth values for \(A\), \(B\), and \(R\) that make the puzzle statement true.

Three of these models assign True to \(R\). In other words, when the answer to the question is Yes, there are three possible combinations of types for A and B, and it is not possible to ascertain their type.

However, our hypothesis is confirmed by the fact that there is only one model in which the answer is No (i.e., \(R\) is assigned the value 0 for False). This is the second model in Mace4's output.

In this model, \(A\) is assigned the value 0 (False), while \(B\) is assigned the value 1 (True).

Since this is the only answer that provides enough information, as per the puzzle statement, the answer to the question must be No, and the solution to the puzzle must be:

• A ("the person to whom I addressed the question") is a knave, while
• B ("the other one") is a knight.

Alternatively, we could have manually built a truth table; however, that would have been a bit more tedious than running Mace4!

Formal solution

Now that we have discovered the solution to the puzzle, we can prove that it is correct with a formal proof by contradiction.

First, recall that A's answer to the question was represented with the formula:

\(A \leftrightarrow (A\ |\ B)\)

Since we inferred that the answer to this question is No, we can represent this knowledge by negating the formula above to yield:

\(-(A \leftrightarrow (A\ |\ B))\)

which is equivalent to:

\(A \leftrightarrow -(A\ |\ B)\)

Now, the goal we are trying to prove is that A is a knave while B is a knight, that is:

\( -A\ \&\ B\)

So, given the input:

Prover9 outputs the following proof:

Again, we were able to use Prover9 to confirm, using a proof by contradiction, the correctness of our previous solution to the puzzle.