Modal Fixpoint Cooperation without Löb's Theorem

post by Andrew_Critch · 2023-02-05T00:58:40.975Z · LW · GW · 32 comments

Contents

  Discussion
  Writing implications backwards
  Conclusion
None
32 comments

Followed By: Payor's Lemma in Natural Language [LW · GW]

TL;DR: This post introduces a novel logical approach to achieving group-scale cooperation, based on modal fixpoint theory.  This approach is both easier to understand and roughly 3x more efficient than previous approaches that factored through Löb's Theorem, measured in terms of the length / complexity of the proofs involved.

The following theorem was inspired by Scott Garrabrant, and uses a lemma of James Payor in place of Löb's Theorem to prove cooperation between a group of agents.  I'll state the theorem for three agents because that's most illustrative of what's going on:

Theorem: Suppose $A,B,$ and $C$ are agents that return "true" to signify cooperation and "false" to signify defection.   Let $E=A\wedge B\wedge C$, so $E$ is the statement that "everyone cooperates".  Let ${\square }_A$, ${\square }_B$, and ${\square }_C$ denote proof systems that extend Peano Arithmetic, let ${\square }_{E}X$ stand for ${\square }_{A}X\wedge {\square }_{B}X\wedge {\square }_{C}X$, and suppose the agents behave in a manner satisfying the following conditions:

1. $⊢{\square }_A({\square }_{E}E\to E)\to A$
2. $⊢{\square }_B({\square }_{E}E\to E)\to B$
3. $⊢{\square }_C({\square }_{E}E\to E)\to C$
   
   Then it follows that $⊢E$, i.e., everyone cooperates (provably!). 
   
   (Intuitively, the strategy of the agents in this theorem is to check that the group is trustworthy in a certain way before joining (cooperating with) the group.  The theorem shows that the collective check on trustworthiness nests inside itself in a way that self-validates and yields cooperation.) 
   
   Proof: 
4. $⊢{\square }_A({\square }_{E}E\to E)\wedge {\square }_B({\square }_{E}E\to E)\wedge {\square }_C({\square }_{E}E\to E)\to A\wedge B\wedge C$, by combining 1, 2, and 3 with $\wedge$.
5. $⊢{\square }_E({\square }_{E}E\to E)\to E$, from 4 by the definition of E and ${\square }_E$.
6. $⊢E$, by the lemma below with $x=E$.
   
   [end proof]

The key to the theorem is the following lemma, due to James Payor:

Lemma: If $⊢\square (\square x\to x)\to x$ then $⊢x$.

      Historical note: Originally this lemma assumed  $⊢\square (\square x\to x)\leftrightarrow x$, but then I realized only the forward implication is needed, so I rewrote it.

      Proof: The proof uses the same modal rules of inference for $\square$ as Löb's theorem, namely, necessitation and distributivity:

1. $⊢x\to (\square x\to x)$, by tautology ($A\to (B\to A)$).
2. $⊢\square x\to \square (\square x\to x)$, from 1 by $\square$ necessitation and distributivity.
3. $⊢\square (\square x\to x)\to x$, by assumption.
4. $⊢\square x\to x$, from 2 and 3 by modus ponens.
5. $⊢\square (\square x\to x)$, from 4 by $\square$ necessitation.
6. $⊢x$, from 5 and 3 by modus ponens.
   
   [end proof]

Sweet!  In comparison to Löb's Theorem, two things are beautiful about Payor's lemma:

• It sidesteps the use of an auxiliary fixpoint $⊢\Psi \leftrightarrow (\square \Psi \to x)$, by examining a proposition of interest ($x$) that itself has the fixpoint structure needed to self-validate; and
• It also allows the construction of unexploitable modal agents without Löb's Theorem, as in the theorem above.

Discussion

In the proof of the Theorem, you might be wondering if it really makes sense to be thinking of ${\square }_E$ as a logical system of its own.  It doesn't need to be, but the answer is yes if ${\square }_A$, ${\square }_B$, and ${\square }_C$ are all finite extensions of PA.  Then the axioms of ${\square }_E$ are just [the conjunction of axioms of ${\square }_A$]$\vee$[the conjunction of axioms of ${\square }_B$] $\vee$ [the conjunction of axioms of ${\square }_C$].

You also might wonder if an alternative approach to group cooperation might be to instead use the following strategies:

1. $⊢A\leftrightarrow \square (\square A\to B\wedge C)$
2. $⊢B\leftrightarrow \square (\square B\to A\wedge C)$
3. $⊢C\leftrightarrow \square (\square C\to A\wedge B)$

Then you'd be right!  Here it also follows that $⊢A\wedge B\wedge C$.  However, the proof involves a lot more nesting, with A thinking about what B's thinking about what C's thinking about (etc.), and it's not as easy or short as the proof of the Theorem above.  

Writing implications backwards

If you think of $\square (\square x\to x)$ in Payor's Lemma as "defining" $x$ as a program, it's fun to write all the implication arrows from right to left, so they look a little like variable assignments.  (And, under the Curry-Howard correspondence, they do actually correspond to maps.)  Here's the lemma and proof again, written that way:

Lemma: If $⊢x\leftarrow \square (x\leftarrow \square x)$ then $⊢x$.

      Proof: The same as above, but with the arrows written leftward!

1. $⊢(x\leftarrow \square x)\leftarrow x$, by tautology ($(A\leftarrow B)\leftarrow A$).
2. $⊢\square (x\leftarrow \square x)\leftarrow \square x$, from 1 by $\square$ necessitation and distributivity.
3. $⊢x\leftarrow \square (x\leftarrow \square x)$, by assumption.
4. $⊢x\leftarrow \square x$, from 2 and 3 by modus ponens.
5. $⊢\square (x\leftarrow \square x)$, from 4 by $\square$ necessitation.
6. $⊢x$, from 5 and 3 by modus ponens.
   
   [end proof]

I find the above somewhat more elegant than the version with rightward arrows, albeit a less standard way of writing.

Conclusion

In my opinion, what's great about the lemma and theorem above is that they're both relatively short and simple (relative to proving and using Löb's Theorem), and they allow a proof of unexploitable group cooperation that's roughly three times shorter than than one that starts by proving Löb's Theorem (only ~6 lines of logic, vs ~18).

PS James says his next idea will be even better ;)

32 comments

Comments sorted by top scores.