I'm interested in establishing that for any partially computable $k$-ary function $f$ there exists a formula $\Phi$ with $k+1$ free variables such that
- If $f(x_1, \dots, x_k) = y$, then $\Phi(x_1, \dots, x_k, y)$ is provable in PA
- If $f(x_1, \dots, x_k) \neq y$, then $\neg\Phi(x_1, \dots, x_k, y)$ is provable in PA
- If $f(x_1, \dots, x_k)$ is undefined (the corresponding program doesn't halt), then we don't care about the status of $\Phi(x_1, \dots, x_k, y)$ for any $y$
There's presumably many different ways of going about this ranging from Gödel's $\beta$-function to the negative solution of Hilbert's tenth problem. What approach would you recommend?
Note that many texts will say "general recursive" rather than "computable". But I find that general recursive functions are a rather opaque model of computation. I'd really prefer to start with something that is more obviously a general model of computation such as Turing machines.
One approach I find intuitive is the following:
First, we show using Kleene's $T$-predicate that every computable function is $\Sigma^0_1$-definable over $\mathbb{N}$. This isn't too hard, but if you haven't constructed the $T$-predicate already it's a bit messy.
This lets us rephrase the problem in model-theoretic terms, as follows:
(In particular, the construction of the $T$-predicate is the only part of this argument where computability as such gets used; from here on out everything is about definability and syntax.)
To prove $(*)$ we'll use the completeness theorem: given a $\Sigma^0_1$ function $f$, we'll whip up a formula $\psi$ which "defines $f$ in all models of $PA$" in the appropriate sense, and the completeness theorem will then give us what we want.
So suppose we have a $\Delta^0_0$ formula $\theta(x,y,z)$ such that the $\Sigma^0_1$ formula $$\varphi(x,y)\equiv\exists z\theta(x,y,z)$$ defines a function $f$. We'll whip up a new formula $\psi(x,y)$ such that for every $M\models PA$ and $k\in dom(f)$ we have $$\forall x\in M(M\models\psi(\underline{k}, x)\iff x=\underline{f(k)}^M).$$ By the completeness theorem this will imply that in fact $\psi$ represents $f$, since everything holding across all models of PA is provable from PA.
The key behind defining $\psi$ is the observation that if the standard natural numbers form an initial segment of any model of PA. The first consequence of this is immediate: $\Sigma^0_1$ sentences are "upwards absolute" between $\mathbb{N}$ and any other model of PA (if $\mathbb{N}$ satisfies some $\Sigma^0_1$ sentence, then so does any other model of PA).
Consequently for any model $M$ of PA and any $k\in dom(f)$, we have:
If $\mathbb{N}\models\theta(k,f(k),c)$ then $M\models\theta(k,f(k),c)$.
For any $a,b\in M$ such that $a\not=\underline{f(k)}^M$ but $M\models\theta(\underline{k},a,b)$, we have that either $a$ or $b$ is nonstandard.
The first bulletpoint says that there are no "false negatives," while the second says that "false positives must be nonstandard." Each of these follows from the above absoluteness observation (this is a good exercise).
But now there's a clear way to pick out the right value of $f$ and witness to that equality, by looking at their sum: consider the formula
By the above analysis, for each $M\models PA$ and each $k\in dom(f)$ we have $$\forall a\in M(M\models\psi(\underline{k}, a)\leftrightarrow a=\underline{f(k)}^M)$$ as desired.
One nice feature of this more model-theoretic approach is that it makes it much clearer that PA as a "representing theory" is overkill. The $\Sigma^0_1$ definability of computable functions is a fact about $\mathbb{N}$, not our theory; all we needed from our theory is that its models "have $\mathbb{N}$ as an initial segment."
The general idea in the above goes by the name invariant definability, and plays an important role in generalized recursion theory.