---
tag: CS82V969DE
kind: concept
name: Prenex normal form
msc: [03B10]
sources:
  - url: https://en.wikipedia.org/wiki/Prenex_normal_form
same_as:
  wikidata: Q281854
  wikipedia: Prenex normal form
---

## Summary

A formula is in prenex normal form when all its quantifiers stand at the front, followed by a part without quantifiers.
In classical first-order logic every formula is equivalent to a formula in prenex normal form.
The string of quantifiers in front measures the logical complexity of the formula, as in the [[arithmetical hierarchy|7CVJCQKY41]].
Prenex form is also the first step towards [[Skolem normal form|GCPQGMJYEV]].

## Explanations

### L1 human

The formula $\forall x \, \exists y \, (x < y \land y < x + 2)$ has all its quantifiers at the start, so it is in prenex form.
The formula $(\forall x \, P(x)) \to Q(c)$ is not, because the quantifier sits inside the implication.
It can be rewritten as $\exists x \, (P(x) \to Q(c))$, which means the same thing and is in prenex form.
Pulling quantifiers to the front like this is always possible in classical logic.