# Löb's Theorem

After a long time of struggling to find an example of formal logic saying something non-trivial other than “self-references are dangerous, maybe we shouldn’t naively allow them”, I finally found a “real” application: open-source game theory.

Consider “bots” (rules) that can look into each others’ source codes and then decide whether to *cooperate* or to *defect*. (For a usual game theoretic analysis we would have to know the payoff structure of this game, but in what follows this turns out to be irrelevant.)

For simplicity’s sake, let us consider the simpler case with unbounded computational resources and the following two bots:

Obviously `FairBot`

cooperates with `CoopBot`

, since `CoopBot`

always cooperates with everyone.

But does `FairBot`

cooperate with another copy of itself? My intuition was something along the lines of “both `FairBot(FairBot)=C`

and `FairBot(FairBot)=D`

are logically consistent, so there cannot be a proof for `FairBot(FairBot)=C`

and hence `FairBot(FairBot)=D`

, i.e. both will defect”.

Enter Löb’s theorem: \(\square(\square P\rightarrow P)\rightarrow\square P\), or in words in Peano arithmetic (PA) (or any formal system including PA), for any formula P, if it is provable in PA that

.*‘if P is provable in PA then P is true’*, then P is provable in PA

Hence `FairBot`

will cooperate with another copy of `FairBot`

!

Time to revisit my notes on mathematical logic.