The book A Friendly Introduction to Mathematical Logic – 2nd Edition by Christopher C. Leary and Lars Kristiansen gives the following proposition without proof:
Proposition 5.3.6. Suppose that $f$ is a total function from $\mathbb{N}^k$ to $\mathbb{N}$. Then $f$ is representable if and only if $f$ is weakly representable.
What/where is the proof of this proposition? After some searching, I'm having trouble finding this exact proposition elsewhere that uses the same definitions of representable and weakly representable defined in the book. I find it odd that the authors chose to omit this proof without any further references.
For ease of reference, here are some definitions from the book:
Definition 5.3.4. Suppose that $f:\mathbb{N}^k\to\mathbb{N}$ is a total function. We will say that $f$ is a representable function (in $N$) if there is an $\mathcal{L}_{NT}$ formula $\phi(x_1,…,x_{k+1})$ such that, for all $a_1,a_2,…a_{k+1}\in\mathbb{N}$,
$$\text{if }f(a_1,…,a_k)=a_{k+1}\text{, then }N\vdash\phi(a_1,…,a_{k+1})$$
$$\text{if }f(a_1,…,a_k)\neq a_{k+1}\text{, then }N\vdash\lnot\phi(a_1,…,a_{k+1})$$.
Definition 5.3.5. Suppose that $A\subseteq\mathbb{N}^k$ and $f:A\to\mathbb{N}$ is a (possibly) partial function. We will say that $f$ is a weakly representable function (in $N$) if there is an $\mathcal{L}_{NT}$ formula $\phi(x_1,…,x_{k+1})$ such that, for all $a_1,a_2,…a_{k+1}\in\mathbb{N}$,
$$\text{if }f(a_1,…,a_k)=a_{k+1}\text{, then }N\vdash\phi(a_1,…,a_{k+1})$$
$$\text{if }f(a_1,…,a_k)\neq a_{k+1}\text{, then }N\not\vdash\phi(a_1,…,a_{k+1}).$$
My secondary question is why are representable functions only defined for total functions (by Definition 5.3.4)? It seems perfectly fine to allow partial functions to be considered representable functions.
Best Answer
This is a cute trick, very similar to Rosser's improvement to Godel's incompleteness theorem:
Suppose $f$ is weakly representable via $\varphi$. Consider the following new formula (conflating numerals and numbers for simplicity):
Since $\varphi$ weakly represents $f$ and $f$ is total, we get that $\psi$ represents $f$.
To see that $N$ proves $\psi(m_1,...,m_k, f(m_1,...,m_k))$, let $u$ be the smallest code for an $N$-proof of $\varphi(m_1,...,m_k, f(m_1,...,m_k))$ (which exists since $\varphi$ weakly represents $f$). In $N$ we can check that $u$ is such a proof, and so prove $\psi(m_1,...,m_k, f(m_1,...,m_k))$.
More interestingly, suppose $n\not=f(m_1,...,m_k)$. Since $\varphi$ represents $f$ and $f$ is total, there is some least $u$ which codes an $N$-proof of $\varphi(m_1,...,m_k, a)$ for some $a$ (namely $a=f(m_1,...,m_k)$). $N$ can verify this property of $u$ (in particular, there are only finitely many possible codes $<u$), and so prove $\neg\psi(m_1,...,m_k, a)$. Note that $N$ does not necessarily prove $\neg\varphi(m_1,...,m_k,n)$ by this analysis, it merely shows that any proof of $\varphi(m_1,...,m_k,n)$ would have to be longer than the shortest proof of $\varphi(m_1,...,m_k, a)$.
As to why we focus on total functions, you're correct, this isn't strictly necessary. However, the notions are better behaved for total functions. For example, the above argument that weak representability implies representability fails if we look at partial functions. (More computability-theoretically, every total c.e. function is actually a computable function, but this fails for partial functions.)