Question Regarding the Replacement Schema

Question

For each formula $\phi(x,y,p)$, we have the following axiom:

$\forall x \forall y \forall z (\phi(x,y,p) \wedge \phi(x,z,p) \rightarrow y = z) \rightarrow \forall X \exists Y \forall y (y \in Y \leftrightarrow (\exists x \in X) \phi(x,y,p))$

This set of axioms has been characterized informally in English as follows:

"If a class $F$ is a function, then for every set $X$, $F(X)$ is a set."

But isn't the English statement saying much less than what the actual schema is saying? That is, it seems that the schema can be interpreted as saying what the English statement is saying only if we interpret $\phi(x,y,p)$ as being the property of "$y$ is the image of $x$ under $p$". But then aren't there many more interpretations of $\phi(x,y,p)$ that might permit this axiom schema to be saying some radically different things than this? In any event, how should one interpret formulae of the sort $\phi(x,y,p)$ as above?

Answer 1

I don't know why you think it only makes sense with "$y$ is the image of $x$ under $p$".

The first part $\forall x \forall y \forall z (\phi(x,y,p) \wedge \phi(x,z,p) \rightarrow y = z)$ defines a class function $F_p$ by saying $F_p(x)=y$ whenever $\phi(x,y,p)$ holds.

The second part $\forall X \exists Y \forall y (y \in Y \leftrightarrow (\exists x \in X) \phi(x,y,p))$ then says there is a set $Y$ such that $Y=\{y : \exists x,\phi(x,y,p)\} = F_p(X)$.

Answer 2

Let me point the problem, and it is also a mistake in your formulation of the axiom:

Your $p$ is a free variable. It should be $\forall p( \ldots )$, where the dots represent your stated axiom. In fact, it should be $\vec p$, because we may have several parameters. This means that whenever we have fixed the parameter and the result is functional, then the image of a set is a set.

The informal gist of the axiom is the same, because we don't specify whether or not $F$ is definable with parameter, without parameters, and so on. We just say that $F$ is a formula. An even more correct formulation would to say that $F$ is a definable formula.

So the axiom says that if $F$ is a formula definable from parameters $p$. Of course we can change the parameters and have another function. Completely different one too.