Axiom schema of replacement

is a definable binary relation (which may be a proper class) such that for every set

Because it is impossible to quantify over definable functions in first-order logic, one instance of the schema is included for each formula

In the formal language of set theory, the axiom schema is: For the meaning of

The axiom schema of replacement is not necessary for the proofs of most theorems of ordinary mathematics.

Indeed, Zermelo set theory (Z) 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.

At any rate, the axiom schema drastically increases the strength of ZF, both in terms of the theorems it can prove - for example the sets shown to exist - and also in terms of its proof-theoretic consistency strength, compared to Z.

Some important examples follow: Some simplifications may be made to the axiom schema of replacement to obtain different equivalent versions.

Azriel Lévy showed that a version of replacement with parameters removed, i.e. the following schema, is equivalent to the original form.

In particular the equivalence holds in the presence of the axioms of extensionality, pairing, union and powerset.

The axiom of collection is stronger than replacement in the absence of the power set axiom[2] or its constructive counterpart of ZF and is used in the framework of IZF, which lacks the law of excluded middle, instead of Replacement which is weaker.

Recall that the axiom schema of separation includes for each formula

This result shows that it is possible to axiomatize ZFC with a single infinite axiom schema.

Separation 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 separation, to ensure that its models contain a sufficiently rich collection of sets.

The proof given above assumes the law of excluded middle for the proposition that

The axiom of separation is explicitly included in constructive set theory, or a bounded variant thereof.

Lévy's principle is as follows:[4] This is a schema that consists of countably many statements, one for each formula

The axiom schema of replacement was not part of Ernst Zermelo's 1908 axiomatisation of set theory (Z).

The axiom was independently discovered and announced by Thoralf Skolem later in the same year (and published in 1923).

The phrase “Zermelo-Fraenkel set theory” was first used in print by von Neumann in 1928.

[8] Zermelo and Fraenkel had corresponded heavily in 1921; the axiom of replacement was a major topic of this exchange.

Zermelo first admitted to a gap in his system in a reply to Fraenkel dated 9 May 1921.

Fraenkel's 1922 publication thanked Zermelo for helpful arguments.

Zermelo was present at this meeting; in the discussion following Fraenkel's talk he accepted the axiom of replacement in general terms, but expressed reservations regarding its extent.

[7] Thoralf Skolem made public his discovery of the gap in Zermelo's system (the same gap that Fraenkel had found) in a talk he gave on 6 July 1922 at the 5th Congress of Scandinavian Mathematicians, which was held in Helsinki; the proceedings of this congress were published in 1923.

Skolem presented a resolution in terms of first-order definable replacements: "Let U be a definite proposition that holds for certain pairs (a, b) in the domain B; assume further, that for every a there exists at most one b such that U is true.

[7] Zermelo himself never accepted Skolem's formulation of the axiom schema of replacement.

[7] At one point he called Skolem's approach “set theory of the impoverished”.

Zermelo envisaged a system that would allow for large cardinals.

[9] He also objected strongly to the philosophical implications of countable models of set theory, which followed from Skolem's first-order axiomatization.