The assumption a proof pays back

The rung below proved formulas by refutation: assume the negation, take it apart, and watch every branch contradict itself. Nothing in that method resembles how anybody argues, and it was chosen because it is a decision procedure and because the proof is already a picture.

Natural deduction was designed the other way round — to resemble how anybody argues — and the design is one idea.

The idea, which is one word #

To prove if $A$ then $B$, assume $A$, derive $B$, and then take the assumption back. What is left is a proof of the implication that rests on nothing.

That is called discharging an assumption, and it is the whole of what distinguishes this system. Every other rule in it is a statement about a connective that a reader would call obvious: from $A$ and $B$ conclude $A \wedge B$; from $A \wedge B$ conclude $A$; from $A \to B$ and $A$ conclude $B$. None of those needs defending. The discharge does, because it is a rule about the proof rather than about the formulas.

The bookkeeping it creates is the entire difficulty. At every point in a derivation there is a set of assumptions still open, and a conclusion is only proved outright when that set is empty. A derivation that used an assumption and forgot to withdraw it proves something conditional and looks exactly like a proof of the unconditional statement.

So the checker tracks the open set at every node, and requires it to be empty at the root. The figures would refuse a derivation that quietly leaked an assumption, which is a defect no drawing shows.

It is worth seeing what the discharge buys, because stated as bookkeeping it sounds like an inconvenience. Without it, a proof system can derive consequences and cannot derive implications: from $p$ and $p \to q$ it reaches $q$, and it has no way of turning “given $p$, one reaches $q$” into the single formula $p \to q$. Every conditional theorem would have to be stated as a rule about the system rather than as a formula in it.

The discharge is what makes the object language able to talk about its own reasoning, one step at a time, and the correspondence is exact: implication is to a derivation what the discharge is to an assumption. That equivalence has a name in the metatheory — the deduction theorem — and in an axiomatic system it is a theorem that takes work to prove. Here it is a rule, which is the whole design.

The connection to what a formula’s table settles is worth stating too. A table decides whether $p \to q$ is true under an assignment; the discharge decides whether it is derivable, from nothing. The first is about a row and the second about a proof, and the completeness theorem is the statement that the two agree.

Introduction and elimination #

Gentzen’s organising observation is that each connective gets exactly two rules — one saying how to make a formula with that connective as its main symbol, one saying how to use one.

Conjunction. To introduce: derive both halves. To eliminate: take either half.

Implication. To introduce: assume the antecedent, derive the consequent, discharge. To eliminate: modus ponens.

Disjunction. To introduce: derive either half. To eliminate: assume each half in turn, derive the same conclusion from both, and discharge both assumptions — which is proof by cases, and is the second rule with a discharge in it.

Negation. To introduce: assume $A$, derive a contradiction, discharge, and conclude $\neg A$.

The symmetry of that list is not decoration. An introduction rule says what evidence for a formula consists of, and the matching elimination rule says exactly what that evidence entitles anybody to — no more and no less. That balance is what makes the system feel like reasoning rather than like a calculus, and it is a real technical property with a name, which is the subject of the rung above.

What the shape of the drawing says #

A tableau grows downward from a single root and branches when a formula forces a choice. A natural deduction grows upward from its leaves to a single conclusion, and it branches where a rule takes several premises.

That difference is not presentational. In a tableau the branching is a case analysis about the world; in a natural deduction it is a decomposition of the argument. A tableau’s branches are possibilities, only one of which can hold; a derivation’s branches are subproofs, all of which are needed.

The leaves are the other difference. A tableau’s leaves are verdicts — closed or open. A derivation’s leaves are assumptions, and the interesting thing about a leaf is whether it has been paid back.

What the system is for, and what it is bad at #

It is what a written proof looks like, in the way a truth table is what an exhaustive check looks like and neither resembles the other. A mathematician assuming something for the sake of argument and later concluding an implication is applying implication-introduction, and every “suppose not” is a negation-introduction. The system was built to formalise that and it succeeds, which is why it is the system taught first.

It is hopeless to search, in the way an axiomatic system is and for the same reason. Nothing about a goal says which rule to apply, and the elimination rules run the wrong way: to use $A \to B$ the derivation needs $A$ from somewhere, and that somewhere is unconstrained. A search would have to guess formulas that do not appear in the goal.

