Cut Elimination and the Subformula Property

The cut rule is the only rule in the sequent calculus that mentions a formula not appearing in its conclusion. Everything else decomposes what is already there. Cut takes a derivation of Γ ⊢ A, Δ, a derivation of Γ, A ⊢ Δ, and produces a derivation of Γ ⊢ Δ, discarding A along the way. It is how a proof uses a lemma, and it is what makes proofs short. Gentzen’s theorem says it can always be removed. The consequence is a normal form whose contents are bounded by the goal, and the cost of reaching it is where the interesting behaviour lives.

What a cut-free derivation looks like

A derivation is cut-free when no step is a cut. In such a derivation every formula occurring in it is a subformula of some formula in the end sequent, where subformula is defined as: A is a subformula of A; if A is a subformula of B then A is a subformula of B ∧ C, B ∨ C, B → C, ¬B, ∀x. B, ∃x. B; and the relation is transitive.

The proof of the property is a one-line induction. The identity rule introduces only formulas already present. Every other rule introduces a formula whose immediate subformulas are in its premises, so by induction everything in the derivation is a subformula of the end sequent. Cut is the only rule whose premises contain a formula absent from the conclusion, and eliminating cut removes the exception.

For a fixed end sequent there are finitely many subformulas, since the formula is a finite tree. The same subformula discipline governs the rule-level analysis in The Sequent Calculus and Why Its Rules Are Invertible, where invertibility decides which rules a search may apply without losing completeness. A backward search that only applies cut-free rules therefore examines a finite space, and in propositional logic that space is bounded by a function of the size of the goal. The bound is not tight and the search is still exponential in the worst case, but it is finite and does not depend on the ingenuity of the prover.

This is the property that makes automated proof search possible at all. Without it, a prover could always try to prove a useful lemma first, and the space of candidate lemmas is unbounded.

How the elimination works

The procedure is an induction on the structure of the derivation, with the cut formula as a secondary measure. There are two kinds of case.

Cut formula is not introduced by the last step of either premise. The cut is pushed upward past the surrounding rule, so the cut acts on a smaller subderivation. If the left premise ends in a rule that does not introduce the cut formula, and the right premise does not either, commute the cut above that rule: the cut formula is unchanged, and the derivation above the cut shrinks. If the right premise introduces the cut formula while the left does not, the cut commutes upward into the left premise, where it acts on the same formula and again on a smaller subderivation.

Cut formula is introduced on both sides. This is the principal case. The left premise ends with a right rule introducing the cut formula, and the right premise ends with the corresponding left rule. For implication and the cut formula A → B, the left premise ends in →R, deriving Γ ⊢ A → B, Δ from Γ, A ⊢ B, Δ; the right premise ends in →L with premises Γ ⊢ A, Δ and Γ, B ⊢ Δ. The cut on A → B is replaced by two cuts: one on A between the derivation of Γ, A ⊢ B, Δ and the derivation of Γ ⊢ A, Δ, and one on B between the derivation of Γ, B ⊢ Δ and the result of the first.

The new cuts are on strict subformulas of the original cut formula. This is the measure that decreases: the cut formula gets smaller even though the derivation may grow. The induction is therefore lexicographic, first on the cut formula’s size and then on the derivation’s height, and it terminates because formulas are finite trees.

For the quantifier rules the principal case introduces a term, and the commutation requires substituting that term into the other premise. The substitution can duplicate the term, which is why cut elimination for first-order logic is more delicate than for propositional logic. It also is where the eigenvariable conditions earn their keep: the variable in a ∀R or ∃L step must not occur free in the context, or the substitution would capture it.

The price, measured in proof length

Cut elimination is effective, and it is not efficient. The transformation can turn a short proof into an enormous one, and the growth is not a constant factor.

The standard example is the propositional formula whose cut-free derivations are all exponential in the length of the formula, while a derivation with one cut in the middle is linear. A cut lets a lemma name a subformula once, and the cut-free derivation has to reintroduce that subformula wherever the lemma was used; when the uses are nested, the reintroduction multiplies. This is not an artefact of a clumsy procedure. Every cut-free derivation of such a formula is exponentially long, because the subformula property fixes exactly which formulas may appear, and the only freedom left is how often each one is repeated.

