# Löb's theorem

(Redirected from Lob's theorem)
Jump to: navigation, search

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 is true", then P is provable. I.e.

$\mathrm{if}\ PA \vdash (Bew(\# P) \rightarrow P)\mathrm{, 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, who formulated it in 1955.

## 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 $\phi$ 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

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

## Modal Proof of Löb's theorem

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

### Modal Formulas

We will assume the following grammar for formulas:

1. If $X$ is a propositional variable, then $X$ is a formula.
2. If $K$ is a propositional constant, then $K$ is a formula.
3. If $A$ is a formula, then $\Box A$ is a formula.
4. If $A$ and $B$ are formulas, then so are $\neg A$, $A \rightarrow B$, $A \wedge B$, $A \vee B$, and $A \leftrightarrow B$

A modal sentence is a modal formula that contains no propositional variables. We use $\vdash A$ to mean $A$ is a theorem.

### Modal Fixed Points

If $F(X)$ is a modal formula with only one propositional variable $X$, then a modal fixed point of $F(X)$ is a sentence $\Psi$ such that

$\vdash \Psi \leftrightarrow F(\Box \Psi)$

We will assume the existence of such fixed points for every modal formula with one free variable. This is of course not an obvious thing to assume, but if we interpret $\Box$ as provability in Peano Arithmetic, then the existence of modal fixed points is in fact true.

### Modal Rules of Inference

In addition to the existence of modal fixed points, we assume the following rules of inference for the provability operator $\Box$:

1. From $\vdash A$ conclude $\vdash \Box A$: Informally, this says that if A is a theorem, then it is provable.
2. $\vdash \Box A \rightarrow \Box \Box A$: If A is provable, then it is provable that it is provable.
3. $\vdash \Box (A \rightarrow B) \rightarrow (\Box A \rightarrow \Box B)$: This rule allows you to do modus ponens inside the provability operator. If it is provable that A implies B, and A is provable, then B is provable.

### Proof of Löb's theorem

1. Assume that there is a modal sentence $P$ such that $\vdash \Box P \rightarrow P$.
Roughly speaking, it is a theorem that if $P$ is provable, then it is, in fact true.
This is a claim of soundness.
2. Let $\Psi$ be a sentence such that $\vdash \Psi \leftrightarrow (\Box \Psi \rightarrow P)$.
The existence of such a sentence follows the existence of a fixed point of the formula $F(X) \leftrightarrow (X \rightarrow P)$.
3. From 2, it follows that $\vdash \Psi \rightarrow (\Box \Psi \rightarrow P)$.
4. From rule of inference 1, it follows that $\vdash \Box(\Psi \rightarrow (\Box \Psi \rightarrow P))$.
5. From 4 and rule of inference 3, it follows that $\vdash \Box\Psi \rightarrow \Box(\Box \Psi \rightarrow P)$.
6. From rule of inference 3, it follows that $\vdash \Box(\Box \Psi \rightarrow P) \rightarrow (\Box\Box\Psi \rightarrow \Box P)$.
7. From 5 and 6, it follows that $\vdash \Box \Psi \rightarrow (\Box\Box\Psi \rightarrow \Box P)$.
8. From rule of inference 2, it follows that $\vdash \Box \Psi \rightarrow \Box \Box \Psi$.
9. From 7 and 8, it follows that $\vdash \Box \Psi \rightarrow \Box P$.
10. From 1 and 9, it follows that $\vdash \Box \Psi \rightarrow P$.
11. From 2, it follows that $\vdash (\Box \Psi \rightarrow P) \rightarrow \Psi$.
12. From 10 and 11, it follows that $\vdash \Psi$
13. From 12 and rule of inference 1, it follows that $\vdash \Box \Psi$.
14. From 13 and 11, it follows that $\vdash P$.

## References

• Hinman, P. (2005). Fundamentals of Mathematical Logic. A K Peters. ISBN 1-56881-262-0.
• Boolos, George S. (1995). The Logic of Provability. Cambridge University Press. ISBN 0-521-48325-5.