Apparent paradox in Peano arithmetic In trying to understand Godel’s incompleteness theorem, I have come across an apparent paradox. There must be a mistake somewhere but I cannot find it and would be very grateful for anyone to point out where it lies. The paradox uses a typical Cantor diagonalization argument. 
Given a relatively rich first order language such as Peano Arithmetic, finite operations such as deciding whether a number is the Godel number of a valid proof, can be captured by wffs in the language. 
Specifically, my understanding of PA is that the following is true. Suppose I give a finite set of operations, each of which could be carried out by a Turing machine, and which take a numeral n as the input, and produce a wff as the output (I am not confining it to the case where the output is another numeral). Call this procedure P. So given any numeral n, the procedure gives a wff which could be written (in the metalanguage) as P(n). Then this procedure can be represented inside the language itself, captured by a wff φ(x) with just one free variable x, such that the outcome of the procedure on the number n as above is given by the sentence φ(n) where n is the numeral in the object language corresponding to n.
Now choose P as follows. Suppose given your n. List the wffs with just one free variable x in an enumerable sequence φ1(x), φ2(x) etc, which can certainly be done by listing such wffs in the order of their Godel numbers. Continue until you get to φn(x). Now substitute n for x in this, and form the sentence “not-φn(n)”.
This provides a method of mechanically writing down the sentence “not-φn(n)” for any n. There must therefore be a wff φ(x) which captures this mechanical process, that is, such that “φ(n)” is the sentence “not-φn(n)”.  
But now the usual argument leads to a contradiction. For the wff φ must be one of the φk in the enumeration for some k, so the sentence φ(k) must be identical to the sentence φk(k), but it is also by definition the sentence not-φk(k). 
The only point at which the argument can break down, as far as I can see, is the assumption that P can be captured by a wff. But that seems to go against the idea that everything finitely computable can be expressed within the language. Any ideas?
 A: The claim in your third paragraph is false (and indeed the rest of your question demonstrates this). In fact, there is a very strong impossibility result here.
Call a formula $\varphi$ complete if there is some computable function $f$ such that for every sentence $\theta$ we have $$PA\vdash\varphi(\underline{f(\ulcorner\theta\urcorner)})\leftrightarrow\theta$$ (where "$\ulcorner\cdot\urcorner$" is the Godel numbering function and "$\underline{k}$" is the numeral corresponding to $k$).
Then we have:

There are no complete formulas.

You can prove this via self-reference, along the lines of what you've done. 

Another approach is to think about logical complexity, which actually yields an even stronger result. All instantiations of a given formula have bounded quantifier complexity, so in order for there to be a complete formula it would need to be the case that the quantifier hierarchy over PA collapses: that there is some $c$ such that every sentence is PA-provably equivalent to a $\Sigma_c$-sentence. 
This should be pretty implausible. We can go further and give it a computability-theoretic interpretation. If PA is sound (= only proves true things), the above phenomenon would imply that the $\Sigma_n$-theory of $\mathbb{N}$ computes the whole theory of $\mathbb{N}$: to tell if an arbitrary-complexity sentence is true, simply search for a PA-proof of $\varphi\leftrightarrow\hat{\varphi}$ for some $c$-quantifier sentence $\hat{\varphi}$ (which exists by assumpion) and then ask whether $\hat{\varphi}$ is true (and note that both the equivalence and the answer to this question are accurate since PA is sound). The usual arithmetization then yields ${\bf 0^{(c)}}\ge_T{\bf 0^{(c+1)}}$, contradicting the relativized unsolvability of the halting problem.

The issue is that the statement

everything finitely computable can be expressed within the language

is rather fragile. One natural formulation of it which is true is via representability. Call a function $f:\mathbb{N}\rightarrow\mathbb{N}$ representable iff there is some formula $\varphi(x,y)$ such that for all $a,b\in\mathbb{N}$ we have $$PA\vdash\varphi(\underline{a},\underline{b})\quad\iff\quad f(a)=b.$$ Similar definitions apply to higher-arity functions and to relations.
(Note that this is not the same as definability: while every representable function is definable, the converse is not true, since we're looking at PA-provability rather than mere truth.)
Then the following are equivalent:


*

*$f$ is computable.

*$f$ is representable.
But this is a much "lower-level" phenomenon than what you're trying to do with the above.
