= 27d567bc2d48d9f40e9ccc20ea370b15)
TezlaKoil comments on Open Thread - Aug 24 - Aug 30 - Less Wrong
You are viewing a comment permalink. View the original post to see all comments and the full post content.
= 783df68a0f980790206b9ea87794c5b6)
Loading…= b715d02e85f7b3b4ae65ca3d3e450868)
Subscribe to RSS Feed
Powered by Reddit
= f037147d6e6c911a85753b9abdedda8d)
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.
Fortunately, H will never find your argument because it is not a correct proof. You rely on hidden assumptions of the following form (given informally and symbolically):
where #φ denotes the Gödel number of the proposition φ.
Statements of these form are generally not provable. This phenomenon is known as Löb's theorem - featured in Main back in 2008.
You use these invalid assumptions to eliminate the first two options from Either H returns true, or false, or loops forever. For example, if H returns true, then you can infer that "FF halts on input FF" is provable, but that does not contradict FF does not halt on input FF.
I'm very confused. Of course if φ is provable then it's true. That's the whole point of using proofs.
But that statement isn't provable.
Then just assume it as an axiom.
Then the paradox you were describing fires and the system becomes inconsistent.
Yes, but it may be true without being provable.
It is not that these statements are "not generally valid", but that they are not included within the axiom system used by H. If we attempt to include them, there will be a new statement of the same kind which is not included.
Obviously such statements will be true if H's axiom system is true, and in that sense they are always valid.
The intended meaning of valid in my post is "valid step in a proof" in the given formal system. I reworded the offending section.
Yes, and one also has to be careful with the use of the word "true". There are models in which the axioms are true, but which contain counterexamples to
Provable(#φ) → φ.