The axioms There are many equivalent formulations of the ZFC axioms; for a rich but somewhat dated discussion of this fact, see Fraenkel et al. (1973). The following particular axiom set is from Kunen (1980). The axioms per se are expressed in the symbolism of first order logic. The associated English prose is only intended to aid the intuition. All formulations of ZFC imply that at least one set exists. Kunen includes an axiom, in addition to the following, which directly asserts the existence of a set. Many authors require a nonempty domain of discourse as part of the semantics of the first-order logic in which ZFC is formalized. The axiom of infinity (below) also asserts that at least one set exists, as it begins with an existential quantifier. 1. Axiom of extensionality: Two sets are equal (are the same set) if they have the same elements.
The converse of this axiom follows from the substitution property of equality. If the background logic does not include equality "=", x=y may be defined as an abbreviation for the following formula (Hatcher 1982, p. 138, def. 1):
In this case, the axiom of extensionality can be reformulated as
which says that if x and y have the same elements, then they belong to the same sets (Fraenkel et al. 1973). 2. Axiom of regularity (also called the Axiom of foundation): Every non-empty set x contains a member y such that x and y are disjoint sets.
3. Axiom schema of specification (also called the axiom schema of separation or of restricted comprehension): If z is a set, and is any property which may characterize the elements x of z, then there is a subset y of z containing those x in z which satisfy the property. The "restriction" to z is necessary to avoid Russell's paradox and its variants. More formally, let
be any formula in the language of ZFC with free variables among
.
So y is not free in . Then:
This axiom is part of Z, but can be redundant in ZF, in that it may follow from the axiom schema of replacement, with (as here) or without the axiom of the empty set. The axiom of specification can be used to prove the existence of the empty set, denoted , once the existence of at least one set is established (see above). A common way to do this is
to use an instance of specification for a property which all sets do not have. For example, if w is a set which already exists, the empty set can be constructed as . If the background logic includes equality, it is also possible to define the empty set as . Thus the axiom of the empty set is implied by the nine axioms presented here. The axiom of extensionality implies the empty set is unique, if it exists. It is common to make a definitional extension that adds the symbol
to the language of ZFC.
4. Axiom of pairing: If x and y are sets, then there exists a set which contains x and y as elements.
This axiom is part of Z, but is redundant in ZF because it follows from the axiom schema of replacement applied to any two-member set. The existence of such a set is assured by either the axiom of infinity, or by the axiom of the power set applied twice to the empty set. 5. Axiom of union: For any set
there is a set A containing every set that is a member of
some member of
6. Axiom schema of collection: Let
be any formula in the language of ZFC whose free
variables are among
. So B is not free in
.
is a quantifier binding
y, meaning that exactly one exists, up to equality. Then:
Less formally, this axiom states that if the domain of a function f is a set, and f(x) is a set for any x in that domain, then the range of f is a subclass of a set, subject to a restriction needed to avoid paradoxes.
7. Axiom of infinity: Let
abbreviate
set X such that the empty set
is a member of X and, whenever a set y is a member of X, then
is also a member of X.
, where is some set. Then there exists a
More colloquially, there exists a set X having infinitely many members. The minimal set X satisfying the axiom of infinity is the von Neumann ordinal ω.
8. Axiom of power set: Let abbreviate For any set x, there is a set y which is a superset of the power set of x. The power set of x is the class whose members are all of the subsets of x.
Alternative forms of axioms 1–8 are often encountered, some of which are listed in Jech (2003). Some ZF axiomatizations include an axiom asserting that the empty set exists. The axioms of pairing, union, replacement, and power set are often stated so that the members of the set x whose existence is being asserted, are just those sets which the axiom asserts x must contain. 9. Well-ordering theorem: For any set X, there is a binary relation R which well-orders X. This means R is a linear order on X such that every nonempty subset of X has a member which is minimal under R.
Given axioms 1-8, there are many statements provably equivalent to axiom 9, the best known of which is the axiom of choice (AC), which goes as follows. Let X be a set whose members are all non-empty. Then there exists a function f, called a "choice function," whose domain is X, and whose range is a set, called the "choice set," each member of which is a single member of each member of X. Since the existence of a choice function when X is a finite set is easily proved from axioms 1-8, AC only matters for certain infinite sets. AC is characterized as nonconstructive because it asserts the existence of a choice set but says nothing about how the choice set is to be "constructed." Much research has sought to characterize the definability (or lack thereof) of certain sets whose existence AC asserts.