# 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.

-

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.

Proof

$${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.

-

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.

-