= Solution
First negate the implication, then move the <negation> through the existential quantifier and the <logical conjunction>:
$$
\begin{aligned}
\neg\varphi
&\equiv(\forall x\,P(x))\land\neg\exists y\,(Q(y)\land z<y)\\
&\equiv\boxed{(\forall x\,P(x))\land\forall y\,(\neg Q(y)\lor\neg(z<y)).}
\end{aligned}
$$
This is <negation normal form>, because each <negation> is immediately in front of an atomic predicate. The occurrence of $z$ remains free. Keeping $\neg(z<y)$ also avoids assuming any additional order axioms for the relation symbol $<$; if it has its usual linear-order interpretation, that atom can instead be expressed as $z\geq y$.
Back to article page
