A lemma, and the proof that never mentions one

Ordinary mathematics is written with lemmas. Prove something useful, then use it, and the proof of the theorem is short because the hard part happened elsewhere — which is how every ladder on this site is organised, including this one. Formalised, that move is a single rule — from $\vdash L$ and $L \vdash F$ conclude $\vdash F$ — and it is called the cut.

The cut is what makes proofs readable and it is the only rule in the system that a search cannot handle, for one reason: $L$ can be anything.

Gentzen proved in 1934 that the cut can always be eliminated: any proof using lemmas can be rewritten as one that never leaves the goal’s own vocabulary. That theorem is the reason a proof system can be searched at all, and the rewriting is not cheap.

What the subformula property is #

A proof has the subformula property when every formula appearing anywhere in it is a subformula of the conclusion, or the negation of one.

The rung below noted that a tableau has it automatically, since every rule takes a formula apart and none assembles anything. The figures here check it rather than asserting it: the goal’s subformulas are collected, every formula appearing in the cut-free proof is looked up, and none is outside.

The property is worth exactly one thing and it is the thing that matters. It bounds the search. A proof of a formula with a dozen subformulas can only ever write down those dozen, signed, so the space of possible next lines is finite, and a search over a finite space terminates.

A proof with a cut has no such bound. The lemma $s \vee \neg s$ in the figure shares not one variable with the goal, and there was nothing about the goal to suggest it. The space of possible lemmas is the space of all formulas, and searching it is not a bounded problem.

The asymmetry between the two situations is worth one number. A goal with a dozen subformulas gives a cut-free search at most twenty-four signed formulas to work with, so the whole space of derivations is finite and can in principle be enumerated. A cut permits any formula in the language, and the language over a handful of variables already contains infinitely many — so the two searches are not a hard one and an easy one, they are a finite one and an infinite one.

That is the sharpest available statement of what the subformula property is worth, and it is why a system’s ability to be searched is treated as a property of the system rather than of anybody’s cleverness at searching it.

Two systems, and why there are two #

The rung below drew tableaux and the rung above it drew natural deductions. This rung’s figures compare proofs in a third notation, and the reason for a third is worth stating because it is not aesthetic.

Gentzen’s sequent calculus works with statements of the form $\Gamma \vdash \Delta$ — from these assumptions, one of these conclusions — and every rule acts on one connective in one position. That makes the system unpleasant to read and pleasant to reason about: an assumption’s scope is local, every rule’s effect on the sequent is visible, and induction on the derivation’s structure works.

Natural deduction has neither property. The discharge makes an assumption’s scope a global fact about the derivation, so an induction has to carry the whole discharge structure along, and the metatheorem that is one page in the sequent calculus is a chapter in natural deduction.

So the two systems are the same logic in two shapes, and the shapes are for two different jobs: one for writing proofs, one for proving things about proofs. Gentzen built both in the same paper for exactly that reason.

What the elimination costs #

Gentzen’s theorem is constructive: it gives a procedure that takes a proof with cuts and returns one without. The procedure works by pushing each cut upward past the rules above it until it reaches the axioms and disappears, and pushing it past a branching rule duplicates it.

That duplication is the cost, and it compounds. Each pass can square the size of the proof, and the number of passes is the depth of the cuts, so the blow-up is a tower of exponentials — a growth rate that no polynomial or exponential bound describes.

And the bound is achieved. There are families of formulas with short proofs using cuts and only enormous cut-free proofs, and the gap is not a weakness of the known elimination procedures — it is a theorem about the proofs themselves. Statman and others established it in the 1970s.

So the trade is exact and unavoidable:

• A system with cut is compact, matches how proofs are written, and cannot be searched.
• A system without cut is searchable, has the subformula property, and is sometimes hopelessly long.

What a sequent is, and why the shape helps #

The notation deserves a paragraph, because the whole advantage of the system is in it.

A sequent $A_1, \ldots, A_m \vdash B_1, \ldots, B_n$ asserts that if all of the $A$s hold then at least one of the $B$s does. Both sides are lists, and the asymmetry a reader expects — one conclusion — is absent on purpose.

