Non-trivial consequences of Löb's theorem

Question

Informally, Löb's theorem (Wikipedia, PlanetMath) shows that:

a mathematical system cannot assert its own soundness without becoming inconsistent [Yudkowsky]

In symbols:

if $PA\vdash$ $Bew$(#P) $\rightarrow P)$, then $PA\vdash P$

where $Bew$(#P) means that the formula $P$ with Gödel number #P is provable.

Other than Leon Henkin's application to show that Santa Claus exists (also see here), Michael Detlefsen wrote about limitations of mechanism which I do not have a copy but I did read through a refutation of it here.

Additionally, Drucker mentions Kripke's 1967 "new proof" of the theorem here.

My question is has there been any other interesting non-trivial applications of the theorem other than the cited ones?

Answer 1

Löb's theorem provides the essential ingredient for a complete axiomatization of propositional provability logic. In detail: Work with the usual notation of propositional modal logic, which has propositional variables, the usual Boolean connectives, and the unary modal operator $\square$. The usual reading of $\square p$ is "necessarily $p$", but in provability logic, the intended reading is "it is provable that $p$." Call a modal formula $\phi$ valid if PA proves all the sentences obtainable from $\phi$ by replacing its propositional variables by sentences of the language of PA and then replacing subformulas of the form $\square\alpha$ with $Bew(\sharp\alpha)$ (starting with the innermost $\square$ and working outward). Solovay showed that this notion of validity is identical to formal provability in an axiomatic system obtained by starting with the standard system K for what is called normal modal propositional logic, and adjoining the schema that formalizes Löb's theorem: $(\square(\square\alpha\to\alpha))\to\square\alpha$.

Answer 2

Löb's theorem can be used to show that there exist equilibria in games like prisoner's dilemma when the participants are computer programs that can read each other's source code.

If player 1 can show that player 2 will cooperate when given player 1's source code, and vice versa, then we can have an equilibrium. The catch is that player 2 needs to predict what will happen when its own source code is fed to player 1 and vice versa. So implicitly each player must reason about itself. Löb's theorem shows there is a consistent way to to this. See Robust Cooperation in the Prisoner's Dilemma: Program Equilibrium via Provability Logic.

It's not entirely practical but it's interesting anyway.