MathOverflow will be down for maintenance for approximately 3 hours, starting Monday evening (06/24/2013) at approximately 9:00 PM Eastern time (UTC-4).

2 added 430 characters in body; edited body

What you have (re)discovered is a proof of Goedel's first incompleteness theorem via the halting problem. Let us suppose that we have already established that the halting problem is undecidable, which is not difficult to prove.

Theorem.(Goedel) There is no computational algorithm to determine whether a given statement is true or not in the natural numbers.

Proof. If there were such an algorithm, then for any program e and input n, we could form the statement "program e halts on input n" and check by the supposed computational procedure whether this statement is true or not. This would enable us to solve the halting problem, which is impossible. QED

The argument can be refined to the following:

Corollary. For any computable collection of axioms of arithmetic T, there is a statement φ that is true, but not provable in T. Furthermore, φ can be taken to be of the form: "a certain Turing machine program e never halts on a particular input n".

Proof. Let us suppose that all true statements of that form were provable in T. Then we would be able to solve the halting problem, as follows: given program e and input n, then during the day, we simultate the progress of e on n. If it ever halts, we say, Yes, it halted. Meanwhile, at night, we search through all possible proofs from T, which is a computably enumerable procedure since T has a computable set of axioms, and look for a proof that e does not halt on n. If we ever find such a proof, then we say, No, it won't halt. Our assumptions ensure that exactly one of these situations will eventually occur, and so we will solve the halting problem, which is impossible. QED

(

In particular, the error in your reasoning was your assumption that if a particular program did not halt, then this was a provable fact.) In contrastfact. You gave an argument for ¬H(A) for the A you found with ¬P(A), and this much is right, for when a program does halt, then this is witnessed by a particular halting computation, and even very weak axiomatic systems can prove that the program does indeed halt. But this proof does not take place within the same formal system as your proof notion used in P. I view this part of your argument as an argument by cases: for the A such that ¬P(A), you have ruled out the case that H(A). The remaining case is that A does not halt, and you have no reason to assume that this fact is provable in your system. What the argument shows is that it is difficult (or impossible in principle) for a system to prove all instances of non-halting behavior.

I like this version of the proof of the Incompleteness theorem very much, because one can explain it to anyone who is familiar with the undecidability of the halting problem. In my view, it makes the otherwise mysterious claims of the Incompleteness theorem relatively accessible.

One drawback of this method, however, is that it does not so easily extend to a proof of the second incompletness theormem, the statement that no computably axiomatizable theory can prove its own consistency.

1

What you have (re)discovered is a proof of Goedel's first incompleteness theorem via the halting problem. Let us suppose that we have already established that the halting problem is undecidable, which is not difficult to prove.

Theorem.(Goedel) There is no computational algorithm to determine whether a given statement is true or not in the natural numbers.

Proof. If there were such an algorithm, then for any program e and input n, we could form the statement "program e halts on input n" and check by the supposed computational procedure whether this statement is true or not. This would enable us to solve the halting problem, which is impossible. QED

The argument can be refined to the following:

Corollary. For any computable collection of axioms of arithmetic T, there is a statement φ that is true, but not provable in T. Furthermore, φ can be taken to be of the form: "a certain Turing machine program e never halts on a particular input n".

Proof. Let us suppose that all true statements of that form were provable in T. Then we would be able to solve the halting problem, as follows: given program e and input n, then during the day, we simultate the progress of e on n. If it ever halts, we say, Yes, it halted. Meanwhile, at night, we search through all possible proofs from T, which is a computably enumerable procedure since T has a computable set of axioms, and look for a proof that e does not halt on n. If we ever find such a proof, then we say, No, it won't halt. Our assumptions ensure that exactly one of these situations will eventually occur, and so we will solve the halting problem, which is impossible. QED

(In particular, the error in your reasoning was your assumption that if a particular program did not halt, then this was a provable fact.) In contrast, when a program does halt, then this is witnessed by a particular halting computation, and even very weak axiomatic systems can prove that the program does indeed halt. What the argument shows is that it is difficult (or impossible in principle) for a system to prove all instances of non-halting behavior.

I like this version of the proof of the Incompleteness theorem very much, because one can explain it to anyone who is familiar with the undecidability of the halting problem. In my view, it makes the otherwise mysterious claims of the Incompleteness theorem relatively accessible.

One drawback of this method, however, is that it does not so easily extend to a proof of the second incompletness theormem, the statement that no computably axiomatizable theory can prove its own consistency.