Proving Instead of Checking
Truth tables decide everything and scale terribly. Natural deduction takes the other route: instead of surveying all assignments, it derives the conclusion from the premises by applying rules, one step at a time. Each step is justified by a rule and by the earlier lines it uses, so a proof is a checkable object rather than a survey.
The rules come in pairs. For each connective there is an introduction rule saying how to derive a sentence with that connective as its main operator, and an elimination rule saying what may be derived from one.
| Connective | Introduction | Elimination |
|---|---|---|
| From and , infer | From , infer (or ) | |
| From , infer | From and both cases giving , infer | |
| Assume , derive , conclude | From and , infer | |
| Assume , derive a contradiction, conclude | From , infer |
Conditional elimination is modus ponens under a formal name. Conjunction rules are trivial. The two that carry real weight are conditional introduction and negation introduction, because both work by making an assumption.
An assumption is a temporary supposition, opened for the sake of argument and later discharged. Its scope is marked by a subproof, and the crucial discipline is that nothing inside a subproof may be used after the assumption is discharged, the conclusion depends on the assumption, so it cannot escape its scope. Violating this is the commonest way to produce a proof of something false.
Conditional introduction is the formal counterpart of ordinary conditional reasoning: to establish "if P then Q", suppose P and get to Q. Negation introduction is reductio ad absurdum: to establish "not P", suppose P and derive a contradiction.
Natural deduction and truth tables agree exactly. The system is sound, everything provable is valid, and complete: everything valid is provable. Neither property is obvious, and both had to be proved.
Common pitfall: using a line from inside a closed subproof. Once an assumption is discharged, everything derived under it is off limits, those lines were only ever conditional on a supposition you have now withdrawn. This single restriction is what keeps the system sound.