math lessons - Löb's theorem

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 $PA \vdash Bew(\# P) \rightarrow P$ , then $PA \vdash P$

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 $φ$ in the given system in the language of modal logic, by means of the modality $\Box \phi$ .

Then we can formalize Löb's theorem by the axiom $\Box(\Box P\rightarrow P)\rightarrow \Box P$ , known as axiom GL (for Gödel-Löb) (sometimes formalised by means of an inference rule that infers $\Box P$ from $\Box P\rightarrow P$ ). 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.

Categories: Mathematical logic

Mathematics Encyclopedia and Lessons

Lessons

Popular
Subjects

References

Löb's theorem

Löb's theorem in provability logic

Mathematics Encyclopedia and Lessons

Lessons

Popular Subjects

References

Löb's theorem

Löb's theorem in provability logic

Popular
Subjects