I understand a proof as a series of statements that are either axioms or follow from previous statements by a small set of rules of inference.
I understand a recursive definition to be something like ($\phi$ is addition):
$$ \phi(x, 0) = x $$
$$ \phi(x, y+1) = \phi(x,y)+1,$$
where formally we would use a successor function $s(x) = x+1$ instead of actually writing "+1" in a formula.
What I'd like to understand is how this function would fit into a formal proof.
For background, I'm trying to understand Godel's original incompleteness proof. I'm having trouble understanding how his many recursive functions/relations would be expressed formally since they are defined symbols.
Best Answer
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.