|
|
In mathematical logic, Löb's theorem states that in a theory with Peano arithmetic, for any formula P, if it is provable that "if P is provable then P", then P is provable. I.e.
- if <math>PA \vdash Bew(\# P) \rightarrow P<math>, then <math>PA \vdash P<math>
where Bew(#P) means that the formula with Gödel number P is provable.
Löb's theorem in provability logic
Provability logic abstracts away from the details of encodings used in Gödel's incompleteness theorems by expressing the provability of <math>\phi<math> in the given system in the language of modal logic, by means of the modality <math>\Box \phi<math>.
Then we can formalize Löb's theorem by the axiom
- <math>\Box(\Box P\rightarrow P)\rightarrow \Box P<math>,
known as axiom GL, for Gödel-Löb. This is sometimes formalised by means of an inference rule that infers
- <math>\Box P<math>
from
- <math>\Box P\rightarrow P<math>.
The provability logic GL that results from taking the modal logic K4 and adding the above axiom GL is the most intensely investigated system in provability logic.Template:Math-stub