Return to Answer

Another fact for classical T is that T is consistent iff Q' is true. We have already shown that if T is consistent then Q' is true. If T is inconsistent and classical then by the principle of explosion T proves both Q and Q', and so H(C,C) halts, and hence C(C) does not halt. Similarly if T is classical then T is consistent iff D(D) does not halt.

Another fact for classical T is that T is consistent iff D(D) does not halt. We have already shown that if T is consistent then D(D) does not halt. If T is inconsistent and classical then by the principle of explosion T proves both W and W', and so G(D,D) halts, and so D(D) halts.

We do not even need T to be classical if we modify G to halt if at some point it has found proofs within T of opposite statements. With this, it suffices to have the following extra condition on T (which is compatible with T being intuitionistic):
  If T proves "It is not true that the program P halts on input X.":
    T proves "It is not true that the program P halts on input X and outputs Y.".
If T is inconsistent:
  G(D,D) halts (due to the modification).
  Thus D(D) halts.
If T is consistent:
  G behaves exactly as before.
  Thus D(D) does not halt.
  And T does not prove "It is not true that the program D halts on input D and outputs 0.".
  Thus T does not prove "It is not true that the program D halts on input D.".
  Thus T does not prove something equivalent to its own consistency!

Given any program H:
  Let C be the program that does the following on input P:
    If H(P,P) = "false" then output "haha" (and halt) otherwise infinite-loop (not halting).
  Then C(C) halts iff H(C,C) = "false", by definition of C.
  Thus H does not solve the halting problem.

Given any program G :
  Let D be the program that does the following on input P:
    If G(P,P) = 0 then output 1 otherwise output 0.
  If D(D) halts:
    D(D) ≠ 0 iff G(D,D) = 0, by definition of D.
  Therefore G does not solve the zero-guessing problem.

Given any program H:
  Let C be the program that does the following on input P:
    If H(P,P) = "false" then output "haha" (and halt) otherwise infinite-loop (not halting).
  If H solves the halting problem:
    H(C,C) halts, and hence C(C) halts iff H(C,C) = "false", by definition of C.
    Contradiction with definition of H.
  Thus H does not solve the halting problem.

Given any program G :
  Let D be the program that does the following on input P:
    If G(P,P) = 0 then output 1 otherwise output 0.
  If G solves the zero-guessing problem:
    G(D,D) halts, and hence D(D) ≠ 0 iff G(D,D) = 0, by definition of D.
    Contradiction with definition of G.
  Therefore G does not solve the zero-guessing problem.

Generalization to uncomputable formal systems

One nice aspect of this computability-based viewpoint is that it automatically relativizes to any kind of class Ω of oracle programs. In particular, the same proof yields the incompleteness theorems for formal systems whose proof verifier is a program in Ω and that can reason about programs in Ω. This result can be used to prove that the arithmetical hierarchy does not collapse to any level, like shown in this post.

The blog post by Scott Aaronson that inspired some of this, which cites Kleene's 1967 Mathematical Logic text as giving a similar computability-based proof of Rosser's theorem (Theorem VIII and Corollary I on pages 286−288).

A formal version of the above proof of Rosser's incompleteness theorem for formal systems that interpret PA− can be found.

A brief discussion of foundational issues and philosophical remarks about the halting problem and the incompleteness theorem.

A brief explanation of the fixed-point combinator in λ-calculus mentioned above.

The blog post by Scott Aaronson that inspired some of this, citing Kleene's 1967 Mathematical Logic text for a similar proof of Rosser's theorem (Theorem VIII and Corollary I on pages 286−288).

A 1944 paper by Emil Post sketching a proof corresponding loosely to the above proof via the halting problem for formal systems that are sound for program halting. (Thanks Philip White!)

A formal version of the above proof of Rosser's theorem for formal systems that interpret PA−.

A discussion of foundational issues regarding the halting problem and the incompleteness theorem.

An explanation of the fixed-point combinator in λ-calculus mentioned in the opening paragraph.