prenex form

A formulaMathworldPlanetmathPlanetmath in first order logic is said to be in prenex form if all quantifiersMathworldPlanetmath occur in the front of the formula, before any occurrences of predicatesMathworldPlanetmath and connectivesMathworldPlanetmath. Schematically, a propositionPlanetmathPlanetmath in prenex form will appear as follows


where each “Q” stands for either “” or “” and “matrix” is constructed from predicates and connectives. For example, the proposition


is in prenex form whilst the statement


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


which is in prenex form.

This requirement that the statement be expressed in prenex form puts no real restrictionPlanetmathPlanetmathPlanetmath 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