Prenex Normal Form

A formula is in Prenex Normal Form (PNF) if it starts with 0 or more quantifiers followed by a quantifier free formula:

$$Q_1{x}_1\dots Q_n{x}_n\varphi$$

Where $Q_i\in \{\exists ,\forall \}$ and $\varphi$ is quantifier free.

In this case, $Q_1{x}_1\dots Q_n{x}_n$ is the (possibly empty) prefix. And $\varphi$ is the matrix. Any first order formula can be translated into PNF.