Preceded by: Modal Fixpoint Cooperation without Löb's Theorem
It turns out Payor's Lemma and its proof can be explained in natural language even more easily than Löb's Theorem. Here's how.
Imagine a group of people, and let x denote the statement "everyone in the group cooperates". Payor's Lemma says the following:
Lemma: If ⊢□(□x→x)→x, then ⊢x
First, let's unpack the meaning of the assumption in words:
Now let's work through the proof in words, too! I'll omit saying "it's verified that..." each time, which is what ⊢ means.
Continuing to use "trustworthiness" in the sense above, the whole proof may be summarized as follows:
"If a group verifiably cooperates, it's verifiably trustworthy (to itself). Assume the group cooperates on the basis of verified trustworthiness. Then, it also cooperates on the basis of verified cooperation (a stronger condition), which is what trustworthiness means. Therefore, the group is trustworthy, hence verifiably trustworthy (assuming we concluded all this using logic), hence the group cooperates (by the assumption)."