Finding prenex normal form of a formula > Find prenex normal form of the formula $(\exists x)S(x,y)\rightarrow (R(x)\rightarrow \neg(\exists u)S(x,u))$ My attempt: * $(\exists x)S(x,y)\rightarrow (R(x)\rightarrow \neg(\exists u)S(x,u))$ * $(\exists x)S(x,y)\rightarrow (R(x)\rightarrow (\forall u)\neg S(x,u))$ * $(\exists x)S(x,y)\rightarrow (\forall u)(R(x)\rightarrow \neg S(x,u))$ * $(\forall u)((\exists x)S(x,y)\rightarrow (R(x)\rightarrow \neg S(x,u)))$ * $(\forall u)(\forall w)(S(w,y)\rightarrow (R(x)\rightarrow \neg S(x,u)))$ I am wondering if the last step is correct. Can anybody tell?

Yes, that is correct, though I would break that step into two: first replace the variable, and then bring out the quantifier. So:

$(\forall u) ((\exists x) S(x,y) \rightarrow (R(x) \rightarrow \
eg S(x,u))) \overset{\text{Replace variables}}\Leftrightarrow$

$(\forall u) ((\exists w) S(w,y) \rightarrow (R(x) \rightarrow \
eg S(x,y)))\overset{\text{Prenex Law}}\Leftrightarrow$

$(\forall u) (\forall w) (S(w,y) \rightarrow (R(x) \rightarrow \
eg S(x,y)))$