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 25 March 2012 11:51:34PM *  0 points [-] 
def A(): Enumerate proofs by length and act on the first one of the form
"A()==a implies U()==u, and A()!=a implies U()<=u"
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 if(A()==1) return 5 if(A()==2) return 10
return 0

The proof of the statement S: "A()==1 implies U()==5, and A()!=1 implies U()<=5" exists, so it will be found by both A() and U(). Any proof of another statement of the same form would imply "there was no proof of length <N of statement S", which would be false given high enough N, so it couldn't be found.

Comment author: cousin_it 26 March 2012 12:10:31AM *  1 point [-]

I can't parse your source code for U, does it return a value in every case?

To write code in comments, prefix lines with four spaces, like this:

# Hello world
print 'Hello World!'
Comment author: gRR 26 March 2012 12:18:08AM 0 points [-]

Thanks, edited.

Comment author: cousin_it 26 March 2012 12:39:17AM *  1 point [-]

Why is S provable? As far as I can see, you can't easily prove it by Löb's theorem, because "if S is provable then S" is not apparent by inspection of A and U, because A could find a different proof earlier.

Comment author: gRR 26 March 2012 01:38:15AM 0 points [-]

I thought it is similar to your proof here.

Comment author: cousin_it 26 March 2012 01:44:17AM *  1 point [-]

In Lobian cooperation, the agents search for proofs of only one statement, never stopping early because they found a proof of something else. Your implementation of A doesn't seem to work like that. Or did I misunderstand and your version of A only looks for proofs where A()==1?

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 26 March 2012 01:57:52AM *  0 points [-]

I thought it couldn't find any other proofs of length < N, because it would imply there was no proof of S. But this is not a problem if S is false... Ok, modification:

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 if(A()==1) return 5 if found any other proof of the same form
then whatever A() return 0
if(A()==2) return 10
return 0

EDIT: Wait, this is not good, now if(A()==2) is unreachable...
EDIT2: No, not actually unreachable, but any proof for a statement of the form "A()==2 => U()==10..." must be of length > N, which is what was needed, I suppose. Still feels like cheating, but I'm not sure why...

Comment author: cousin_it 26 March 2012 07:56:48AM *  1 point [-]

What's the intended consequence of A()==2 in your implementation of U? Is it U()==0 or U()==10? And which of those would actually happen?

Powered by Reddit Powered by Reddit