Questions: Prenex Normal Form

Question 1

Which of the following formulas is in prenex normal form?

• A. ∀x (P(x) → ∃y Q(x, y))
• B. ∃y ∀x (P(x) → Q(x, y))
• C. ∀x (∃y P(y) ∧ Q(x))
• D. (∀x P(x)) ∧ (∃y Q(y))

Answer: (B)

Prenex normal form requires all quantifiers to appear at the front in a single uninterrupted prefix, followed by a quantifier-free matrix. Option B (∃y ∀x (P(x) → Q(x, y))) satisfies this: the prefix is '∃y ∀x' and the matrix is 'P(x) → Q(x, y)', which contains no quantifiers. Options A and C have quantifiers nested inside connectives. Option D has two separate quantifier blocks interrupted by the ∧ — the prefix is not contiguous.

Question 2

When converting ∀x P(x) ∧ ∃x Q(x) to prenex normal form, why must you rename one of the bound variables before pulling both quantifiers to the front?

• A. Because PNF only allows one quantifier per formula
• B. Because ∀ and ∃ quantifiers cannot appear in the same prefix
• C. Because both quantifiers use the variable name x — pulling them both to the front without renaming would cause the single prefix variable x to be bound by both quantifiers simultaneously, creating ambiguity
• D. Because PNF requires all variables to appear in alphabetical order in the prefix

Answer: (C)

The two x's are separate bound variables that happen to share a name. They bind independently in the original formula (∀x P(x) quantifies over P; ∃x Q(x) quantifies over Q). If you write ∀x ∃x (P(x) ∧ Q(x)) without renaming, the inner ∃x overwrites the ∀x binding, changing the formula's meaning. Alpha-renaming — replacing one of the x's with a fresh variable z — separates the two binding contexts so both quantifiers can safely share the prefix: ∀x ∃z (P(x) ∧ Q(z)).

Question 3

Every first-order formula can be converted to a logically equivalent formula in prenex normal form.

• T. True
• F. False

Answer: True

True. There are systematic equivalences (prenex laws) for migrating each quantifier outward through every logical connective: through ∧, ∨, ¬, and →, with alpha-renaming applied whenever a variable conflict would arise. These rules can be applied repeatedly until all quantifiers reach the front. The resulting PNF formula is logically equivalent to the original (not just equisatisfiable — it has the same truth value in every interpretation).

Question 4

A formula in prenex normal form whose prefix consists mostly of universal quantifiers (∀x ∀y ∀z ...) is logically equivalent to one whose prefix consists mostly of existential quantifiers, as long as the matrix is the same.

• T. True
• F. False

Answer: False

False — the quantifier type profoundly changes the formula's meaning. ∀x P(x) asserts P holds for every element of the domain; ∃x P(x) asserts it holds for at least one. These have opposite truth conditions and cannot be made equivalent by changing only the prefix. The alternation pattern (which quantifiers are ∀ and which are ∃) determines the logical content of the formula and its position in the arithmetical hierarchy.

Question 5

Why is prenex normal form a necessary preprocessing step before Skolemization, rather than something Skolemization could be applied to directly on the original formula?

Model answer: Skolemization eliminates existential quantifiers by replacing ∃y with a Skolem function symbol that depends on all universally quantified variables appearing to the left of ∃y in the prefix. This 'left of' relationship only makes sense when quantifiers are in a linear prefix order. In a formula where existentials and universals are interleaved inside connectives — e.g., ∀x (P(x) → ∃y Q(x,y)) — there is no clear prefix, and it's ambiguous which universals govern which existentials. PNF resolves this by creating an explicit ordered prefix, making the dependency structure of each existential on surrounding universals unambiguous.

The Skolem function for ∃y must encode all the universal variables that y might depend on. In PNF ∀x ∃y φ, y depends on x, so the Skolem function is f(x). Without PNF, this dependency chain cannot be read off mechanically, making automated Skolemization error-prone.