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