That is the same difficulty the rung below named in the tableau’s favour: a tableau only ever writes down subformulas of what it started with — the subformula property — so there is a finite stock of things to try. A natural deduction has no such bound, and the rung above is about exactly which step is responsible.

And its trees are not proofs of what they look like. A derivation drawn with all its assumptions bracketed looks like a proof of the conclusion; whether it is depends on the discharges, which are annotations on the bars rather than features of the shape. The picture is a proof only together with its labels, which is a weaker claim than the rung below could make about a tableau.

Counting what a derivation costs #

The three derivations here take seven, nine and fourteen steps, and the counts are worth putting against what the same formulas cost the other systems.

The contraposition formula has two variables, so its truth table has four rows and settles the question in four evaluations. Its tableau closes in a handful of nodes. Its natural deduction takes seven steps and three discharges. All three are small and the ordering between them is not stable — on a different formula it reverses.

What is stable is the shape of the growth. A truth table costs $2^n$ rows for $n$ variables, always, whatever the formula. A tableau costs at most the number of subformulas times the number of branches, which is often far less and is $2^n$ in the worst case. A natural deduction costs whatever a person needs, and there is no bound at all, because the search space it lives in is unbounded.

That unboundedness is not only a cost. A derivation can be shorter than any tableau for the same formula, because it may introduce a helpful intermediate formula that the tableau, restricted to subformulas, cannot write down. The freedom that makes the system unsearchable is the same freedom that makes it sometimes very much shorter, and there are formulas where the gap is enormous.

So the four systems on this ladder are four points on one trade. The truth table is fixed-cost and unreadable; the tableau is searchable and restricted; natural deduction is readable and unbounded; and resolution is one rule, unreadable, and what a machine runs. No system is best and each is the answer to a different question.

Two systems, one verdict #

Every figure here is cross-checked against the truth table, as the tableau’s are, and the check is worth stating carefully because it is testing two different things at once.

The derivation is verified step by step: every node’s rule is applied to its children’s formulas and the result compared against what the node claims. That catches an invalid inference and a misapplied rule.

The conclusion is then verified semantically: the formula is evaluated over all assignments and required to be true in every one. That catches a derivation which is internally consistent and proves the wrong thing — because it was checking a different formula from the one the goal names.

Neither check subsumes the other. A derivation can be a correct application of rules to a formula nobody wanted, and a formula can be a tautology with a broken derivation attached. Both failures are silent in a drawing.

The rule that is not in the list #

There is one classical principle the four introduction-and-elimination pairs do not produce, and its absence is the sharpest thing about the system.

The list gives, for negation: assume $A$, derive a contradiction, conclude $\neg A$. What it does not give is the reverse — assume $\neg A$, derive a contradiction, conclude $A$. That is reductio ad absurdum in its classical form, and it has to be added as an extra rule because no combination of the others yields it.

The distinction looks like hair-splitting and is not. With the extra rule, $A \vee \neg A$ is a theorem and every classical tautology is derivable. Without it, $A \vee \neg A$ is not derivable, and neither is $\neg\neg A \to A$, and the system proves a strictly smaller set of formulas — the intuitionistic ones.

The difference is about what counts as evidence. An introduction rule says what evidence for a formula is, and the intuitionistic reading takes that literally: evidence for $A \vee B$ is evidence for one of them, so $A \vee \neg A$ requires deciding which, which for an undecided statement nobody has. Classical logic reads the connectives as truth functions instead, where the disjunction is true because one of the two is, whether or not anybody knows which.

What is worth registering is that the systems differ by exactly one rule and the difference was invisible until the rules were written down. Arguing about whether excluded middle is legitimate is a philosophical dispute; identifying it as the single rule whose presence or absence separates two coherent logics is what the formalism supplies, and it is the thing an informal account of reasoning cannot do.

The derivations on this page use no classical rule and are therefore theorems of both logics. That is a fact about the three formulas chosen rather than about the system — the contraposition of an implication is intuitionistically fine, and its converse is not.

Where it needs care #

A discharge withdraws every occurrence. An assumption used three times is one assumption and is discharged once, taking all three occurrences with it. The figures label each occurrence with the assumption’s name for that reason.

