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.
- Anybody can ask a question
- Anybody can answer
- The best answers are voted up and rise to the top
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.
Then we apply the Substitution lemma [see Sara Negri & Jan von Plato, Structural Proof Theory (2001), page 68] :
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 :
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.