Is axiom of replacement nicely stateable in the language of ETCS?

Question

ETCS has a nice category-theoretic formulation: "well-pointed topos with a natural numbers object and axiom of choice."

I'm too new to topoi to really understand all of what's going on, but I read that ETCS is weaker than ZFC and is missing the axiom of replacement. However, ETCS+R is the same strength as ZFC.

Maybe this is really just a question about aesthetics. Is there a nice category-theoretic way to express replacement?

Answer 1

You'll likely be interested in a discussion about replacement that happened in the category theory mailing list a few years ago. You can find it here. Just grep for "replacement" and you'll get to the right area in the email chain.

In particular, you'll likely be interested in Mike Shulman's question

What I would really like to know is, can one formulate an elementary property of a topos which does allow one to reproduce the standard arguments of Replacement?

which Colin McLarty answers as follows (minor mathjax related edits are mine):

Yes, What you do is start with ETCS, and adjoin an axiom scheme of replacement.

The axiom scheme says: Suppose a formula associates to each element $x$ of a set $S$ a set we may call $Sx$ (unique up to isomorphism). Then there is some function $f:X \to S$ such that the fiber of $f$ over each element $x$ is isomorphic to $Sx$.

Lawvere's ETCS plus this axiom scheme is intertanslateable in the obvious way with ZF, preserving theorems in both directions (you may include AxCh in both ETCS and ZF, or exclude it from both).

This has been known from the earliest days of categorical set theory. My favorite early published proof was stated slightly differently, using reflection rather than replacement, but it trivially comes to the same thing.

The "early published proof" he's referring to is Gerhard Osius's Logical and Set Theoretical Tools in Elementary Topoi. Later in the same email, he mentions his own paper Exploring Categorical Structuralism as a good reference for details on replacement (rather than reflection, as discussed in Osius's paper).

Even though I copied the relevant section here, there are many other interesting tidbits about replacement and other aspects of categorical set theory that you're likely to be interested in scattered throughout that email thread (it's also linked from the nlab page on replacement, which you might also be interested in). It's definitely worth a read!

---

I hope this helps ^_^

Answer 2

There are a number of equivalent (over ETCS) formulations of replacement in the posts Large Sets 12 and Large Sets 12.5 on the n-Category Café.

The first of these posts describes a formulation by Colin McLarty Exploring categorical structuralism (2004) (this is the one in HallaSurvivor's answer)

Axiom scheme of replacement Let $I$ be a set and $\Phi$ a functional formula on $I$. Then there exist a set $X$ and a function $p : X \to I$ such that $\Phi(i,p^{−1}(i))$ for all $i \in I$.

A functional formula here is almost a function, but only determines its values up to isomorphism. This axiom states that for such a formula, there is a set that collects all the values of the formula and a way of projecting from that set into the indexing set so that the inverse image at an index is the value of the formula at that index.

Large Sets 12.5 considers a number of other formulations of replacement. For some more context, you can read the linked post, but here's a quick rundown:

Gerhard Osius Categorical set theory: a characterization of the category of sets (1973):

If $\Phi(X,A,m,B)$ is a formula, where $X,A,B$ are set-variables and $m : A \to X$ is a function-variable, then for any set $X$ there exists a set $Y$ such that for any set $A$ and monomorphism $m : A \rightarrowtail X$, if there exists a set $B$ such that $\Phi(X,A,m,B)$, then there exists such a $B$ with $B \leq Y$.

This axiom expresses that for a relation between subsets of a given set and sets, there is a set large enough to contain the possible values of that relation.

F. William Lawvere An elementary theory of the category of sets (long version) with commentary (2005):

If $\Phi(A,B)$ is a formula with set-variables $A,B$ such that whenever $\Phi(A,B)$ and $\Phi(A,B′)$ we have $B \cong B′$, then for any set $X$ there exists a set $Y$ such that $X < Y$ and for any $A$ and $B$ with $A < Y$ and $\Phi(A,B)$, we have $B < Y$.

This versions says that for a functional formula, there are arbitrarily large sets so that if the inputs are restricted to be smaller than that set, the outputs are smaller too.

J. C. Cole. Categories of sets and models of set theory (1971):

If $\Phi(A,B)$ is a formula with set-variables $A,B$, then for any set $X$ there exists a set $Y$ such that for any set $A < X$, if there exists a set $B$ with $\Phi(A,B)$, then there exists such a $B$ with $B < Y$.

This one says that for a formula and a set, there is a set that contains values of the formula.

Michael Shulman Comparing material and structural set theories (2018):

If $\Phi(i,S)$ is a formula with an element-variable $i$ and a set-variable $S$, and $I$ is a set such that for all $i \in I$ there exists a set $S$ with $\Phi(i,S)$, then there exists a surjection $p : V \twoheadrightarrow I$ and a $V$-indexed family of sets $q : A \to V$, such that for all $v \in V$ we have $\Phi(p(v),q^{−1}(v))$.

This one is similar to McLarty's, where there is a collected set and a projection from that set to an indexing set. This version is designed to work in very weak theories, so it's a bit careful about making sure that it uses weak enough assumptions and a strong enough conclusion.