How does a recursive definition fit into a formal proof? 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.
 A: 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: I also used to have a lot of trouble understanding this. Let me see if the following helps.
I assume we're working in some flavor of set theory and that I have already defined ordered pairs, nonnegative integers, and the notations $+$ and $\times$. I'll write $\mathbb{N}$ for the set of all nonnegative integers. Suppose I now need to define the function $n \mapsto 2^n$ from $\mathbb{N}$ to itself, and I am going to do it recursively.
Here is what I should prove:

Theorem: There is a unique subset $F$ of $\mathbb{N} \times \mathbb{N}$ such that

*

*For every $x \in \mathbb{N}$, there is precisely one $y \in \mathbb{N}$ such that $(x,y) \in F$.

*$(0,1) \in F$.

*If $(x,y) \in F$ then $(x+1, 2 \times y) \in F$

Then, whenever you want to write $y=2^{10}$, you instead write "Let $F$ be the unique subset of $\mathbb{N} \times \mathbb{N}$ such that ... and let $y$ be the unique element of $\mathbb{N}$ such that $(10, y) \in F$."
Of course, I haven't used fully formal language here. Statement 1, unpacks to "For all $x$ in $\mathbb{N}$, there exists $y \in \mathbb{N}$ such that $(x, y) \in F$ and, for all $x$, $y_1$ and $y_2$ in $\mathbb{N}$, if $(x,y_1) \in F$ and $(x,y_2) \in F$, then $y_1 = y_2$." A similar unpacking must be done with the statement that $F$ is unique.
This is a good point to pause and make sure you understand what I've written so far.

So, how do we prove this? I will sketch two proofs because I don't know whether you are comfortable with writing inductive proofs formally. So the first proof treats induction informally and assumes you can fill in the gaps, and the second proof fills in those gaps for you.
Proof sketch (informal induction):
For $n \in \mathbb{N}$, let $\mathbb{N}_{\leq n}$ be the set of nonnegative integers less than or equal to $n$. We first show

Claim For all $n\in \mathbb{N}$, there exists a unique subset $G$ of $\mathbb{N}_{\leq n} \times \mathbb{N}$ such that

*

*For every $x \in \mathbb{N_{\leq n}}$, there is precisely one $y \in \mathbb{N}$ such that $(x,y) \in G$.

*$(0,1) \in G$.

*If $(x,y) \in G$ and $x<n$ then $(x+1, 2 \times y) \in G$

Our proof is by induction on $n$. If $n=0$, take $G= \{ (0,1) \}$. I leave it to you to check that this works and is unique.
For $n>0$, let $G'$ be the subset of $\mathbb{N}_{\leq n-1} \times \mathbb{N}$ we ave inductively constructed. Let $y$ be the unique integer such that $(n-1, y) \in G'$. Set $G = G' \cup \{ (n, 2 \times y ) \}$. Again, you must check that this works and is unique.
Define $F$ to be the set of ordered pairs $(x,y)$ in $\mathbb{N} \times \mathbb{N}$ such that for some $(n, G)$ as above, the ordered pair $(x,y)$ is in $G$. The rest of the proof is left to you. $\square$
Proof sketch (formal induction):
I will assume that, when you constructed $\mathbb{N}$, you proved the Well Ordering Principle:

Any nonempty subset of $\mathbb{N}$ has a least element.

Let $S$ be the set of $n$ such that there does not exist a set $G$ as in the Claim. If $S=\emptyset$, then the claim holds and we finish the proof as above.
When $n=0$, the set $\{ (0,1) \}$ satisfies the Claim (details omitted), so $0 \not \in S$. Assume for the sake of contradiction that $S$ is nonempty. Then, by the Well Ordering Principle, $S$ has a least element $n$. By the first sentence of this paragraph, $n >0$.
Since $n-1 \not \in S$, there is a set $G'$ which satisfies the claim with respect to $n-1$. Let $y$ be the unique integer such that $(n-1, y) \in G'$. Set $G = G' \cup \{ (n, 2 \times y ) \}$. Then $G$ satisfies the claim with respect to $n$ (details omitted). So $n$ is not in $S$ after all, a contradiction. $\square$
Remark for experts I deliberately phrased the above proof to avoid the Axiom of Replacement. The full strength of the Recursion Theorem requires Replacement, but I thought it was best pedagogically to dodge this issue while I could.
