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

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

Then we can formalize Löb's theorem by the axiom

[itex]\Box(\Box P\rightarrow P)\rightarrow \Box P[itex],

known as axiom GL, for Gödel-Löb. This is sometimes formalised by means of an inference rule that infers

[itex]\Box P[itex]

from

[itex]\Box P\rightarrow P[itex].

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

• Art and Cultures
• Countries of the World (http://www.academickids.com/encyclopedia/index.php/Countries)
• Space and Astronomy