What is meant by "function" in the axiom schema of replacement.

Solution 1:

The usual statement of the axiom schema of replacement is as follows:

For any formula $\phi(x,y,p)$:

$$\forall p( \forall x,y,z(\phi(x,y,p)\land \phi(x,z,p) \to y = z) \to \forall X \exists Y \forall u(u \in Y \leftrightarrow \exists v(v \in X \land \phi(v,u,p))))$$

Here, $p$ is to be thought of as a "parameter", e.g. used if $\phi(x,y,p)$ is the formula $y = (x,p)$; the resulting set $Y$ will depend on $p$. The first part expresses that $\phi(\cdot,\cdot,p)$ is a functional relation: any $x$ admits at most one $y$ such that $\phi(x,y,p)$.

It is this $\phi(x,y,p)$ that is referred to, sloppily, as a "function". But we see that $\phi$ has to be of a rather more explicit form: it needs to be a formula that is expressible using the language of set theory, and we need to be able to verify that it constitutes a functional relation. Only then may we invoke replacement to conclude that $Y_p = \{y\mid\exists x: \phi(x,y,p)\}$ is a set.

We have thus crafted sort of a "formal analogue" of a "function", by using certain formulae (which are syntactical objects) in place of certain sets (which are semantical objects). By imposing functionality, we ensure that our formal analogue behaves more or less like a function. However, we did not specify either "domain" or "codomain", and they may very well not be sets (they can be empty, or consist of all sets!).

The unspecified domain and codomain are what separates a "formal function" from an "internal function", using the standard "suitable collection of ordered pairs" definition.

Now why aren't "formal functions" more general than sets? This is because they are still expressed in terms of "sets" (rather, in terms of the variables $x,y,z,p,u,v,X,Y$, which we want to think of as sets). We cannot dispose of these variables and still sensibly talk about the formulae that we have called "formal functions" cq. "functional relations".

What we have seen above is actually an example of a phenomenon that can be very confusing. We have seen "functions" that are of a different form than what our usual definition of function is. They can be "too large" to fit the usual definition of function.

We, external to the model of set theory, can reason about these "functions". However, the model itself does not have the means to contemplate them as a single object. We say the "function" is external to the model. The usual definition of a function could appropriately (but at the expense of considerable tedium) be called an internal function, because the model is able to reason about it as a single object.

This internal vs. external doctrine comes back at many, sometimes unexpected places in logic, and can give rise to intuitively bewildering statements. You can think of the distinction between $A \vdash B$ and $A \to B$ in propositional calculus as a further example: the former is the external way of saying "if $A$ holds, so does $B$", while the latter is its internal analogue. In propositional calculus, the two notions agree, but in more complicated systems, sometimes one can fail while the other holds (!).

Solution 2:

If the quoted axiom were part of a theory of sets and classes, like Morse-Kelley or Neumann-Bernays-Gödel, then I'd simply say that a function is a class of ordered pairs in which no two distinct ordered pairs have the same first component. But in such a theory, this form of replacement would be a single axiom, not an axiom schema. Since it's labeled as a schema in the question, I must assume that we're dealing with a theory of sets, not classes, like Zermelo-Fraenkel set theory. In that context, this usage of the word "function" is rather unusual but not unheard-of. I'd say it's unusual enough that any text using it should give an explanation or at least a pointer to an explanation. (Suggestion: Look for such an explanation in the source where you found this formulation of the replacement schema.) The usual meaning of "function" in ZF (or similar theories) is a set of ordered pairs, no two of which have the same first component, and that is definitely not what is meant here. As some of the previous answers have explained, the intended notion of "function" here is what I'd call a parametrically definable operation. Technically, this consists of two things: First, there is a (first-order) formula $\phi(x,y,\vec p)$ with two "important" free variables $x$ and $y$ and possibly some additional "auxiliary" variables or "parameters" $\vec p$; second there are specific sets as values for those parameters $\vec p$. To say that the formula $\phi$ with those values of $\vec p$ constitutes a "function" is to say that the formula $$ \forall x\,\forall y\,\forall z\,[(\phi(x,y,\vec p)\land\phi(x,z,\vec p))\implies y=z] $$ is true (for the given values of $\vec p$). This mixture of syntax (\phi) and semantics (values for $\vec p$) is rather awkward to formalize carefully (though it has been done), so, when introducing the axioms of set theory, I prefer not to introduce these strange "functions" and instead to formulate replacement as Lord_Farin did.

Solution 3:

The simplest approach, conceptually, is to view a function as a relation in a more general sense. Normally, a relation is a subset of a Cartesian product of sets. For this purpose, we need instead a subclass of a Cartesian product of classes. In a class-set theory (e.g., NBG theory or Morse-Kelley theory), classes are defined formally. In ZF, classes are informally used to describe certain propositional functions. Any "first order" logical formula is associated with the class of all sets that satisfy it. Two important relations of this sort are the "epsilon relation" $E$, which relates two sets whenever the first is an element of the second, and the set inclusion relation, which relates two sets whenever the first is a subset of the second. The functions used for the axiom of replacement are of this generalized sort. The situation is very similar to that of the axiom of specification, really.

Addendum: The set theorist's notion of function is sometimes somewhat different than other mathematician's. In many cases, where a set theorist writes "function", it would be better to read "many-to-one relation", where a "relation" means a class whose elements are ordered pairs.