4 July 2010
One of the most amazing facts about (un)computability is the existence of functions $f \colon \mathbb{N} \to \mathbb{N}$ that grow faster than any recursive function, that is, for all computable $g \colon \mathbb{N} \to \mathbb{N}$ we have
\[\displaystyle \lim_{n \to \infty} \frac{g(n)}{f(n)} = 0.\]The most common function of this kind is the busy beaver function, described by Tibor Radó in his paper On non-computable functions; for an introduction to this topic, you can read the excellent paper Who can name the bigger number? by Scott Aaronson (that’s where I first read about it).
Radó’s paper was published in the Bell System Technical Journal in 1962 but, as often happens, related work was done before by Kurt Gödel; see, for instance, the paper bearing the same title as this post, whose translation can be found in the classic collection The Undecidable (edited by Martin Davis).
A cool result that can be proved is that the length of the proofs of arithmetical statements also grows faster than any recursive function. Quoting Juliette Kennedy’s article about Gödel on the Stanford Encyclopedia of Philosophy:
Theorem 5. Given any recursive function $f$ there are provable sentences $\varphi$ of arithmetic such that the shortest proof is greater than $f(\ulcorner\varphi\urcorner)$ in length.
In other words, some theorems just have really freaking long proofs. See the SEP article for the details.