Informally, Löb's theorem ([Wikipedia](https://en.wikipedia.org/wiki/L%C3%B6b%27s_theorem), [PlanetMath](https://planetmath.org/lobstheorem)) shows that:



> 
> a mathematical system cannot assert its own soundness without becoming inconsistent [[Yudkowsky]](https://www.lesswrong.com/posts/ALCnqX6Xx8bpFMZq3/the-cartoon-guide-to-loeb-s-theorem)
> 
> 
> 


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](https://web.archive.org/web/20050114064256/http://people.cs.uchicago.edu/%7Ekaharris/phil525/week_1/paradox.html) (also [see here](http://www.ltn.lv/%7Epodnieks/gt6.html#BM6_6)), [Michael Detlefsen wrote about limitations of mechanism](https://doi.org/10.1023/A:1016104127745) which I do not have a copy but I did read through a refutation of it [here](https://web.archive.org/web/20150421124804/https://www.seberry.org/detlefson_lob.pdf).


Additionally, Drucker mentions Kripke's 1967 "new proof" of the theorem [here](https://books.google.com/books?ei=CaKtT-TrA-ikiQKLp-2xBA&id=7ED2HmmqKw0C&dq=consequences+of+lob%2527s+theorem&q=%2522mini-developments+related+to+lob%2527s+theorem%2522#v=snippet&q=%2522mini-developments%2520related%2520to%2520lob%2527s%2520theorem%2522&f=false).


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



Non-trivial consequences of Löb's theorem
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$. 


