Representability of Goodstein function in PA

Question

I have a doubt concerning the representability of Goodstein's function in Peano Arithmetic ($PA$). Specifically, the function

$G(n) =$ “The length of the Goodstein sequence starting from $n$”

is total recursive, but $PA$ cannot prove its totality. However, in Mendelson's book Introduction to Mathematical Logic, exercise 3.32 states that

Every total recursive function is strongly representable in $PA.$

We can apply the theorem for the Goodstein function $G,$ the definition of strong representability says:

There exists a formula $\mathscr A$ such that

1. If $G(n) = m$ then $PA \vdash \mathscr A (\overline n, \overline m)$
2. $PA \vdash \exists_1 x_{2}\ (\mathscr A(x_1, x_2))$

So clearly $PA$ has a version of the function $G$ (by $1$) that it can prove total (by $2$), contradicting the above result. So am I misunderstanding strong representability or Goodstein's theorem?

Answer 1

Strong representability (in a given theory) does not imply provable totality (in that theory). Specifically, a function $f:\mathbb{N}\rightarrow\mathbb{N}$ is strongly representable in an appropriate theory $T$ iff there is some formula $\theta(x,y)$ such that the following hold:

1. For each $m,n\in\mathbb{N}$, if $f(m)=n$ then $T\vdash \theta(\underline{m},\underline{n})$.

2. For each $n\in\mathbb{N}$, we have $T\vdash\forall x,y[\theta(\underline{n},x)\wedge\theta(\underline{n},y)\rightarrow x=y]$.

(See section 3 of Salehi, which also includes a number of variants on the notion.)

Note that that second bulletpoint does not say that $T$ proves that $f$ is total. This would remain the case even if we strengthened it to "$T\vdash\forall x,y,z[\theta(x,y)\wedge\theta(x,z)\rightarrow y=z]$" - that clause just says "$T$ proves that $f$ is at-most-single-valued." In particular, note that the quantification over $n$s happens outside of the $\vdash$-instance.

So there is no contradiction between the non-$\mathsf{PA}$-provable-totality of the Goodstein function and its strong representability in $\mathsf{PA}$.

---

OK, the above isn't quite correct. If $f$ is strongly representable in $T$ via $\theta$, then there is some other formula $\widehat{\theta}$ also defining $f$ such that $\widehat{\theta}$ is $T$-provably total. But this $\widehat{\theta}$ may be significantly more complicated than $\theta$.

In particular, given that we're looking at computable functions, let's suppose we restrict attention to $\Sigma_1$ definitions. Then in fact strong representability and provable totality do separate after all. This is by a simple diagonalization argument. List the $T$-provably-total $\Sigma_1$ definitions of functions (that is, $T$ should also prove that these formulas are at most single-valued) as $(\upsilon_i)_{i\in\omega}$. Since $T$ is c.e., we can do this effectively, which in turn means that we can express the following as a $\Sigma_1$ formula: $$\mu(x,y)\iff \upsilon_x(x,y-1).$$ The function $m$ defined by $\mu$ is obviously total computable (assuming $T$ is appropriately sound of course) but distinct from every function with a $T$-provably-total $\Sigma_1$ definition.

Note that there's nothing special about $\Sigma_1$ here: there is similarly a $\Sigma_2$-definable total function with no $T$-provably-total $\Sigma_2$ definition, and so on up the arithmetical hierarchy. Of course, as soon as we go this high Salehi's trick means that these functions won't be computable.