A formula of the predicate calculus is in prenex 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. 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 ϕ ( y ) {\displaystyle \phi (y)} , ψ ( z ) {\displaystyle \psi (z)} , and ρ ( x ) {\displaystyle \rho (x)} are quantifier-free formulas with the free variables shown then
∀ x ∃ y ∀ z ( ϕ ( y ) ∨ ( ψ ( z ) → ρ ( x ) ) ) {\displaystyle \forall x\exists y\forall z(\phi (y)\lor (\psi (z)\rightarrow \rho (x)))}
is in prenex normal form with matrix ϕ ( y ) ∨ ( ψ ( z ) → ρ ( x ) ) {\displaystyle \phi (y)\lor (\psi (z)\rightarrow \rho (x))} , while
∀ x ( ( ∃ y ϕ ( y ) ) ∨ ( ( ∃ z ψ ( z ) ) → ρ ( x ) ) ) {\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
Every first-order formula is logically equivalent (in classical logic) to some formula in prenex normal form. 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
( ∀ x ϕ ) ∧ ψ {\displaystyle (\forall x\phi )\land \psi } is equivalent to ∀ x ( ϕ ∧ ψ ) {\displaystyle \forall x(\phi \land \psi )} under (mild) additional condition ∃ x ⊤ {\displaystyle \exists x\top } , or, equivalently, ¬ ∀ x ⊥ {\displaystyle \lnot \forall x\bot } (meaning that at least one individual exists),
( ∀ x ϕ ) ∨ ψ {\displaystyle (\forall x\phi )\lor \psi } is equivalent to ∀ x ( ϕ ∨ ψ ) {\displaystyle \forall x(\phi \lor \psi )} ; and
( ∃ x ϕ ) ∧ ψ {\displaystyle (\exists x\phi )\land \psi } is equivalent to ∃ x ( ϕ ∧ ψ ) {\displaystyle \exists x(\phi \land \psi )} ,
( ∃ x ϕ ) ∨ ψ {\displaystyle (\exists x\phi )\lor \psi } is equivalent to ∃ x ( ϕ ∨ ψ ) {\displaystyle \exists x(\phi \lor \psi )} under additional condition ∃ x ⊤ {\displaystyle \exists x\top } . The equivalences are valid when x {\displaystyle x} does not appear as a free variable of ψ {\displaystyle \psi } ; if x {\displaystyle x} does appear free in ψ {\displaystyle \psi } , one can rename the bound x {\displaystyle x} in ( ∃ x ϕ ) {\displaystyle (\exists x\phi )} and obtain the equivalent ( ∃ x ′ ϕ [ x / x ′ ] ) {\displaystyle (\exists x'\phi [x/x'])} . For example, in the language of rings,
( ∃ x ( x 2 = 1 ) ) ∧ ( 0 = y ) {\displaystyle (\exists x(x^{2}=1))\land (0=y)} is equivalent to ∃ x ( x 2 = 1 ∧ 0 = y ) {\displaystyle \exists x(x^{2}=1\land 0=y)} , but
( ∃ x ( x 2 = 1 ) ) ∧ ( 0 = x ) {\displaystyle (\exists x(x^{2}=1))\land (0=x)} is not equivalent to ∃ x ( x 2 = 1 ∧ 0 = x ) {\displaystyle \exists x(x^{2}=1\land 0=x)}
… excerpt ends here. Continue reading the full article.
