A note on the size of prenex normal forms

• Prenex normal forms (PNF) of logical sentences are often used computational logic.
• Converting to PNF with the standard method can lead to exponentially larger formulas.
• We show that the conversion is possible with polynomial growth.

The textbook method for converting a first-order logic formula to prenex normal form potentially leads to an exponential growth of the formula size, if the formula is allowed to use all of the classical logical connectives ∧, ∨, →, ↔, ¬. This note presents a short proof which shows that the conversion is possible with polynomial growth of the formula size.