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

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 $\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. This is 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.