Provability of termination. Whats wrong with my reasoning?

Remember to vote up questions/answers you find interesting or helpful (requires 15 reputation points)

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

-

4 Answers

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.

-

+1                  . – Joel David Hamkins Apr 17 2010 at 21:31

You can accept an answer to one of your own questions by clicking the check mark next to it. This awards 15 reputation points to the person who answered and 2 reputation points to you.

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.

-
(In particular, the error...) I thought of deleting my answer since yours makes the same point but is much more elaborate but then I saw this sentence. No, epthh hasn't made this particular error. His actual error was exactly in the opposite direction. – fedja Apr 16 2010 at 22:55
"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. " Is there any way to do this with the recursion theorem? I know Sipser uses it to construct an explicit statement in arithmetic which is not provable (from any recursively enumerable proof system, I suppose). Is there any connection between the self-reference in the recursion theorem and in the second incompleteness theorem? – Akhil Mathew Apr 16 2010 at 23:31

2
The error in the argument begins with the phrase "But now we have a proof that not H(A)...", which is exactly the error that I mentioned, of assuming that since A does not halt that there is a proof that A does not halt. The argument up to that point is that if H(A) is true, then this is provable (which is fine), but this doesn't mean that if H(A) is not true, then THAT fact is provable. – Joel David Hamkins Apr 16 2010 at 23:38

1
You are right: once you have an erratic argument, there is more than one way to find the closest correct one and decide what exactly went wrong. Anyway, I guess we've covered all possible interpretations by now and there is no real point in trying to discuss which meaning was originally intended :-). – fedja Apr 17 2010 at 1:20

1
Epthh, in fact one can always find a particular A, which does not halt, but such that the original theory T does not prove this. For example, let A be the program that searches for a proof of a contradiction in T, halting when one is found. If T is consistent, then this program does not halt, but T cannot prove that it does not halt, since then it would prove its own consistency. The proof I just gave that A does not halt--analogous to your proof of not-H(A)--is not a proof in T, however, but a proof in T+Con(T), a stronger theory. – Joel David Hamkins Apr 17 2010 at 11:13
show 7 more comments

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.

-

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

-
{"extraction_info": {"found_math": true, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 31, "mathjax_display_tex": 0, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0}, "config": {"markdown_headings": false, "markdown_code": true, "boilerplate_config": {"ratio_threshold": 0.18, "absolute_threshold": 10, "end_threshold": 15, "enable": true}, "remove_buttons": true, "remove_image_figures": true, "remove_link_clusters": true, "table_config": {"min_rows": 2, "min_cols": 3, "format": "github"}, "remove_chinese": true, "remove_edit_buttons": true, "extract_latex": true}, "english_confidence": 0.9490441083908081, "perplexity_flag": "head"}