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.

cousin_it 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: cousin_it 27 March 2012 12:51:08PM 1 point [-]

I think this reasoning is valid:

  1. either Provable(S)=>S, or there exists T such that Provable(T) and Provable(~T)

  2. either Provable(S)=>S, or Provable(Anything)

  3. either Provable(S)=>S, or Provable(Provable(S)=>S)

But the last step doesn't seem to imply Provable(S)=>S. Or am I missing something again?

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...

Comment author: gRR 27 March 2012 01:32:58PM *  0 points [-]

[EDIT: this is wrong] You're saying, I don't get "Provable(Provable(S) => S)", but only "Provable(Provable(Provable(S) => S))"?

But then,
Provable(Provable(Provable(S) => S)) =>
Provable(Provable(Provable(S)) => Provable(S)) => /Loeb's theorem/
Provable(Provable(S)) =>
[EDIT: this is also wrong] Provable(S)

Comment author: cousin_it 27 March 2012 01:46:26PM *  2 points [-]

I still don't get it... Why does Provable(Provable(S)) lead to Provable(S)?

Comment author: gRR 27 March 2012 02:10:49PM 1 point [-]

Sorry, my error. Two errors, even. I'll think more.

Powered by Reddit Powered by Reddit