timtyler comments on Metaphilosophical Mysteries - Less Wrong

35 Post author: Wei_Dai 27 July 2010 12:55AM

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

Comments (255)

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

Comment author: Wei_Dai 28 July 2010 06:45:11PM *  2 points [-]

Also, there are entities that are impossible to distinguish from halting oracles using all the computational resources in the universe, which are not actually halting oracles. For example, a "can be proven to halt using a proof shorter than 3^^^3 bits" oracle has nonzero probability under the Solomonoff prior.

"proof shorter than 3^^^3 bits" means "proof shorter than 3^^^3 bits in some formal system S", right? Then I can write a program P that iterates through all possible proofs in S of length < 3^^^3 bits, and create a list of all TMs provable to terminate in less than 3^^^3 bits in S. Then P checks to see if P itself is contained in this list. If so, it goes into an infinite loop, otherwise it halts.

Now we know that if S is sound, then P halts AND can't be proven to halt using a proof shorter than 3^^^3 bits in S. What happens if we feed this P to your impostor oracle?