Natural Deduction

Syntactic consequence was defined three articles ago as the existence of a derivation, and the definition referred to the axioms and rules of a system without naming any. That gap has been left open ever since. This article closes it by setting out a system in full, and it starts with the more general question of what a system has to supply.

What has to be specified

Two constraints govern the choice and neither is severe. The rules must be checkable: whether a given line follows by a given rule has to be settleable by inspecting the shapes of the formulas involved, with no appeal to what they mean. And the system should be sound, since one that licensed a step from truths to a falsehood would be useless. Beyond that a great deal is open, and systems that look nothing alike can prove exactly the same formulas.

The checkability requirement has a consequence worth naming, because it is the source of the asymmetry noted three articles ago. Since every rule is a condition on shapes, verifying that a completed proof is a proof is a mechanical matter: read the lines in order, and for each one confirm that it is a premise, an axiom, or the result of a rule applied to earlier lines. That procedure always terminates. Finding a proof is a different matter entirely, because there is no bound on how long the proof might be, and nothing in the specification of a system suggests a search strategy. A system can therefore be perfectly precise and still leave one with no idea how to use it.

Systems tend to fall along a spectrum according to how they divide labour between axioms and rules. At one end sit the systems with many axioms and almost no rules; at the other, systems with no axioms at all and a rule for every move. The system in this article is at the second extreme, and the article on axiomatic systems takes up the first.

Reasoning the way people reason

The design was published twice within a year by people who did not know of each other's work. Stanisław Jaśkowski gave a system of suppositions in "On the Rules of Suppositions in Formal Logic" in 1934, and Gerhard Gentzen gave another in the two-part "Untersuchungen über das logische Schließen" in the Mathematische Zeitschrift in 1935. Gentzen's paper is the one usually cited, partly because the second part of it introduces the sequent calculus and proves the result that made his name.

What both were reacting against is worth stating, since it explains the shape of what follows. An axiomatic system proves things by producing tautologies and detaching consequences from them, and a derivation in such a system typically opens with two or three long formulas that come out of nowhere and are justified only by turning out to be useful ten lines later. Nothing in an ordinary mathematical proof looks like that. What ordinary proofs do is suppose something, work under the supposition, and then draw a conclusion that no longer depends on it. A system built to model that will need machinery for supposing and for un-supposing, and that machinery is the substance of natural deduction.

Two rules for each connective

The pairing is the organising principle of the whole system. Each connective gets exactly two rules, one for putting it in and one for taking it out, and the two are meant to fit: whatever the introduction rule demands for asserting a compound is exactly what the elimination rule allows one to recover from it.

Conjunction is the clearest case. To introduce a conjunction, have both conjuncts on separate lines and write their conjunction. To eliminate one, have the conjunction and write either conjunct. Nothing is gained and nothing is lost, which is the fit in its simplest form.

The conditional's elimination rule is already familiar. From a conditional and its antecedent, write its consequent. That is modus ponens under a new name, and the renaming is not pedantry: in this system it is one of a matched pair rather than a rule standing on its own, and its partner is the more interesting of the two.

Disjunction runs the other way round. Introduction is trivial, since from any formula one may write its disjunction with anything whatever. Elimination is the demanding one, because a disjunction says very little: knowing that one of two things holds licenses a conclusion only if the conclusion follows from each of them separately. That rule is proof by cases, and stating it properly requires the machinery of the next section.

The biconditional's rules are the two conditionals taken together, which is why some presentations drop the connective and treat it as an abbreviation. Negation is the awkward one, and it is treated below.

Supposing and un-supposing

The bookkeeping is what the vertical bars and indentation in the proofs below are for. A line at indentation depth one is inside a subproof; a line at depth zero is not. The rule governing citation is simple and absolute: a line may be cited only from a depth at or below its own, and only if every subproof it sits inside is still open.

That restriction is the whole safety mechanism, and it is easy to see what happens without it. Assume $P$. Derive $P$ from the assumption, trivially. If the assumption could be discharged while the line derived from it stayed citable, $P$ would have been proved from nothing at all, and every formula would be a theorem. The scoping is not a notational nicety; it is the difference between a system and a disaster.

Conditional proof

Here is the rule at work, deriving the transitivity of the conditional.

Read it as an argument in English and it is entirely ordinary. Suppose $P$. Then $Q$, by the first premise. Then $R$, by the second. So if $P$ then $R$, and the supposition has been dropped. That correspondence is the case for calling the system natural.

