Timeline for Provability of termination. Whats wrong with my reasoning?
Current License: CC BY-SA 2.5
14 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Apr 18, 2010 at 7:05 | comment | added | Charles Stewart | @Joel: You are quite right about the error in my, now deleted, answer. | |
| Apr 17, 2010 at 11:13 | comment | added | Joel David Hamkins | 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. | |
| Apr 17, 2010 at 10:29 | comment | added | user5415 | "What I meant was that by ruling out H(A), I have a proof of $\neg P(A)$" should be "proof of $\neg H(A)$" of course | |
| Apr 17, 2010 at 10:21 | comment | added | user5415 | Thanks for the detailed explanations. "for the A such that $\neg 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 I meant was that by ruling out H(A), I have a proof of $\neg P(A)$. Which is true but requires the assumption of $\neg P(A)$ which is not provable. (I only showed that there exists an A with $\neg P(A)$ but this is not equal to being able to a proof that a given A has that property. JBL pointed that out directly, that's why I marked his answer.) | |
| Apr 17, 2010 at 1:20 | comment | added | fedja | 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 :-). | |
| Apr 17, 2010 at 0:41 | comment | added | Joel David Hamkins | Fedja, I suppose there are several ways to take the argument. One can take it as an argument by cases, as I did, first ruling out the case H(A), and then considering the case ¬H(A), but making the error I mention. Another way is to take the argument, as you do, as a claim to have proved ¬H(A) for that A, but here the error is that this proof is not a proof in the same formal system as in the original statement. | |
| Apr 17, 2010 at 0:10 | comment | added | fedja | @Joel. Not quite. As far as I understand it, he meant that his argument itself was a valid proof of $\neg H(A)$. Actually, as a proof, it has two errors: the first is "then we have a solution of the halting problem" and the second is that "there exists $A$ such that $\neg P(A)$" constitutes a valid proof of $\neg P(A)$. JBL pinpointed the second and I pinpointed the first. But the derivation of $\neg H(A)$ from $\neg P(A)$ is perfectly fine. He never used the statement that "not halting" implies "provably not halting". Moreover, he clearly distinguished the two from the very beginning. | |
| Apr 16, 2010 at 23:54 | comment | added | Joel David Hamkins | Fedja, I added some explanation about this point. | |
| Apr 16, 2010 at 23:53 | history | edited | Joel David Hamkins | CC BY-SA 2.5 |
added 430 characters in body; edited body
|
| Apr 16, 2010 at 23:44 | comment | added | Joel David Hamkins | Akhil, it seems that many logicians have remarked that the second incompletness theorem is more profound than the first, which is amenable to these kinds of proofs. The proof I explain above also provides an explicit statement that is true but not provable, just as you claim for Sipser. Namely, I proved that for every true formal system, there is a statement having the form "program e halts on input n" that is true but not provable. I don't know of any way to turn these kinds of arguments into a proof about proving consistency, without basically re-proving the second incompleteness theorem. | |
| Apr 16, 2010 at 23:38 | comment | added | Joel David Hamkins | 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. | |
| Apr 16, 2010 at 23:31 | comment | added | Akhil Mathew | "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? | |
| Apr 16, 2010 at 22:55 | comment | added | fedja | (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. | |
| Apr 16, 2010 at 22:28 | history | answered | Joel David Hamkins | CC BY-SA 2.5 |