Mathematical logic and foundations Definition

Prenex normal form

Definition

Let $\sigma$ be a signature. A first-order formula over $\sigma$ is in prenex normal form if it has the form $Q_1 x_1 \, Q_2 x_2 \cdots Q_n x_n \, \psi,$ where $n \ge 0$ and each $Q_i$ is $\forall$ or $\exists$ . The $x_i$ are variables. Here $\psi$ is a formula with no quantifiers. The string $Q_1 x_1 \cdots Q_n x_n$ is the prefix and $\psi$ is the matrix.

Remarks

The formula $\forall x \, \exists y \, (R(x, y) \lor \neg P(x))$ is in prenex normal form: its prefix is $\forall x \, \exists y$ and its matrix has no quantifiers. The formula $\neg \forall x \, P(x)$ is not: the quantifier is inside a negation, so the formula is not a prefix followed by a quantifier-free matrix. It is equivalent to $\exists x \, \neg P(x)$ , which is in prenex normal form. In classical first-order logic, every formula is logically equivalent to a formula in prenex normal form. The proof moves quantifiers outwards with rules such as $(\forall x \, \varphi) \to \psi \equiv \exists x \, (\varphi \to \psi)$ , when $x$ is not free in $\psi$ . This rule uses that structures have nonempty domains.

Reading path

To understand this page from the ground up, read these 2 pages in order. The foundations come first.

Show the path as a graph

Each page uses the pages above it. The colour of the bar on a box shows how strong the evidence is, and the box also gives it as text. The list has the same pages.

no evidence level

Well-formed formula concept
Prenex normal form definition

Tag	`1NKD8P3PS0`
URI	`m2://1NKD8P3PS0`
Kind	definition
Writing	W0 stub
MSC	03B10
Defines	Prenex normal form
Uses	Well-formed formula
Changed	2 November 2026

Prenex normal form

Definition

Remarks

Reading path

Further reading

What this page needs for W1

What links here