Assume that the cut-elimination theorem holds for a system $T$. Then, for any proof that makes use of the cut-rule in $T$, there is a proof that does not make use of the cut-rule. An immediate corollary of it is that if there is a proof of the sequent $\Rightarrow \bot$, there is a cut-free proof of the absurd. Then the usual conclusion is that $T$ is consistent. But I wonder why it is so natural that there is a cut-free proof of the absurd in $T$? In other words,

Why is that the cut-elimination rule implies consistency of a logical system?

For dependently typed theories, cut-elimination corresponds to (strong) normalization. It is easier for me to see the argument from this viewpoint: if every term of a dependently typed theory reduces in a finite steps to a normal form, and there is no canonical inhabitant of the False type, then, it goes without saying that the theory is consistent, i.e. there are no inhabitants of the False.

But how is that the argument is given in the general context of cut-elimination?

  • $\begingroup$ Well, if you have a rule that allows you to immediately deduce $\bot$, then cut elimination is not going to save you there... $\endgroup$ – Zhen Lin Jan 2 '16 at 4:36

For the Gentzen sequent calculus, cut-free proofs have the subformula property: every formula that occurs in a proof of $\Gamma \Rightarrow \Delta$ is a subformula of an element of $\Gamma\cup\Delta$. Indeed, the cut-rule is the only rule that doesn't have this property. It follows immediately that there is no cut-free derivation of the contradictory sequent $\varnothing \Rightarrow \varnothing$.

  • 1
    $\begingroup$ This is exactly right. It's not about cut, it's about the fact that all the other rules follow a strict form. $\endgroup$ – Henry Towsner Jan 2 '16 at 6:54

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.