tl;dr: Löb’s Theorem is much easier to grok if you separate the parts of the proof that use the assumption □p→p from the parts that don’t. The parts that don’t use □p→p can be extracted as a stand-alone result, which I hereby dub “Löb’s Lemma”.
Here’s how it works.
Key properties of ⊢ and □
Here is some standard notation. In short, ⊢ is our symbol for talking about what PA can prove, and □ is shorthand for PA’s symbols for talking about what (a copy of) PA can prove.
“⊢ 1+1=2” means “Peano Arithmetic (PA) can prove that 1+1=2”. No parentheses are needed; the “⊢” applies to the whole line that follows it. Also, ⊢ does not stand for an expression in PA; it’s a symbol we use to talk about what PA can prove.
“□(1+1=2)” basically means the same thing. More precisely, it stands for a numerical expression within PA that can be translated as saying ”⊢ 1+1=2″. This translation is possible because of something called a Gödel numbering which allows PA to talk about a (numerically encoded version of) itself.
″□X ” is short for “□(X)” in cases where “X” is just a single character of text.
“X⊢Y” means “PA, along with X as an additional axiom/assumption, can prove Y”. In this post we don’t have any analogous notation for □.
The proofs here will use the following standard properties of ⊢ and □ (source: Wikipedia), which respectively stand for provability and provability encoded within arithmetic.
(necessitation) From ⊢A, conclude ⊢□A. Informally, this says that if A can be proven, then it can be proven that it can be proven (by just writing out and checking the proof within arithmetic). Note that from X⊢A we cannot conclude X⊢□A, because □ still means “PA can prove”, and not “PA+X can prove”.
(internal necessitation) ⊢□A→□□A . If A is provable, then it is provable that it is provable (basically the same as the previous point).
(box distributivity)⊢□(A→B)→(□A→□B). This rule allows one to apply modus ponens inside the provability operator. If it is provable that A implies B, and A is provable, then B is provable.
(deduction theorem) From A⊢B, conclude ⊢A→B: if assuming A is enough to prove B, then it’s possible to prove under no assumptions that A→B.
Point 4 is helpful and pretty intuitive, but for whatever reason isn’t used in the main Wikipedia article on Löb’s Theorem.
Löb’s Lemma
Claim: Assume Ψ and p are any statements satisfying ⊢Ψ↔□Ψ→p. Then ⊢□Ψ↔□p.
Intuition: By assumption, the sentence Ψ is equivalent to saying “If this sentence is provable, then p”. Intuitively, Ψ has very little content, except for the p part at the end, so it makes sense that □Ψ boils down to nothing more than □p in terms of logical equivalence.
Reminder: this does not use the assumption □p→p from Löb’s Theorem at all.
Proof:
Let’s do the forward implication first:
□Ψ⊢□□Ψ by internal necessitation (□Ψ→□□Ψ).
□Ψ⊢□(□Ψ→p) using box distributivity on the assumption, with A=Ψ and B=□Ψ→p.
Now for the backwards implication, which isn’t needed for Löb’s Theorem, but is handy anyway:
⊢p→(□Ψ→p) is a tautology.
⊢□p→□(□Ψ→p) by box distributivity on 1.
⊢□Ψ↔□(□Ψ→p) by box distributivity on the assumption.
⊢□p→□Ψ by 2 and 3.
I like this result because both directions of the proof are fairly short, it doesn’t use the assumption □p→p at all, and the conclusion itself is also fairly intuitive. The statement Ψ just turns out to have no content except for p itself, from the perspective of writing proofs.
Löb’s Theorem, now in just 6 lines
If you can remember Löb’s Lemma, you can write a very straightforward proof of Löb’s Theorem in just 6 lines:
Claim: If p is any sentence such that ⊢□p→p, then ⊢p
Proof:
Let Ψ be any sentence satisfying ⊢Ψ↔(□Ψ→p), which exists by the existence of modal fixed points (or by the Diagonal Lemma).
Löb’s Lemma: an easier approach to Löb’s Theorem
Related to: Löb’s Theorem for implicit reasoning in natural language: Löbian party invitations
tl;dr: Löb’s Theorem is much easier to grok if you separate the parts of the proof that use the assumption □p→p from the parts that don’t. The parts that don’t use □p→p can be extracted as a stand-alone result, which I hereby dub “Löb’s Lemma”.
Here’s how it works.
Key properties of ⊢ and □
Here is some standard notation. In short, ⊢ is our symbol for talking about what PA can prove, and □ is shorthand for PA’s symbols for talking about what (a copy of) PA can prove.
“⊢ 1+1=2” means “Peano Arithmetic (PA) can prove that 1+1=2”. No parentheses are needed; the “⊢” applies to the whole line that follows it. Also, ⊢ does not stand for an expression in PA; it’s a symbol we use to talk about what PA can prove.
“□(1+1=2)” basically means the same thing. More precisely, it stands for a numerical expression within PA that can be translated as saying ”⊢ 1+1=2″. This translation is possible because of something called a Gödel numbering which allows PA to talk about a (numerically encoded version of) itself.
″□X ” is short for “□(X)” in cases where “X” is just a single character of text.
“X⊢Y” means “PA, along with X as an additional axiom/assumption, can prove Y”. In this post we don’t have any analogous notation for □.
The proofs here will use the following standard properties of ⊢ and □ (source: Wikipedia), which respectively stand for provability and provability encoded within arithmetic.
(necessitation) From ⊢A, conclude ⊢□A. Informally, this says that if A can be proven, then it can be proven that it can be proven (by just writing out and checking the proof within arithmetic). Note that from X⊢A we cannot conclude X⊢□A, because □ still means “PA can prove”, and not “PA+X can prove”.
(internal necessitation) ⊢□A→□□A . If A is provable, then it is provable that it is provable (basically the same as the previous point).
(box distributivity) ⊢□(A→B)→(□A→□B). This rule allows one to apply modus ponens inside the provability operator. If it is provable that A implies B, and A is provable, then B is provable.
(deduction theorem) From A⊢B, conclude ⊢A→B: if assuming A is enough to prove B, then it’s possible to prove under no assumptions that A→B.
Point 4 is helpful and pretty intuitive, but for whatever reason isn’t used in the main Wikipedia article on Löb’s Theorem.
Löb’s Lemma
Claim: Assume Ψ and p are any statements satisfying ⊢Ψ↔□Ψ→p. Then ⊢□Ψ↔□p.
Intuition: By assumption, the sentence Ψ is equivalent to saying “If this sentence is provable, then p”. Intuitively, Ψ has very little content, except for the p part at the end, so it makes sense that □Ψ boils down to nothing more than □p in terms of logical equivalence.
Reminder: this does not use the assumption □p→p from Löb’s Theorem at all.
Proof:
Let’s do the forward implication first:
□Ψ⊢□□Ψ by internal necessitation (□Ψ→□□Ψ).
□Ψ⊢□(□Ψ→p) using box distributivity on the assumption,
with A=Ψ and B=□Ψ→p.
□Ψ⊢□p from 1 and 2 by box distributivity.
⊢□Ψ→□p from 3 by the deduction theorem.
Now for the backwards implication, which isn’t needed for Löb’s Theorem, but is handy anyway:
⊢p→(□Ψ→p) is a tautology.
⊢□p→□(□Ψ→p) by box distributivity on 1.
⊢□Ψ↔□(□Ψ→p) by box distributivity on the assumption.
⊢□p→□Ψ by 2 and 3.
I like this result because both directions of the proof are fairly short, it doesn’t use the assumption □p→p at all, and the conclusion itself is also fairly intuitive. The statement Ψ just turns out to have no content except for p itself, from the perspective of writing proofs.
Löb’s Theorem, now in just 6 lines
If you can remember Löb’s Lemma, you can write a very straightforward proof of Löb’s Theorem in just 6 lines:
Claim: If p is any sentence such that ⊢□p→p, then ⊢p
Proof:
Let Ψ be any sentence satisfying ⊢Ψ↔(□Ψ→p), which exists by the existence of modal fixed points (or by the Diagonal Lemma).
⊢□Ψ→□p by Löb’s Lemma.
⊢□p→p by assumption.
⊢□Ψ→p by 1 and 2 combined.
⊢Ψ by 3 and the defining property of Ψ
⊢□Ψ by necessitation.
⊢p by 3 and 5.
«mic drop»