Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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|cite|improve this question

The statement of the problem is not clear to me.

First, the formula $∀x∀yR(x,y) \rightarrow R(y,y)$ is valid; thus, it must be provable.

With an Hilbert-style proof system [see Herbert Enderton, A Mathematical Introduction to Logic (2nd - 2001)] we have :

(1) $∀x∀yR(x,y) \vdash ∀z∀wR(z,w)$ --- by Theorem 24I (Existence of Alphabetic Variants), page 126]

(2) $∀wR(y,w)$ --- from (1) by Ax.2 [i.e.$\forall x \alpha \rightarrow \alpha[t/x]$, page 112] and modus ponens

(3) $R(y,y)$ --- from (2) by Ax.2 and mp

(4) $\vdash ∀x∀yR(x,y) \rightarrow R(y,y)$ --- from (1) and (3) by Deduction Theorem.

Thus, it must be provable also in sequent calculus.


$${R(z,y) \Rightarrow R(z,y) \over \forall yR(z,y) \Rightarrow R(z,y) }$$ $${ \over \forall x\forall yR(z,y) \Rightarrow R(z,y) }\ \text{by two applications of}\, \forall \text{-left}$$

Then we apply the Substitution lemma [see Sara Negri & Jan von Plato, Structural Proof Theory (2001), page 68] :

if $\Gamma \Rightarrow C$ is derivable and $t$ is free for $z$ in $\Gamma, C$, then $\Gamma[t/z] \Rightarrow C[t/z]$ is derivable.

We apply it to the end-sequent above, with $y$ as $t$ and $R(z,y)$ as $C$; thus $C[t/z]$ is $R(z,y)[y/z]=R(y,y)$ to conclude :

$${ \over \forall x\forall yR(z,y) \Rightarrow R(y,y) }$$

In conclusion we have a proof of it which is intuitionistically valid and without cut ... Please, check.

share|cite|improve this 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|cite|improve this answer

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.