# Derivation of cut rule in sequent calculus

I searched internet but could not find any good weblink which shows how the cut rule for sequent calculus can be derived.

I found this paper but it uses implication elimination rule which I cannot find as a standard rule anywhere (see page 2).

• I don't think the cut-rule can be derived from other rules in the sequent calculus. It is independent of them. Cuts can be eliminated, but not derived. – Dilworth Oct 21 '13 at 9:41
• @Dilworth but to best of my knowledge (and also the literature says this) that it is a derived rule and that cut-free logic can be used to prove whatever can be proved using cut rule. – Harshdeep Oct 21 '13 at 17:13
• By standard rules, you mean other rules from Gentzen's sequent calculus? – bellpeace Oct 22 '13 at 4:53
• @bellpeace yes, precisely! – Harshdeep Oct 22 '13 at 6:47
• @Harshdeep, as Kaveh also explained, the cut-rule cannot be derived by other rules in the Gentzen sequent calculus. This is a crucial point in Gentzen's work. This follows from the subterm property of the cut-free sequent calculus. Also, the cut-free sequent calculus is implicationaly complete, while the cut-free calculus is not. – Dilworth Nov 7 '13 at 7:39

In fact it is not difficult to construct counter-examples. Consider $\Rightarrow A \rightarrow B$ and $\Rightarrow A$. From these assumptions it would follow that $\Rightarrow B$. But you cannot derive it without using a cut.
Showing that from two cut-free derivations $\Gamma \vdash A$ and $\Gamma, A \vdash C$ you can produce a cut-free derivation of $\Gamma \vdash C$ is called cut admissibility.