Is there only one FairBot?

[transhumanist_atom_understander]

The FairBot from the MIRI prisoner’s dilemma tournament is defined by a theorem of Peano arithmetic (PA) that holds for each opponent:

where is “the FairBot cooperates” and is “the opponent cooperates”.

As a source for FairBot, the paper cites Vladimir Slepnev, aka cousin_it. Though this isn’t what’s cited in the paper, he made a post about a kind of FairBot. But the FairBot definition he gave translates to:

This biconditional here is equivalent to the previous one, in the sense that for arbitrary formulas and of PA, if one of these sentences is a PA theorem, then so is the other. To prove this, you replace with in this second formula, and verify that what you get is a theorem of Gödel-Löb provability logic (GL). From there you can prove equivalence with some facts about GL (uniqueness of fixed points and arithmetic soundness).

Now, this isn’t the only time I’ve encountered an equivalent formula for FairBot. The other was James Payor’s cooperation condition:

Again, you can just plug in for , verify the resulting theorem, and there’s your proof of equivalence.

But doesn’t the space of provability bots feel rather tight, if we keep on bumping into the same FairBot?

It makes me wonder, is there just one FairBot?

Maybe any rank-zero modal agent that’s unexploitable but cooperates with itself is FairBot (in the sense that its defining formula is equivalent to ). Or if not that, what’s the condition?

[joseph_c]

A sort of meta-comment on modal agents: I dislike the way they are presented mathematically, in terms of logical expressions and formulas. I think it would be simpler to use some model of computation, such as the lambda calculus, and then make the agents programs instead of formulas.

For example: We first define a runtime with an evaluator, (eval exp), and then a macro (prove exp) which hands the expression to a theorem prover, and returns true if and only if the theorem prover determines that the expression will terminate and the resulting value will be true. We can also use the special form (quote exp) to quote an expression, the replacement for declaring that some parts of formulas are implicitly encoded as Gödel numbers.

An agent becomes simply a function (agent my-code opponent-code). During testing against other agents, the runtime provides the agent with its own quoted code and the opponent’s quoted code. (It’s not strictly necessary to provide the agent’s own code to itself, but doing so makes it easier to avoid having to write quines.) The runtime then evaluates both functions, to see who cooperates and who defects. Note that the agent might never terminate—which is an ambiguity that the mathematical presentation doesn’t really resolve. One way to resolve this ambiguity is to say that such is undefined behavior, and the runtime may choose cooperate or defect as it wishes.

Some examples of agents in this framework, using a Lisp-like syntax:

;; DefectBot
(define (defect-bot my-code opponent-code)
  #f) ;; False stands for defection, true for cooperation

;; CliqueBot
(define (clique-bot my-code opponent-code)
  (equal? my-code opponent-code))

;; FairBot
(define (fair-bot my-code opponent-code)
  (prove `(,opponent-code ',opponent-code ',my-code)))

;; Payorian FairBot
(define (payorian-fair-bot my-code opponent-code)
  (define (implies X Y)
	(or (not X) Y))
  (prove `(implies (prove `(,my-code ',my-code ',opponent-code))
		           (,opponent-code ',opponent-code ',my-code))))

;; JustBot
(define (just-bot my-code opponent-code)
  (prove
	`(,opponent-code
	    ',opponent-code
		;; Play the opponent against a copy of FairBot's code, not JustBot's code:
		'(λ (my-code opponent-code)
		   (prove `(,opponent-code ',opponent-code ',my-code))))))

Maybe I should vibe-code this so we can have a tournament :)

[programjames]

You have a typo. JustBot is inserting a copy of FairBot’s code. I think, given the name JustBot, you probably meant to play the opponent against a copy of CooperateBot:

(define (just-bot my-code opponent-code)
    (define (cooperate-bot my-code opponent-code)
        #t)
    (prove
        `(,opponent-code ',opponent-code ',cooperate-bot)))

[joseph_c]

The JustBot I was copying in fact simulates against FairBot, not CooperateBot. You’re right that I did have two typos—but those were in missing quotes. I’ve now fixed it.

Also, your quotation of cooperate-bot is incorrect, because quote as a special form simply says to look at the next expression and treat it as literal data, so if an expression has already been loaded and evaluated (to give you your function cooperate-bot), you can’t get its code by just putting a quote before the symbol referring to that function. That would take some kind of environment inspection.

[programjames]

Can you please fix your comment?

;; Play the opponent against a copy of 𝐂𝐨𝐨𝐩𝐞𝐫𝐚𝐭𝐞𝐁𝐨𝐭'𝐬 𝐜𝐨𝐝𝐞, not JustBot's code:
'(λ (my-code opponent-code)
    (prove `(,opponent-code ',opponent-code ',my-code)))

The source of my confusion is:

1. You say “CooperateBot’s code” but insert Fairbot’s code.

2. What is “just” about cooperating with FairBot?

[joseph_c]

Done! I’m not going to argue about whether it’s more just to test against FairBot or CooperateBot. I’m just copying the standard JustBot.

[kbear]

can the prove function make use of facts like ’(prove X)?

[joseph_c]

Yes! The prover is really any function with two semantic guarantees:

1. If (eval exp) returns #f, so does (prove exp).

2. (prove exp) does not do unbounded computation, and always returns either #t or #f.

The prover does not need to be a good prover, but ideally it would be self-aware, looking for instances of prove in the expression to try to find fixed points. Note that when writing a bot, one can internally define and use their own theorem prover if they wish—and in a more barebones competition the competitor would be required to.

[Canaletto]

Maybe any rank-zero modal agent that’s unexploitable but cooperates with itself is FairBot

Can you elaborate on what “rank-zero modal” mean? (unexploitable = (C, D) outcome does not happen?)

“If there is a proof that outcome of the game of me and this opponent is (D,C) under 1000 symbols, then I defect, otherwise I run fair bot condition”—is this non “rank-zero”?

[transhumanist_atom_understander]

The definitions of “modal agent”, “rank”, and “unexploitable” are in the paper.