Löb's theorem

From Free net 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 <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:Mathlogic-stub