# 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}\u27e8\text{matrix}\u27e9$$ |

where each “$Q$” stands for either “$\forall $” or “$\exists $” and “$\u27e8\text{matrix}\u27e9$” 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 |