Bakkot comments on Prisoner's Dilemma (with visible source code) Tournament - LessWrong

47 Post author: AlexMennen 07 June 2013 08:30AM

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

Comments (232)

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

Comment author: Bakkot 09 June 2013 02:44:10AM 0 points [-]

Just "there exists a valid proof in PA". If you're playing with bounded time, then you want efficient proofs; in that case the definition would be as you have it.

Comment author: Decius 09 June 2013 03:03:04AM 0 points [-]

At that point you can't implement it in a halting Turing machine. I'm not sure what PA can prove about the behavior of something that isn't a halting Turing machine regarding a particular input.

Comment author: Bakkot 09 June 2013 03:23:06AM 0 points [-]

By "implement it", you mean, one can't verify something is Reasonable on a halting TM? Not in general, of course. You can for certain machines, though, particularly if they come with their own proofs.

Note that the definition is that Reasonable programs cooperate with those they can prove are Reasonable, not programs which are Reasonable.

Comment author: ialdabaoth 09 June 2013 03:34:59AM *  1 point [-]

So then a program which can present a flawed proof which is not necessarily recognizable as flawed to machines of equivalent scale, can dominate over those other machines?

Also, if we want this contest to be a model of strategies in the real world, shouldn't there be a fractional point-cost for program size, to model the fact that computation is expensive?

I.e., simpler programs should win over more complex programs, all else being equal.

Perhaps the most accurate model would include a small payoff penalty per codon included in your program, and a larger payoff penalty per line of codon actually executed.

EDIT: What's wrong with this post?

Comment author: Bakkot 09 June 2013 06:24:55AM 0 points [-]

(I didn't downvote you.)

It's quite straightforward to write an algorithm which accepts only valid proofs (but might also reject some proofs which are valid, though in first-order logic you can do away with this caveat). Flawed proofs are not an issue - if A presents a proof which B is unable to verify, B ignores it.

Comment author: ialdabaoth 09 June 2013 06:25:55AM 0 points [-]

There's someone who consistently downvotes everything I ever write whenever he comes onto the site; I'm not sure what to do about that.

Comment author: Decius 09 June 2013 05:56:08PM 0 points [-]

A proves that A is inconsistent, then proves that A cooperates with every program that A proves is Reasonable and that B is reasonable.

B accepts A's proof that A is inconsistent, and the rest follow trivially.

Comment author: Bakkot 09 June 2013 11:20:29PM 1 point [-]

I'm not sure I understand. A is a TM - which aspect is it proving inconsistent?

Comment author: Decius 09 June 2013 11:44:37PM 0 points [-]

A proves that the logic A uses to prove that B is Reasonable is inconsistent. It is sufficient to say "If I can prove that B is Reasonable, B is Reasonable".