(or **Gentzen's _Hauptsatz_**) [source: wikipedia](https://en.wikipedia.org/wiki/Cut-elimination_theorem) The Cut Elimination Theorem is the result that established the significance of Gentzen's Sequent Calculus. 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.[[1]](https://en.wikipedia.org/wiki/Cut-elimination_theorem#cite_note-1)[[2]](https://en.wikipedia.org/wiki/Cut-elimination_theorem#cite_note-2) # The Cut Rule Notes The cut rule takes advantage of the fact that the left hand side of a [sequent](Sequent%20Calculus.md) is a conjunction, and the right hand side is a disjunction. If the LHS is empty, then this sequent is a tautology. If the RHS is empty, then the sequent is a contradiction. In both relevant forms of sequent calculus, LJ (one or more RHS statements) and LK (zero or more RHS statements), allowing more than one formula in the RHS is equivalent to the law of the excluded middle, an accepted axiom of logic (that a statement is either true or false). An analytic proof in sequent calculus does not use Cut, and this can make the proof significantly longer. For proof systems based on higher-order [typed lambda calculus](https://en.wikipedia.org/wiki/Typed_lambda_calculus "Typed lambda calculus") through a [Curry–Howard isomorphism](Curry%20Howard%20Isomorphism.md), cut elimination algorithms correspond to the [strong normalization property](Strong%20Normalization%20Property.md) (every proof term reduces in a finite number of steps into a [normal form](https://en.wikipedia.org/wiki/Normal_form_(term_rewriting) "Normal form (term rewriting)")). # The Cut Rule Itself *Cut* is a rule of inference in sequent calculus.[^1]. Given: *Given Gamma, then either A **or** Delta is true* $ \Gamma \vdash A, \Delta $ and: *Given Pi and A, then Lambda is true* $ \Pi, A \vdash \Lambda $ we can infer that: *Given Gamma and Pi, then either Delta or Lambda is true* $\Gamma,\Pi \vdash \Delta,\Lambda$ We have now "cut" out occurrences of *A*. [^1]: *Cut* is equivalent to certain inference rules in other proof theories, as well. # The Cut Elimination Theorem The cut-elimination theorem states that (for a given system) any sequent provable using the rule Cut can be proved without use of this rule. Given: *Given Gamma, then A is true* $\Gamma \vdash A$ and: *Given Pi and A, then B is true* $\Pi,A \vdash B$ we can infer that: $\Gamma,\Pi \vdash B$