The context is MIRI's twist on Axelrod's Prisoner's Dilemma tournament. Axelrod's competitors were programs, facing each other in an iterated Prisoner's Dilemma. MIRI's tournament is a one-shot Prisoner's Dilemma, but the programs get to read their opponent's code. Or, rather, a description of the behavior of the code in Gödel-Löb provability logic, which turns out to be enough to determine their behavior in the setup.

One fun result, right in the beginning of the paper, is about a program, FairBot, whose behavior is specified by "I'll cooperate with you if you (provably) cooperate with me". Despite the appearance of circularity, FairBot cooperates with itself. The proof involves Löb's theorem, so we call this Löbian cooperation.

Andrew Critch has suggested another way of proving self-cooperation. Instead of Löb's theorem, we use what he calls "Payor's lemma". It suggests a different way of defining a FairBot, something more like "If, when I hypothetically cooperate with you, you would cooperate with me, then I really will cooperate."

This post is my attempt to explain why I think this approach is more promising, or at least why I like it more.

When thinking through these kinds of reflection problems [...]

---

Outline:

(02:04) Löbian FairBot

(03:03) Payorian FairBot

(04:02) Kripke frames

(07:15) Proving cooperation with Kripke frames, and CooperateBot

(09:23) One Payorian FairBot will cooperate with another

(10:30) Why this procedure feels right to me

(11:23) The sense in which this is simpler than Löbian cooperation

---

First published:
March 9th, 2026

Source:
https://www.lesswrong.com/posts/LaCP6WyNzX8kiZn3w/payorian-cooperation-is-easy-with-kripke-frames

---

Narrated by TYPE III AUDIO.

“Payorian Cooperation is easy with Kripke frames” by transhumanist_atom_understander

LessWrong (30+ Karma)