Cut-elimination theorem

The cut-elimination theorem (or Gentzen's Hauptsatz) is the central result establishing the significance of the sequent calculus. It was originally proved by Gerhard Gentzen 1934 in his landmark paper "Investigations in Logical Deduction" for the systems LJ and LK formalising intuitionistic and classical logic respectively. The cut-elimination theorem states that any judgement that possesses a proof in the sequent calculus making use of the cut rule also possesses a cut-free proof, that is, a proof that does not make use of the cut rule.

A sequent is a logical expression relating multiple formulas, in the form "${\displaystyle A_{1},A_{2},A_{3},\ldots \vdash B_{1},B_{2},B_{3},\ldots }$", which is to be read as "${\displaystyle A_{1},A_{2},A_{3},\ldots }$ proves ${\displaystyle B_{1},B_{2},B_{3},\ldots }$", and (as glossed by Gentzen) should be understood as equivalent to the truth-function "If (${\displaystyle A_{1}}$ and ${\displaystyle A_{2}}$ and ${\displaystyle A_{3}}$ …) then (${\displaystyle B_{1}}$ or ${\displaystyle B_{2}}$ or ${\displaystyle B_{3}}$ …)." Note that the left-hand side (LHS) is a conjunction (and) and the RHS is a disjunction (or).

...
Wikipedia