Pfft comments on Open Thread - Aug 24 - Aug 30 - Less Wrong Discussion
You are viewing a comment permalink. View the original post to see all comments and the full post content.
You are viewing a comment permalink. View the original post to see all comments and the full post content.
Comments (318)
I'm very confused about something related to the Halting Problem. I discussed this on the IRC with some people, but I couldn't get across what I meant very well. So I wrote up something a bit longer and a bit more formal.
The gist of it is, the halting problem lets us prove that, for a specific counter example, there can not exist any proof that it halts or not. A proof that it does or does not halt, causes a paradox.
But if it's true that there doesn't exist a proof that it halts, then it will run forever searching for one. Therefore I've proved that the program will not halt. Therefore a proof that it doesn't halt does exist (this one), and it will eventually find it. Creating a paradox.
Just calling the problem undecidable doesn't actually solve anything. If you can prove it's undecidable, it creates the same paradox. If no Turing machine can know whether or not a program halts, and we are also Turing machines, then we can't know either.
I guess the answer to this point is that when constructing the proof that H(FL, FL) loops forever, we assume that H can't be wrong. So we are working in an extended set of axioms: the program enumerates proofs given some set of axioms T, and the English-language proof in the tumblr post uses the axiom system T + "T is never wrong" (we can write this T+CON(T) for short).
Now, this is not necessarily a problem. If you have reason to think that T is consistent, then most likely T+CON(T) is consistent also (except in weird cases). So if we had some reason to adopt T in the first place, then working in T+CON(T) is also a reasonable choice. (Note that this is different from working in a system which can prove its own consistency, which would be bad. The difference is that in T+CON(T), there is no way to prove that proofs using the additional "T is never wrong" axiom are correct).
More generally, the lesson of Gödel's incompleteness theorem is that it does not make sense to say that something is "provable" without specifying which proof system you are using, because there are no natural choice for an "ideal" system, they are all flawed. The tumblr post seems paradoxical because it implicitly shifts between two different axiom sets. In particular, it says
but a correct statement is, we can't prove it either using the same set of axioms as H used. We have to use some addtional ones.