In his classic book Computational Complexity, Papadimitriou writes (page 59) that
Undecidability is in some sense the most lethal form of complexity.
I’ve just come across a paper with a very interesting remark along the same lines: Making proofs without Modus Ponens: An introduction to the combinatorics and complexity of cut elimination by A. Carbone and S. Semmes, published in the Bulletin of the American Mathematical Society. This paper is about the length of proofs (a subject I’ve already touched upon here and here) without cut elimination.
On page 113, the authors write
By contrast [with propositional logic] in predicate logic one typically faces issues of algorithmic decidability or undecidability. That is, whether there is an algorithm at all that always gives the right answer, never mind how long it takes. The problem of determining whether a formula in predicate logic is a tautology is algorithmically undecidable. One can think of this as a matter of complexity, as follows. The tautologies in predicate logic of length at most n form a finite set for which one can choose a finite set of proofs. Let f(n) denote the maximum of the lengths of the shortest proofs of tautologies of length ≤ n. The fact that there is no algorithm for determining whether or not a formula is a tautology means that f(n) grows very fast, faster than any recursive function.
Essentially, this means that we can’t design an algorithm to solve an undecidable problem because the search space is too large, and the only way to somehow bound it is via a function that grows faster than any computable function. Compare this with the search space of the “witnesses” for an NP-complete problem: its size is exponential, which is too large to be explored efficiently (at least, as far as we know at the moment), but still small enough to make the problem decidable.
While digging in the early computability literature, I found a precious and long forgotten account of the history of Hilbert’s problems. I’m proud to present my discovery to the scientific community.
*** david (daboss@uni-göttingen.de) has joined #logic
<david> plz, solve integer eqns and prove completness of teh arithmetics
<kurt> just 1 sec, brb
* kurt is away: proving some stuff
* kurt is back
<kurt> lol dave, taek a look at this: http://is.gd/dAo7d
<david> at least solve teh entsk^Wentschi^W entscheidungsproblem...
<alonzo> cant do that, lambada calculus proves it
<kurt> oh stfu alonzo
<alan> my machiens are liek people and cant do it
<alonzo> alan: your right, and so am i (told ya)
<kurt> lol dave, epic fail!!1!
<david> wtf is wrong with you ppl??
<gottlob> i kno the feeling bro
*** david (daboss@uni-göttingen.de) has left #logic (pwnd)
After a few pages (omitted here) there’s a final remark on the subject:
<yuri> oh btw, cant solve integer eqns either
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.
One of the most amazing facts about (un)computability is the existence of functions f : ℕ → ℕ that grow faster than any recursive function, that is, for all computable g : ℕ → ℕ we have
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 φ of arithmetic such that the shortest proof is greater than f(⌜φ⌝) in length.
In other words, some theorems just have really freaking long proofs. See the SEP article for the details.