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.