Overview
The universal quantifier turns a claim about an unspecified object into a claim about every object in a domain. It is written , read “for all.” Many mathematical theorems have this shape, even when prose hides the symbol. Stating the domain and the position of other quantifiers is part of stating the theorem correctly.
Prerequisites
Understand predicates, variables, and implication. A structure supplies a domain and meanings for function and relation symbols. Free variables receive values from an assignment; bound variables are controlled by quantifiers. These distinctions prevent an assertion about a chosen example from being mistaken for a general law.
Definition and conventions
For a first-order structure with nonempty domain and an assignment ,
The assignment changes only the value of . Use parentheses to specify scope. Restricted notation abbreviates in a language where that membership condition is meaningful. An empty restricting set therefore makes this statement true, even though ordinary first-order structures here have nonempty domains.
Intuition
A universal assertion survives every permitted challenge. An opponent chooses the input; the argument must handle it without imposing extra conditions. A proof beginning “let be arbitrary” expresses exactly this obligation. Arbitrary does not mean randomly sampled, nor does it mean selected because it has a convenient special property.
Examples and non-examples
For every integer , the product is even: one of two consecutive integers is even, and multiplication preserves divisibility by two. This is a proof for an arbitrary integer, rather than a check of a finite list. In contrast, fails at .
Over the integers, holds: after receiving , choose . The reversed statement fails. For it requires , while requires . A single witness cannot meet both requirements.
Important properties
Universal elimination substitutes a suitable term for the quantified variable, with substitution arranged to avoid capture. Universal introduction requires that the variable be absent from the undischarged assumptions on which the conclusion depends. From the temporary assumption , one cannot conclude that every equals zero.
Classically, negating a universal statement gives an existential counterexample: is equivalent to . This is why one explicit failure disproves a universal claim. Constructive logic treats some of these equivalences more cautiously.
Connections and further reading
Quantifier order distinguishes pointwise choices from uniform choices and appears throughout analysis and algebra. Read Logic and Proof, §7.2–§7.3 for proof rules and §10.2 for semantics. Yang’s slides, PDF pages 17–20 independently document the Chinese terminology.