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

Comment author: orthonormal 25 March 2012 04:26:12PM 2 points [-]

Excellent! I wonder how far the malicious behavior can be extended.

Here the problem is that A directly uses a valid but malicious inference module Q. If A were built to enumerate proofs by length and act on the first one of the form "A()==a implies U()==u, and A()!=a implies U()<=u", can U be rewritten to guarantee that a particular spurious proof comes up first?

Or if A uses a halting oracle to check through statements of that form, can U be written (incorporating that oracle) so that the halting oracle fails to return for the genuine counterfactual and only returns "True" for a particular spurious one?

Comment author: cousin_it 25 March 2012 09:56:48PM *  4 points [-]

These are reasonable questions. I don't know the answers. Would be cool if someone else figured them out ;-)

Comment author: gRR 01 April 2012 03:03:35PM *  2 points [-]

My next attempt :) Below, "PA" means Peano Arithmetic.

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

Proposition: A() returns 1 (if PA is consistent).
Proof:
Let X = "there exist a!=1 and u, such that: A()==a => U()==u and A()!=a => U()<=u".
Let S = "there exists u, such that: A()==1 => U()==u and A()!=1 => U()<u".
Let T = "A()==1".
Let ProvableU(P) = the provability formula of U (PA+Consistent(PA), with proofs of length < N).
Let ProvableA(P) = the provability formula of A (PA).
Let "U⊦ P" mean P is a theorem of U's proof system.
Then:

1. U⊦ ProvableU(T) => S // by inspection of U 2. U⊦ S => ~X // by definitions of X and S 3. U⊦ ProvableU(T) => ~X // from the previous two 4. U⊦ ~X => ~ProvableA(X) // by the axiom Consistent(PA) 5. U⊦ ProvableA(ProvableU(T) => S) // by A's inspection of U 6. U⊦ ProvableA(ProvableU(T)) => ProvableA(S) // from the previous 7. U⊦ ProvableU(T) => ProvableA(ProvableU(T))
// because PA is sufficient to model provability in any formal system 8. U⊦ ProvableU(T) => ProvableA(S) and ~ProvableA(X) // from 3, 4, 6, and 7 9. U⊦ ProvableA(S) and ~ProvableA(X) => T // by inspection of A 10. U⊦ ProvableU(T) => T // from the previous two 11. U⊦ T // by Loeb's theorem

QED

Comment author: cousin_it 29 May 2012 10:12:09AM *  0 points [-]

Sorry for not noticing your comment earlier. It would be nice to have a way to subscribe to comment threads.

I don't understand why the definitions of X and S imply that S => ~X. Does that rely on specific features of your A and U? For example, if we take a different A and U so that A()==2 and U()==0, then X is true for a=2 and u=0, and S is true for u=1.

Comment author: Vladimir_Nesov 29 May 2012 12:13:22PM 2 points [-]

It would be nice to have a way to subscribe to comment threads.

Use "Subscribe to RSS Feed" on the right.

Comment author: cousin_it 26 March 2012 09:20:43AM *  1 point [-]

Here's another interesting followup question. My implementation of Q relies on enumerating all proofs in order, so running Q requires exponential time. Is there a "Henkin-style" implementation of Q that constructs the self-referential proof quickly and directly, maybe using the steps of Löb's theorem or something? That's how I first tried to construct Q after reading your comments, and failed, but it might still be possible.

Comment author: gRR 01 April 2012 07:37:40PM *  0 points [-]

Maybe something like this:

def Q():
return Proof1("IsValidProof(X, Q()) => X") +
Proof2("IsValidProof(X, Q())") +
X

where IsValidProof(Statement, Proof) is Goedel's Bew function, Proof1 is a formalization of the argument that "if Q() returns a valid proof of X, then A() will return 1, and X will be true", and Proof2 is a formalization of the argument that "a valid proof of A=>B, followed by a valid proof of A, followed by B, is a valid proof".

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