2.12 Universal Quantifiers

A universal statement asserts that a property holds for every element of a type. In Lean, a proof of a universally quantified statement is a function that takes an arbitrary element and returns a proof of the property for that element.

The usual notation:

∀ x : α, P x

is implemented as a dependent function type.

Problem

You want to prove or use a statement of the form:

∀ x : α, P x

To prove it, introduce an arbitrary element x and prove P x. To use it, apply the function to a specific argument.

Solution

Use intro to introduce the quantified variable.

theorem forall_example
    (α : Type)
    (P : α -> Prop)
    (a : α)
    (ha : ∀ x : α, P x) :
    P a := by
  exact ha a

The hypothesis ha is a function. Applying it to a produces a proof of P a.

To prove a universal statement:

theorem forall_intro_example
    (α : Type)
    (P : α -> Prop) :
    (∀ x : α, P x) -> (∀ x : α, P x) := by
  intro h
  intro x
  exact h x

After intro x, the goal becomes:

⊢ P x

where x is arbitrary.

Discussion

A universal quantifier behaves like a function:

∀ x : α, P x

is equivalent to:

(x : α) -> P x

The difference is that the result type depends on the input. The expression P x changes as x changes.

Proving Universals

To prove:

⊢ ∀ x : α, P x

introduce a variable:

intro x

and then prove:

⊢ P x

Example:

theorem forall_identity
    (α : Type) :
    ∀ x : α, x = x := by
  intro x
  rfl

The proof works for any x, so it works for all x.

Using Universals

If you have:

h : ∀ x : α, P x

then:

h a

is a proof of P a.

theorem forall_use
    (α : Type)
    (P : α -> Prop)
    (h : ∀ x : α, P x)
    (a : α) :
    P a := by
  exact h a

This is direct function application.

Multiple Quantifiers

Multiple universal quantifiers introduce multiple variables.

theorem forall_two_variables
    (α : Type)
    (P : α -> α -> Prop) :
    (∀ x y : α, P x y) -> (∀ a b : α, P a b) := by
  intro h
  intro a b
  exact h a b

The type:

∀ x y : α, P x y

means:

∀ x : α, ∀ y : α, P x y

Each variable is introduced in order.

Combining Universals and Implications

Universal quantifiers often appear with implications.

theorem forall_implication
    (α : Type)
    (P Q : α -> Prop) :
    (∀ x : α, P x -> Q x) ->
    (∀ x : α, P x) ->
    (∀ x : α, Q x) := by
  intro hPQ
  intro hP
  intro x
  exact hPQ x (hP x)

The structure is:

Introduce both hypotheses
Introduce an arbitrary x
Apply both functions at x

Dependent Behavior

The key feature of ∀ is that the property depends on the chosen value.

theorem dependent_example
    (n : Nat) :
    ∀ m : Nat, m + 0 = m := by
  intro m
  simp

The property:

m + 0 = m

depends on m.

Universals with Equality

Universal quantifiers are often used to state algebraic laws.

theorem add_zero_all :
    ∀ n : Nat, n + 0 = n := by
  intro n
  simp

This says that the identity holds for all natural numbers.

Using it:

theorem use_add_zero_all
    (h : ∀ n : Nat, n + 0 = n)
    (k : Nat) :
    k + 0 = k := by
  exact h k

Universals and Existentials

A universal statement can produce an existential statement.

theorem forall_to_exists
    (α : Type)
    (P : α -> Prop)
    (h : ∀ x : α, P x)
    (a : α) :
    ∃ x : α, P x := by
  use a
  exact h a

The universal property guarantees that any chosen witness satisfies the predicate.

Universals Over Propositions

Universal quantification also applies to propositions.

theorem forall_prop_identity :
    ∀ P : Prop, P -> P := by
  intro P
  intro hp
  exact hp

Here the variable P ranges over propositions, not data.

Term Form

A universal proof is a function.

theorem forall_term
    (α : Type) :
    ∀ x : α, x = x :=
  fun x => rfl

The lambda abstraction corresponds directly to intro.

Special Case: Nondependent Functions

If the property does not depend on the variable, the universal reduces to a simple function type.

theorem forall_nondependent
    (α : Type)
    (P : Prop) :
    (∀ _ : α, P) -> P := by
  intro h
  exact h arbitrary

Here the variable is unused in the predicate.

Common Patterns

To prove:

⊢ ∀ x : α, P x

use:

intro x

then prove:

⊢ P x

To use:

h : ∀ x : α, P x

use:

h a

To handle multiple variables:

intro x y

To combine with implications:

hPQ x (hP x)

Common Pitfalls

Do not forget to introduce the quantified variable. Without intro, the goal cannot be reduced.

Do not assume a specific value for x. The proof must work for an arbitrary element.

Do not confuse ∀ x, P x with a conjunction over all elements. It is a function, not a finite collection of proofs.

Do not forget that the result type depends on the input. Each application produces a different proposition.

Takeaway

A universal statement is a dependent function. To prove ∀ x, P x, introduce an arbitrary x and prove P x. To use it, apply the function to a specific value. This correspondence between quantifiers and functions is a central pattern in Lean.