A formula in first order logic is said to be in prenex form if all quantifiers occur in the front of the formula, before any occurrences of predicates and connectives. Schematically, a proposition in prenex form will appear as follows $$ (Q_1 x_1) (Q_1 x_1) \hdots \langle \hbox{matrix} \rangle $$

where each ``$Q$ '' stands for either ``$\forall$ '' or ``$\exists$ '' and ``$\langle {matrix} \rangle$ '' is constructed from predicates and connectives. For example, the proposition $$ (\forall x) (\exists y) (\forall z) \, (x > z \rightarrow y > z) $$

is in prenex form whilst the statement $$ (\forall x) \, (x > 0 \rightarrow (\exists y) (x = y^2)) $$

is not in prenex form, but is equivalent to the statement $$ (\forall x) (\exists y) \, (x > 0 \rightarrow x = y^2) $$

which is in prenex form.

This requirement that the statement be expressed in prenex form puts no real restriction on the statements which we may consider because it is possible to systematically express any statement in prenex form by a systematic use of the several equivalences: