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:

 def CoopBot(opponent):
  return C 

 def FairBot(opponent):
  if there exists a proof that opponent(FairBot) = C:
    return C 
  else:
    return D 

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.