Prenex Normal Form

Mathematical Logic · Axiom Academy

Converting formulas to a standard form with all quantifiers at the front 1. What is Prenex Normal Form? A formula is in prenex normal form if it has the structure Q₁x₁ Q₂x₂ ... Qₙxₙ M, where each Qᵢ is a quantifier (∀ or ∃) and M is a quantifier-free formula called the matrix. Prenex normal form provides several important advantages for working with first-order logic formulas. 3. Renaming Variables to Avoid Capture Before moving quantifiers, we must ensure that variable names don't clash. If a variable is bound by one quantifier and free in another part, we must rename to avoid variable capture. 4. Rules for Moving Quantifiers To convert a formula to prenex form, we use equivalence rules that allow us to move quantifiers outward past logical connectives. 5. Algorithm for Prenex Conversion Here is a systematic procedure for converting any first-order formula to prenex normal form. Eliminate implications and biconditionals: Rewrite φ → ψ as ¬φ ∨ ψ, and φ ↔ ψ as (φ → ψ) ∧ (ψ → φ) Move negations inward: Apply De Morgan's laws and quantifier negation rules until all negations are directly before atomic formulas Rename bound variables: Ensure each quantifier binds a uniquely named variable (no variable appears in two different quantifiers) Move quantifiers outward: Repeatedly apply the quantifier movement rules from step 4, moving quantifiers to the front from innermost to outermost Verify: Check that all quantifiers are at the front and the matrix is quantifier-free

This is the written version of the interactive lesson above. See the full Mathematical Logic course.