Growth-rate vs totality
How can one prove the statement, "If a function grows fast enough, it cant be proven total in PA, unless PA is inconsistent"? How fast must it grow to be not provably total?
Solution 1:
There is a hierarchy of fast-growing functions $f_\alpha:\mathbb N\to\mathbb N$ indexed by ordinals $\alpha<\epsilon_0$, where $\epsilon_0$ is the first ordinal fixed point of the ordinal exponentiation map $\tau\mapsto\omega^\tau$, that is, $$ \epsilon_0=\omega^{\omega^{\dots}}. $$ (Note that this is a countable ordinal.) Let $\zeta_0=1$ and $\zeta_{k+1}=\omega^{\zeta_k}$ for $k\in\mathbb N$.
For each $k\ge0$, let $I\Sigma_{k+1}$ denote the restriction of Peano Arithmetic where the induction axiom is only stated for $\Sigma_{k+1}$-formulas, so $\mathsf{PA}$ is the union of all the $I\Sigma_{k+1}$ for $k\in\mathbb N$.
Theorem. (Wainer) If $f$ is a recursive function, provably total in $I\Sigma_{k+1}$ , then $f$ is eventually dominated by some $f_\alpha$, $\alpha<\zeta_{k+1}$. In particular, any recursive $f$ provably total in $\mathsf{PA}$ is eventually dominated by some $f_\alpha$, $\alpha<\epsilon_0$.
Note that the function $f$ must be recursive. There are non-recursive functions that only take the values $0$ and $1$, so this restriction is essential. The specific hierarchy of functions we pick is not so important. All natural hierarchies that have been considered give the same result that $\epsilon_0$ is the limit. The specific hierarchy mentioned in the theorem is defined as follows:
Any ordinal $\alpha<\epsilon_0$ can be written in a unique way as $\alpha=\omega^\beta(\gamma+1)$ where $\beta<\alpha$ (note that $\beta$ could be $0$). By transfinite recursion, define for limit $\alpha<\epsilon_0$ an increasing sequence $(d(\alpha, n)\mid n<\omega)$ cofinal in $\alpha$ by setting $$ d(\alpha, n) = \omega^\beta\gamma+\left\{\begin{array}{cl}\omega^\delta n&\mbox{ if }\beta=\delta+ 1,\\ \omega^{d(\beta,n)}&\mbox{ if }\beta \mbox{ is limit.}\end{array}\right. $$ The fast growing hierarchy $(f_\alpha)_{\alpha<\epsilon_0}$ of functions $f:\mathbb N\to\mathbb N$, due to Löb and Wainer, can now be defined as follows:
- $f_0 (n) = n + 1$.
- For $\alpha<\epsilon_0$, $f_{\alpha+1} (n) = f^n_\alpha(n)$, where the superindex indicates that $f_\alpha$ is iterated $n$ times.
- For limit $\alpha<\epsilon_0$, $f_\alpha(n) = f_{d(\alpha,n)} (n)$.
Note that these functions grow very fast indeed. One can prove that these functions are strictly increasing, and that whenever $\alpha<\beta<\epsilon_0$, there is a number $m$ such that $f_\alpha(n)<f_\beta(n)$ for all $n\ge m$. We say that $f_\beta$ eventually dominates $f_\alpha$.
In Ramsey theory one sometimes encounters the first four or five levels $f_0$–$f_4$ and rarely one needs to go up to $f_\omega$: Note that $f_1(n)=2n$, $f_2(n)=n2^n$, $f_3(n)$ is larger than a stack of $n$ powers of $2$, etc. The function $f_\omega$ grows roughly as fast as the diagonal of Ackermann's function, so it eventually dominates all primitive recursiev functions. Goodstein's problem requires all the functions up to $\epsilon_0$ and therefore the totality of Goodstein's function is not provable in $\mathsf{PA}$. Several famous unprovability results have been established the same way. Typically, unprovability in arithmetic considers $\Pi^0_2$ sentences, statements $\phi$ of the form "For all $n$ there is an $m$ such that $\psi(n,m)$" where $\psi(n,m)$ is an easily verifiable (recursive) statement about $n,m$. This naturally gives rise to a function, $f(n)=m$ iff $m$ is the least number such that $\psi(n,m)$ holds. If $\phi$ is true, then $f$ is a recursive function: To compute $f(n)$, you consider in succession all natural numbers, verifying for each $k$ whether $\psi(n,k)$ holds. As soon as we find one such $k$, that is the value of $f$. This search succeeds, since $\phi$ is true, so $\psi(n,m)$ holds for some $m$, and therefore there is a least such $m$. The issue is whether the formal statement $\phi$ is provable from $\mathsf{PA}$, which is equivalent to the question of whether $\mathsf{PA}$ can prove that $f$ is a total function. In view of Wainer's theorem, this means that we should verify whether $f$ is eventually dominated by some $f_\alpha$, $\alpha<\epsilon_0$. In practice, when $\phi$ is not provable, we usually show that in fact $f$ eventually dominates each $f_\alpha$, $\alpha<\epsilon_0$. This is the case, for example, for Goodstein's function.
I list now some references, taken from my paper on Goodstein's function, available at my papers page. To get an idea of how fast these functions grow, I suggest you look at the few values of Goodstein's function I compute in that paper.
Fairtlough, M., and Wainer, S. Handbook of Proof Theory. Elsevier-North Holland, 1998, ch. Hierarchies of provably recursive functions, pp. 149–207.
Löb, M., and Wainer, S. Hierarchies of number theoretic functions. I. Arch. Math. Logik Grundlagenforsch. 14 (1970), 39–51.
Wainer, S. A classification of the ordinal recursive functions. Arch. Math. Logik Grundlagenforsch. 13 (1970), 136–153.
Note that the hierarchy can be extended significantly past $\epsilon_0$ (maintaining that the functions are increasing, and each new one eventually dominates its predecessors), and unprovability results in stronger systems are sometimes obtained by appropriate generalizations of Wainer's results to these other systems. The question of how to extend these functions is always the question of how to pick for (smallish) countable ordinals $\alpha$ a cofinal sequence in an explicit fashion. This leads to the delicate topic of natural well-orderings, see
John N. Crossley, Jane Bridge Kister. Natural well-orderings, Archiv für mathematische Logik und Grundlagenforschung, 26 (1), (1987), 57-76.
Solution 2:
The fast-growing hierarchy (or Wainer hierarchy) has the property that a recursive function is $\sf{PA}$-provably total iff it is dominated by $f_\alpha$ for some $\alpha < \varepsilon_0$. (Similarly with the Hardy hierarchy.)
For example, the Goodstein function grows asymptotically with $f_{\varepsilon_0}$, and so is not $\sf{PA}$-provably total (this is essentially Cichon's and Caicedo's proofs of the Kirby-Paris result that Goodstein's theorem is not $\sf{PA}$-provable).