In praise of Replacement

I have often seen people complain about Replacement axioms. For example, this MathOverflow question, or this one, or that one, and also this one. This technical-looking schema of axioms state that if \(\varphi\) defines a function on a set \(x\), then the image of \(x\) under that function is a set. And this axiom schema is a powerhouse! It is one of the three component that give \(\ZF\) its power (the others being power set and infinity, of course).

You'd think that people in category theory would like it, from a foundational point of view, it literally tells you that functions exists if you can define them! And category theory is all about the functions (yes, I know it's not, but I'm trying to make a point).

One of the equivalences of Replacement is the following statement: Suppose that \(\varphi(x,y,z,p)\) is a formula such that for some parameter \(p\), \(\varphi(x,y,z,p)\leftrightarrow\varphi(x,y,z',p)\) if and only if \(z=z'\). Namely, \(\varphi\) (modulo the parameter \(p\)) defines the ordered pair \((x,y)\). Then the Cartesian product \(A\times_{\varphi,p} B=\{z\mid\exists a\in A\exists b\in B\varphi(a,b,z,p)\}\) is a set.

In other words, Replacement is equivalent to saying "I don't care how you're coding ordered pairs, as long as it's going to satisfy the axioms of ordered pairs!". So you'd think people from non-\(\ZFC\) foundations would be happy to have something like that, especially if they are focused on category theory (which is all about functions (yes, again, I know, I'm just trying to make a point)).

Well. It is exactly the opposite. Since the Kuratowski coding of ordered pairs is so simple, it's an easy solution to the problem. So from a foundational point of view, there's no problem anymore, and nothing else matter. Once you have one coding that lets you have ordered pairs from a set theoretic point of view, the rest is redundant. This is very much reflected in how \(\ETCS\) is equivalent to a relatively weak set theory: bounded Zermelo.

So you might want to say, well, if category theory is not really using it, then maybe it's not that necessary. And indeed, the uses of Replacement outside of set theory are rare. Borel determinacy is one of them, and arguably it is a set theoretic statement.

But, like many other posts, this too was inspired by some discussion on Math.SE. And here is a very nice example of why Replacement is important.

Theorem. If \(A\) is a set, then \(\{A^n\mid n\in\Bbb N\}\) exists.

One would like to prove that by saying that this is just a bunch of subsets of \(A^{<\omega}\), which itself is a subset of \(\mathcal P(\omega\times A)\), so by power set and very bounded separation axioms, we can get that very set. But this depends on how \(A^n\) is defined. If \(A^n\) is the set of functions from \(n\) to \(A\), that's fine, the above suggestion works just fine. However, it is not uncommon to see the following inductive definition: \(A^0=\{\varnothing\}\) and \(A^{n+1}=A^n\times A\), or \(A^1=A\) and \(A^{n+1}=A^n\times A\).

Under that latter definition and using the Kuratowski definition of ordered pairs, \(A^{n+1}\) has a strictly larger von Neumann rank comapred to \(A^n\). At least when starting with \(A=V_{\omega+1}\), or something like that. So the von Neumann ranks of \(V_{\omega+1}^n\) are strictly increasing under the Kuratowski definition, and so there is no set in \(V_{\omega+\omega}\) which contains exactly the \(V_{\omega+1}^n\)'s. But since \(V_{\omega+\omega}\) is a model of Zermelo, that means that we cannot prove without Replacement that \(\{A^n\mid n\in\Bbb N\}\) is a set for any set \(A\).

Hey hey, wait a minute, you might claim. You might argue that you don't care that \(A\times A\) and \(\{f\colon\{0,1\}\to A\}\) are two different sets. They both satisfy the same properties from an abstract point of view. BUT THIS IS THE POINT!

This is exactly the point! When you say that you don't want to distinguish between \(A\times A\) and \(A^2\), you are ostensibly replacing one object with another. You are literally appealing to Replacement!

Yes, this argument does not use a lot of Replacement, but it does use some of it. And it might just be enough to clarify of its necessity.

(And I haven't even started on talking about how it is equivalent to Reflection, which is so awesome on its own (foundationally speaking)...)