You're looking at Less Wrong's discussion board. This includes all posts, including those that haven't been promoted to the front page yet. For more information, see About Less Wrong.

gRR comments on An example of self-fulfilling spurious proofs in UDT - Less Wrong Discussion

20 Post author: cousin_it 25 March 2012 11:47AM

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

Article Navigation

Comments (39)
Tags: adt decision_theory udt

Comments (39)

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

Comment author: gRR 27 March 2012 10:02:16PM 0 points [-]

Ok, how about this:
Provable(Anything)
=> Provable(S is the moral argument with the shortest proof of length <N)
=> S
=> (Provable(S) => S)
?

Comment author: cousin_it 27 March 2012 10:13:06PM *  5 points [-]

Let X be the statement "S is the moral argument with the shortest proof of length <N". Then it's true that X=>S and Provable(X)=>Provable(S), but I don't see why Provable(X)=>S.

In general I think your proof is missing a compelling internal idea, so you probably can't patch it by manipulating symbols. You'll just be inviting more and more subtle mistakes. When I find myself in a situation like this, I usually try to rethink the whole thing until it becomes obvious, and then the proof becomes inevitable even if I compose it sloppily. It's kinda hard to explain...

Comment author: orthonormal 27 March 2012 11:37:40PM 1 point [-]

When I find myself in a situation like this, I usually try to rethink the whole thing until it becomes obvious, and then the proof becomes inevitable even if I compose it sloppily. It's kinda hard to explain...

Good way of putting it.

Comment author: gRR 28 March 2012 01:06:03AM 0 points [-]

Yes, I think I know what you mean... it just feels as if there must be an easy technical proof, but, I can't find it...

So I tried to change the solution again, to make the proof easier:

def U(): Enumerate proofs by length up to a very large N if found a proof that "A()==1 implies U()==5, and A()!=1 implies U()<=5" then return (A()==1 ? 5 : 0) Enumerate proofs by length up to a very large N if found any other proof of the form "A()==a implies U()==u, and A()!=a implies U()<=u" then return (A()==a ? u-1 : u+1) return (A()==2 ? 10 : 0)

With this, Provable(S) implies S directly, so S is provable, so A must find it, because there are no other short-proof moral arguments if A an U are consistent.

But the provability of S does not depend on A, so U() will never get past the first loop, no matter against which agent it is played. So this is a wrong solution to the original problem. And the previous one would be wrong for the same reason, even if I did find the proof...

Powered by Reddit Powered by Reddit