prenex form

A formula in first order logic is said to be in prenex form if all quantifiers occur in the front of the formula, before any occurrences of predicates and connectives. Schematically, a proposition in prenex form will appear as follows

$$(Q_1{x}_1)(Q_1{x}_1)\mathrm{\dots }⟨\text{matrix}⟩$$

where each “$Q$” stands for either “$\forall$” or “$\exists$” and “$⟨\text{matrix}⟩$” is constructed from predicates and connectives. For example, the proposition

$$(\forall x)(\exists y)(\forall z)(x>z\to y>z)$$

is in prenex form whilst the statement

$$(\forall x)(x>0\to (\exists y)(x=y^2))$$

is not in prenex form, but is equivalent to the statement

$$(\forall x)(\exists y)(x>0\to x=y^2)$$

which is in prenex form.

This requirement that the statement be expressed in prenex form puts no real restriction on the statements which we may consider because it is possible to systematically express any statement in prenex form by a systematic use of the several equivalences:

Title	prenex form
Canonical name	PrenexForm
Date of creation	2013-03-22 15:06:55
Last modified on	2013-03-22 15:06:55
Owner	rspuzio (6075)
Last modified by	rspuzio (6075)
Numerical id	7
Author	rspuzio (6075)
Entry type	Definition
Classification	msc 03B10
Classification	msc 03C07