Does the notion of provably total function depend on the chosen representation?

Question

A typical definition of "provably total function in a theory $T$" goes like this (paraphrased from Odifreddi, Classical Recursion Theory II):

A function $f : \mathbb{N}^n \to \mathbb{N}$ is provably total in a theory $T$ (over a language that includes $0$ and successor) iff $$T\models (\forall x_1)...(\forall x_n)(\exists y) \varphi(x_1,...,x_n,y)$$ where for any $\vec{x}\in\mathbb{N}^n$, $y \in \mathbb{N}$, $$f(\vec{x})=y \Leftrightarrow T \models \varphi(\underline{x_1},...,\underline{x_n},\underline{y})$$ where for any $n \in \mathbb{N}$ we have denoted by $\underline{n}$ a canonical term representing $n$ (like $s^{(n)}(0)$).

I haven't been able to find any reference where this definition is fully formalized, in the sense that the first relation must happen for any $\varphi$ that "weakly represents" $f$ according to the second relation, or only for some $\varphi$, or even a (short?) proof that "$\exists$ implies $\forall$".

Can anyone enlighten me?

Answer 1

Yes, this concept depends on how you represent the function.

For example, the constant zero function is provably total, under that description, that is, using the formula $\varphi(x,y)$ equal to "$y=0$".

But consider the formula $\psi(x,y)$ that asserts, "$y=0$ and $x$ is not the code of a contradiction in PA."

This formula also weakly represents the constant zero function in the sense you requested, since no actual natural number will be the code of a proof of a contradiction. But PA does not prove $\forall x\exists y\ \psi(x,y)$.

Answer 2

It's probably useful to note that every property that somehow depends on provability depends quite critically on the representation. From On Provable Recursive Functions (H. B. Enderton, 1968)

Theorem: (a) We can choose $\mathrm{M}$ as above such that no function is provable.

where $\mathrm{M(e,x,y,z)}$ is a formula that is true iff $e$ is a code for a machine that on input $x$ returns $y$ in fewer than $z$ steps.

It's useful to note that even the second incompleteness theorem is subject to encoding trouble: surely $\mathrm{Con}(PA)$ is equivalent to $0=0$ if $PA$ is consistent! But $PA\vdash 0=0$, so all formulae expressing $\mathrm{Con}(PA)$ must not be created equal.

In practice one fixes an encoding of the computational model in the hopes that the encoding is straightforward enough to have the "right" meaning. The Enderton paper discusses this to some extent.