Löb’s Theorem states that, if , then . To explain the symbols here:
PA is Peano arithmetic, a first-order logic system that can state things about the natural numbers.
means there is a proof of the statement in Peano arithmetic.
is a Peano arithmetic statement saying that is provable in Peano arithmetic.
I’m not going to discuss the significance of Löb’s theorem, since it has been discussed elsewhere; rather, I will prove it in a way that I find simpler and more intuitive than other available proofs.
Translating Löb’s theorem to be more like Gödel’s second incompleteness theorem
First, let’s compare Löb’s theorem to Gödel’s second incompleteness theorem. This theorem states that, if , then , where is a PA statement that is trivially false (such as ), and from which anything can be proven. A system is called inconsistent if it proves ; this theorem can be re-stated as saying that if PA proves its own consistency, it is inconsistent.
We can re-write Löb’s theorem to look like Gödel’s second incompleteness theorem as: if , then . Here, is PA with an additional axiom that , and expresses provability in this system. First I’ll argue that this re-statement is equivalent to the original Löb’s theorem statement.
Observe that if and only if ; to go from the first to the second, we derive a contradiction from and , and to go from the second to the first, we use the law of excluded middle in PA to derive , and observe that, since a contradiction follows from in PA, PA can prove . Since all this reasoning can be done in PA, we have that and are equivalent PA statements. We immediately have that the conclusion of the modified statement equals the conclusion of the original statement.
Now we can rewrite the pre-condition of Löb’s theorem from to . This is then equivalent to . In the forward direction, we simply derive from and . In the backward direction, we use the law of excluded middle in PA to derive , observe the statement is trivial in the branch, and in the branch, we derive , which is stronger than .
So we have validly re-stated Löb’s theorem, and the new statement is basically a statement that Gödel’s second incompleteness theorem holds for .
Proving Gödel’s second incompleteness theorem using computability theory
The following proof of a general version of Gödel’s second incompleteness theorem is essentially the same as Sebastian Oberhoff’s in “Incompleteness Ex Machina”. See also Scott Aaronson’s proof of Gödel’s first incompleteness theorem.
Let L be some first-order system that is at least as strong as PA (for example, ). Since L is at least as strong as PA, it can express statements about Turing machines. Let be the PA statement that Turing machine M (represented by a number) halts. If this statement is true, then PA (and therefore L) can prove it; PA can expand out M’s execution trace until its halting step. However, we have no guarantee that if the statement is false, then L can prove it false. In fact, L can’t simultaneously prove this for all non-halting machines M while being consistent, or we could solve the halting problem by searching for proofs of and in parallel.
That isn’t enough for us, though; we’re trying to show that L can’t simultaneously be consistent and prove its own consistency, not that it isn’t simultaneously complete and sound on halting statements.
Let’s consider a machine Z(A) that searches over all L-proofs of (where is an encoding of a Turing machine that runs A on its own source code), and halts only when finding such a proof. Define a statement G to be , i.e. Z(Z) doesn’t halt. If Z(Z) halts, then that means that L proves that Z(Z) doesn’t halt; but, L can prove Z(Z) halts (since it in fact halts), so this would show L to be inconsistent.
Assuming L is consistent, G is therefore true. If L proves its own consistency, all this reasoning can be done in L, so . But that means , so Z(Z) finds a proof and halts. L therefore proves , but L also proves G, making it inconsistent. This is enough to show that, if L proves its own consistency, it is inconsistent.
Let’s now prove Löb’s theorem. We showed that Löb’s theorem can be re-written as, if , then . This states that, if proves its own consistency, it is inconsistent. Since is at least as strong as PA, we can set in the proof of Gödel’s second incompleteness theorem, and therefore prove this statement which we have shown to be equivalent to Löb’s theorem.
I consider this proof more intuitive than the usual proof of Löb’s theorem. By re-framing Lob’s theorem as a variant of Gödel’s second incompleteness theorem, and proving Gödel’s second incompleteness theorem using computability theory, the proof is easy to understand without shuffling around a lot of math symbols (especially provability boxes).