Every rule then has two forms, one acting on the left of the turnstile and one on the right, and the pair says how a connective behaves as an assumption and as a goal. A conjunction on the right needs both halves proved; a conjunction on the left may be used as either half. The introduction-and-elimination pairs of natural deduction become left-and-right pairs here, and the symmetry is the thing that makes an induction over the rules manageable.

Two structural rules sit outside that scheme and they are the ones the metatheory cares about. Weakening adds a formula to either side, and contraction merges two copies into one. Together with the cut they are the rules that mention no connective at all — the rules about the bookkeeping rather than about the logic — and cut elimination is the statement that the most powerful of the three is dispensable.

That framing also explains why removing the cut is delicate. Weakening and contraction are harmless because they only shuffle formulas already present; the cut introduces a formula that is present in neither the premises’ conclusions nor the conclusion, and it is the only rule that does. A rule that mentions a formula appearing nowhere else is exactly a rule a search cannot invert, and the classification of rules by that property is the whole of what the sequent notation buys.

What every real prover does #

Nothing practical accepts either side of that trade, and the standard resolution is worth stating because it is what modern satisfiability solvers are.

A solver runs a cut-free search — it works with the clauses it was given and derives consequences of them, with no invented formulas — and then, when a branch of the search fails, it learns a clause recording why. That clause is a lemma. It was not guessed; it was extracted from a failure the search actually encountered.

So the lemmas are reintroduced, and the search chooses them rather than a person. That is clause learning, it is the single change that made satisfiability solving practical in the 1990s, and it is exactly the cut rule readmitted under a rule for when it may be applied.

The restriction is worth being precise about, because “a restricted cut” sounds like a compromise and is a definite object. The learned clause is always a resolvent of clauses already derived — one rule applied to two clauses — so it is built from material the search already has, and its variables are among the problem’s. That keeps the search space finite while allowing the derivation to record intermediate facts, and the resulting system is provably stronger than plain cut-free search on some families and no weaker on any.

The theoretical statement of the same thing is that a solver with clause learning is as strong as a proof system with a restricted cut, and strictly stronger than one without. The restriction is what makes it searchable and the readmission is what makes it fast.

The theorem’s other consequences #

Cut elimination is remembered for the searchability, and it settles several other questions immediately, which is the mark of a theorem doing structural work.

Consistency. A cut-free proof of a contradiction would have the subformula property, so every formula in it would be a subformula of the contradiction — and there is no such proof, by inspection of the finitely many possibilities. So the system is consistent, and the argument is a page rather than a programme.

The subformula property, as a corollary about the whole system. Every provable formula has a proof mentioning nothing outside its own vocabulary. That is not obvious and it is false for systems that fail to admit elimination.

Interpolation. If $A \to B$ is provable, there is a formula $C$ in the vocabulary shared by $A$ and $B$ with $A \to C$ and $C \to B$ both provable. Craig proved that in 1957 and the standard proof reads $C$ off a cut-free derivation, where it can be constructed because everything appearing is a subformula.

And decidability. For propositional logic, cut-free proof search terminates, which is a decision procedure — the same one the rung below drew as a tableau, since a closed tableau is a cut-free sequent proof turned upside down.

That last correspondence is exact enough to be worth spelling out, since it explains why this ladder has drawn the same object three times. A tableau branch is a set of formulas assumed jointly satisfiable; a sequent is a set of formulas assumed to entail one of another set. Negate everything on the right of the turnstile and move it left, and a sequent becomes a set to be refuted — which is a tableau branch. Closing a branch is deriving an axiom; branching is a rule; and the two trees are the same tree with the arrows reversed.

So the readable system, the searchable system and the metatheoretical system are three notations for one thing, and which to use depends entirely on whether the goal is to write a proof, to find one, or to prove something about proofs.

Where the account needs care #

The figures compare sizes and not lower bounds. The cut proof here is smaller than the cut-free one on these formulas, which is an instance; that there exist families where the gap is a tower of exponentials is a theorem quoted rather than exhibited, and no small example could exhibit it.

