Axiom Schema of Replacement - Relation To The Axiom Schema of Specification

Relation To The Axiom Schema of Specification

The axiom schema of specification, the other axiom schema in ZFC, is implied by the axiom schema of replacement and the axiom of empty set. Recall that the axiom schema of specification includes

for each formula θ in the language of set theory in which B is not free.

The proof is as follows. Begin with a formula θ(C) that does not mention B, and a set A. If no element E of A satisfies θ then the set B desired by the relevant instance of the axiom schema of separation is the empty set. Otherwise, choose a fixed E in A such that θ(E) holds. Define a class function F such that F(D) = D if θ(D) holds and F(D) = E if θ(D) is false. Then the set B = F "A = A∩{x|θ(x)} exists, by the axiom of replacement, and is precisely the set B required for the axiom of specification.

This result shows that it is possible to axiomatize ZFC with a single infinite axiom schema. Because at least one such infinite schema is required (ZFC is not finitely axiomatizable), this shows that the axiom schema of replacement can stand as the only infinite axiom schema in ZFC if desired. Because the axiom schema of specification is not independent, it is sometimes omitted from contemporary statements of the Zermelo-Fraenkel axioms.

Specification is still important, however, for use in fragments of ZFC, because of historical considerations, and for comparison with alternative axiomatizations of set theory. A formulation of set theory that does not include the axiom of replacement will likely include some form of the axiom of specification, to ensure that its models contain a robust collection of sets. In the study of models of set theory, it is sometimes useful to consider models of ZFC without replacement.

The proof above uses the law of excluded middle in assuming that if A is nonempty then it must contain an element (in intuitionistic logic, a set is "empty" if it does not contain an element, and "nonempty" is the formal negation of this, which is weaker than "does contain an element"). The axiom of specification is included in intuitionistic set theory.