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

where each is a quantifier and is a quantifier-free formula called the matrix.

Sentences Conversion

Theorem

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

Algorithm

1. Eliminate all occurrences of and
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 to PNF:

Step 1: Eliminate .

Step 2: Move negations inward (NNF).

Step 3: Rename variables apart.

Step 4: Move quantifiers to the front.

Examples

In PNF

Not in PNF