Say I have a first-order logic formula given like this one:
$$ \forall x \exists y ( (\forall z \ P(x,z) \land Q(x,y) ) \lor (\exists g \ G( (f(x),g) )$$
Now I am interested in creating the prenex-form, which is just pulling the quantifiers from the "local scope" in to the "global scope".
Now to my problem: How do I pull out the quantifiers to the front.
In what order do I pull out the quantifiers and where do they go with respect to the existing quantifiers ?
My current understanding is that the quantifers get pushed to the right side of the preexisting quantifiers.
Also since the variables from the quantifiers are not free in any predicates I can write the above formula like this:
$$ \forall x \exists y \forall z \exists g( P(x,z) \land Q(x,y) ) \lor G( f(x),g) )$$
Is my undestanding correct ?
I don't understand what you mean by the quantifiers being 'pushed to the right side of the formula', but your result is indeed correct.
To clarify why this is correct:
If you have something like:
$$\forall x A(x) \lor \exists y B(y)$$
then, since $\exists y B(y)$ does not contain any free variable $x$, we can 'pull out' the $\forall x$, and thus get:
$$\forall x (A(x) \lor \exists y B(y))$$
Then, because there is no free variable $y$ in $A(x)$, we can pull out the $\exists y$ ... but where does it end up?
Well, the relevant equivalence is that where $\phi$ is some formula that does not have a free variable $v$, we have that ($Q$ is some quantifier, and $\psi$ some formula):
$$\phi \lor Qv \ \psi(v)\Leftrightarrow Qv(\phi \lor \psi(v))$$
So, applying this to the example, we have that:
$$A(x) \lor \exists y B(y) \Leftrightarrow \exists y (A(x) \lor B(y))$$
And applying this equivalence to the larger $\forall (A(x) \lor \exists y B(y))$, we thus get:
$$\forall x (A(x) \lor \exists y B(y)) \Leftrightarrow \forall x \exists y (A(x) \lor B(y))$$