Editing Cut-elimination theorem (section)

==The cut rule==
A [[sequent]] is a logical expression relating multiple formulas, in the form {{nowrap|"<math>A_1, A_2, A_3, \ldots \vdash B_1, B_2, B_3, \ldots</math>"}}, which is to be read as "If all of {{nowrap|<math>A_1, A_2, A_3, \ldots</math>}} hold, then at least one of {{nowrap|<math>B_1, B_2, B_3, \ldots</math>}} must hold", or (as Gentzen glossed): "If (<math>A_1</math> and <math>A_2</math> and <math>A_3</math> …) then (<math>B_1</math> or <math>B_2</math> or <math>B_3</math> …)."<ref>Wilfried Buchholz, [http://www.mathematik.uni-muenchen.de/~buchholz/articles/beweisth.ps Beweistheorie] (university lecture notes about cut-elimination, German, 2002-2003)</ref> Note that the left-hand side (LHS) is a conjunction (and) and the right-hand side (RHS)  is a disjunction (or).  

The LHS may have arbitrarily many or few formulae; when the LHS is empty, the RHS is a [[tautology (logic)|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 rule]]s that is the key here.

"Cut" is a [[rule of inference]] in the normal statement of the [[sequent calculus]], and equivalent to a variety of rules in other [[proof theory|proof theories]], which, given

<ol><li><math> \Gamma \vdash A,\Delta</math></li></ol>

and 

<ol start="2"><li><math> \Pi, A \vdash \Lambda</math></li></ol>

allows one to infer

<ol start="3"><li><math>\Gamma, \Pi \vdash \Delta,\Lambda</math></li></ol>

That is, it "cuts" the occurrences of the formula <math>A</math> out of the inferential relation.