What exactly is prenex normal form (PNF)?

In the study of formal logic, the idea of normalization is a pretty useful one. It simply means to reduce a given logical expression into an equivalent or refined form which is based on a given structure and/or set of symbols.

Basically, normalization brings consistency in the specification of logical expressions. Normalization ensures that different expressions are represented in the same manner.

In predicate logic, a well-known normalization is called the prenex normal form (PNF). In this article, I'll show you exactly what it is, how to convert a predicate logic expression into PNF, and its larger application to computational logic and automated theorem provers.

What is prenex normal form?

Prenex normal form (PNF) is a normalization employed in predicate logic (or first-order logic). The main idea is to take all quantifiers to the left end of the expression. For example, consider the following:

This is NOT in prenex normal form. Why? you ask. Because all the quantifiers are not at the beginning. Here's the equivalent expression in PNF:

Both the ::\forall x:: and ::\forall y:: quantifiers are now at the left side and therefore the expression is in prenex normal form. In general, PNF can be expressed as:

where each one of ::Q_1::, ::Q_2::, ..., ::Q_n:: represents a universal quantifier or an existential quantifier, and ::P(x_1, x_2, ..., x_n):: denotes a predicate without any quantifiers (sometimes referred to as being a quantifier-free predicate).

There is an interesting theorem that states that any logical expression can be written equivalently in PNF.

How to convert to PNF?

Converting to PNF isn't a difficult thing to do if you are well-versed with equivalences in propostional logic, De Morgan laws for quantifiers, and some equivalences related to quantifiers. Once you know these basics, converting any expression in PNF involves a couple of simple steps.

• Remove any negation (::\neg::) by taking it inwards.
• Take quantifiers to the left side based on simple equivalences in quantifiers.

Let me show you some examples.

First, the same example as the one shown above:

It's easy to reason that this expression would be exactly the same if the quantifiers are all brought to the left side. Here's its PNF:

Now, consider the following:

Converting this to PNF is easy because the ::\exists y:: quantifier can be take:

As another example, consider the following, where ::A:: denotes a proposition containing no quantifiers:

To convert this to PNF, first let's take the negation inwards:

And now, it's just a matter of bringing the existential quantifier outside:

The application of PNF

It's all good to know what is PNF and how to convert to it but what exactly is the purpose of this normalization? Is it just an interesting, abstract theory or some practical prerequisite for something much bigger and practical.

Well, it's indeed the latter — PNF is highly practical. PNF is a prerequisite for the more computationally useful Skolem normal form.

Without delving too much into its details, Skolemization — the process of converting an expression into Skolem normal form — takes a PNF expression and removes all existential quantifiers from it and replaces the existentially-quantified variables with a function, called the Skolem function.

For example, the PNF expression

would become the following after Skolemization:

Here, ::f(x):: is the Skolem function, which depends on the value of ::x:: (which comes from the fact that the original statement states that For every ::x::, there is some ::y::; in other words, every ::x:: has a corresponding ::y::).

This Skolem normal form is in turn used in automatic theorem provers — like Vampire or Prover9 — because removing the existential quantifier makes working with the expression easier algorithmically.