Predicate Logic

Quantifiers, variable binding, and prenex normal form

Predicate Logic

Predicate logic (first-order logic) extends propositional logic with variables, predicates, and quantifiers. The universal quantifier ∀ ("for all") and existential quantifier ∃ ("there exists") let us make statements about elements of a domain. This is the language of mathematics itself.

In this lesson, you will evaluate quantified formulas over a small universe, visualize variable binding, and convert formulas to prenex normal form.

Quantifier Playground

Quantifiers range over a domain of discourse. In a small universe, we can check ∀x P(x) by testing every element and ∃x P(x) by finding just one. The order of quantifiers matters: ∀x ∃y and ∃y ∀x can have very different meanings.

Universe = {1, 2, 3, 4, 5, 6, 7, 8}12345678P(x) = "x is even"Satisfying: {2, 4, 6, 8} (4/8)∀x P(x) = FALSE∃x P(x) = TRUE

Blue highlights mark elements satisfying the predicate. Grid cells show where the relation holds for each (x, y) pair.

Key insight: ∀x ∃y (x < y) says "every element has something bigger" -- true in infinite sets but also in finite ones depending on the predicate. Swapping quantifier order changes meaning fundamentally.

Variable Binding

In ∀x P(x, y), the variable x is bound by the quantifier and y is free. A formula with free variables is like a template -- it becomes a statement only when the free variables are assigned values or bound by quantifiers. Understanding binding is essential for avoiding logical errors.

Variable Binding Visualizer∀x (P(x) → Q(x))Bound variableFree variableFree variables: {∅}Bound variables: {x}✓ Formula is closed (a sentence) — has a definite truth value

Arcs connect each bound variable to its quantifier. Free variables (red) have no binding quantifier.

Key insight: A sentence (closed formula) has no free variables and is either true or false in a given structure. A formula with free variables defines a relation on the domain.

Prenex Normal Form

Any first-order formula can be converted to prenex normal form: all quantifiers at the front, followed by a quantifier-free body. This requires renaming variables to avoid capture and flipping quantifiers when moving past negations (¬∀x becomes ∃x¬).

Prenex Normal Form Conversion1.¬∀x P(x)
Step 1 / 2

Key insight: Prenex form separates the quantifier prefix (the "structure" of a formula) from the matrix (the propositional core). The prefix pattern (∀∃∀...) determines the formula's complexity in the arithmetical hierarchy.

Key Takeaways

  • Predicate logic adds variables, predicates, and quantifiers to propositional logic.
  • Quantifier order matters: ∀∃ and ∃∀ are fundamentally different.
  • Bound variables are placeholders; free variables make a formula into a relation.
  • Prenex normal form puts all quantifiers first, revealing the formula's logical complexity.