Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

Want to show the a proof of the sequent $\forall x \forall y R(x,y) \Rightarrow R(y,y)$ must have a cut. For this question we are in the Gentzen calculus. I am even having trouble just finding a proof of this sequent first off. There are two results I know of that may be relate, namely: (i) if $\Sigma$ is a cut free proof with endsequent $\alpha$ , then every formula which occurs in $\Sigma$ is a subformula of some formual in $\alpha$ and (ii) if constant c, a relation symbol R or a function symbol f does no occur in he endsequent of a Cut-free proof $\Sigma$, then c, R or f does not occur at all in $\Sigma$. That being said I don't think that these help and the only other thing I can think of is induction on grade and mix rank.

share|improve this question
add comment

1 Answer

I guess this response is a bit late but...

As you observe, a cut-free proof contains only subformulas of formulas of the endsequent. This means that no sequent in a cut-free proof of your sequent can have a formula common to its left and right sides. But there is no such proof.

share|improve this answer
add comment

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

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