Math 2.0

Mathematical logic and foundations Proof theory Theorem

Cut-elimination theorem

Builds on Sequent calculusSequent calculusProof theory

Statement

Let Γ⊢Δ\Gamma \vdash \Delta be a sequent of first-order logic. If Γ⊢Δ\Gamma \vdash \Delta has a derivation in the sequent calculus LK, then it has a derivation in LK that does not use the cut rule. The same holds for the intuitionistic calculus LJ.

Remarks

Gentzen proved the theorem in 1934, and called it the Hauptsatz. The proof is a double induction. The outer induction is on the complexity of the cut formula, and the inner one is on the heights of the derivations above the cut. Each step pushes a topmost cut upward or replaces it by cuts on smaller formulas. The cost is large: removing cuts can make a derivation super-exponentially longer.

In a cut-free derivation, every formula is a subformula of a formula in the final sequent, up to the substitution of terms for variables. This subformula property gives quick consequences. For example, the empty sequent ⊢\vdash has no cut-free derivation, since no rule other than cut can produce it. So LK is consistent.

Going deeper

For a student

Cut elimination is the central result of structural proof theory. It gives the subformula property, the consistency of pure logic, and Craig interpolation and Herbrand's theorem by short arguments. For arithmetic, cuts cannot be fully removed in the presence of induction. Gentzen's consistency proof for Peano arithmetic instead removes cuts partly, with a transfinite induction up to the ordinal ε0\varepsilon_0 to show that the process ends. Through the Curry–Howard correspondence, the removal of cuts is related to the evaluation of programs.

Reading path

To understand this page from the ground up, read these 16 pages in order. The foundations come first.

Show the path as a graph
Proposition, concept, no evidence levelPropositionconceptConjunction, definition, no evidence levelConjunctiondefinitionDisjunction, definition, no evidence levelDisjunctiondefinitionImplication, definition, no evidence levelImplicationdefinitionNegation, definition, no evidence levelNegationdefinitionPredicate, definition, no evidence levelPredicatedefinitionBiconditional, definition, no evidence levelBiconditionaldefinitionLaw of excluded middle, statement, no evidence levelLaw of excluded middlestatementModus ponens, concept, no evidence levelModus ponensconceptPropositional logic, concept, no evidence levelPropositional logicconceptMathematical proof, concept, no evidence levelMathematical proofconceptPredicate logic, concept, no evidence levelPredicate logicconceptProof theory, concept, no evidence levelProof theoryconceptSequent calculus, definition, no evidence levelSequent calculusdefinitionSequent calculus, concept, no evidence levelSequent calculusconceptCut-elimination theorem, statement, no evidence levelCut-elimination theor…statement
Each page uses the pages above it. The colour of the bar on a box shows how strong the evidence is, and the box also gives it as text. The list has the same pages.
  • no evidence level
  1. Proposition concept
  2. Conjunction definition
  3. Disjunction definition
  4. Implication definition
  5. Negation definition
  6. Predicate definition
  7. Biconditional definition
  8. Law of excluded middle statement
  9. Modus ponens concept
  10. Propositional logic concept
  11. Mathematical proof concept
  12. Predicate logic concept
  13. Proof theory concept
  14. Sequent calculus definition
  15. Sequent calculus concept
  16. Cut-elimination theorem statement

Further reading

  1. Web https://en.wikipedia.org/wiki/Cut-elimination_theorem
About this page
TagAYRZ98Y0NW
URIm2://AYRZ98Y0NW
Kindstatement, theorem
WritingW0 stub
MSC03F05
StatusThis copy of the site has no build data. Run m2 status AYRZ98Y0NW.
AboutSequent calculus
UsesSequent calculus, Sequent calculus, Proof theory
Same as
Changed2 November 2026

Markdown · JSON · Edit on GitHub

What this page needs for W1

  • a source with a locator (0 of 1)

The writing levels say how complete the text of a page is. They do not measure its truth.

What links here

No page links to this page yet.