Two details in the notation repay attention. The justification at line 6 cites a range of lines rather than particular lines, because the rule appeals to the shape of the whole subproof and not to any one formula in it. And the conclusion sits at depth zero, outside the subproof, which is what records that it does not depend on the assumption. Lines 3 through 5 depend on $P$; line 6 does not.

Reductio

Negation is handled this way because there is nothing simpler available. A conjunction can be built from its conjuncts and a conditional can be built by conditional proof, but a negation cannot be built out of anything positive. The only route to it is to show that the unnegated formula cannot be sustained.

The rule of modus tollens, which the beginner tier listed alongside modus ponens as a basic form, turns out not to be basic here. It is a six-line derivation from rules that do not mention it. That is characteristic of the system: a small stock of rules generates the familiar patterns as results, and the familiar patterns can then be used as shorthand once derived.

Line 2 being cited from inside the subproof is worth pausing on. It sits at depth zero, outside, and the citation rule permits looking outward. Premises and anything established at an outer level remain available inside every subproof opened beneath them. What is forbidden is the reverse: looking into a subproof from outside, or into a subproof that has closed.

Proof by cases

Disjunction elimination can now be stated properly. Given a disjunction, and given a subproof deriving some formula from the first disjunct, and another deriving the same formula from the second, the formula may be written at the outer level.

Two assumptions are made and both are discharged by the single application at line 8. The rule is the formal counterpart of an argument that says: either way, the same thing follows. Its shape also explains why disjunction is the connective beginners find hardest to use. Introducing one is free and gains nothing; getting anything out of one costs two subproofs.

Nesting

Subproofs can sit inside subproofs, and the depth is unbounded. Proving a formula of the form of a conditional whose consequent is itself a conditional requires two nested assumptions, the inner one discharged first and the outer one after; the indentation in the display then runs two levels deep, and the citation rule applies at every level in the same way. A line at depth two may cite lines at depth two, one, and zero, provided all the subproofs containing them are still open, and may not be cited from anywhere shallower once its own subproof has closed.

Nothing new has to be said about this case, which is a point in the system's favour. The rules were stated once, in terms of a subproof and the level containing it, and they apply unchanged however deeply the structure is stacked.

Finding a proof

The rules say what is permitted. They say nothing about what to do, and a beginner facing a blank page with three premises and a conclusion is entitled to feel that something has been withheld.

The gap is real and cannot be closed by any rule of the system, but the shape of the rules does supply a strategy, and it is the same one every textbook teaches. Work backwards from the conclusion rather than forwards from the premises. If the conclusion is a conditional, the last line of the proof will almost certainly be a conditional introduction, so assume its antecedent and set the consequent as the new target. If the conclusion is a conjunction, prove the two conjuncts separately. If it is a negation, assume the unnegated formula and look for a contradiction. If it is an atomic formula, or if nothing else suggests itself, assume its negation and try for a contradiction, since reductio is the rule of last resort and very often works.

Only then look at the premises, and take apart what can be taken apart: break conjunctions into their conjuncts, apply conditional elimination wherever an antecedent is available, and see whether what accumulates meets the target coming the other way. Most proofs at this level are built from both ends and joined in the middle.

None of that is a decision procedure and none of it is guaranteed to terminate. It is a heuristic, and the next article's method is the contrast that shows what a genuine procedure looks like.

The classical extra

One rule remains and it does not fit the pattern.

Double negation elimination takes $\neg \neg \varphi$ to $\varphi$. In a system of matched pairs it is an oddity: negation already has its introduction rule and an elimination rule of its own, and this is a third. The related rule of classical reductio, which assumes $\neg \varphi$, derives a contradiction, and concludes $\varphi$, is equally awkward for the same reason.

The awkwardness is not an accident of presentation. Removing that rule and keeping everything else yields intuitionistic logic, a system in which the law of excluded middle is not provable and a great deal else changes. That the classical system needs one rule that spoils the symmetry, and that the symmetric fragment is a coherent logic in its own right, is a discovery rather than a design flaw, and the article on intuitionistic logic takes it up in full.

Next

The system just given is convenient for constructing proofs and inconvenient for a particular purpose: it offers no help at all when an argument is invalid. There is no point at which the search for a proof reports failure rather than simply continuing. The next article gives a method with the opposite character, one that either produces a proof or produces a countermodel, and which terminates either way.