I have always had trouble understanding Godel's proof of his first incompleteness theorem, because the diagonalization part is done on the logical side, which is unfamiliar to me, rather than on the computational side, which I find more familiar. I decided to replicate the proof but do as much of the work as possible in terms of computation, rather than logic.
Consider the Turing machine $H$ which when run on input $x$:
- (firstly a triviality) checks whether $x = \lceil \phi \rceil$ for some two-place predicate $\phi$ and if not then loops forever (or indeed it could do anything – I don't believe this part of the argument is important!)
- searches for proofs in PA of
- $\phi(\lceil\phi\rceil, 1)$ and
- $\lnot\phi(\lceil\phi\rceil, 1)$ [A]
- if it finds the former first, it halts writing $0$ on its tape
- if it finds the latter first, it halts writing $1$ on its tape
- if there is a proof of neither, it loops forever
Since computable functions are expressible in PA, there is a two-place predicate $h$ such that $H(x) = y$ implies $\vdash h(\underline{x}, \underline{y})$ and $H(x) \not= y$ implies $\vdash \lnot h(\underline{x}, \underline{y})$ [B].
Then what is $H(\lceil h \rceil)$?
- if $H(\lceil h \rceil) = 0$ then $\vdash h(\lceil h \rceil, 1)$ (by definition of $H$) and $\vdash \lnot h(\lceil h \rceil, 1)$ by definition of $h$
- if $H(\lceil h \rceil) = 1$ then $\vdash \lnot h(\lceil h \rceil, 1)$ (by definition of $H$) and $\vdash h(\lceil h \rceil, 1)$ by definition of $h$
- if $H(\lceil h \rceil)$ is anything else, including a non-terminating computation, then neither $\vdash h(\lceil h \rceil, 1)$ nor $\vdash \lnot h(\lceil h \rceil, 1)$
My conclusion is that either PA is inconsistent (first two possibities) or incomplete (third possibility).
My first question is: is this a correct proof that PA is either inconsistent or incomplete? I don't want to be misled by a simple misunderstanding!
My second question is: if indeed it is a correct proof, why are the common expositions not done this way? It seems much more easy to do the diagonalization part of the argument in the world of Turing machines and computation than in the world of wffs and logic. Moreover no weakening to $\omega$-consistency is necesary.
Footnotes:
[A] In wffs, $1$ is my abbreviation for $s(0)$ of course.
[B] I use $\vdash \psi$ to mean there is a proof in PA of $\psi$. Perhaps this is more usually denoted $\vdash_{PA} \psi$, but I wanted to conserve space and typing!
Best Answer
There are indeed many proofs of the incompleteness theorem, and when I teach my introductory graduate logic course, we usually give at least four or five different proofs as they arise naturally with the different topics. Here are a few sketches of different proof methods that commonly arise:
Traditional proof via the fixed point lemma. This is the traditional proof via the fixed-point lemma, by which we know that for each formula $\varphi(x)$ there is a sentence $\psi$ such that $PA\vdash\psi\leftrightarrow\varphi(\psi)$. With this lemma, one makes the Goedel sentence $\psi$ that asserts that $\psi$ is not provable in PA. It follows that indeed it is not provable in PA, and hence it is true and unprovable.
Via the halting problem. This is the proof via the halting problem, and uses some similar ideas to your proposed proof. First, one proves that the halting problem is not decidable by any computable procedure. Next, one argues that there must be a Turing machine $p$ which does not halt, but we cannot prove it in PA, since otherwise we can solve the halting problem as follows: given a Turing machine program, we simulate it during the day, waiting to see if it halts, and at night, we search for a proof that it doesn't halt. If all instances of non-halting were provable, we would thereby solve the halting problem.
Via the existence of undecidable problems. Indeed, if there is any computably undecidable problem that is expressible in arithmetic, then there must be instances that cannot be settled in PA (or any othere computably axiomatizable theory), since otherwise by searching for proofs we would be able to decide the problem. This observation is at the core of the connection between two common uses of the word "undecidable". Namely, any c.e. set $A$ that is not (computably) decidable must admit infinitely many natural numbers $n$ such that $n\notin A$ but this is not provable in your favorite formal system, since otherwise $A$ would be decidable. So the computably undecidable sets are saturated with non-instances that are undecidable in your formal system.
Via Tarski's theorem. Tarski's theorem is that there is no arithmetic predicate true of exactly the Goedel codes of true arithmetic assertions. That is, arithmetic truth is not arithmetically definable. This is a generalization of the incompleteness theorem, since provability is arithmetically definable, and so it cannot coincide with truth. One can prove Tarski's theorem in a variety of ways, including the fixed point lemma, or the non-collapse of the arithmetic hierarchy, among others.
Via the non-collapse of the arithmetic hierarchy. It is not difficult to prove the existence of a universal $\Sigma_1^0$-set of natural numbers. This is analogous to the arithmetization of syntax in the traditional syntactic proof or to the existence of universal machines used in the halting problem proof. Once one knows that there are universal $\Sigma_1^0$ sets, it follows by an easy diagonalization that $\Sigma^0_1\neq\Pi^0_1$ and the arithmetic hierarchy does not collapse. This immediately implies Tarski's theorem, which as we've said implies that provability (which is arithmetic) does not coincide with truth.
By the end of my course, it often becomes a running joke that every new theorem also implies the incompleteness theorem, and I usually try to make those conclusions explicit. So there are indeed many other proof methods besides the main ones I mention above, and perhaps other users will post them. It is generally much easier to find proofs of the first incompleteness theorem than the second, but by now there are also interesting proofs of the second incompleteness theorem from various directions.