Prenex normal form

A <a href="/facts/Formula_(mathematical_logic)/YpTVlzuj">formula</a> of the <a href="/facts/Predicate_calculus/lcISqWIg">predicate calculus</a> is in prenex <a href="/facts/Normal_form_(abstract_rewriting)/JERru3Fx">normal form</a> (PNF) if it is <a href="/facts/Rewriting/9PHlnnnJ">written</a> as a string of <a href="/facts/Quantifier_(logic)/bgmvwxoo">quantifiers</a> and <a href="/facts/Bound_variable/ndWnXXYs">bound variables</a>, called the prefix, followed by a quantifier-free part, called the matrix. Together with the normal forms in <a href="/facts/Propositional_calculus/MNt5v31V">propositional logic</a> (e.g. <a href="/facts/Disjunctive_normal_form/hsw2pRPu">disjunctive normal form</a> or <a href="/facts/Conjunctive_normal_form/B3sY1lTW">conjunctive normal form</a>), it provides a <a href="/facts/Canonical_normal_form/SSb88ExW">canonical normal form</a> useful in <a href="/facts/Automated_theorem_proving/vKGvuKFI">automated theorem proving</a>. 
Every formula in <a href="/facts/Classical_logic/ls62MAms">classical logic</a> is <a href="/facts/Logically_equivalent/ysCWmsxA">logically equivalent</a> 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.

Prenex normal form open-in-new

Prenex normal form