nLab axiom of replacement

Axioms of replacement and collection




The basis of it all

 Set theory

set theory

Foundational axioms

foundational axioms

Removing axioms

Axioms of replacement and collection


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

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 replacement2 of Zermelo-Fraenkel set theory that was suggested by A. Fraenkel and formulated by T. Skolem in 1922. Given a unary operation FF and a set xx it permits to collect all F(y)F(y) for yxy\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 loss3. Even in the context of a ZF-equivalent material set theory the axiom of replacement can be traded in for a reflection principle4.

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 II carrying some inductive structure as, typically, the set NN of natural numbers.5

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


In general, these axioms apply to a binary relation that relates elements of one set AA 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 ϕ(x,Y)\phi(x,Y), where xx stands for an elment of AA and YY 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 xAx \in A, there is some YY such that ϕ(x,Y)\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 xAx \in A, there is a unique YY such that ϕ(x,Y)\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 YYs belong. In a material set theory, we can simply state the existence of set \mathcal{F} such that certain YY \in \mathcal{F}. In a structural set theory, we state the existence of an index set II, a total set EE, and a function f:EIf\colon E \to I such that each fibre f *(x)f^*(x) for xIx \in I is equal to (or at least isomorphic to) certain YY. (Often we can take II to be AA, 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 Δ 0\Delta_0-replacement: for any Δ 0\Delta_0-formula ϕ(x,y)\phi(x, y), for any aa, if for every xax \in a there exists a unique yy with ϕ(x,y)\phi(x, y), then the set {y|xa.ϕ(x,y)}\{y \vert \exists x \in a.\phi(x, y)\} exists.

  • Full replacement: for any formula ϕ(x,y)\phi(x, y), for any aa, if for every xax \in a there exists a unique yy with ϕ(x,y)\phi(x, y), then the set {y|xa.ϕ(x,y)}\{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 TT, all imaginable families of sets parametrized by TT can be represented by ETE\to T for some EE 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} TT-parametrized family of objects of 𝒮\mathcal{S}” to mean just a morphism of 𝒮\mathcal{S} with domain TT. Lawvere (1976, p.121)

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


  • 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)

  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 ω+ωV_{\omega +\omega} and the handling of similar iterated collection processes in toposes by universes.

Last revised on November 13, 2022 at 04:31:42. See the history of this page for a list of all contributions to it.