Discharging nothing is allowed. Implication-introduction may withdraw an assumption that was never used, giving $A \to B$ from a proof of $B$ alone. That is correct and it is where the material conditional’s oddities come from.

The negation rule as drawn is intuitionistic. From $A$ and $\neg A$ conclude $\neg C$ for the assumed $C$ — that is negation-introduction and it is uncontroversial. Concluding $C$ instead, from an assumption of $\neg C$ leading to a contradiction, is a different rule and is the classical one; the difference is the whole of what separates the two logics, and none of the derivations here needs it.

And “natural” is a claim about resemblance, not a theorem. The system was designed to look like reasoning and it does; whether it is how anybody actually reasons is a question this collection has no way of answering.

There is one more caution about the drawings specifically. A derivation tree drawn with an assumption appearing at three leaves has three leaves and one assumption, and the three are the same hypothesis used three times rather than three separate suppositions. The distinction matters because discharging withdraws all three at once, and a reader counting leaves is not counting assumptions. The figures print each occurrence’s label for that reason, and two leaves with the same label are one assumption.

Systems that track how many times an assumption is used exist and are a genuinely different logic — the substructural ones, where an assumption is a resource that is consumed. In those, using a hypothesis twice is not allowed without an explicit rule permitting it, and the resulting logics describe situations where the hypothesis is a physical thing rather than a fact. The freedom to reuse an assumption is a rule in disguise, and it is invisible here because it is never stated.

Gentzen, and a thesis with two systems in it #

Gerhard Gentzen introduced natural deduction in 1934, in the paper that also introduced the sequent calculus — two systems in one publication, and the relationship between them is the reason both exist.

He wanted a system in which formal derivations resembled informal proofs, and he built one. Then he found it awkward to prove things about, because the discharge makes an assumption’s scope a global property of the derivation rather than a local one, and metatheorems need locality. So he built a second system with the same content and a shape suited to metatheory, and proved his central theorem there.

The two systems are the same logic and the second exists because the first was the wrong shape for the argument he needed, which is a fair description of what a technical reformulation is for. The rung above is that second system and that theorem.

There is a second reason worth knowing. Gentzen’s thesis was a step in Hilbert’s programme, and its aim was a consistency proof; natural deduction was the setting he chose to make the notion of a proof concrete enough to reason about. The programme had already been damaged by Gödel four years earlier, and Gentzen’s eventual consistency proof for arithmetic uses transfinite induction — which is what remained available.

What the pictures cannot show #

A derivation is a tree with annotations, and the annotations carry the load. The bars, the rule names and the assumption labels are drawn, and the scope of each discharge — which occurrences of an assumption a given bar withdraws — is not, because it is a relation between distant parts of the tree with no place on a page.

The figures also show correct derivations only. There is no drawing here of a derivation that leaks an assumption, because such a derivation would be refused by the checker before anything was drawn, and the refusal is the point.

And nothing here shows the system’s completeness. That every tautology has such a derivation is a theorem; three derivations are three instances, and the theorem’s proof goes through a different system entirely.

The ladder from here #

Rungs above: the lemma and the proof that never mentions one, where the sequent calculus makes the metatheory tractable and the cut is shown to be removable. The quantifier that does not go away, where the same machinery stops terminating. The Curry–Howard correspondence, where a derivation is a program and a discharge is a function definition. Normalisation, which is cut elimination stated for natural deduction and says every derivation can be brought to a form with no detours. And the intuitionistic system, which is this one with the classical negation rule removed and which has a completely different set of theorems.

A rule about the proof rather than about the formulas #

The habit worth carrying is the distinction the discharge draws.

Almost every rule in a proof system is a statement about formulas: given these, conclude that. The discharge is not. It says something about the derivation so far — that an assumption made earlier is no longer needed — and its correctness cannot be checked by looking at the formulas involved.

That is why the system is easy to read and hard to search. A rule that depends only on its premises can be applied by pattern-matching; a rule that depends on the derivation’s history has to be applied by somebody who knows the history. A reader has it and a search does not.

The general shape recurs wherever a formalism has scope in it. A bound variable’s name is a fact about a term rather than about its parts; a local definition’s extent is a fact about a program rather than about its expressions. Every such construct buys expressiveness and costs locality, and the trade is the same one every time.