Editing Cut-elimination theorem (section)

==Cut elimination==
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.

For sequent calculi that have only one formula in the RHS, the "Cut" rule reads, given

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

and 

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

allows one to infer

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

If we think of <math>B</math> as a theorem, then cut-elimination in this case simply says that a lemma <math>A</math> used to prove this theorem can be inlined. Whenever the theorem's proof mentions [[lemma (mathematics)|lemma]] <math>A</math>, we can substitute the occurrences for the proof of <math>A</math>. Consequently, the cut rule is [[admissible rule|admissible]].