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

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 26 March 2012 12:18:08PM 0 points [-] 
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) 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) if(A()==2) return 10 return 0
Comment author: cousin_it 26 March 2012 12:46:45PM 1 point [-]

I see what you're trying to do, but can you explain why A would return 1?

Comment author: gRR 26 March 2012 01:06:58PM 1 point [-]

The intuition is that the proof of "A()==1 implies U()==5, and A()!=1 implies U()<=5", if it exists, would not depend on N, whereas any proof of "A()==2 implies U()==10..." would have to be longer than N, so by making N large enough...

The setup should make "if S has a proof of length < N, then S" apparent by inspection, answering your earlier objection: if S is (<N)-provable, then U() will find the proof (because finding any other proof first would imply U() is unsound), and then return (A()==1 ? 5 : 0), which requires A() to return 1, otherwise U() is unsound again.

Comment author: cousin_it 26 March 2012 01:17:10PM *  1 point [-]

I don't think A can assume soundness of the proof system, because soundness implies consistency. Or is there some way for A to reach the proof for A()==1 without using consistency?

Comment author: gRR 27 March 2012 12:13:46PM *  1 point [-]

But A can use consistency arguments when proving "Provable(S) => S", can't it?

Let S be "A()==1 implies U()==5, and A()!=1 implies U()<=5".
Then the following is provable by inspection: "if T is a moral argument with the shortest proof of length <N, then either T=S or ~T". From this it follows that "either Provable(S) => S, or there exists T, such that Provable(T) and Provable(~T)". From the second part everything provably follows, including "Provable(S) => S". Putting everything together, we get Provable(Provable(S) => S).

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