Provability of termination. Whats wrong with my reasoning?

Question

Let A be a pair (i, x)

$H(A)$ <=> program i halts on input x

$P(A)$ <=> (there exists a proof for $H(A)$) $\vee$ (there exists a proof for $\neg H(A)$)

Assume $\forall A: P(A)$ then we can solve the halting problem (write an algorithm that enumerates all proofs and checks whether they proof $H(A)$ or $\neg H(A)$) Therefore $\exists A: \neg P(A)$.

For such an A:

Assume $H(A)$: Then we have a proof for $H(A)$ (the sequence of steps that lead to the halting state). Therefore $\neg H(A)$.

But now we have a proof for $\neg H(A)$ and therefore $P(A)$ which contradicts the definition of A???

I assume I have a basic misconception about something. Please tell me what went wrong?

Thanks

Answer 1

I believe that the error sneaks in with the phrase "for such an A." It is indeed true that for any $A$ such that $\neg P(A)$ we have that $\neg H(A)$; it follows that to be able to prove $\neg P(A)$ actually requires us to be able to prove $\neg H(A)$. You've substituted the a priori knowledge "this is such an $A$" for the proof that this $A$ has the property $\neg P(A)$, but it's the latter of these that you actually need. This avoids any paradox.

Answer 2

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. 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.

Answer 3

The subtlety is that the halting problem asks whether i actually stops on x, not whether we can give a formal proof that i stops or doesn't stop on x. The whole point is that if $\forall A P(A)$ is true you must have proofs of false statements but not the solution of the halting problem. Your first "then" is thus flawed and what you actually proved is just the classical weak form of Godel's theorem.

Answer 4

It is true that $H(A)$ implies that we have a proof of $H(A)$, and we can find it by enumeration: as you noted, a proof of $H(A)$ is just a finite sequence of configurations or states of program $i$ on input $x$, each one of them reachable from the previous one according to the rules described by program $i$ itself (hence, such a proof is algorithmically verifiable).

The problem with your argument is that $\neg H(A)$ does not necessarily imply that we have a proof of it, as you assume when saying “But now we have a proof of $\neg H(A)$”. Some programs can indeed have a non-termination proof; for instance, a finite sequence of configurations of the program that repeat cyclically. But other programs can go through an infinite number of non-recurring configurations: thus, the notion of non-termination proof as a finite sequence of configurations is flawed.

Even by giving a lot of thought to the question, you won’t probably find any satisfying notion of “non-termination proof” applicable to all programs. The reason is that such a notion is provably nonexistent (formally, the set of non-halting programs is not recursively enumerable).