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?