Last week I wrote a post about arithmetical theorems having very long proofs, and linked to an article on the SEP for the details. Today, me and my colleague Luca Manzoni realised that there is a much simpler proof; it is essentially the same proof described by Scott Aaronson for the uncomputability of the busy beaver function, and it holds for any undecidable, recursively axiomatisable theory T (that is, if there exists a recursive set of axioms generating the sentences of the theory, but no decision procedure for checking whether a sentence is a theorem).
Let L(φ) be the length in symbols of the shortest proof of the sentence φ, using a standard set of inference rules together with any recursive set of axioms for T; set L(φ) = 0 if φ is not a theorem. Also, let L(n) be the maximum L(φ) among all sentences φ of length at most n.
Theorem. L grows faster than any computable function.
Proof. Otherwise, given a sentence φ, we can first compute an integer f (|φ|) ≥ L(|φ|), then enumerate all proofs of length at most f (|φ|) and check them. If at least one of these is a proof of φ, we answer “yes”, otherwise “no”. But this is a decision procedure for T, since we know that if φ is a theorem, then it has a proof of length at most f (|φ|); contradiction. □
In particular, the theorem holds for Peano arithmetic and friends.