MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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?

share|cite|improve this question
up vote 7 down vote accepted

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$.

share|cite|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.