The Prenex Normal Form is about to
clean up Formulas so that Quantifiers are all bound to the same Variables need to be bound in in each single part to another Variable.
By doing this one has a unique Identification that a quantifier denotes a defined Variable and each Formula relates to a Quantifier.
The reason for doing the Prenex Normal form is to put all Quantifications in front of the Formula without losing its Connections to the Formula were the Quantifier is applied to.
( (∃X)( penguin(X) ∧ ¬blackandwhite(X) ) ∨ (∀X)(¬oldTVshow(X) ∨ ¬blackanwhite(X) ) ) ∨ (∃X)( penguin(X) ∧ oldTVshow(X) )
is transformed into
( (∃X)( penguin(X) ∧ ¬blackandwhite(X) ) ∨ (∀Y)( ¬oldTVshow(Y) ∨ ¬blackandwhite(Y) ) ) ∨ (∃Y)( penguin(Z) ∧ oldTVsow(Z) )
(∃X)(∀Y)(∃Z)(( penguin(X) ∧ ¬blackandhite(X) ) ∨ ( ¬oldTVshow(Y) ∨ ¬blackandwhite(Y) ) ) ∨ ( penguin(Z) ∧ oldTVshow(Z) )