red75 comments on AI cooperation in practice - Less Wrong

26 Post author: cousin_it 30 July 2010 04:21PM

You are viewing a comment permalink. View the original post to see all comments and the full post content.

Article Navigation

Comments (157)

Comments (157)

You are viewing a single comment's thread. Show more comments above.

Comment author: AlephNeil 01 August 2010 11:26:08AM 0 points [-]

Yes, that occurred to me too, and I think it does the job.

I wonder if there are theorems of the form "There's no significantly better way to show that P isn't provable in N steps than by listing all proofs of length N and observing that P isn't proved". Then of course maxsteps would need to be exponential in maxDC.

Comment author: red75 01 August 2010 12:09:54PM *  1 point [-]

On the other hand the fact that proves("A()=="Cooperate" && B()=="Cooperate"") was called means that A()=="Defect" && B()=="Cooperate" is unprovable under maxDC proof length. The question is can this fact be used in proof. The proof checker can be programmed to add such self-evident propositions into set of axioms, but I can't clearly see consequences of this. And I have a bad feeling of mixing meta- and object levels.

Comment author: cousin_it 01 August 2010 02:42:26PM *  1 point [-]

I'm not sure if your idea will work, but have some notation to help you avoid mixing the levels. Here's how you say "try to prove this fact conditional on some other fact":

function main()
{
if (proves(outputs(1), n1))
return 1;
else if (proves("implies(!proves(outputs(1), n1), eval(outputs(2)))", n2))
return 2;
else
return 0;
}
Powered by Reddit Powered by Reddit