I don't think I have posted here about probably my favourite paper, and I have recently been reminded that it might be a good idea: https://intelligence.org/files/ParametricBoundedLobsTheorem.pdf
It's about achieving cooperation in the open-source version of the Prisoner's Dilemma in practice. (It's predecessor paper about doing this with infinite resources is also pretty good.) It uses Löb's theorem in such a beautiful way and the end result is somewhat surprizing, especially to people not used to thinking about provability.
@jmw150 This was one of the links you might be interested in. And don't get discouraged by PA being required for Löb's theorem to work in most explanations – all that is actually needed is the ability to embed proofs in the system, which I would argue is a property one would usually like even in non-PA contexts.
