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?

  • $\begingroup$ See Peter Smith, An Introduction to Gödel's Theorems (Cambridge UP, 2nd ed 2013), Ch.30.2 The unprovability-in-PA of Goodstein’s Theorem, page 223-24: Note next that the sequence-computing function $g(n, k) = n_k$ is evidently primitive recursive (to calculate the k-th value of the Goodstein sequence starting at n, we can write a program just using ‘for’ loops). Hence this two-place function is expressible in LA by a three-place Σ1 wff S(x, y, z)." $\endgroup$ Commented Jul 24, 2023 at 14:59
  • 2
    $\begingroup$ For every specific $n$ , PA can prove that the Goodstein sequence with start value $n$ terminates , but (assuming PA is consistent) PA cannot prove that it terminates for every $n$. ZFC can however prove this , even more , it can prove that PA is consistent iff every Goodstein sequence terminates. The second incompleteness theorem of Goedel immediately implies that PA cannot prove the theorem since then it could prove its own consistency which is impossible. $\endgroup$
    – Peter
    Commented Jul 24, 2023 at 15:50

1 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.

  • $\begingroup$ But Salehi says in that link that strong representability implies provable totality. But for that the author has to change the formula $\theta$ by another formula $\eta$ with a trick, so does Goodstein give us a formula $\theta$ that (strongly) represents $G$ but does not prove its totality? So there would exist other formulas that prove its totality, but not specifically $\theta$. Am I interpreting the result correctly now? $\endgroup$
    – Keplerto
    Commented Jul 24, 2023 at 22:02
  • $\begingroup$ @Keplerto Yes, that's accurate. The choice of definition is absolutely crucial. $\endgroup$ Commented Jul 24, 2023 at 22:03
  • 2
    $\begingroup$ In particular, note that the trick Salehi describes results in an increase in quantifier complexity. If we restrict attention to $\Sigma_1$ definitions of functions - and this is the "right" choice if we're thinking about computable/recursive functions as such - then we get a sharp distinction: there are total computable functions which have no $\mathsf{PA}$-provably-total $\Sigma_1$ definition. (Proof: diagonalize.) $\endgroup$ Commented Jul 24, 2023 at 22:06
  • 1
    $\begingroup$ @Keplerto I've added the diagonalization mentioned in my previous comment to the answer. $\endgroup$ Commented Jul 24, 2023 at 22:46
  • $\begingroup$ Thank you, now it makes sense $\endgroup$
    – Keplerto
    Commented Jul 25, 2023 at 8:43

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .