nLab axiom of replacement

Idea

Zwei äquivalente Vielheiten sind entweder beide ‘Mengen’ oder beide inkonsistent. Georg Cantor (1899)¹

Axioms of collection and replacement are axiom schemata in set theory that permit to construct new sets from other already given sets, thereby contributing substantially to the size of the set-theoretic universe, and hence are seen as ‘strong’ foundational axioms.

The most famous of these axiom schemata is the axiom of replacement² of Zermelo-Fraenkel set theory that was suggested by A. Fraenkel and formulated by T. Skolem in 1922. Given a unary operation $F$ and a set $x$ it permits to collect all $F(y)$ for $y\in x$ into a new set.

The resulting expansiveness of the set-theoretic universe is somewhat peripheral to the practice of ‘ordinary’ mathematics and therefore a structural set theory like ETCS can omit replacement without incurring a great loss³. Even in the context of a ZF-equivalent material set theory the axiom of replacement can be traded in for a reflection principle⁴.

Axioms of replacement and collection become useful, however, whenever recursively constructing a set that is ‘larger’ than any set known before:

what the axiom of replacement is mainly needed for in mathematical practice is to define families of sets indexed by some set $I$ carrying some inductive structure as, typically, the set $N$ of natural numbers.⁵

There are many variations on these axiom schemata, but any given system should only need one.

Statements

In general, these axioms apply to a binary relation that relates elements of one set $A$ to arbitrary sets. However, we do not expect that the relation itself be an object in the theory; really, we have an axiom schema with one axiom for every binary predicate of the proper form. We will write this predicate as $\phi(x,Y)$, where $x$ stands for an elment of $A$ and $Y$ stands for any set. (Note that there may well be other free variables in the predicate.)

Generally, $\phi$ will need to be an entire relation for the axiom to apply; that is, the axiom has as a hypothesis that, for every $x \in A$, there is some $Y$ such that $\phi(x,Y)$ holds. In versions called ‘replacement’ instead of ‘collection’, $\phi$ also needs to be functional; that is, the axiom has the hypothesis that, for every $x \in A$, there is a unique $Y$ such that $\phi(x,Y)$ holds. Thus, most of the ‘replacement’ versions only make sense if the language has a notion of equality of sets.

So much for the hypothesis of the axiom; the conclusion asserts the existence of a family of sets to which appropriate $Y$s belong. In a material set theory, we can simply state the existence of set $\mathcal{F}$ such that certain $Y \in \mathcal{F}$. In a structural set theory, we state the existence of an index set $I$, a total set $E$, and a function $f\colon E \to I$ such that each fibre $f^*(x)$ for $x \in I$ is equal to (or at least isomorphic to) certain $Y$. (Often we can take $I$ to be $A$, but that does not come into the statement of the axioms.)

Who wants to write out some of these?

• Bounded replacement or restricted replacement or $\Delta_0$-replacement: for any $\Delta_0$-formula $\phi(x, y)$, for any $a$, if for every $x \in a$ there exists a unique $y$ with $\phi(x, y)$, then the set $\{y \vert \exists x \in a.\phi(x, y)\}$ exists.

• Full replacement: for any formula $\phi(x, y)$, for any $a$, if for every $x \in a$ there exists a unique $y$ with $\phi(x, y)$, then the set $\{y \vert \exists x \in a.\phi(x, y)\}$ exists.

Lawvere on replacement

A question that has been much of a “foundational” interest, though of hardly any significance for the practice of algebra, topology, functional analysis, etc. is whether, for a given $T$, all imaginable families of sets parametrized by $T$ can be represented by $E\to T$ for some $E$ and some mapping; if “imaginable” is interpreted to mean “definable”, an affirmative answer to this question is essentially equivalent (for abstract, constant sets) to the postulation of the so-called “replacement schema”, whereas if $\mathcal{S}$ is considered as an object in some larger realm, an affirmative answer means that $\mathcal{S}$ itself has “inaccessible cardinality”. However, in view of practice and in view of the role of $\mathcal{S}$ as a limiting case of the general notion of continuously variable sets, it seems appropriate to simply define “an internal-to-$\mathcal{S}$ $T$-parametrized family of objects of $\mathcal{S}$” to mean just a morphism of $\mathcal{S}$ with domain $T$. Lawvere (1976, p.121)

See also the remarks on pages 721 and 727 of (Lawvere 2000).

Related discussion

• Thomas Streicher, William Lawvere, Colin McLarty et al, Categorical formulations of replacement, March 2008. (link)

