I have the following statement: $$\ \forall Z \forall X ((A(Z) \land S(Z,X)\land (\exists Q (P(Q) \land E(Z,Q)))) \implies E(X,Z)) $$ Which (I hope) can be read as "For all X and Z, if A(Z) and S(Z,X) and there exists a Q with P(Q) and E(Z,Q)) then E(X,Z))
In the process of reducing to CNF (this is part of a resolution problem), I have reached this: $$\ \forall Z \forall X (¬A(Z) \lor ¬S(Z,X)\lor (\forall Q (¬P(Q) \lor ¬E(Z,Q)) \lor E(X,Z)) $$ I'm aware of skolemising where Exists is used instead of ForAll, but not sure how to deal with the nested ForAll. My intuition says to move the ForAll Q to the beginning of the sentence, as surely this would have the same meaning, but I'm not sure how to justify this.
Would this be valid to do?
Thanks!
The Prenex Laws specify if and how you can pull out quantifiers.
Specific to your sentence, you have that where $\varphi$ is any formula and $x$ is not a free variable in $\psi$:
$$ \psi \lor \forall x \ \varphi \Leftrightarrow \forall x (\psi \lor \varphi)$$
So yes, you can indeed pull out the quantifier as is, and obtain:
$$\ \forall Z \forall X \forall Q (¬A(Z) \lor ¬S(Z,X)\lor ¬P(Q) \lor ¬E(Z,Q) \lor E(X,Z)) $$
Now, why does this prenex law hold? I'll give a very informal 'proof':
A universal can be seen as kind of conjunction, that is, if $a,b,c,...$ denote the objects in your domain, then you can think of a universal like this:
$$\forall x \: \varphi(x) \approx \varphi(a) \land \varphi(b) \land \varphi(c) \land ...$$
(I use $\approx$ here, since this is really not any kind of properly defined equivalence, and why this isn't a genuine proof either ... but it'll get the basic idea across)
As such, we thus have:
$$ \psi \lor \forall x \varphi(x) \approx$$
$$\psi \lor (\varphi(a) \land \varphi(b) \land \varphi(c) \land ...) \Leftrightarrow$$
$$(\psi \lor \varphi(a) ) \land (\psi \lor \varphi(b)) \land (\psi \lor \varphi(c) ) \land ... \approx$$
$$\forall x (\psi \lor \varphi(x) ) $$