Predicate Logic

Quantifiers, variable binding, and prenex normal form

Predicate Logic

Quantifiers let logic say "for all" and "there exists," which is enough to write down almost all of mathematics. Test them on the numbers 1 to 8.

Quantifier Playground

Pick a predicate or a formula and see which of the numbers 1 to 8 make it true. Then compare ∀x ∃y (x < y) with ∃y ∀x (x ≤ y): swapping the quantifiers changes the answer.

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.

Go deeper:Quantifiers and their order

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.

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.

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

Pick a formula and see which quantifier binds each variable. Any variable no quantifier reaches is free.

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.

Go deeper:Bound and free variables

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.

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

Pick an example and step through the conversion. Watch the quantifiers move to the front, getting renamed or flipped as they pass a negation.

Prenex Normal Form Conversion1.¬∀x P(x)
Step 1 / 2
Go deeper: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¬).

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.

Spot a mistake or have an idea?

Search