Convert predicate to prenex normal form

Question

$$\color{red}{(}\neg A(x)\lor \exists x\text{ }\color{green}{(}\forall y\text{ } B(x,y) \to \exists y \text{ }C(x,y)\color{green}{)}\color{red}{)}$$

So far I could only perform the following operation:

$$\color{red}{(}\neg A(x)\lor \exists x\text{ }\color{blue}{(}\exists y\text{ }\color{green}{(} B(x,y) \to \text{ }C(x,y)\color{green}{)}\color{blue}{)}\color{red}{)}$$

I can't really factor out the $\exists x$ because $x$ is free in $\neg A(x)$. What know?

Answer 1

You are right that you cannot move the $\exists x$ over the $\neg A(x)$.

But you can rename variables!

So, you could replace the $x$ in $A(x)$ with a $z$, and now bring the $\exists x$ out.

Remember, variables are just dummy placeholders.