Home > Axiom schema of replacement
2 Relation to the axiom schema of specification
The axiom schema of specification can almost be derived from the axiom schema of replacement.
First, recall this axiom schema:
-
for any predicate P in one variable that doesn't use the symbol B.
Given such a predicate P, define the mapping F by F(D) = D if P(D) is true and F(D) = E if P(D) is false, where E is any member of A such that P(E) is true.
Then the set B guaranteed by the axiom of replacement is precisely the set B required for the axiom of specification.
The only problem is if no such E exists.
But in this case, the set B required for the axiom of specification is the empty set, so the axiom schema follows in general using also the axiom of empty set.
For this reason, the axiom schema of specification is often left out of modern lists of the Zermelo-Fraenkel axioms.
However, specification is still important for historical considerations, and for comparison with alternative axiomatisations of set theory.
For example, the argument above used the law of excluded middle, so specification can't be left out of an intuitionistic set theory.
And any formulation of set theory that excludes replacement as unnecessary certainly will want to keep specification.
