Godel's incompleteness: can the diagonalization be done in computation rather than logic? 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!
 A: 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.
