Johnicholas comments on LW/OB Quotes - Fall 2009 - Less Wrong
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 (48)
Assume there is either a proof for, against or for independence for every statement within the Peano axiom system.
For every program P you could create a statement S(P)="does this program ever halt?". Now you could solve the halting problem: For given P, iterate over every proof and check whether it is a proof for either S(P), not S(P) or S(P) is independent. Once the machine finds a proof for not S(P) or S(P) is independent, it stops with false. If it proves S(P), it stops with true. It will necessarily stop according to your original assumption.
This works even if you would look for an arbitrarily long chain of "it is not provable that not provable that not provable .... that not provable that S", since every finite proof has to be checked for only a finite number of chains. (Since proof must be longer than the statement)
That is plausible. But as you mentioned, the original quote, catchy though, was different and unfortunately (unlike most philosophical statements) formally wrong.
There's a flaw in your proof - the step from "The machine will necessarily stop" to "This solves the halting problem" is unjustified.
Despite the flaw, I agree with your general conclusion - there are and will be challenging as well as unsolvable problems.
It's justified. If a machine halts, then there's a proof of that in PA (simply the list of steps it performs before halting). Therefore, "independent of PA" implies "doesn't halt". Therefore, a provability decider is the same as a halting decider.
With the added steps, yes, there is a proof.