In mathematical logic

Mathematical logic

Mathematical logic is a subfield of mathematics with close connections to foundations of mathematics, theoretical computer science and philosophical logic. The field includes both the mathematical study of logic and the applications of formal logic to other areas of mathematics...

, 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 , then

where Bew(#P) means that the formula P with Gödel number

Gödel number

In mathematical logic, a Gödel numbering is a function that assigns to each symbol and well-formed formula of some formal language a unique natural number, called its Gödel number. The concept was famously used by Kurt Gödel for the proof of his incompleteness theorems...

 #P is provable.

Löb's theorem is named for Martin Hugo Löb

Martin Löb

Martin Hugo Löb was a German mathematician. He settled in the United Kingdom after the Second World War and specialised in mathematical logic. He moved to the Netherlands in the 1970s, where he remained in retirement...

, who formulated it in 1955.

Löb's theorem in provability logic

Provability logic

Provability logic

Provability logic is a modal logic, in which the box operator is interpreted as 'it is provable that'. The point is to capture the notion of a proof predicate of a reasonably rich formal theory, such as Peano arithmetic....

 abstracts away from the details of encodings used in Gödel's incompleteness theorems

Gödel's incompleteness theorems

Gödel's incompleteness theorems are two theorems of mathematical logic that establish inherent limitations of all but the most trivial axiomatic systems capable of doing arithmetic. The theorems, proven by Kurt Gödel in 1931, are important both in mathematical logic and in the philosophy of...

 by expressing the provability of in the given system in the language of modal logic

Modal logic

Modal logic is a type of formal logic that extends classical propositional and predicate logic to include operators expressing modality. Modals — words that express modalities — qualify a statement. For example, the statement "John is happy" might be qualified by saying that John is...

, by means of the modality .

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


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


from


The provability logic GL that results from taking the modal logic

Modal logic

Modal logic is a type of formal logic that extends classical propositional and predicate logic to include operators expressing modality. Modals — words that express modalities — qualify a statement. For example, the statement "John is happy" might be qualified by saying that John is...

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 is a propositional variable, then is a formula.
2. If is a propositional constant, then is a formula.
3. If is a formula, then is a formula.
4. If and are formulas, then so are , , , , and

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

Modal Fixed Points

If is a modal formula with only one propositional variable , then a modal fixed point of is a sentence such that

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 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 :

1. From conclude : Informally, this says that if A is a theorem, then it is provable.
2. : If A is provable, then it is provable that it is provable.
3. : 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 such that . Roughly speaking, it is a theorem that if is provable, then it is, in fact true. This is a claim of soundness.
2. Let be a sentence such that . The existence of such a sentence follows the existence of a fixed point of the formula .
3. From 2, it follows that .
4. From rule of inference 1, it follows that .
5. From 4 and rule of inference 3, it follows that .
6. From rule of inference 3, it follows that
7. From 5 and 6, it follows that
8. From rule of inference 2, it follows that
9. From 7 and 8, it follows that
10. From 1 and 9, it follows that
11. From 10 and 2, it follows that
12. From 11 and rule of inference 1, it follows that
13. From 12 and 10, it follows that

External links

• Löb's theorem at PlanetMath
• The Cartoon Guide to Löb’s Theorem, by Eliezer Yudkowsky