Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It only takes a minute to sign up.
Sign up to join this community
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.
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.
