Löb's theorem
From Wikipedia, the free encyclopedia
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
, then 
where Bew(#P) means that the formula with Gödel number P is provable.
Löb's theorem is named for Martin Hugo Löb.
[edit] 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 φ in the given system in the language of modal logic, by means of the modality 
.
Then we can formalize Löb's theorem by the axiom
,
known as axiom GL, for Gödel-Löb. This is sometimes formalised by means of an inference rule that infers
from
.
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.
 |
This mathematical logic-related article is a stub. You can help Wikipedia by expanding it. |
