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