Example of prenex normal form in Harrison's Handbook

Question

The following example appears in John Harrison's "Handbook of Practical Logic and Automated Reasoning", page 144.

The prenex normal form of $(\forall x. P(x) \lor R(y)) \implies \exists y,z. Q(y) \lor \lnot (\exists z. P(z) \land Q(z))$ is $\exists x. \forall z. \lnot P(x) \land \lnot R(y) \lor Q(x) \lor \lnot P(z) \lor \lnot Q(z)$.

Is this correct? My naive understanding does not see how $Q(x)$ appeared in the result nor why the $\forall z.$ was not pulled out leaving unchanged $\land$.

Answer 1

Yes, it is correct.

In the RHS part $∃y,z.Q(y)∨¬(∃z.P(z)∧Q(z))$ the ∃z is useless; thus we have to remove it getting: $∃y(Q(y)∨∀z(¬P(z)∨¬Q(z)))$ which is equiv to:

$∃y∀z(Q(y)∨¬P(z)∨¬Q(z))$.

In the LHS part $(∀x.P(x)∨R(y))$ $y$ is free; thus we cannot rename it.

The complete formula is:

$\lnot (∀x.P(x)∨R(y)) \lor ∃x∀z(Q(x)∨¬P(z)∨¬Q(z))$,

and thus:

$∃x (\lnot P(x) \land \lnot R(y)) \lor ∃x∀z(Q(x)∨¬P(z)∨¬Q(z))$.

---

Having said that, we have a formula like $\exists x A \lor \exists x B$ which is equivalent to: $\exists x (A \lor B)$.

Thus:

$∃x ∀z[(\lnot P(x) \land \lnot R(y)) \lor (Q(x)∨¬P(z)∨¬Q(z))]$.