<p>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. </p>

<p>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.</p>

CC BY-SA 3.0
2013-10-22T16:56:48.990Z
2013-10-22T16:56:48.990Z
Kaveh
<p>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 <em>cut admissibility</em>. </p>

<p>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.  </p>

<p>A good description of this proof, for a variety of logics, can be found in Frank Pfenning's 1995 LICS paper, <a href="http://www.cs.cmu.edu/~fp/papers/lics95.pdf" rel="nofollow"><em>Structural Cut Elimination</em></a>. </p>

CC BY-SA 3.0
2013-10-22T08:52:17.670Z
2013-10-22T08:52:17.670Z
Neel Krishnaswami
<p>I searched internet but could not find any good weblink which shows how the <a href="http://en.wikipedia.org/wiki/Sequent_calculus#Inference_rules" rel="nofollow">cut rule</a> for sequent calculus can be derived.</p>

<p>I found <a href="http://www.iam.unibe.ch/~kai/Papers/ace.pdf" rel="nofollow">this</a> paper but it uses implication elimination rule which I cannot find as a standard rule anywhere (see page 2).</p>

<p>Thanks in advance.</p>

CC BY-SA 3.0
2013-10-21T17:13:09.583Z
@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
CC BY-SA 3.0
2013-10-22T04:53:45.690Z
By standard rules, you mean other rules from Gentzen's sequent calculus?
zpavlinovic
CC BY-SA 3.0
2013-10-22T06:47:43.783Z
@bellpeace yes, precisely!
Harshdeep
<lo.logic><proof-theory><sequent-calculus><formal-systems>
Derivation of cut rule in sequent calculus
Harshdeep
# Derivation of cut rule in sequent calculus

(Asked by: username_0 on 2013-10-21)

I searched internet but could not find any good weblink which shows how the [cut rule](http://en.wikipedia.org/wiki/Sequent_calculus#Inference_rules) for sequent calculus can be derived.

I found [this](http://www.iam.unibe.ch/~kai/Papers/ace.pdf) paper but it uses implication elimination rule which I cannot find as a standard rule anywhere (see page 2).

Thanks in advance.

**Tags:** lo.logic, proof-theory, sequent-calculus, formal-systems
> **Comments:**
> **username_0**: @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.  
> **username_1**: By standard rules, you mean other rules from Gentzen's sequent calculus?  
> **username_0**: @bellpeace yes, precisely!  

---

## 2 answers

### Answer by username_2 on 2013-10-22. Score: 4 | Accepted answer

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.


---

### Answer by username_3 on 2013-10-22. Score: 2

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*](http://www.cs.cmu.edu/~fp/papers/lics95.pdf).


---

