[Part 10] A Propositional Logic approach to Raymond Smullyan's Knights and Knaves puzzles Automating puzzle proofs with Mace4

Earlier in this series, we solved the following Knights and Knaves puzzle in a variety of ways:

A makes the following statement, "At least one of us is a knave."  

What are A and B?

First, we solved it informally.

Second, we solved it using a rather linear, direct formal proof. 

Third, we solved it using a hierarchical, natural deduction-style proof.

Fourth, we solved it using a truth table.

Fifth, we solved it using a proof by contradiction.

Sixth, in the previous post, we solved it using automated theorem proving in Prover9.

The way we used Prover9 in the previous post was to input both the statement of the puzzle and its solution. This use case would correspond to a scenario where:

1. we are able to solve the puzzle informally, but 
2. we want to check our solution formally without having to write a formal proof ourselves.

In other words, we were able to automate step 2.

But can we automate step 1 as well?

In other words, could we simply feed the puzzle statement, but not its solution, to an automated theorem prover that would then discover a provably correct solution?

The answer is yes; but Prover9 will not do for this.

Recall, from the previous post, that the app I used, namely Prover9-Mace4, is described as a "front end to the programs Prover9 (which searches for proofs) and Mace4 (which searches for finite models and counterexamples)." 

It turns out that Mace4 will allow us to automate step 2 above.

Mace4 takes, as input, a set of formulas and returns one or more models for it.

In the context of propositional logic, a model for a given set of formulas is an interpretation that makes all formulas in the set true, where an interpretation is an assignment of truth values (i.e., True or False) to all propositions in the set of formulas. 

When solving Knights and Knaves puzzles, the input to Mace4 is a set of one or more formulas that encode the puzzle statement. Mace4 will then return the truth values that all propositions in the formulas must take on to make the puzzle statement true, that is, to solve the puzzle.

And since the propositions, for us, will be \(A\), \(B\), etc., that is, the propositions that represent, "A is a knight, "B is a knight", etc., the output of Mace4 will be a solution to the puzzle!

Let's then use Mace4 to solve the puzzle above.

Here again is what the GUI for the Prover9-Mace4 app looks like:

It is the same GUI as before; but we will use it differently:

1. We will use the top-left input box (as before) to specify the input to Mace4 
2. but this time, we will leave the bottom left input box empty: note that, under our current use case, we do not yet know the solution to the puzzle; and we do not need it since we are not looking for a proof by contradiction
3. we will use the Mace4 panel in the bottom-right corner instead of the Prover9 panel in the top-right corner.

Here is the same GUI with the input formula typed in:

Before we run Mace4, we want to override one of its default options. To do this, we click on the "Mace4 Options" tab toward the top of the window...

... and set the maximum number of models to 4 (circled in red above). 

Since our puzzle statement involves exactly two propositions (\(A\) and \(B\)) and each one of them can be either True or False, the total number of distinct interpretations is equal to 4.

We are using Mace4 to find out which one(s) of these four interpretations is a (are) solution(s) to the puzzle. 

Now, if we set this option to 1, Mace4 would return the first solution it finds. But then we may miss alternative solutions (for puzzles that have more than one solution). 

If we set this option to a number larger than 4, we may make Mace4 work harder than it needs to, since there cannot possibly be more than 4 distinct solutions.

Having set this option to a reasonable value (and left the other options to their default values), we click on the "Formulas" tab to return to the main window and we launch Mace4 by clicking on the "Start" button in the bottom-right pane.

Mace4 returns an answer almost instantaneously (given the tiny size of our problem), namely:

This output lists four models, that is, four interpretations (numbered 1 through 4) that make the puzzle statement true.

Each interpretation associates (i.e., establishes a relation between) a truth value
(1 for True and 0 for False) to the propositions \(A\) and \(B\).

In the first model, we see that \(A\) is True and \(B\) is False, which is the expected solution to this puzzle. In other words, A must be a knight and B must be a knave.

