I didn't get any responses to this question the first time around, so I've tried rewriting parts of it. If there's anything glaringly wrong with the questions I'm asking, please leave a comment!
First-order logic supports the notion of a "function." Furthermore, if we axiomatize set theory using first-order logic, then we also get an "internal" notion of a function; in particular, a function is a kind of set.
Suppose we wanted to be very rigorous. I assume it would be important to distinguish between these two concepts.
Question I. What is the most useful terminology here? Should we refer to
- Functions (a kind of set) versus metafunctions (a logical concept), or
- Internal functions (a kind of set) versus functions (a logical concept)?
- Something else?
For the remainder of this question, lets refer to "internal functions" versus "metafunctions," just for emphasis.
A few examples.
The powerset function $x \mapsto \mathcal{P}(x)$ cannot be viewed as an internal function, because the set that encodes this function would be "too big." Thus powerset is a metafunction.
I presume that every internal function $f$ can be viewed as a metafunction. However, I could be wrong; what if $f$ is undefinable?
This begets the following questions.
Question II. Is every internal function associated with a metafunction? Furthermore, given a metafunction, do we ever speak of its "internalization"? That is, a set which essentially encodes that metafunction? And given an internal function, do we ever speak of its "externalization"?
Question III. Do some/all internal functions fail to be a metafunctions?
And my final question is this.
Question IV. Suppose we now choose a "metatheory" (e.g. PA) to study the set theory. Does this result in three kinds of function? And if so, what do we call these different kinds? (Metametafunctions?)
For (I), the usual practice is to call both "functions", but to distinguish between whether the existence of the function is proved in the object theory or the metatheory. The distinction is sometimes not explicitly stated; the author might think that people who know enough to ask will be able to answer for themselves, while mentioning it explicitly becomes distracting.
For (II), recall that in the metatheory, where we define what it means for a structure to satisfy the object theory, a function symbol in a first-order language is interpreted in each first-order structure by a function - which is a metafunction, in this point of view. For example, if we take set theory with an extra function symbol $P$ which is axiomatized to represent the powerset operation, then in any ZFC($P$) structure, $P$ will be interpreted as the metafunction which is the powerset operation on that structure, while internally $P$ is not an "object function" in the sense that it is not coded by any internal set. This points to another distinction: in ZFC($P$) structures, there is a function symbol for powerset in the language, but this is just a "class function" in the usual terminology of set theory, not a genuine "function", i.e. not an internal function.
For (III): each internal function in a model of ZFC corresponds to a metafunction with the same domain as the internal function that takes the same values as the internal function.
For (IV), it is not clear what you mean when you say a function is a "logical" concept. In order for the idea of metafunctions to make sens,e we must work in a metatheory that has a syntax that includes functions. The usual metatheory that we use to study first-order logic is a kind of set theory, in which we define the notion of a first-order structure and a first-order interpretation. IF we study ZFC with PA as a metatheory, the idea of "metafunction" makes less sense, because PA does not have syntax to directly handle functions (apart from functions whose domain and range are finite sets of numbers).