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