Surprisingly, the last three interpretations are identical to the first one. This simply means that there is only one solution to this puzzle.

The reason for the duplication is that internally, these interpretations are represented in such a way that Mace4 cannot immediately tell that they are actually identical to each other.

In fact, they are identical to us (technically, they are isomorphic to each other). What we really want is only one such solution, called a canonical form.

To ask Mace4 to remove all isomorphic solutions and only display what we consider to be distinct solutions, we can:

1. click on the "Isofilter..." button at the top of the output window,
2. select the "Canonical Forms" algorithm in the pop-up window, and
3. click the "Start" button in this same pop-up window.

Mace4 will then output:

which is the unique solution to this puzzle.

[Part 9] A Propositional Logic approach to Raymond Smullyan's Knights and Knaves puzzles Automating puzzle proofs with Prover9

Earlier in this series, we solved the following Knights and Knaves puzzle in a variety of ways:

A makes the following statement, "At least one of us is a knave."  

What are A and B?

First, we solved it informally.

Second, we solved it using a rather linear, direct formal proof. 

Third, we solved it using a hierarchical, natural deduction-style proof.

Fourth, we solved it using a truth table.

Fifth, in the previous post, we solved it using a proof by contradiction.

In this post, we'll describe how a software program can solve this type of puzzle using automated theorem proving.

When searching for relevant tools, I came across the Prover9-Mace4 app that, according to its documentation, is a "front end to the programs Prover9 (which searches for proofs) and Mace4 (which searches for finite models and counterexamples)." 

I played a little bit with Prover9 for this post and will give a brief demo of it here. In the next post, I will turn to Mace4.

Here is what the GUI for the Prover9-Mace4 app looks like:

For this demo, I'll use Prover9 to complete a proof by contradiction of the puzzle's solution.

For this use case, I first entered the logical formula that makes up the puzzle into the top (larger) input box labeled "Assumptions:".

As discussed in previous posts, the statement of this puzzle translates to a single formula, namely:

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

which, in Prover9, can be typed up as:

A <-> (-A | -B).

Note the period that must end each formula in Prover9.

Then, I entered the logical formula that makes up the puzzle's solution into the bottom (smaller) input box labeled "Goals:".

As discussed in previous posts, the statement of this solution translates to a single formula, namely:

\( A\ \&\ {-B}\)

which, in Prover9, can be typed up as:

A & -B.

Again, note the period at the end of the formula.

Before running the theorem prover, I clicked on the "Show Current Input" button in the top-right corner of the GUI. This popped up a window containing the input that is put together into a text file made up of what I typed into the GUI and that will be fed to the command-line tool that this app is a front end for.

This window looks like this:

This automatically generated input file contains Prover9 options (e.g., limits on the running time; many other options are available) followed by the two groups of input formulas: assumptions and goals.

Everything looked good to me. So I closed this window. Then, back in the main window, I clicked on the "Start" button in the Prover9 section (the top one, above the Mace4 section).

For such a simple example, Prover9 finds a proof almost instantaneously.

Here is its output:

The numbered lines at the bottom of the output window show the proof's steps.

Since the proof is abbreviated (when compared to the level of detail that was used in the proofs of previous posts), I will go through it step by step.

The first two lines show the two input formulas, that is, the assumption and the goal.

The "non_clause" annotation on each one of these lines means that these two formulas are not in the format that Prover9 expects: they are not clauses.

A clause is a formula that has a special form: it must be a disjunction of literals, where a literal is a single proposition, optionally negated. Here is an example of a clause:

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

with three literals, two of which are negated.

As a pre-processing step, Prover9 first converts all input formulas, including assumptions and goals (the latter is first negated, as we discuss below), to clauses. This algorithm is called "clausify".

This is a general yet simple algorithm that converts any input formula \(\varphi\) in propositional logic into a conjunction of clauses that is logically equivalent to \(\varphi\).

Here is a (reconstructed) trace of this algorithm when applied to \(\varphi = A \leftrightarrow (-A\ |\ {-B})\). It simply uses a series of logical equivalences to rewrite \(\varphi\) as follows:

