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).

Thanks in advance.

  • 2
    $\begingroup$ 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. $\endgroup$
    – user13756
    Oct 21, 2013 at 9:41
  • $\begingroup$ @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. $\endgroup$
    – Harshdeep
    Oct 21, 2013 at 17:13
  • 1
    $\begingroup$ By standard rules, you mean other rules from Gentzen's sequent calculus? $\endgroup$ Oct 22, 2013 at 4:53
  • $\begingroup$ @bellpeace yes, precisely! $\endgroup$
    – Harshdeep
    Oct 22, 2013 at 6:47
  • $\begingroup$ @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. $\endgroup$
    – user13756
    Nov 7, 2013 at 7:39

2 Answers 2


The fact that a system is complete for proving valid formulas without the cut rule doesn't mean you can derive the cut rule from other rules.

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.

Admissibility of cut is actually equivalent to showing that cut can be eliminated. If you have cut-elimination, you just cut the two derivations together and then eliminate the cut. On the other hand, if you have cut-admissibility, you can use it to recursively eliminate all the cuts, starting at the leaves and working down to the root.

A good description of this proof, for a variety of logics, can be found in Frank Pfenning's 1995 LICS paper, Structural Cut Elimination.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.