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.

Article Navigation

Comments (37)
Tags: adt decision_theory udt

Comments (37)

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

Comment author: JGWeissman 20 March 2012 08:08:09PM 2 points [-]

But that can't happen if A's proof system is sound, therefore A will find only "intended" proofs rather than "spurious" ones in the first place.

If A's proof system is sound, that directly implies that A won't generate "spurious" proofs. I don't see the point of deriving this from the fact that "spurious" proofs lead to contradictions.

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. What is the point?

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.

Powered by Reddit Powered by Reddit