1.  \(A \leftrightarrow (-A\ |\ {-B})\)  [initial formula]
2.  \((A \rightarrow (-A\ |\ {-B}))\ \&\ ((-A\ |\ {-B})\ \rightarrow A)\) [a. + equivalence of a bi-conditional to a conjunction of conditionals]
3. \(A \rightarrow (-A\ |\ {-B})\) [first half of conjunction elimination on b.]
4. \((-A\ |\ {-B}) \rightarrow A\) [second half of conjunction elimination on b.]

At this point, \(\varphi\) is equivalent to the conjunction of the two formulas above (c. and d.), each one of which must be "clausified".

5. \(-A\ |\ (-A\ |\ {-B})\) [c.+ conditional to disjunction equivalence] 
6. \(-A\ |\ {-B}\) [e.+ idempotence of disjunction]

This last step works because \(-A\ |\ {-A}\) is logically equivalent to \(-A\). 

This is how Prover9 infers the clause on line 3 in the output image above, that is, as (partial) output of the clausify algorithm applied to the formula on line 1.

Now, continuing the trace of the clausify algorithm, we get:

7. \(-(-A\ |\ {-B})\ |\ A\) [d.+ conditional to disjunction equivalence] 
8. \((A\ \&\ B)\ |\ A\) [g.+ De Morgan's law + double negation elimination] 
9. \((A\ |\ A)\ \&\ (B\ |\ A)\) [h.+ distributivity of disjunction over conjunction] 
10. \(A\ |\ A\) [first half of conjunction elimination on i.] 
11. \(A\) [j.+ idempotence of disjunction]

And this is how Prover9 infers the clause on line 4 in the output image above, that is, as (partial) output of the clausify algorithm applied to the formula on line 1.

This step also marks the completion of the clausify algorithm.

Now, recall that Prover9 is searching for a proof by contradiction, which requires negating the goal formula.

So, line 5 of Prover9's output is simply the negation of the conjunction of the two clauses on line 2.  Note that the negation of the goal formula is already a clause, and therefore does not need to be clausified in this sample proof.

As the next-to-last step, Prover9 infers, on line 6,  the clause \(B\) by applying the resolution inference rule to the clauses on lines 4 and 5.

Note that Prover9 uses the phrase unit deletion here (instead of resolution) because one of the premises, namely the clause \(A\) on line 4, is a unit clause (that is, a clause made up of a single literal). This clause is combined with the premise \(-A\ |\ B\) on line 5 to cancel its literal \(-A\), yielding \(B\) on line 6.

Finally, Prover9 infers \(\$F\) on line 7, which is its symbol for \(\perp\).

Note that Prover9 uses the phrase back unit deletion here because the newly inferred formula \(B\) on line 6 is used to cancel out the \(-B\) (hence the unit deletion) in the previously inferred formula on line 3 (that is, an inference step that goes back and modifies a previously inferred formula).

This back unit deletion step yields the clause \(-A\) which, in this same step (i.e., on line 7) is cancelled out with the clause \(A\) on line 4 (another unit deletion operation) to yield the contradiction.

This last step concludes the proof, since a contradiction was inferred. 

The (non-negated) goal formula is therefore a logical consequence of the assumption. 

In other words, Prover9 has formally proved our solution to the Knights and Knaves puzzle.

In the next post, we will use Mace4 to solve this same puzzle using another application of automated theorem proving.

[Part 7] A Propositional Logic approach to Raymond Smullyan's Knights and Knaves puzzles First example - Proof by contradiction

So far in this series, we have been working on the following Knights and Knaves puzzle:

A makes the following statement, "At least one of us is a knave."  

What are A and B?

First, we solved it informally.

Second, we solved it using a rather linear, direct formal proof. 

Third, we solved it using a hierarchical, natural deduction-style proof.

In the previous post, we solved it using a truth table.

In this post, we'll write one last proof pertaining to this puzzle, namely a proof by contradiction.

A proof by contradiction is a type of indirect proof, whereas our previous formal proofs were direct ones.

In a direct proof, we assume only the premises (in our case, the puzzle statement) and use them to move forward step by step, using inference rules, until we derive the conclusion (in our case, the solution of the puzzle).

In contrast, in a proof by contradiction, we assume both the premises (in our case, the puzzle statement) and the negation of our conclusion (in our case, the negation of the puzzle's solution). From there, we move forward step by step, using inference rules, until we derive a contradiction.

In such proofs, we'll use the symbol \(\perp\) (the "falsum" or absurdity constant) as a well-formed formula that always evaluates to False. It represents the existence of a contradiction and can be derived using the following absurdity rule:

P

-P

----

\(\perp\)

In other words, if we can derive both a proposition (any proposition) and its negation, then we will have reached a contradiction, denoted by \(\perp\).

Using this new inference rule, we can build a new type of natural deduction-style proof with the following structure:

1.	...		...
2.		\(A\)	Assumption
3.		\(\vdots\)	\(\vdots\) (some reasoning, using our usual inference rules, leading to Formula 4)
4.		\(\perp\)	Formulas ?,? + Absurdity rule
5.	\(-A \)		Sub-proof 2-4 + Reductio ad absurdum

This is the structure of a proof by contradiction (or Reductio ad absurdum) whereby, if we can infer a contradiction from assuming \(A\), then A must be False, or equivalently, \(-A\) must hold.

Similarly, if we assume \(-A\) and infer \(\perp\), then we can conclude the negation of the assumption, namely \(A\).

How can we use this type of proof when working on a Knights and Knave puzzle?

Suppose that you solved the puzzle informally and found a solution \(S\), but you would like to convince yourself that you got it right. One way to do so is to formally prove that \(S\) logically follows from the puzzle statement.

We will use a proof by contradiction. First, we will assume that the puzzle statement is True (as always). Second, we will assume that the negation of the solution is true, that is, the formula \(-S\). Finally, we will try to derive a contradiction from these assumptions alone. 

If we succeed, we will be able to conclude that the negation of \(S\) cannot be true (since it leads to a contradiction in the context of the puzzle). Therefore, \(S\) indeed must logically follow from the puzzle statement and is thus its solution.

Since our informal analysis of the puzzle led us to believe that the solution is \(S = A\ \&\ {-B}\), we start our proof with:

• the puzzle statement \(A \leftrightarrow (-A\ |\ {-B})\), and
• \(-S\), that is,  \({-(A\ \&\ {-B})}\)

Here is a full proof:

Step	True formula		Justification
1.	\(A \leftrightarrow (-A\ |\ {-B})\)		Puzzle statement
2.	\(-(A\ \&\ {-B})\)		Negation of solution statement
3.	\(-A\ |\ {-{-B}}\)		Formula 2 + De Morgan's law
4.	\(-A\ |\ B\)		Formula 3 + Double negation elimination
5.	\((A \rightarrow (-A\ |\ {-B}))\ \&\  ((-A\ |\ {-B}) \rightarrow A)\)		Formula 1 + Logical equivalence #1 discussed in this post
6.	\((-A\ |\ {-B})\ \rightarrow\ A\)		Formula 5 + Simplification (or Conjunction Elimination)
7.	\(A \rightarrow\ (-A\ |\ {-B})\)		Formula 5 + Simplification (or Conjunction Elimination)
8.		\(-A\)	Assumption
9.		\(-A\ |\ {-B}\)	Formula 8 + Disjunction introduction
10.		\(A\)	Formulas 6,9 + Modus ponens
11.		\(\perp\)	Formulas 8,10 + Absurdity rule
12.	\(A\)		Sub-proof 8-11 + Reductio ad absurdum
13.	\(-A\ |\ {-B}\)		Formulas 7,12 + Modus ponens
14.	\(-A\ |\ {-A}\)		Formulas 4,13 + Resolution
15.	\(-A\)		Formula 14 + Idempotency of disjunction
16.	\(\perp\)		Formulas 12,15 + Absurdity rule

Having reached a contradiction from the puzzle statement and the assumed negation of its tentative solution, we conclude that this solution logically follows from the puzzle statement. It is therefore its correct solution.

All doubts removed!

[Part 6] A Propositional Logic approach to Raymond Smullyan's Knights and Knaves puzzles First example - Truth table approach

So far in this series, we have been working on the following Knights and Knaves puzzle:

A makes the following statement, "At least one of us is a knave."  

What are A and B?

First, we solved it informally.

Second, we solved it using a rather long, linear formal proof. 

Third, in the previous post, we solved it using a hierarchical, natural deduction-style proof.

In this post, we will solve it using the truth table approach.

A truth table is a two-dimensional representation (as a grid) of all the possible values that a logical formula can take based on the values of the propositions that it contains.

A truth table for formula \(\varphi\) contains one column for each proposition in \(\varphi\). If \(\varphi\) contains \(n\) distinct propositions, the \(n\) leftmost columns of its truth table will correspond to these \(n\) propositions, in arbitrary (usually alphabetical) order.

Each row of the table contains one possible assignment of truth values to all \(n\) propositions in \(\varphi\).

Therefore, the number of rows in a truth table is equal to the total number of distinct assignments of truth values to the propositions in \(\varphi\). 

Since each proposition has exactly two possible values (\(T\) or \(F\), for True or False, respectively), the number of distinct assignments to all \(n\) distinct propositions in a formula is equal to \(2^n\).

The rightmost column in a truth table contains the truth value of the whole formula \(\varphi\) for each assignment of truth values to the propositions in \(\varphi\).

The middle columns of a truth table correspond to sub-formulas of \(\varphi\).

With this layout, the truth table can easily be filled in from left to right, a process that we now illustrate using our Knight and Knaves puzzle.

Recall that our puzzle is represented by the following formula \(\varphi\):

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

In this case, \(\varphi\) contains \(n=2\) propositions, namely \(A\) and \(B\).

We start building our truth table for \(\varphi\) with the two leftmost columns corresponding to \(A\) and \(B\), respectively.

\(A\)	\(B\)
\(F\)	\(F\)
\(F\)	\(T\)
\(T\)	\(F\)
\(T\)	\(T\)

Note that \(n=2\) propositions give use \(2^n = 2^2 = 4\) rows, not counting the header row. 

It is common to order these rows in a systematic way. Here, I ordered them going downward by counting in binary from 0 up to 3 (i.e., 00, 01, 10, 11) while mentally mapping \(F\) to the digit 0 and \(T\) to the digit 1.

Then, since \(-A\) and \(-B\) are the next two smallest sub-formulas in \(\varphi\), we add a column for each one of these sub-formulas based on the truth table for negation:

\(A\)	\(B\)	\(-A\)	\(-B\)
\(F\)	\(F\)	\(T\)	\(T\)
\(F\)	\(T\)	\(T\)	\(F\)
\(T\)	\(F\)	\(F\)	\(T\)
\(T\)	\(T\)	\(F\)	\(F\)

Next, since \(-A\ |\ {-B}\) is the next smallest sub-formula in \(\varphi\), we add a column for it based on the truth table for disjunction:

\(A\)	\(B\)	\(-A\)	\(-B\)	\(-A\ |\ {-B}\)
\(F\)	\(F\)	\(T\)	\(T\)	\(T\)
\(F\)	\(T\)	\(T\)	\(F\)	\(T\)
\(T\)	\(F\)	\(F\)	\(T\)	\(T\)
\(T\)	\(T\)	\(F\)	\(F\)	\(F\)

Finally, the next smallest sub-formula is \(\varphi\) itself; so we add a final column for it based on the truth table for the biconditional connective:

\(A\)	\(B\)	\(-A\)	\(-B\)	\(-A\ |\ {-B}\)	\(A \leftrightarrow (-A\ |\ {-B})\)
\(F\)	\(F\)	\(T\)	\(T\)	\(T\)	\(F\)
\(F\)	\(T\)	\(T\)	\(F\)	\(T\)	\(F\)
\(T\)	\(F\)	\(F\)	\(T\)	\(T\)	\(T\)
\(T\)	\(T\)	\(F\)	\(F\)	\(F\)	\(F\)

Looking at the rightmost column in this complete table, we observe that \(\varphi\) is only True in the third row:

\(A\)	\(B\)	\(-A\)	\(-B\)	\(-A\ |\ {-B}\)	\(\varphi\)
\(F\)	\(F\)	\(T\)	\(T\)	\(T\)	\(F\)
\(F\)	\(T\)	\(T\)	\(F\)	\(T\)	\(F\)
\(T\)	\(F\)	\(F\)	\(T\)	\(T\)	\(T\)
\(T\)	\(T\)	\(F\)	\(F\)	\(F\)	\(F\)

This means that there is only one assignment of truth values to \(A\) and \(B\) that make \(\varphi\) True.

Since \(\varphi\) represents the statement of our puzzle, this means that there is only one solution to the puzzle, namely the one corresponding to the truth values of \(A\) and \(B\) in the third row.

\(A\)	\(B\)	\(-A\)	\(-B\)	\(-A\ |\ {-B}\)	\(\varphi\)
\(F\)	\(F\)	\(T\)	\(T\)	\(T\)	\(F\)
\(F\)	\(T\)	\(T\)	\(F\)	\(T\)	\(F\)
\(T\)	\(F\)	\(F\)	\(T\)	\(T\)	\(T\)
\(T\)	\(T\)	\(F\)	\(F\)	\(F\)	\(F\)

Not surprisingly, the solution yielded by the truth table approach is the same one yielded by all of our previous proofs:

A is Knight and B is a Knave.

[Part 5] A Propositional Logic approach to Raymond Smullyan's Knights and Knaves puzzles First example - A natural-deduction proof

In the previous post, we solved this Knights and Knaves puzzle:

A makes the following statement, "At least one of us is a knave."  

What are A and B?

by writing this formal proof:

Step	True formula	Justification
1.	\(A \leftrightarrow (-A\ |\ {-B})\)	Puzzle statement
2.	\((A \rightarrow (-A\ |\ {-B}))\ \&\  ((-A\ |\ {-B}) \rightarrow A)\)	Formula 1 + Logical equivalence #1 discussed in this post
3.	\((-A\ |\ {-B})\ \rightarrow\ A\)	Formula 2 + Simplification (or Conjunction Elimination)
4.	\(A \rightarrow\ (-A\ |\ {-B})\)	Formula 2 + Simplification (or Conjunction Elimination)
5.	\(-(-A\ |\ {-B})\ |\ A\)	Formula 3 + Logical equivalence #2 discussed in this post
6.	\((-{-A}\ \&\ {-{-B}})\ |\ A\)	Formula 5 + De Morgan's law
7.	\((A\ \&\ {B})\ |\ A\)	Formula 6 + Double negation elimination (applied twice)
8.	\((A\ |\ A)\ \&\ (B\ |\ A)\)	Formula 7 + Distribution of disjunction over conjunction
9.	\(A\ |\ A\)	Formula 8 + Simplification (or Conjunction Elimination)
10.	\(A\)	Formula 9 + Idempotency of disjunction
11.	\(-A\ |\ {-B}\)	Formulas 4,10 + Modus ponens
12.	\(-B\)	Formulas 10,11 + Resolution (generalization of modus ponens)
13.	\(A\ \&\ {-B}\)	Formulas 10,12 + Adjunction (or Conjunction Introduction)

But, as Peter Smith explains, there are several types of proof (or proof system) for propositional logic, including axiomatic systems and natural deduction systems.

An axiomatic system (sometimes called a Hilbert-style deductive system) uses a large number of logical axioms (typically an infinite number of them defined by axiom schemata) and a very small number of (often just one or two) inference rules. 

Note that our proof above does not follow this pattern because it uses a large number of inference rules. Also, the only axiom we use (i.e., the puzzle statement) is not a logical axiom, that is, a formula that is universally true (or true for all possible truth values of A and B).

One feature of our proof that does resemble proofs in axiomatic systems is that it is a linear sequence of formulas that has no internal structure. It does not much look like natural ways of reasoning, e.g., our informal proof in a previous post.

In contrast, natural deduction systems are intended to mimic more closely our informal ways of reasoning. They replace the use of axiom schemata with the application of many inference rules, as we did above. 

Most importantly, natural deduction systems allow us to make temporary suppositions after which we can make inferences "for the sake of argument". These are called "conditional proofs" (denoted by CP below).

For example, a natural way of proving a conditional formula \(A \rightarrow B\) is to suppose, for the sake of argument, that \(A\) is true, making \(A\) a new assumption to be used in the following steps of the proof. Now, if under this assumption, \(B\) can be proved, then we can infer that \(A \rightarrow B\) is true.

When this type of reasoning is allowed, proofs are not linear any longer. They contain (nested) subproofs that give the overall proof a hierarchical (or tree) structure. 

Since we did not use conditional subproofs for our Knights and Knaves puzzle, our proof (repeated above) is rather long and completely linear.

We will now write a natural deduction-style proof for the same puzzle.

First, how are we going to visualize the hierarchical structure of our proof? 

We will use the so-called Fitch notation. Here is an annotated example of this notation taken from page 6 of Peter Smith's write-up, (in which "MP" stands for Modus Ponens, an inference rule that we described earlier in this series):

Smith's example above proves that \(P \rightarrow Q\) and \(Q \rightarrow R\) together imply \(P \rightarrow R\).

Let's now use this approach and this notation to formalize our informal proof by cases presented in this post.

In the first case of that informal proof, we assumed that A was a knave and concluded that this case was impossible. 

Here is a possible, natural deduction-style proof of this reasoning (in which the symbol \(\bot\) denotes "contradiction"):

1.	\(A \leftrightarrow (-A\ |\ {-B})\)		Puzzle statement
2.		\(-A\)	Assumption (Case 1)
3.		\(-A\ |\ {-B}\)	Formula 2 + Disjunction introduction
4.		\(A\)	Formulas 1,3 + Biconditional elimination
5.		\(\perp\)	Formulas 2,4 + Law of non-contradiction
6.	\(-A \rightarrow\, \perp\)		Sub-proof 2-5 + CP

In other words, assuming that A is a knave leads to a contradiction, once we accept the statement of the puzzle as true.

Similarly, we can formalize our reasoning for Case 2 of our informal proof with a natural deduction-style proof like the one below. 

In that case, we assumed that A is a knight and inferred that B must be a knave.

1.	\(A \leftrightarrow (-A\ |\ {-B})\)		Puzzle statement
2.		\(A\)	Assumption (Case 2)
3.		\(-A\ |\ {-B}\)	Formulas 1,2 + Biconditional elimination
4.		\(-B\)	Formulas 2,3 + Resolution
5.	\(A \rightarrow\, {-B}\)		Sub-proof 2-4 + CP

Now, combining both cases, we get:

1. \(-A\) does not hold [Case 1 showed that \(-A\) being true leads to a contradiction]
2. either \(A\) or \(-A\) must hold [law of excluded middle]
3. \(A\) must hold [combining 1. and 2. above] 
4. \(A \rightarrow\, {-B}\) [Case 2]
5. \(-B\) [modus ponens applied to 3. and 4. above]
6. \(A\ \&\ {-B}\) [conjunction introduction applied to 3. and 5. above]

This concludes our natural deduction-style proof by cases of the solution to our first puzzle. Again, the only possible solution is that A must be a knight and B must be a knave.

[Part 4] A Propositional Logic approach to Raymond Smullyan's Knights and Knaves puzzles First example - Formal proof

In the previous post, we gave an informal derivation of the solution for the following puzzle:

A makes the following statement, "At least one of us is a knave."  

What are A and B?

In this post, we will present a formal proof of this solution.

First, we must represent this puzzle statement in propositional logic. Applying our representation principle from Part 2 of this series, we represent the first line of this puzzle with the following logical formula:

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

Second, using this formula as our only premise, we must derive one of the following formulas that represent all possible answers to the second line (i.e., the question) in the puzzle:

1. \(A\ \&\ B\)
2. \(-A\ \&\ B\)
3. \(A\ \&\ {-B}\)
4. \(-A\ \&\ {-B}\)

Actually, having already solved the puzzle informally in the previous post, we know that the solution is the third formula above.

Therefore we must build a formal proof of: 

\(A\ \&\ {-B}\) 

assuming only:

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

But what is a formal proof?

It is a sequence of true formulas with the following properties:

1. Each formula in the proof can be true because it is an axiom or an assumption whose truth can be taken for granted with no further justification.
2. Each formula in the proof can be true because it logically follows from one or more formulas that have been proved (or assumed) to be true earlier in the proof.
3. The last formula of the sequence is the one that the proof is meant to establish as a true statement given the agreed upon axioms/assumptions.

In the Knights and Knaves puzzles, the assumptions (part 1 above) will be all of the formulas that make up the statement of the puzzle, that is, all of the facts that are considered to be true if one takes the puzzle statement for granted.

In contrast, the formula to be proved (part 3 above) will be the answer to the puzzle.

Finally, intermediate or inferred formulas (part 2 above) are obtained by applying rules of inference.

A rule of inference is often represented like this:

Premise #1

Premise #2

...

Premise #n

-----------

Conclusion

A rule of inference is a logical step that allows one to infer that a new formula (the conclusion shown below the line) is true based on the truth of one or more premises (previously established true formulas shown above the line). 

For example, modus ponens is the following inference rule:

\(P \rightarrow Q\)

\(P\)

------

\(Q\)

This is a sound inference rule because the conclusion is necessarily true whenever the two premises are true.

There exist many other sound inference rules, some of which we use in the following proof of the solution to our Knights and Knaves puzzle.

Step	True formula	Justification
1.	\(A \leftrightarrow (-A\ |\ {-B})\)	Puzzle statement
2.	\((A \rightarrow (-A\ |\ {-B}))\ \&\  ((-A\ |\ {-B}) \rightarrow A)\)	Formula 1 + Logical equivalence #1 discussed in this post
3.	\((-A\ |\ {-B})\ \rightarrow\ A\)	Formula 2 + Simplification (or Conjunction Elimination)
4.	\(A \rightarrow\ (-A\ |\ {-B})\)	Formula 2 + Simplification (or Conjunction Elimination)
5.	\(-(-A\ |\ {-B})\ |\ A\)	Formula 3 + Logical equivalence #2 discussed in this post
6.	\((-{-A}\ \&\ {-{-B}})\ |\ A\)	Formula 5 + De Morgan's law
7.	\((A\ \&\ {B})\ |\ A\)	Formula 6 + Double negation elimination (applied twice)
8.	\((A\ |\ A)\ \&\ (B\ |\ A)\)	Formula 7 + Distribution of disjunction over conjunction
9.	\(A\ |\ A\)	Formula 8 + Simplification (or Conjunction Elimination)
10.	\(A\)	Formula 9 + Idempotency of disjunction

Let 's take a short breath to rejoice at the fact that we have just proved half of the puzzle's solution, namely the fact that A is a knight!

Luckily, the second half of the solution will be much quicker to prove.

Step	True formula	Justification
11.	\(-A\ |\ {-B}\)	Formulas 4,10 + Modus ponens
12.	\(-B\)	Formulas 10,11 + Resolution (generalization of modus ponens)
13.	\(A\ \&\ {-B}\)	Formulas 10,12 + Adjunction (or Conjunction Introduction)

Which concludes our proof that A must be a knight and B must be a knave!