= 27d567bc2d48d9f40e9ccc20ea370b15)
Wei_Dai comments on Metaphilosophical Mysteries - 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 (255)
The last step doesn't look valid to me. After updating on the evidence, you have a human who thinks they've seen a halting oracle, and a Solomonoff agent who thinks he's seen a highly improbable event that doesn't involve a halting oracle. The fact that the human assigns a higher probability to the observations is unconvincing, because he could've just been extraordinarily lucky.
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?
That works if you can guess S, or some S' that is more powerful than S. But might there be a formal system that couldn't be guessed this way? My first thought was to construct a parameterized system somehow, S(x) where S(x) can prove that S(y) halts when a trick like this is used; but that can be defeated by simply iterating over systems, if you figure out the parameterization. But suppose you tried a bunch of formal logics this way, and the oracle passed them all; how could you ever be sure you hadn't missed one? What about a proof system plus a tricky corner case detection heuristic that happens to cover all your programs?