Vladimir_Nesov 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: Vladimir_Nesov 20 March 2012 08:57:32PM *  0 points [-]

It seems like step 2 is just validating that proofs are correct, and when it finds a problem, it doesn't seem to do anything good about it.

The activity of step 2 results in proofs of statements like [A()==1 => U()==100] being long (in agent's proof system, compared to length of proofs of the "natural" moral arguments like [A()==1 => U()==5]), something that wouldn't be the case had step 2 been absent. So it does perform tangible work.