Prenex Normal Form (First-Order Logic)

first-order-logic

Definition

Prenex Normal Form (First-Order Logic)

A formula is in prenex normal form (PNF) if it has the shape

$$Q_1{x}_1{Q}_2{x}_2\cdots Q_n{x}_n\phi$$

where each $Q_i\in \{\forall ,\exists \}$ is a quantifier and $\phi$ is a quantifier-free formula called the matrix.

Sentences Conversion

Theorem

Every sentence $\phi$ can be converted into an equivalent formula in prenex normal form.

Algorithm

1. Eliminate all occurrences of $\to$ and $\leftrightarrow$
2. Move all negations inward to the atomic level (NNF)
3. Standardise the variables apart via renaming
4. Move all quantifiers to the front

Step-by-step conversion

Convert $\forall x(\exists yR(x,y)\wedge \forall y\neg S(x,y))\to \neg (\exists yR(x,y)\wedge P)$ to PNF:

Step 1: Eliminate $\to$.

$$\forall x(\neg (\exists yR(x,y)\wedge \forall y\neg S(x,y))\vee \neg (\exists yR(x,y)\wedge P))$$

Step 2: Move negations inward (NNF).

$$\forall x((\forall y\neg R(x,y)\vee \exists yS(x,y))\vee (\forall y\neg R(x,y)\vee \neg P))$$

Step 3: Rename variables apart.

$$\forall x(\forall y_1\neg R(x,y_1)\vee \exists y_{2}S(x,y_2)\vee \forall y_3\neg R(x,y_3)\vee \neg P)$$

Step 4: Move quantifiers to the front.

$$\forall x\forall y_1\exists y_2\forall y_3(\neg R(x,y_1)\vee S(x,y_2)\vee \neg R(x,y_3)\vee \neg P)$$

Examples

In PNF

$$\forall x\exists y(P(x)\to Q(x,y)),\exists x\forall y\forall z(R(x,y)\wedge \neg R(y,z))$$

Not in PNF

$$P(x)\wedge \exists yQ(y)\text{(quantifier not at the front)},\forall x(P(x)\to \exists yQ(y))\text{(quantifier inside)}$$