3
$\begingroup$

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.

| cite | improve this question | |
$\endgroup$
  • 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$ – Dilworth Oct 21 '13 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 '13 at 17:13
  • 1
    $\begingroup$ By standard rules, you mean other rules from Gentzen's sequent calculus? $\endgroup$ – bellpeace Oct 22 '13 at 4:53
  • $\begingroup$ @bellpeace yes, precisely! $\endgroup$ – Harshdeep Oct 22 '13 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$ – Dilworth Nov 7 '13 at 7:39
4
$\begingroup$

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.

| cite | improve this answer | |
$\endgroup$
2
$\begingroup$

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.

| cite | improve this answer | |
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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