Prenex normal forms in the first-order logic

Definition: A formula F in the first-order logic is said to be a prenex normal form if the formula F is in the form of (Q₁x₁) … (Q_nx_n)(M), where every (Q_ix_i), i = 1, …, n, is either (∀x_i) or (Ǝx_i), and M is a formula containing no quantifiers. (Q₁x₁) … (Q_nx_n) is called the prefix and M is called the matrix of the formula F.

Here are some formulas in prenex normal form:

(∀x)(∀y)(P(x, y) Ù (Q(y));

(∀x)(∀y) ~(P(x, y)→Q(y));

(∀x)(∀y)(Ǝz)(Q(x, y)→R(z)).

In order to transform a formula into a prenex normal form we need basic pairs of equivalent formulas in the first-order logic. We remember that two formulas F and G are equivalent, (denoted F º G or F = G), if and only if the truth values of F and G are the same under every interpretation.

The basic pairs of equivalent formulas for propositional logic are true for the first-order logic also. In addition, there are other pairs of equivalent formulas containing quantifiers.

Let F be a formula containing a free variable x. To emphasize that the free variable is in F, we represent F by F[x]. Let G be a formula that does not contain variable x. We call each of the following pairs of equivalent formulas a “law”.

(3.1 a) (∀x) F[x] v G = (∀x)(F[x] v G).

(3.1 b) (Ǝx) F[x] v G = (Ǝx)(F[x] v G).

(3.1 c) (∀x) F[x] ʌ G = (∀x)(F[x] ʌ G).

(3.1 d) (Ǝx) F[x] ʌ G = (Ǝx)(F[x] ʌ G)

(3.2 a)~((∀x)F[x]) = (Ǝx)(~F[x]).

(3.2 b)~(Ǝx)(F[x]) = (∀x)(~ F[x]).

Laws (3.1 a) to (3.1 d) are obviously true, since G does not contain x and therefore can be brought into scope of the quantifier.

Laws (3.2 a) and (3.2 b) are not difficult to prove. Let ¡ be an arbitrary interpretation over a domain D. If ~ ((∀x)F[x]) is true in ¡, then (∀x) F[x] is false in ¡. This means there is an element e in D such that F[e] is false, that is, ~F(e) is true in I. Therefore, (Ǝx)(~F[x]) is true in ¡. On other hand, if ~ ((∀x) F[x]) is false in ¡, then (∀x) F[x] is true in ¡. This means that F[x] is true for every element x in D, that is, ~ F[x] is false for every element x in D. Therefore, (Ǝx)(~ F[x]) is false in ¡. Since ~(∀x) F[x] and (Ǝx)(~ F[x]) always assume the same truth values for every arbitrary interpretation, by definition, ~(∀x) F[x] = (Ǝx)(~ F[x]). Hence, law (3.2 a) is proved. Similarly, we can prove law (3.2 b).

Suppose F[x] and H[x] are two formulas containing x. There are two other laws:

(3.3 a) (∀x) F[x] ʌ (∀x) H[x] = (∀x)(F[x] ʌ H[x]).

(3.3 b) (Ǝx) F[x] v (Ǝx) H[x] = (Ǝx)(F[x] v H[x]).

That is, the universal quantifier ∀ and the existential quantifier Ǝ can distribute over ʌ and v, respectively. However, the universal quantifier ∀ and the existential quantifier Ǝ cannot distribute over v and ʌ, respectively. So (∀x) F[x] v (∀x) H[x] ≠ (∀x) (F[x] v H[x]);