In mathematical logic, Löb's theorem states that in any formal system F with Peano arithmetic (PA), for any formula P, if it is provable in F that "if P is provable in F then P is true", then P is provable in F. More formally, if Bew(#P) means that the formula P with Gödel number #P is provable (from the German "beweisbar"), then
Contents
- Lbs theorem in provability logic
- Modal proof of Lbs theorem
- Modal formulas
- Modal fixed points
- Modal rules of inference
- Proof of Lbs theorem
- Examples
- Converse Lbs theorem implies the existence of modal fixed points
- References
or
An immediate corollary 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
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
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 K4 (or K, since the axiom schema 4,
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 (the K4 system) plus the existence of modal fixed points.
Modal formulas
We will assume the following grammar for formulas:
- If
X is a propositional variable, thenX is a formula. - If
K is a propositional constant, thenK is a formula. - If
A is a formula, then◻ A is a formula. - If
A andB are formulas, then so are¬ A ,A → B ,A ∧ B ,A ∨ B , andA ↔ B
A modal sentence is a modal formula that contains no propositional variables. We use
Modal fixed points
If
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
Modal rules of inference
In addition to the existence of modal fixed points, we assume the following rules of inference for the provability operator
- (necessitation) From
⊢ A conclude⊢ ◻ A : Informally, this says that if A is a theorem, then it is provable. - (internal necessitation)
⊢ ◻ A → ◻ ◻ A : If A is provable, then it is provable that it is provable. - (box distributivity)
⊢ ◻ ( A → B ) → ( ◻ A → ◻ 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
- Assume that there is a modal sentence
P such that⊢ ◻ P → P .
Roughly speaking, it is a theorem that ifP is provable, then it is, in fact true.
This is a claim of soundness. - From the existence of modal fixed points for every formula (in particular, the formula
X → P ) it follows there exists a sentenceΨ such that⊢ Ψ ↔ ( ◻ Ψ → P ) . - From 2, it follows that
⊢ Ψ → ( ◻ Ψ → P ) . - From the necessitation rule, it follows that
⊢ ◻ ( Ψ → ( ◻ Ψ → P ) ) . - From 4 and the box distributivity rule, it follows that
⊢ ◻ Ψ → ◻ ( ◻ Ψ → P ) . - Applying the box distributivity rule with
A = ◻ Ψ andB = P gives us⊢ ◻ ( ◻ Ψ → P ) → ( ◻ ◻ Ψ → ◻ P ) . - From 5 and 6, it follows that
⊢ ◻ Ψ → ( ◻ ◻ Ψ → ◻ P ) . - From the internal necessitation rule, it follows that
⊢ ◻ Ψ → ◻ ◻ Ψ . - From 7 and 8, it follows that
⊢ ◻ Ψ → ◻ P . - From 1 and 9, it follows that
⊢ ◻ Ψ → P . - From 2, it follows that
⊢ ( ◻ Ψ → P ) → Ψ . - From 10 and 11, it follows that
⊢ Ψ - From 12 and the necessitation rule, it follows that
⊢ ◻ Ψ . - From 13 and 10, it follows that
⊢ P .
Examples
An immediate corollary 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. Given we know PA is consistent (but PA does not know PA is consistent), here are some simple examples:
In Doxastic logic, Löb's theorem shows that any system classified as a reflexive "type 4" reasoner must also be "modest": such a reasoner can never believe "my belief in P would imply that P is true", without first believing that P is true.
Converse: Löb's theorem implies the existence of modal fixed points
Not only does the existence of modal fixed points imply Löb's theorem, but the converse is valid, too. When Löb's theorem is given as an axiom (schema), the existence of a fixed point (up to provable equivalence)