This is related to my previous question on expressions. Consider a countably infinite set of variables, indexed by the positive integers. Suppose also we are considering the set of real numbers as our domain. How would we associate a function to an expression, as in how would we formally define it. For example, should $x_2$ be associated to the identity function on $\mathbb{R}$, or to the projection function on $\mathbb{R}^2$ that returns the second coordinate? Also, should something like $x_1+x_2-x_3+x_3$ be defined on $\mathbb{R}^3$, or $\mathbb{R}^2$? Is there some mathematical text where the mapping from expressions to functions is formally defined?
Associate a function to an expression
definitionlogic
Related Solutions
There is indeed a problem to solve here -- and Gödel does solve it, but much later in his 1931 paper than one tends to expect if one approaches it armed with knowledge of modern paraphrases.
We're looking at section 2 of Über formal unentscheidbare Sätze. Gödel first [pp. 176-180] describes a formal proof system P for number theory (simplified from Principia Mathematica). Then [pp. 179-181] he very briefly defines a concept of "recursive functions" (which are what we today call "primitive recursive"), and then [182ff] immediately launches into a laundry list of recursive functions that arithmetize the formal system.
But wait! the modern reader cries. It is not at all clear how all of these recursive functions can be said to exist within system P. And indeed it isn't -- at this point in the development Gödel treats the recursive functions as existing entirely outside the formal system; they appear on the metalevel.
(I think this is what he means when he describes them as "number-theoretic functions". Today, we would probably be inclined to understand "number-theoretic function" to imply that the function can be defined in some particular formal system such as Peano arithmetic, but this is to a large extent due to Gödel's own work. Before that, "number theoretic" must have evoked ideas of "that kind of mathematics that doesn't need to rest on axiomatic development, because it is intuitively obvious how it works".)
Immediately after the laundry list, the recursive functions are finally connected to the formal system in Proposition V, which says that every recursive relation corresponds to a formula of system P. The strange thing is that Proposition V is not really proved -- Gödel just waves his hands a bit and leaves it as an exercise for the reader. This is quite puzzling for a reader who is used to seeing Gödel's argument developed for something like Peano arithmetic. In that case, Proposition V is not at all obvious, but what we tend to forget is that system P is a higher-order system where one can quantify over all functions and so forth. So something like the usual set-theoretic argument that a recursive definition actually defines something (as given in David's answer) can be carried out directly in system P.
Later in the paper, in section 3 that is almost an afterthought, Gödel shows as Proposition VII that a recursive relation can also be represented as a first-order formula that contains only addition, multiplication and quantification over the natural numbers. Here is where we find the somewhat-famous $\beta$ function construction, and it is this argument that in most modern retellings take the place of Gödel's own Proposition V.
A sequence in a set $X$ is, intuitively, a list $x_1, x_2, x_3, \ldots$ of elements of $X$ (there is an $x_i$ for every positive integer $i$). Formally, this sequence is a function $f : \{1, 2, \ldots\} \to X$ given by $f(i) = x_i$.
An indexed family in $X$ is a collection of elements $x_i \in X$, indexed by $i \in I$, where $I$ can be any set. Formally, this indexed family is a function $f : I \to X$ given by $f(i) = x_i$.
Here you can see that a sequence is a special type of indexed family: one where the indexing set $I$ is the set of positive integers. Of course, with sequences you have the additional notion that the terms are in some sort of order (e.g., $x_1$ is "before" $x_2$). This notion isn't present with general indexed families, unless the indexing set has some sort of order relation defined on it.
Best Answer
You're right that there's some flexibility here. The simplest approach is to just clear everything up by adding some "metadata." Say that an annotated term (in a given language, using $\mathbb{N}$-indexed variables) is a pair $(t,n)$ where $t$ is a term in the language and every variable occurring in $t$ has index $\le n$. Then we can construe each annotated term $(t,n)$ as a function from the $n$th Cartesian power of our structure to itself.
The default, then, is to use the smallest possible $n$. So for example (abusing parentheses for simplicity) "$x_1+x_2$" and "$x_1+x_2+x_3-x_3$" would refer to functions from $\mathbb{R}^2$ and from $\mathbb{R}^3$ respectively; their "equivalence" would amount to the fact that the former is the projection of the latter.
Unfortunately this is generally swept under the rug, but hopefully the above indicates that it's pretty straightforward to treat if you really want to. It's also worth noting that usually we go the other way: we first declare that we're going to consider functions $\mathbb{R}^n\rightarrow\mathbb{R}$, and then interpret terms with variables only from $\{x_1,...,x_n\}$ as maps $\mathbb{R}^n\rightarrow\mathbb{R}$ in the obvious way. So a lot of the time this doesn't come up at all: while it's true that we can interpret a given term as living on different domains, since we specify what domain we're interested in at the outset we don't care about this ambiguity.