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?**