Axiom schema of replacement


In set theory, the axiom schema of replacement is a schema of axioms in Zermelo–Fraenkel set theory that asserts that the image of any set under any definable mapping is also a set. It is necessary for the construction of certain infinite sets in ZF.
The axiom schema is motivated by the idea that whether a class is a set depends only on the cardinality of the class, not on the rank of its elements. Thus, if one class is "small enough" to be a set, and there is a surjection from that class to a second class, the axiom states that the second class is also a set. However, because ZFC only speaks of sets, not proper classes, the schema is stated only for definable surjections, which are identified with their defining formulas.

Statement

Suppose is a definable binary relation such that for every set there is a unique set such that holds. There is a corresponding definable function, where if and only if. Consider the class defined such that for every set, if and only if there is an with. is called the image of under, and denoted or .
The axiom schema of replacement states that if is a definable class function, as above, and is any set, then the image is also a set. This can be seen as a principle of smallness: the axiom states that if is small enough to be a set, then is also small enough to be a set. It is implied by the stronger axiom of limitation of size.
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 language of set theory with free variables among ; but is not free in. In the formal language of set theory, the axiom schema is:
For the meaning of, see uniqueness quantification.
For clarity, in the case of no variables, this simplifies to:
So whenever specifies a unique -to- correspondence, akin to a function on, then all reached this way can be collected into a set, akin to.

Applications

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. 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.
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:
  • Using the modern definition due to von Neumann, proving the existence of any limit ordinal greater than requires the replacement axiom. The ordinal number is the first such ordinal. Indeed, the axiom of infinity asserts the existence of an infinite set. One may hope to define as the union of the sequence. However, arbitrary such classes of ordinals need not be sets; for example, the class of all ordinals is not a set. Replacement now allows one to replace each finite number in with the corresponding, and thus guarantees that this class is a set. As a clarification, note that one can easily construct a well-ordered set that is isomorphic to without resorting to replacement: simply take the disjoint union of two copies of, with the second copy greater than the first; however, that is not an ordinal since it is not totally ordered by inclusion.
  • Larger ordinals rely on replacement less directly. For example,, the first uncountable ordinal, can be constructed as follows: the set of countable well orders exists as a subset of by the axioms of separation and power set. Replace each well-ordered set with its ordinal. This is the set of countable ordinals, which can itself be shown to be uncountable. The construction uses replacement twice; once to ensure an ordinal assignment for each well ordered set and again to replace well ordered sets by their ordinals. This is a special case of the result of Hartogs number, and the general case can be proved similarly.
  • In light of the above, the existence of an assignment of an ordinal to every well-ordered set requires replacement as well. Similarly the von Neumann cardinal assignment, which assigns a cardinal number to each set requires replacement, as well as axiom of choice.
  • For sets of tuples recursively defined as and for large, the set has too high of a rank for its existence to be provable from set theory with just the axiom of power set, choice and without replacement.
  • Similarly, Harvey Friedman showed that at least some instances of replacement are required to show that Borel games are determined. The proven result is Donald A. Martin's Borel determinacy theorem. A later, more careful analysis by Martin of the result showed that it only requires replacement for functions with domain an arbitrary countable ordinal.
  • ZF proves the consistency of Z, as the set is a model of Z whose existence can be proved in ZF. The cardinal number is the smallest cardinal that can be shown to exist in ZF but not in Z. For clarification, note that 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.

    Relation to other axiom schemas

Simplifications

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.

Collection

The axiom schema of collection is closely related to and frequently confused with the axiom schema of replacement.
Over the remainder of the ZF axioms, it is equivalent to the axiom schema of replacement. The axiom of collection is stronger than replacement in the absence of the power set axiom 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.
While replacement can be read to say that the image of a given set under a function is also a set, collection speaks about images of relations and then merely says that some class whose relational preimage is a given set is also a set.
In other words, the resulting set has no minimality requirement, i.e. this variant also lacks the uniqueness requirement on.
That is, the relation defined by is not required to be a function—some may correspond to many 's in. In this case, the image set whose existence is asserted must contain at least one such for each in the original set, with no guarantee that it will contain only one.
Suppose that the free variables of are among ; but neither nor is free in. Then the axiom schema is:
The axiom schema is sometimes stated without prior restrictions on the predicate, :
In this case, there may be elements in that are not associated to any other sets by. However, the axiom schema as stated requires that, if an element of is associated with at least one set, then the image set will contain at least one such. The resulting axiom schema is also called the axiom schema of boundedness.

Separation

The axiom schema of separation, 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 separation includes
for each formula in the language of set theory in which is not free, i.e. that does not mention.
The proof is as follows: Either contains some element validating, or it does not. In the latter case, taking the empty set for fulfills the relevant instance of the axiom schema of separation and one is done. Otherwise, choose such a fixed in that validates. Now define for use with replacement. Using function notation for this predicate, it acts as the identity wherever is true and as the constant function wherever is false. By case analysis, the possible values are unique for any, meaning indeed constitutes a class function. In turn, the image of under, i.e. the class, is granted to be a set by the axiom of replacement. This precisely validates the axiom of separation.
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, 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 separation is not independent, it is sometimes omitted from contemporary statements of the Zermelo–Fraenkel axioms.
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. In the study of models of set theory, it is sometimes useful to consider models of ZFC without replacement, such as the models in the von Neumann hierarchy.
The proof given above assumes the law of excluded middle for the proposition that is inhabited by a set validating, and for any when stipulating that the relation is functional. The axiom of separation is explicitly included in constructive set theory, or a bounded variant thereof.

Reflection

Lévy's reflection principle for ZFC is equivalent to the axiom schema of replacement, assuming the axiom of infinity. Lévy's principle is as follows:
This is a schema that consists of countably many statements, one for each formula. Here, means with all quantifiers bounded to, i.e. but with every instance of and replaced with and respectively.