My "Payorian FairBot" was just the original FairBot

MIRI's proof-based prisoner's dilemma tournament defined agents encoded as formulas of Peano arithmetic (PA) with one free variable. means the agent cooperates in a match against the agent, and is constructed by plugging the Gödel number of the formula defining into the formula defining.

The simplest interesting agent in the tournament was called FairBot. Using to mean FairBot cooperates with another agent, for all agents we have:

I will call this condition Löbian fairness, and refer to this agent as the Löbian FairBot.

In a previous post I defined an alternative "Payorian FairBot", which satisfies a condition I'll call Payorian fairness:

I wondered, though, is this really a distinct agent? The answer is no: these two fairness conditions are equivalent. The Payorian FairBot is Löbian-fair, and the original Löbian FairBot is Payorian-fair.

Elementary and sophisticated proofs

One way to prove the equivalence of these two fairness conditions is to simply grind through provability logic in both directions. I'll call this the "elementary proof", since it doesn't use any of the theorems about provability logic beyond the one that says it applies to PA. The bulk of the proof is just mechanically applying the rules of inference of provability logic. In fact, since the logic is decidable, I should have been able to just plug the question into a computer program. But I don't know how to do that, so I did the proof on paper.

After working out the elementary proof, I was reviewing the MIRI paper I linked earlier, and realized that to anyone who fully understood it, it might be obvious that the Payorian and Löbian FairBots are equivalent. Note that both FairBots cooperate ( ) if and only if some sentence is provable, but only for the Payorian FairBot does that sentence include. Theorem 4.6 of the paper shows that when an agent's cooperation condition references its own cooperation in this way, this reference can be eliminated. That is, there's another equivalent conditio…