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
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 ) ] $$