Prenex normal form

Every formula in first-order logic is equivalent to a formula where all quantifications are on the outside.

Quantifiers are essential syntactic ingredients of first-order formulas. They can be separated from the rest in the sense that they come first and then everything else follows.

Example In the formula $\neg \exists x_0 R(x_0)$ the existential quantification is within the use of the 'not' connective. This formula is equivalent to the formula $\forall x_0 \neg R(x_0)$, where the quantification is on the outside.

Basic definitions

Definition A first-order formula is quantifier-free if no quantification occurs in it. More formally, it is built inductively just as formulas are built in general, but the last inductive rule must not be used.

Definition The first-order formulas in prenex normal form (PNF) are defined inductively as follows.

Base elements. Every quantifier-free first-order formula is in PNF.

Inductive rule. If $\varphi$ is a formula in prenex normal form, then so are $\exists x_i \varphi$ and $\forall x_i \varphi$ for every $i \in \mathbf N$.

Observe that the above inductive definition is unique. In particular, the quantifier free formula one starts with is unique. This formula is called the matrix of the formula in PNF. The quantifications added by the inductive rule are called the quantifier block.

Example The formula $\exists x_1 \exists x_0 \forall x_2 (\neg R(x_0, x_1, x_2) \vee S(f(x_0, x_3)))$ is in PNF. Its quantifier block is given by $\exists x_1 \exists x_0 \forall x_2$; its matrix is given by $\neg R(x_0, x_1, x_2) \vee S(f(x_0, x_3))$.

A main feature of the formulas in PNF is that every $\exists$ stands for an existential quantification just as every $\forall$ stands for a universal quantification as illustrated by the following example.

Example The formula $\neg \exists x_0 R(x_0)$ really says that $R(x_0)$ does not hold for any element of the universe, which is a universal statement.

Conversion theorem with proof

Theorem Every first-order formula can be converted into an equivalent first-order formula in PNF.

For the proof, it is enough to work with formulas in BNF, because every first-order formula can be converted into an equivalent formula in BNF.

For converting formulas in BNF into PNF, inductive constructions can be used. One option is to use an ordinary induction. This then requires further nested inductive constructions. Another option is the following inductive construction, which uses a more complex parameter.

The proof is by induction on the sum of the sizes of the subformulas which are not in PNF, $n$. Since the subformulas of every formula in PNF are in PNF themselves, the induction base, $n=0$, is trivial. Now suppose $\varphi$ is a formula which is not in PNF. Let $\psi$ be a smallest subformula not in PNF in the sense that no subformula of $\psi$ is not in PNF. Then there are three cases to consider.

First case, $\psi$ can be written as $\neg \psi_0$. Then $\psi_0$ must be in PNF. If $\psi_0$ is quantifier free, then $\psi$ is in PNF. So $\psi_0$ is of the form $Q x_i \psi_1$ for some quantifier $Q$. By the quantifier laws, $\neg \psi_0 \SemEquiv \bar Q x_i \neg \psi_1$ where $\bar Q$ is the dual of $Q$. By induction hypothesis there is a formula in PNF equivalent to $\neg \psi_1$, say $\chi$. Thus, by the congruence principle, $\psi$ can be replaced by $\bar Q x_i \chi$ in $\varphi$ to obtain an equivalent formula, to which the induction hypothesis can be applied.

Second case, $\psi$ can be written as $\psi_0 \vee \psi_1$. Then $\psi_0$ and $\psi_1$ are in PNF and one of them, say $\psi_0$, must be of the form $Q x_i \psi_2$. By renaming bound variables and choosing a $j$ such that $x_j \notin \text{vars}(\varphi)$, $Q x_i \psi_2 \SemEquiv Q x_j \psi_2\{x_i \mapsto x_j\}$. By shifting the quantifier, we obtain $Q x_i \psi_2 \vee \psi_1 \SemEquiv Q x_j (\psi_2\{x_i \mapsto x_j\} \vee \psi_1)$. The induction hyptothesis can be applied to the latter formula to obtain a formula $\chi$ such that $Q x_i \psi_2 \vee \psi_1 \SemEquiv \chi$ and $\chi$ is in PNF. Thus, by the congruence principle, $\psi$ can be replaced by $\chi$ in $\varphi$ to obtain an equivalent formula, to which the induction hypothesis can be applied.

Third case, $\psi$ can be written as $\psi_0 \wedge \psi_1$. This case can be dealt with just as with the second case.

Existential and universal formulas

Definition A first-order formula is existential if it is in prenex normal form, it has no free variables, and $\forall$ does not occur in it. A first-order formula is universal if it is in prenex normal form, it has no free variables, and $\exists$ does not occur in it.

Definition Let $\varphi$ be a formula with $n$ variables and $\text{fvars}(\varphi) = \{x_{i_0}, \dots, x_{i_{n-1} }\}$. Then an existential closure of $\varphi$ is a formula of the form $\exists x_{i_0} \dots \exists x_{i_{n-1} } \varphi$ and any such formula is denoted $\exists \varphi$.

The universal closure of a formula is defined in the same fashion.