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