On the length of proofs (episode II)

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.


Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s