Is the Axiom of Replacement necessary to construct any function in ZFC?

Question

A while back, I read a source that I believe mentioned something along the lines of needing the Axiom of Replacement to define functions in ZFC Set Theory. I was convinced the entire time up to that point that to define a function $f \colon X \longrightarrow Y$, one mearly considers it as a subset of the product $X \times Y$, and thus only needs the Axiom of Powerset in order to define the Cartesian product, and the Axiom Schema of Comprehension to define subsets satisfying a particular predicate. However, the more that I think about it, the more I am confused in trying to define a function by a single predicate as a subset $f = \{(x, y) \in X \times Y \mid P(x, y)\}$, where $P(x,y)$ describes that each $x \in Y$ is associated to a $\textit{unique}$ $y \in Y$. So which is it? What is the Axiom of Replacement really needed for? Thanks in advance.

Answer 1

I'm not sure how you think replacement comes into play here.

Given sets $X$ and $Y$, we can as you say form the set $X\times Y$ without invoking replacement in any way. Now, for any formula $\varphi(x, y)$ we can form the set $$R_\varphi=\{\langle x, y\rangle\in X\times Y: \varphi(x, y)\}$$ as follows:

Before I do this, note that this is not as trivial as it may first appear: "$\varphi(x, y)$" is a formula of two variables, not a formula of a single (ordered pair) variable. This is why I've used the angle-brackets notation for ordered pairs.

Namely, let $\psi_\varphi(z)$ be the formula "there are $x\in X, y\in Y$ such that $z=\langle x, y\rangle$ and $\varphi(x, y)$." Then $$R_\varphi=\{z\in X\times Y: \psi_\varphi(z)\},$$ which exists by separation. If, now, $\varphi$ happens to have the property that for each $x\in X$ there is exactly one $y\in Y$ with $\varphi(x, y)$, the set $R_\varphi$ is in fact a function. So replacement plays no role here.

---

What replacement/collection is used for is building the range of a definable "function"/"relation." Namely, if we have a formula $\varphi(x, y)$ (the definable "function") and a set $X$ (the domain) such that for each $x\in X$ there is exactly one $y$ with $\varphi(x, y)$ (but note, we don't know where these $y$s "live"), then without replacement we can't generally conclude that the set $\{y: \exists x\in X(\varphi(x, y))\}$ exists, hence we can't argue that the class $$\{(x, y): x\in X, \varphi(x, y)\}$$ actually is a set, and hence a genuine function.

So for example, in set theory without replacement we can take $X=\omega$, $\varphi(x, y)\equiv$ "$y=V_x$;" then we can prove that for each $x\in X$ there is exactly one $y$ with $\varphi(x, y)$, but we can't even prove that $V_\omega$ exists!