The Goodstein-sequence is a total function, but PA cannot prove this.

Is this true for any other function with growth rate at least $f_{\epsilon_0}$ or are there functions growing at least as fast as the Goodstein-sequence that PA can prove to be total ?

I heard that the "power" of the PA is below the $f_{\epsilon_0}$-level, but I do not know if this answers my question.

  • 6
    $\begingroup$ This is the first question I've seen correctly tagged with [proof-theory] in a very long time. It makes me sad to realize how often I have to remove this tag, and even sadder that I'm happy not to remove it here. $\endgroup$ – Asaf Karagila Dec 25 '14 at 21:40
  • $\begingroup$ Thanks for this compliment. $\endgroup$ – Peter Dec 25 '14 at 21:41
  • $\begingroup$ You can find some discussion in the final half of this answer and its links. $\endgroup$ – Bill Dubuque Dec 25 '14 at 23:53

Every function which eventually outgrows $f_{\varepsilon_0}$ cannot be proven to be total in Peano arithmetic. This is implied by more general result:

PA can prove a computable function $F$ to be total if and only if $F$ is primitively recursive in $f_{\omega\uparrow\uparrow n}$ for some finite $n$, where $\omega\uparrow\uparrow n=\omega^{...^\omega}$ with $\omega$ $n$ times.

In particular, if $F$ outgrows all of $f_{\omega\uparrow\uparrow n}$ for finite $n$, then PA cannot prove $F$ total.


  • $\begingroup$ Very nice, thank you! $\endgroup$ – Peter Dec 25 '14 at 21:54
  • $\begingroup$ Do you also know the limit for ZFC ? $\endgroup$ – Peter Dec 25 '14 at 21:55
  • 1
    $\begingroup$ The result I mentioned is related to the fact that $\varepsilon_0$ is so called proof theoretic ordinal of PA. For similar result for ZFC we would need ordinal which is at least its proof theoretic ordinal, which is far beyond the reach of all known notations. Even then, we are not guaranteed such classification exists. $\endgroup$ – Wojowu Dec 25 '14 at 21:58
  • 1
    $\begingroup$ @Peter ZFC can actually handle fast growing hierarchy up to $\Gamma_0$ (a.k.a. Feferman-Schutte ordinal). $\endgroup$ – Wojowu Dec 25 '14 at 22:02
  • 1
    $\begingroup$ @Peter In fact, the proof theoretic ordinal of ZFC is much, much larger than $\Gamma_0$. Even the Takeuti-Feferman-Buchholz ordinal $\psi(\varepsilon_{\Omega_\omega+1})$ is not coming close. Nor is the proof theoretic ordinal of KPI, which is even larger. The comparison of these ordinals with the proof theoretic ordinal of ZFC is like the comparison of a googolplex with Graham's number, to put it mildly. $\endgroup$ – wythagoras Jul 27 '15 at 8:14

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.