Want to show the a proof of the sequent $\forall x \forall y R(x,y) \Rightarrow R(y,y)$ must have a cut 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.
 A: 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.

Edit Feb '17 : I do no longer think that it works...
We can write the derivation:
\begin{align}
{\cfrac{\cfrac{R(z,y) \Rightarrow R(z,y)} {\forall yR(z,y) \Rightarrow R(z,y)}}{ \forall x\forall yR(x,y) \Rightarrow R(z,y) } \text{by two applications of}\, \forall \text{-left}}
\end{align}
and then 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 with:


$$\forall x\forall yR(x,y) \Rightarrow R(y,y)$$


A: 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.
