cuteliminatie

Cut elimination, or the cut-elimination theorem, is a central result in proof theory related to sequent calculi. It concerns the use of the cut rule, which allows a proof to introduce an intermediate formula A and then use it to derive the final conclusion. Intuitively, a proof with a cut uses A as a lemma; cut elimination shows that every such proof can be transformed into an equivalent proof that does not rely on any intermediate lemma.

In the standard sequent calculi for classical logic (LK) and intuitionistic logic (LJ), the cut rule has a specific form: from a proof of a sequent that ends with A on the right, and a proof of a sequent that has A on the left, one can derive the sequent where A is removed. A cut-free proof contains no instances of this rule. Gentzen proved that every provable sequent in these systems has a cut-free proof, a result known as Gentzen’s Hauptsatz (main theorem).

The consequences of cut elimination are significant. Cut-free proofs enjoy the subformula property: every formula occurring in the proof is a subformula of the end sequent. This gives a form of analytic proof and helps establish consistency results, normalization, and structured proof search. The theorem also has deep connections to computation via the Curry–Howard correspondence, where cut elimination corresponds to beta reduction in lambda calculus. Variants and extensions cover many logics and systems, though the transformation to cut-free proofs can cause substantial growth in proof size.