# Using Sequent Calculus to prove $\exists x_1 x_2 [ B ( x_1 , x_2 ) \rightarrow \forall y_1 y_2 B ( y_1 , y_2 ) ]$

I need to prove the validity of the following formula using the sequent calculus LK: $$\exists x_1 x_2 [ B ( x_1 , x_2 ) \rightarrow \forall y_1 y_2 B ( y_1 , y_2 ) ] \text{.}$$ I already had a look at the post First-order logic: nested quantifiers for same variables and understand why this formula is valid, but I just can't seem to find a proof for it in LK.

My previous attempts looked like this (proceeding in bottom-up manner): $$B ( a , b ) \vdash \forall y_1 y_2 B ( y_1 , y_2 )$$ $$\text{--------------------------------------------------- } \rightarrow-r$$ $$\vdash B ( a , b ) \rightarrow \forall y_1 y_2 B ( y_1 , y_2 )$$ $$\text{--------------------------------------------------- } \exists-r$$ $$\vdash \exists x_2 [ B ( a , x_2 ) \rightarrow \forall y_1 y_2 B ( y_1 , y_2 ) ]$$ $$\text{--------------------------------------------------- } \exists-r$$ $$\vdash \exists x_1 x_2 [ B ( x_1 , x_2 ) \rightarrow \forall y_1 y_2 B ( y_1 , y_2 ) ]$$ Now for the uppermost sequent it doesn't make sense to eliminate the remaining quantifiers (since I would have to use fresh variables) and so I thought, that there might be some way to apply the cut-rule here. However, I couldn't figure out how to do it. Can anyone give me a hint on how to continue?

Thank you! Best, Patrick

• Hi Mauro! I started with the proof from the bottom and moved upwards, since I usually find it easier to proceed this way. Sorry this wasn't clear, I added it to the problem description. The eigenvariables are exactly the reason why I thought that I have to use the cut-rule to continue from the uppermost sequent. – patrickH Jun 23 '15 at 21:18

Alright, eventually I figured it out by myself, not the easiest proof: $$B ( a , b ) \vdash B ( a , b )$$ $$\text{----------------------- weakening-r}$$ $$B ( a , b ) \vdash \forall y_1 y_2 B ( y_1 , y_2 ) , B ( a , b )$$ $$\text{------------------------------------- \to-r}$$ $$\vdash B ( a , b ) \to \forall y_1 y_2 B ( y_1 , y_2 ) , B ( a , b )$$ $$\text{----------------------------------------- \exists-r 2 times}$$ $$\vdash \exists x_1 x_2 [ B ( x_1 , x_2 ) \to \forall y_1 y_2 B ( y_1 , y_2 ) ] , B ( a , b )$$ $$\text{----------------------------------------- exchange-r}$$ $$\vdash B ( a , b ) , \exists x_1 x_2 [ B ( x_1 , x_2 ) \to \forall y_1 y_2 B ( y_1 , y_2 ) ]$$ $$\text{-------------------------------------------------- \forall-r 2 times}$$ $$\vdash \forall y_1 y_2 B ( y_1 , y_2 ) , \exists x_1 x_2 [ B ( x_1 , x_2 ) \to \forall y_1 y_2 B ( y_1 , y_2 ) ]$$ $$\text{--------------------------------------------------------- weakening-l}$$ $$B ( a , b ) \vdash \forall y_1 y_2 B ( y_1 , y_2 ) , \exists x_1 x_2 [ B ( x_1 , x_2 ) \to \forall y_1 y_2 B ( y_1 , y_2 ) ]$$ $$\text{---------------------------------------------------------------------- \to-r}$$ $$\vdash B ( a , b ) \to \forall y_1 y_2 B ( y_1 , y_2 ) , \exists x_1 x_2 [ B ( x_1 , x_2 ) \to \forall y_1 y_2 B ( y_1 , y_2 ) ]$$ $$\text{------------------------------------------------------------------------- \exists-r 2 times}$$ $$\vdash \exists x_1 x_2 [ B ( x_1 , x_2 ) \to \forall y_1 y_2 B ( y_1 , y_2 ) ] , \exists x_1 x_2 [ B ( x_1 , x_2 ) \to \forall y_1 y_2 B ( y_1 , y_2 ) ]$$ $$\text{----------------------------------------------------------------------- contraction-r}$$ $$\vdash \exists x_1 x_2 [ B ( x_1 , x_2 ) \to \forall y_1 y_2 B ( y_1 , y_2 ) ]$$