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’ axioms.
The most famous of these 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 and a set it permits to collect all for 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 I carrying some inductive structure as, typically, the set 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 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 , where stands for an elment of and stands for any set. (Note that there may well be other free variables in the predicate.)
Generally, will need to be an entire relation for the axiom to apply; that is, the axiom has as a hypothesis that, for every , there is some such that holds. In versions called ‘replacement’ instead of ‘collection’, also needs to be functional; that is, the axiom has the hypothesis that, for every , there is a unique such that 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 s belong. In a material set theory, we can simply state the existence of set such that certain . In a structural set theory, we state the existence of an index set , a total set , and a function such that each fibre for is equal to (or at least isomorphic to) certain . (Often we can take to be , but that does not come into the statement of the axioms.)
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 , all imaginable families of sets parametrized by can be represented by for some 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 is considered as an object in some larger realm, an affirmative answer means that itself has “inaccessible cardinality”. However, in view of practice and in view of the role of as a limiting case of the general notion of continuously variable sets, it seems appropriate to simply define “an internal-to- -parametrized family of objects of ” to mean just a morphism of with domain . Lawvere (1976, p.121)
See also the remarks on pages 721 and 727 of (Lawvere 2000).
Streicher, Lawvere, McLarty et al, Categorical formulations of replacement , 2008. (link)
MO-discussion: Who needs Replacement anyway ? (link)
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.
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.
Colin McLarty, Exploring Categorical Foundations , Phil. Math. 12 no.3 (2004) pp.37-53.
Gerhard Osius, Categorical Set Theory: A Characterization of the Category of Sets , JPAA 4 (1974) pp.79-119.
D. A. Martin, Borel determinacy , Ann. Math. 102 (1975) pp.363-371.
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.
George Tourlakis, Lectures in Logic and Set Theory, Volume 2: Set Theory, Cambridge University Press (2003). (section III.8)
‘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). ↩
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). ↩
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! ↩