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

Powered by Reddit Powered by Reddit