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. (Note: The first page of Detlefsen's paper can be accessed 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$.