August 26th, 2015
(written by lawrence krubner, however indented passages are often quotes). You can contact lawrence at: email@example.com
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 that makes 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 sentences, in the form “A_1, A_2, A_3, \ldots \vdash B_1, B_2, B_3, \ldots”, which is to be read as “A_1, A_2, A_3, \ldots proves B_1, B_2, B_3, \ldots”, and (as glossed by Gentzen) should be understood as equivalent to the truth-function “If (A_1 and A_2 and A_3 …) then (B_1 or B_2 or B_3 …).” Note that the left-hand side (LHS) is a conjunction (and) and the RHS is a disjunction (or).
The LHS may have arbitrarily many or few formulae; when the LHS is empty, the RHS is a tautology. In LK, the RHS may also have any number of formulae—if it has none, the LHS is a contradiction, whereas in LJ the RHS may only have one formula or none: here we see that allowing more than one formula in the RHS is equivalent, in the presence of the right contraction rule, to the admissibility of the law of the excluded middle. However, the sequent calculus is a fairly expressive framework, and there have been sequent calculi for intuitionistic logic proposed that allow many formulae in the RHS. From Jean-Yves Girard’s logic LC it is easy to obtain a rather natural formalisation of classical logic where the RHS contains at most one formula; it is the interplay of the logical and structural rules that is the key here.