A formula of the predicate calculus is in prenex^[1] normal form (PNF) if it is written as a string of quantifiers and bound variables, called the prefix, followed by a quantifier-free part, called the matrix.^[2] Together with the normal forms in propositional logic (e.g. disjunctive normal form or conjunctive normal form), it provides a canonical normal form useful in automated theorem proving.

Every formula in classical logic is logically equivalent to a formula in prenex normal form. For example, if ${\displaystyle \phi (y)}$, ${\displaystyle \psi (z)}$, and ${\displaystyle \rho (x)}$ are quantifier-free formulas with the free variables shown then

${\displaystyle \forall x\exists y\forall z(\phi (y)\lor (\psi (z)\rightarrow \rho (x)))}$

is in prenex normal form with matrix ${\displaystyle \phi (y)\lor (\psi (z)\rightarrow \rho (x))}$, while

${\displaystyle \forall x((\exists y\phi (y))\lor ((\exists z\psi (z))\rightarrow \rho (x)))}$

is logically equivalent but not in prenex normal form.

Conversion to prenex form

This section needs additional citations for verification. Please help improve this article by adding citations to reliable sources in this section. Unsourced material may be challenged and removed. (August 2018) (Learn how and when to remove this message)

Every first-order formula is logically equivalent (in classical logic) to some formula in prenex normal form.^[3] There are several conversion rules that can be recursively applied to convert a formula to prenex normal form. The rules depend on which logical connectives appear in the formula.

Conjunction and disjunction

The rules for conjunction and disjunction say that

${\displaystyle (\forall x\phi )\land \psi }$ is equivalent to ${\displaystyle \forall x(\phi \land \psi )}$ under (mild) additional condition ${\displaystyle \exists x\top }$, or, equivalently, ${\displaystyle \lnot \forall x\bot }$ (meaning that at least one individual exists),

${\displaystyle (\forall x\phi )\lor \psi }$ is equivalent to ${\displaystyle \forall x(\phi \lor \psi )}$;

and

${\displaystyle (\exists x\phi )\land \psi }$ is equivalent to ${\displaystyle \exists x(\phi \land \psi )}$,

${\displaystyle (\exists x\phi )\lor \psi }$ is equivalent to ${\displaystyle \exists x(\phi \lor \psi )}$ under additional condition ${\displaystyle \exists x\top }$.

The equivalences are valid when ${\displaystyle x}$ does not appear as a free variable of ${\displaystyle \psi }$; if ${\displaystyle x}$ does appear free in ${\displaystyle \psi }$, one can rename the bound ${\displaystyle x}$ in ${\displaystyle (\exists x\phi )}$ and obtain the equivalent ${\displaystyle (\exists x'\phi )}$.

For example, in the language of rings,

${\displaystyle (\exists x(x^{2}=1))\land (0=y)}$ is equivalent to ${\displaystyle \exists x(x^{2}=1\land 0=y)}$,

but

${\displaystyle (\exists x(x^{2}=1))\land (0=x)}$ is not equivalent to ${\displaystyle \exists x(x^{2}=1\land 0=x)}$

because the formula on the left is true in any ring when the free variable x is equal to 0, while the formula on the right has no free variables and is false in any nontrivial ring. So ${\displaystyle (\exists x(x^{2}=1))\land (0=x)}$ will be first rewritten as ${\displaystyle (\exists x'(x'^{2}=1))\land (0=x)}$ and then put in prenex normal form ${\displaystyle \exists x'(x'^{2}=1\land 0=x)}$.

Negation

The rules for negation say that

${\displaystyle \lnot \exists x\phi }$ is equivalent to ${\displaystyle \forall x\lnot \phi }$

and

${\displaystyle \lnot \forall x\phi }$ is equivalent to ${\displaystyle \exists x\lnot \phi }$.

Implication

There are four rules for implication: two that remove quantifiers from the antecedent and two that remove quantifiers from the consequent. These rules can be derived by rewriting the implication ${\displaystyle \phi \rightarrow \psi }$ as ${\displaystyle \lnot \phi \lor \psi }$ and applying the rules for disjunction and negation above. As with the rules for disjunction, these rules require that the variable quantified in one subformula does not appear free in the other subformula.

The rules for removing quantifiers from the antecedent are (note the change of quantifiers):

${\displaystyle (\forall x\phi )\rightarrow \psi }$ is equivalent to ${\displaystyle \exists x(\phi \rightarrow \psi )}$ (under the assumption that ${\displaystyle \exists x\top }$),

${\displaystyle (\exists x\phi )\rightarrow \psi }$ is equivalent to ${\displaystyle \forall x(\phi \rightarrow \psi )}$Zdroj:https://en.wikipedia.org?pojem=Prenex_normal_form
Text je dostupný za podmienok Creative Commons Attribution/Share-Alike License 3.0 Unported; prípadne za ďalších podmienok. Podrobnejšie informácie nájdete na stránke Podmienky použitia.

---