Foundation·F09
Universal quantifier
For all x: instantiate at any term, prove at an arbitrary one.
Elimination instantiates: what holds of everything holds of any particular term
. Introduction generalizes: if
was derived using no assumption about
, conclude
.
Part of the logical framework beneath ZFC (classical first-order logic with equality): taken as given rather than proven, it belongs to the language the set-theoretic axioms are stated in.
Remarks
"Arbitrary" is a precise side condition:
must not occur free in any assumption the derivation of
still depends on. That condition is the entire content of the phrase "let
be arbitrary" that opens so many proofs. Elimination has fine print of its own: the term
must be free for
in
, that is, substituting
must not place any variable of
under a quantifier that captures it; otherwise instantiating
at
would yield the absurd
. The same condition governs the
premise of existential introduction in the existential quantifier. In ZFC the quantifiers range over sets: everything in the universe of discourse is a set. Like implication, the universal quantifier is primitive rather than defined (see the logical framework); in Lean it is the dependent function type, and a proof of
is a function assigning to each
a proof of
.
Used by
Propose an edit3 published revisions
- 7/12/2026 · Benjamin· Remove the In words reading and its highlight markup: this article states two inference rules, not a single formula with a natural plain-English translation.what changed →
- 7/12/2026 · Benjamin· Rewrite the In words reading with clearer introduction/elimination phrasing.what changed →
- 7/11/2026 · Benjamin· Logic layer: connectives and quantifierswhat changed →