The growth can be worse than exponential. In systems with induction schemata, cut elimination corresponds to the elimination of general lemmas, and the resulting proofs can be non-elementary: the length grows faster than any fixed tower of exponentials. The theorem still holds, so the cut-free proof exists, and the bound is a statement about the difficulty of finding it rather than about its existence.

The practical reading is that cut elimination is a normalisation theorem, not a compilation strategy. A prover that eliminates cut from a large derivation will produce a term too big to store. What implementations do instead is search directly for cut-free derivations, using the subformula property as a search bound rather than as a post-processing step.

What the theorem proves

Cut elimination is the engine behind most of the metatheory of a logic, and the derivations are short.

Consistency. If the empty sequent ⊢ were derivable, it would have a cut-free derivation. In a system that absorbs weakening and contraction into the logical rules, the last step of such a derivation has an empty right side and a possibly non-empty left side, and no logical rule has that shape: a right rule puts the formula it introduces on the right, and the identity rule puts the same formula on both sides. A derivation whose last step is a weakening from Γ ⊢ inherits the same problem at the step above. So no cut-free derivation of the empty sequent exists, and since cut elimination preserves derivability, none exists at all. The argument works for any logic whose rules satisfy the subformula property, and it does not depend on a model.

The disjunction property. If ⊢ A ∨ B is derivable, take a cut-free derivation. Its last step cannot be anything but ∨R, since the other rules would leave a connective undecomposed or a formula in the context, so either ⊢ A or ⊢ B is derivable. The witness is in the derivation.

Interpolation. Craig’s interpolation theorem for first-order logic can be proved by induction over cut-free derivations, splitting each rule into the part that belongs to the left formula and the part that belongs to the right. The proof requires cut-free derivations precisely because a cut would introduce a formula standing between the two sides, with no derivation above it to attribute it to. The resulting interpolant mentions only the vocabulary shared by the two sides.

Each of these is a syntactic result. None requires a semantics, a model, or a translation, and each survives when the logic is extended in ways that make semantics harder to come by.

Where the property fails or thins out

The subformula property is a property of the particular formulation, not of the logic. Change the presentation and it can disappear.

Classical logic in the one-sided sequent calculus has the property. Add an induction schema, as in Peano arithmetic, and it fails: the induction step introduces the induction formula at a substitution instance, so an instance of a formula already in the derivation can bring in formulas that are not subformulas of anything in the end sequent. Arithmetic admits cut elimination, but the cut-free derivations still contain such instances, because the induction rule generates them.

Second-order logic is worse. Cut elimination holds for the second-order sequent calculus, and the cut-free derivations can be enormous. Consistency of first-order arithmetic follows from consistency of the second-order calculus together with a faithful encoding of arithmetic’s axioms and inference rules, so the encoding, not cut elimination on its own, is what carries the proof.

Modal and substructural logics each have their own behaviour. In linear logic, cut elimination holds and the subformula property holds in the expected form, but the exponential modalities introduce their own contraction-like steps, and the complexity of cut-free search is correspondingly higher. In provability logic, the natural sequent presentation needs rules for the modality of a kind that the standard cut-elimination argument does not handle directly, and the system has to be reformulated, for instance with labels or hypersequents, before cut elimination can be established.

Why the theorem still matters for implementations

The practical consequence of cut elimination is a design principle for proof search: a complete search that never applies cut will find a proof if one exists, so a prover can omit cut and lose nothing in completeness. Every resolution prover, every tableau prover, and every backward search in a sequent calculus relies on this. The omitted rule is the one that would make the search unbounded.

The second consequence is a design principle for proof terms. In the typed reading, a cut corresponds to a let-binding or to the substitution of a term for a variable. Cut elimination corresponds to the elimination of these intermediate definitions, and the size blow-up is the same phenomenon as the loss of sharing when a program is inlined. This is why compilers keep let-bindings and why proof terms with explicit sharing are preferred over fully substituted ones; the normal form is canonical but not compact.

A third consequence concerns proof identity. Two derivations of the same sequent are considered the same proof when they have the same cut-free normal form, up to the order of independent commutations. This is a definition, not a theorem, and it is the definition that makes proof equivalence decidable in many propositional systems. It is the starting point for the treatment of equality in Definitional and Propositional Equality.