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