Proof of Godel's Incompleteness Theorem based on Recursion Theorem

Question

I'm looking for a proof of Godel's Incompleteness Problems based on the recursion theorem in computability theory. I've skimmed lots of textbooks but I haven't found such proof. Can you name some useful books? or simply bring such proof here.

Answer 1

Here is such a proof (of the strong version of GIT$1$ - that every consistent recursively axiomatizable theory extending PA is incomplete). See also this Mathoverflow post (and the rest of the answers there).

---

Short version: Let $T$ be a recursively axiomatizable extension of PA. By the recursion theorem and the recursive axiomatizability of $T$, there is some $\Phi_c$ such that $T$ proves

• $\Phi_c(0)\downarrow$ if there is a $T$-proof of $\Phi_c(0)\uparrow$ shorter than any $T$-proof of $\Phi_c(0)\downarrow$, and

• $\Phi_c(0)\uparrow$ if there is a $T$-proof of $\Phi_c(0)\downarrow$ shorter than any $T$-proof of $\Phi_c(0)\uparrow$.

But then if $T$ decides whether $\Phi_c(0)\downarrow$, we have a contradiction in $T$: there must be a $T$-proof of one answer shorter than any $T$-proof of the other answer, but then $T$ also proves the opposite of that answer.

---

Long version:

• Fix a recursive set of axioms $T$ extending PA. Since $T$ is recursive, we can "search through all $T$-proofs" - that is, there is a recursive function $f$ such that $T$ proves that for every $e$ we have:

  • If there is some $T$-proof of $\Phi_e(0)\downarrow$ shorter than any $T$-proof of $\Phi_e(0)\uparrow$, then $\Phi_{f(e)}(0)\uparrow$.

  • If there is some $T$-proof of $\Phi_e(0)\uparrow$ shorter than any $T$-proof of $\Phi_e(0)\downarrow$, then $\Phi_{f(e)}(0)\downarrow$.

  • If there is no $T$-proof of either $\Phi_e(0)\downarrow$ or $\Phi_e(0)\uparrow$, then $\Phi_{f(e)}(0)\uparrow$.

    • Specifically, $\Phi_{f(e)}(0)$ searches in order of length through $T$-proofs until it finds a $T$-proof of either $\Phi_{e}(0)\downarrow$ or $\Phi_e(0)\uparrow$. As soon as it finds one, it stops searching, and it goes into an endless loop in the former case and halts immediately in the latter case (and if the search never stops, i.e. if there is no $T$-proof of either statement, then $\Phi_{f(e)}(0)$ never halts). It's easy but tedious to cook up a recursive $f$ which has this property provably in PA (and hence in $T$).

• Now by the recursion theorem, we get some $c$ such that $\Phi_c\cong\Phi_{f(c)}$ - in particular, we have $$\Phi_c(0)\downarrow\iff\Phi_{f(c)}(0)\downarrow.$$

• We now use a basic-but-important fact about PA: for any recursive set of sentences $S$ and any pair of sentences $\varphi,\psi$, if there is an $S$-proof of $\varphi$ shorter than any $S$-proof of $\psi$ then PA (and hence $T$) proves that there is an $S$-proof of $\varphi$ shorter than any $S$-proof of $\psi$. This just amounts to PA's ability to $(i)$ verify validity of $S$-proofs (this again comes down to the recursiveness of $S$) and $(ii)$ "perform finite searches" (that is, search through all possible proofs shorter than a given one).

• OK, what does this fact have to do with our argument? Well, I claim that this gives a contradiction in $T$, unless $T$ leaves "$\Phi_c(0)\downarrow$" undecided. Here's why:

  • Suppose there is a $T$-proof of $\Phi_c(0)\downarrow$ shorter than any $T$-proof of $\Phi_c(0)\uparrow$. Then by our above discussion, PA (and hence $T$ as well) proves $\Phi_c(0)\downarrow$. But then $T$ proves both $\Phi_c(0)\uparrow$ and $\Phi_c(0)\downarrow$, and hence is inconsistent.

  • Similarly, if there is a $T$-proof of $\Phi_c(0)\uparrow$ shorter than any $T$-proof of $\Phi_c(0)\downarrow$, PA - and hence $T$ - proves that, and so proves in turn that $\Phi_c(0)\downarrow$; but then we have again that $T$ proves both $\Phi_c(0)\uparrow$ and $\Phi_c(0)\downarrow$.

  • OK, so we've ruled out both a $T$-proof of $\Phi_c(0)\downarrow$ shorter than any $T$-proof of $\Phi_c(0)\uparrow$ and a $T$-proof of $\Phi_c(0)\uparrow$ shorter than any $T$-proof of $\Phi_c(0)\downarrow$. But this means that $T$ can't decide whether $\Phi_c(0)\downarrow$!

(In fact, the entire argument above goes through in PA itself, so in fact we've shown that PA proves that every consistent recursively axiomatizable extension of PA is incomplete - the key facts we need to be able to prove in PA are the recursion theorem, basic properties of "arithmetizing" computations, and the "$\Sigma_1$-completeness" of PA.)

---

Remark: The "shorter than any proof of" clause is very similar to Rosser's trick, which improved Godel's incompleteness theorem to its usually-stated strong form: Godel's original argument needed $T$ to be $\omega$-consistent, which is a strictly stronger property than mere consistency; actually, all he really needed was $\Sigma_1$-soundness, but that's still stronger than mere consistency. Essentially, the original Godel sentence was "This sentence is unprovable," and Rosser showed that if we use "For every proof of this sentence there is a shorter disproof of this sentence" gave a stronger result.

The point here is that while Rosser's trick in the standard "sentence-based" proof was clever, in the "machine-based" proof it's forced upon us right from the get-go: when we search for a proof, we're searching in some order, and all we can ever be totally sure of is that we know what's happened so far. So the machine-based argument in some sense makes Rosser's idea more natural - at least, in my opinion.

Answer 2

Indeed there is a computability-based proof of the generalized incompleteness theorems (only requiring that the system has a proof verifier program and interprets arithmetic) explained in this post, showing that if it does not prove (the translation of) "$0=1$" then it also does not prove some true arithmetic sentence, and we can even uniformly generate such a sentence given the proof verifier program.

The trick is very simple and elegant: we simply reduce the incompleteness theorem to the uncomputability of the zero-guessing problem, in which the solver must halt on every input pair $(p,x)$ and guess whether the program $p$ on the input $x$ will produce $0$ as the output, and must be correct whenever $p$ really halts on $x$. Details are in the linked post. Naturally, one can use the recursion theorem to show that a particular formal system in question can reason about programs.

I learnt this trick from Scott Aaronson's blog post, but it can also be found in Kleene's 1967 logic text.