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!