“Is there only one FairBot?” by 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 [...] --- First published: August 29th, 2026 Source: https://www.lesswrong.com/posts/auAq7Rcstop3FBEob/is-there-only-one-fairbot --- Narrated by TYPE III AUDIO.