The lemma has to be a theorem. A cut on a formula that is not provable proves nothing, and the figure checks that its lemma is itself derivable before using it. That check is what makes the “proof with a cut” a proof.

The theorem is about the sequent calculus. Its natural-deduction counterpart is normalisation — every derivation reduces to one with no detours, where a detour is an introduction immediately followed by the matching elimination. The two theorems are the same fact and their statements look nothing alike.

And elimination fails in some extensions. Adding rules to the calculus can break the theorem, and whether a proposed system admits elimination is the first question asked of it. A system that does not is generally not worth having, which is a strong statement about how central the property is.

The most important instance is worth naming. Adding the axioms of arithmetic as extra rules gives a system in which cut elimination fails outright — and it must, since a system with the subformula property for arithmetic would be a decision procedure for arithmetic, which Gödel’s argument forbids. What survives instead is a partial elimination: cuts on formulas from the theory’s own axioms remain, and cuts on everything else go. The measure of how much survives is exactly the ordinal Gentzen’s consistency proof needs, which is the link between this rung’s theorem and the boundary the previous section describes.

Gentzen, and a theorem in the middle of a programme #

Gentzen proved the Hauptsatz — the main theorem — in 1934, as a graduate student, and the name he gave it says what he thought it was for.

The setting was Hilbert’s programme: prove the consistency of mathematics by finitary means. Gödel had shown in 1931 that no such proof can be given inside the system, which closed the programme’s original form and did not close the question of what could be proved and with what.

Cut elimination for propositional and first-order logic is a finitary result, and it gives consistency for those systems by the argument above. For arithmetic, Gentzen’s consistency proof of 1936 needs more: an induction along the ordinals up to $\varepsilon_0$, which is not finitary and is the exact amount of extra strength Gödel’s theorem says is required. A sequence that explodes and still stops is that same ordinal doing that same job in a different setting, and the sentence that says it has no proof is Gödel’s half of the boundary.

So the theorem sits precisely at the boundary Gödel had drawn, and what makes it valuable is that it says how much is needed rather than that something is impossible. Gentzen died in 1945, aged thirty-five.

What the pictures cannot show #

The figure is a table of sizes rather than two drawn derivations, and the reason is that a cut-free derivation of a modest formula has a dozen nodes and a comparison of two such drawings would show two similar trees. The property that separates them is not visible in either — it is a statement about which formulas appear, which is checked and reported rather than drawn.

Nothing here shows the elimination procedure. Pushing a cut upward and watching it duplicate is a rewriting of a tree, and a picture of it would be a sequence of trees with no single frame carrying the point.

And the tower-of-exponentials gap is unrepresentable. The formulas exhibiting it have proofs whose cut-free versions have more steps than there are atoms in anything, and the figures use formulas small enough to check.

The ladder from here #

Rungs above: the quantifier that does not go away, where the same machinery stops terminating and the decision procedure becomes a semi-decision procedure. The Curry–Howard correspondence, where a cut is a function application and cut elimination is running a program. Proof complexity, which measures how large a proof must be in a given system and where the pigeonhole principle is the standing example. Craig interpolation and its uses in verification, where the interpolant extracted from a cut-free proof is what a model checker abstracts with. And ordinal analysis, which measures a theory’s strength by the ordinal its consistency proof needs.

The step that is both the point and the problem #

The habit is about what to do with a feature that is simultaneously a system’s strength and its defect.

The cut is not a flaw to be removed. It is what a lemma is, it is why mathematics is organised into theorems rather than into one enormous derivation, and a system without it is a system in which nothing can be reused. Eliminating it is a theorem about what is possible in principle and not a recommendation about how to write anything.

What the theorem buys is knowing that the two things are separable: the expressiveness the cut provides and the searchability its absence provides are both available, on the same logic, in two presentations. Neither has to be given up permanently, and the choice can be made per task.

That is the general shape worth carrying: when a feature is both indispensable and obstructive, the useful theorem is the one saying it can be removed rather than the one saying it should be. The removal is then a tool — used in a metatheorem, used in a decision procedure, and not used when writing a proof for a reader.