[3] Provability logic abstracts away from the details of encodings used in Gödel's incompleteness theorems by expressing the provability of
This is sometimes formalized by means of the inference rule: The provability logic GL that results from taking the modal logic K4 (or K, since the axiom schema 4,
, then becomes redundant) and adding the above axiom GL is the most intensely investigated system in provability logic.
Löb's theorem can be proved within normal modal logic using only some basic rules about the provability operator (the K4 system) plus the existence of modal fixed points.
We will assume the following grammar for formulas: A modal sentence is a formula in this syntax that contains no propositional variables.
is a modal formula with only one propositional variable
such that We will assume the existence of such fixed points for every modal formula with one free variable.
This is of course not an obvious thing to assume, but if we interpret
as provability in Peano Arithmetic, then the existence of modal fixed points follows from the diagonal lemma.
In addition to the existence of modal fixed points, we assume the following rules of inference for the provability operator
, known as Hilbert–Bernays provability conditions: Much of the proof does not make use of the assumption
, so for ease of understanding, the proof below is subdivided to leave the parts depending on
Given we know PA is consistent (but PA does not know PA is consistent), here are some simple examples: In Doxastic logic, Löb's theorem shows that any system classified as a reflexive "type 4" reasoner must also be "modest": such a reasoner can never believe "my belief in P would imply that P is true", without also believing that P is true.
[4] Gödel's second incompleteness theorem follows from Löb's theorem by substituting the false statement
for P. Not only does the existence of modal fixed points imply Löb's theorem, but the converse is valid, too.
When Löb's theorem is given as an axiom (schema), the existence of a fixed point (up to provable equivalence)
[5] Thus in normal modal logic, Löb's axiom is equivalent to the conjunction of the axiom schema 4,
, and the existence of modal fixed points.