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:
FairBot cooperates with
CoopBot always cooperates with everyone.
FairBot cooperate with another copy of itself? My intuition was something along the lines of “both
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.
FairBot will cooperate with another copy of
Time to revisit my notes on mathematical logic.