earthwormchuck163 comments on From the "weird math questions" department... - Less Wrong

5 Post author: CronoDAS 09 August 2012 07:19AM

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

Comments (49)

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

Comment author: earthwormchuck163 10 August 2012 02:18:49AM 0 points [-]

Did you mean to write "for all programs that halt in less than (some constant multiple of) N steps", because what you wrote doesn't make sense.

Yes. Edited.

What if I give you a program that enumerates all proofs under PA and halts if it ever finds proof for a contradiction? There is no proof under PA that this program doesn't halt, so your fake oracle will return HALT, and then I will have reasonable belief that your oracle is fake.

That's cool. Can you do something similar if I change my program to output NOT-HALT when it doesn't find a proof?

Comment author: Wei_Dai 10 August 2012 02:56:30AM *  2 points [-]

Can you do something similar if I change my program to output NOT-HALT when it doesn't find a proof?

Consider a program that enumerates all proofs under PA of length up to N^c for some c. If it finds a contradiction, it loops forever, otherwise it halts. I have reasonable belief that it halts, but your fake oracle can't prove that it does using a proof of length at most N, if c is sufficiently large (see On the length of proofs of finitistic consistency statements in first order theories).

Or here's another way that doesn't depend on that result. Define program A as follows: Enumerate all proofs under PA up to length N. If it finds a proof for "program A halts", then it loops forever, otherwise it halts. If PA is consistent, then it must be that A halts but there's no proof for it under PA of length N or less.

Comment author: earthwormchuck163 10 August 2012 03:16:28AM 1 point [-]

Okay, I concede. I recognize when I've been diagonalized.