0
$\begingroup$

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

$\endgroup$
  • 1
    $\begingroup$ 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. $\endgroup$ – patrickH Jun 23 '15 at 21:18
0
$\begingroup$

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

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.