Löb's theorem

In mathematical logic, Löb's theorem states that in Peano arithmetic (PA) (or any formal system including PA), for any formula P, if it is provable in PA that "if P is provable in PA then P is true", then P is provable in PA. If Prov(P) is the assertion that the formula P is provable in PA, we may express this more formally as

If

P

A

⊢

P

r

o

v

(

P

)

→

P

{\displaystyle {\mathit {PA}}\vdash {\mathrm {Prov} (P)\rightarrow P}}

then

P

A

⊢

P

{\displaystyle {\mathit {PA}}\vdash P}

.

An immediate corollary (the contrapositive) of Löb's theorem is that, if P is not provable in PA, then "if P is provable in PA, then P is true" is not provable in PA. For example, "If

1

+

1

=

3

{\displaystyle 1+1=3}

is provable in PA, then

1

+

1

=

3

{\displaystyle 1+1=3}

" is not provable in PA.

Löb's theorem is named for Martin Hugo Löb, who formulated it in 1955. It is related to Curry's paradox.

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

ϕ

{\displaystyle \phi }

in the given system in the language of modal logic, by means of the modality

◻

ϕ

{\displaystyle \Box \phi }

. That is, when

ϕ

{\displaystyle \phi }

is a logical formula, another formula can be formed by placing a box in front of

ϕ

{\displaystyle \phi }

, and is intended to mean that

ϕ

{\displaystyle \phi }

is provable.

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

◻

(

◻

P

→

P

)

→

◻

P

,

{\displaystyle \Box (\Box P\rightarrow P)\rightarrow \Box P,}

known as axiom GL, for Gödel–Löb. This is sometimes formalized by means of the inference rule:

If

⊢

◻

P

→

P

{\displaystyle \vdash \Box P\rightarrow P}

then

⊢

P

{\displaystyle \vdash P}

.

The provability logic GL that results from taking the modal logic K4 (or K, since the axiom schema 4,

◻

A

→

◻

◻

A

{\displaystyle \Box A\rightarrow \Box \Box A}

, then becomes redundant) and adding the above axiom GL is the most intensely investigated system in provability logic.

Modal proof of Löb's theorem

Löb's theorem can be proved within normal modal logic using only some basic rules about the provability operator (the K4 system) plus the existence of modal fixed points.

Modal formulas

We will assume the following grammar for formulas:

If

X

{\displaystyle X}

is a propositional variable, then

X

{\displaystyle X}

is a formula.