Axiom Schema of Replacement - History and Philosophy

History and Philosophy

The axiom schema of replacement was not part of Ernst Zermelo's 1908 axiomatisation of set theory (Z); its introduction by Adolf Fraenkel in 1922 is what makes modern set theory Zermelo-Fraenkel set theory (ZF). The axiom was independently invented by Thoralf Skolem later in the same year. Although it is Skolem's final version of the axiom list that we use today, he usually gets no credit since each individual axiom was developed earlier by either Zermelo or Fraenkel.

The axiom schema of replacement drastically increases the strength of ZF, both in terms of the theorems it can prove and in terms of its proof-theoretic consistency strength, compared to Z. In particular, ZF proves the consistency of Z, as the set V_ω·2 is a model of Z constructible in ZF. (Gödel's second incompleteness theorem shows that each of these theories contains a sentence, "expressing" the theory's own consistency, that is unprovable in that theory, if that theory is consistent (this result is often loosely expressed as the claim that neither of these theories can prove its own consistency, if it is consistent, but the work of Solomon Feferman shows that care must be taken in stating the content of the second incompleteness theorem.) The cardinal number is the first one which can be shown to exist in ZF but not in Z.

The axiom schema of replacement is not necessary for the proofs of most theorems of ordinary mathematics. Indeed, Zermelo set theory already can interpret second-order arithmetic and much of type theory in finite types, which in turn are sufficient to formalize the bulk of mathematics. A notable mathematical theorem that requires the axiom of replacement to be proved in ZF is the Borel determinacy theorem.

The axiom of replacement does have an important role in the study of set theory itself. For example, the replacement schema is needed to construct the von Neumann ordinals from ω·2 onwards; without replacement, it would be necessary to find some other representation for ordinal numbers.

Although the axiom schema of replacement is a standard axiom in set theory today, it is often omitted from systems of type theory and foundation systems in topos theory.