Manfred comments on A model of UDT without proof limits - Less Wrong

13 Post author: cousin_it 20 March 2012 07:41PM

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

Comments (37)

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

Comment author: Manfred 21 March 2012 11:28:37PM 0 points [-]

Hm. So what would you still need to win. You'd still need to prove that A()==1 implies U()==10^6. But if that's true, the only way the agent doesn't prove that A()==2 implies U()==10^6+10^3 is if the predictor is really always right. But that's not provable to the agent, because I'm pretty sure that relies on the consistency of the agent's formal system.

Comment author: cousin_it 22 March 2012 01:51:27AM *  0 points [-]

The ASP post already has a rigorous proof that this implementation of A will fail. But maybe we can find a different algorithm for A that would search for proofs of some other form, and succeed?