• MO-discussion: Who needs Replacement anyway ? (link)

• Akihiro Kanamori (2012). In Praise of Replacement. The Bulletin of Symbolic Logic 18:1 (2012 March). pdf.

• $n$-category Cafe (2021), Large Sets 12 (Tom Leinster) and Large Sets 12.5 (Mike Shulman) – includes discussion of a number of different replacement axioms for ETCS and more general structural set theory.

Related entries

• Zermelo-Fraenkel set theory

• reflection principle

• axiom of choice

• ETCS, SEAR

• large cardinals

• type theoretic axiom of replacement

References

• J. L. Bell, M. Machover, A Course in Mathematical Logic, North-Holland Amsterdam 1977. (ch. 10, §5)

• Georg Cantor, Brief an Dedekind vom 22. Juli 1899, pp.443-447 in Cantor, Gesammelte Abhandlungen, Springer Berlin 1932. English transl. pp.113-117 of van Heijenoort (ed.), From Frege to Gödel , Harvard UP 1967.

• A. Fraenkel, Zu den Grundlagen der Cantor-Zermeloschen Mengenlehre, Math. Ann. 86 (1922) pp.230-237. (gdz)

• H. J. Friedman, Higher Set Theory and Mathematical Practice, Ann. Math. Logic 2 (1971) pp.326-357.

• André Joyal, Ieke Moerdijk, A categorical theory of cumulative hierarchies of sets, C. R. Math. Rep. Acad. Sci. Canada 13 (1991) pp.55-58.

• F. William Lawvere, Variable Quantities and Variable Structures in Topoi, pp.101-131 in Heller, Tierney (eds.), Algebra, Topology and Category Theory: a Collection of Papers in Honor of Samuel Eilenberg , Academic Press New York 1976.

• F. William Lawvere, Comments on the development of topos theory, pp.715-734 in Pier (ed.), Development of Mathematics 1950 - 2000 , Birkhäuser Basel 2000. (tac reprint)

• Colin McLarty, Exploring Categorical Structuralism, Phil. Math. 12 no.3 (2004) pp.37-53 doi:10.1093/philmat/12.1.37.

• D. A. Martin, Borel determinacy, Ann. Math. 102 (1975) pp.363-371.

• Gerhard Osius, Categorical Set Theory: A Characterization of the Category of Sets, JPAA 4 (1974) pp.79-119.

• Thoralf Skolem, Einige Bemerkungen zur axiomatischen Begründung der Mengenlehre, Mathematikerkongressen i Helsingfor 4-7 Juli 1922. English transl. pp.290-301 of van Heijenoort (ed.), From Frege to Gödel , Harvard UP 1967.

• Thomas Streicher, Universes in Toposes, pp.78-90 in Crosilla, Schuster (eds.), From Sets and Types to Topology and Analysis , Oxford UP 2005. (preprint)

• Paul Taylor, Practical Foundations of Mathematics, Cambridge UP 1999. (ch. 9)

• George Tourlakis, Lectures in Logic and Set Theory, Volume 2: Set Theory, Cambridge University Press (2003). (section III.8)

category: foundational axiom

---

1. ‘Two equivalent multiplicities either are both “sets” or are both inconsistent’, letter to Dedekind from 28th July 1899 (Cantor 1932, p.444). This is suggested as an early formulation of the axiom of replacement by van Heijenoort (1967, p.113). A categorical formalization of Cantor’s idea as an extension for ETCS is given in McLarty (2004). ↩

2. The term ‘replacement’, or ‘Ersetzungsaxiom’ in German, is apparently due to Fraenkel (1922) and was intended as a provisory terminology until the final formalization of Zermelo’s notion of a ‘definite property’ which was identified with a first-order formula in the language of set theory by Skolem in the same year (and independently earlier by H. Weyl). ↩

3. It is possible, however, to augment a categorical set theory with a version of replacement if necessary as shown in (Osius 1974, section 9) resulting in a system with the full strength of ZF. According to McLarty (2004), Osius’ ideas go back to discussions between Lawvere and the Berkeley logicians on reflection principles in 1963. McLarty’s paper proposes another equivalent way to flesh out replacement categorically! ↩

4. See Bell-Machover 1977, p.495. ↩

5. Thomas Streicher (2005, p.79). See there for further discussion of the role of replacement for mathematics beyond $V_{\omega +\omega}$ and the handling of similar iterated collection processes in toposes by universes. ↩