You're looking at Less Wrong's discussion board. This includes all posts, including those that haven't been promoted to the front page yet. For more information, see About Less Wrong.

Houshalter comments on Open Thread - Aug 24 - Aug 30 - Less Wrong Discussion

7 Post author: Elo 24 August 2015 08:14AM

You are viewing a comment permalink. View the original post to see all comments and the full post content.

Comments (318)

You are viewing a single comment's thread. Show more comments above.

Comment author: TezlaKoil 28 August 2015 12:35:24AM *  4 points [-]

Now here is the weird and confusing part. If the above is a valid proof, then H will eventually find it. It searches all proofs, remember?

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

 If φ is provable, then φ holds.
Provable(#φ) → φ

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.

Comment author: Houshalter 29 August 2015 07:54:03PM *  0 points [-]

I'm very confused. Of course if φ is provable then it's true. That's the whole point of using proofs.

Comment author: VoiceOfRa 29 August 2015 08:29:10PM 4 points [-]

But that statement isn't provable.

Comment author: Houshalter 29 August 2015 08:41:57PM 0 points [-]

Then just assume it as an axiom.

Comment author: VoiceOfRa 29 August 2015 08:44:28PM 4 points [-]

Then the paradox you were describing fires and the system becomes inconsistent.

Comment author: RolfAndreassen 31 August 2015 05:30:37AM 0 points [-]

Yes, but it may be true without being provable.