A More Intuitive Proof of Löb’s Theorem

After my previous post, I spent more time trying to better understand both of the theorems I mentioned, and want to post here a more intuitive proof of Löb’s theorem from some random planetmath URL by user dankomed, referencing this book of Podnieks. I am going to copy it out here (hopefully also being in native unicode helps legibility). I added some {brackets} where I was finding it hard to grok too many symbols in a row.

We’ll use P(·, ·) to mean proof arithmetization in a formal system F which is Peano Arithmetic or stronger, because we need Gödel’s second incompleteness theorem, which states that such systems cannot prove they are consistent (whereas the first states they can’t prove all true statements).

Löb’s theorem: If F ⊢ {∃xP(x, ň) ⇒ ϕ_n}, where x is the Gödel number of the proof of the formula with Gödel number n, and ň is the numeral of the Gödel number of the formula ϕ_n, then F ⊢ ϕ_n.

Proof: Suppose F ⊢ {∃xP(x, ň) ⇒ ϕ_n}. Let F* be the new proof system that is equal to F plus the new axiom ¬ϕ_n. By modus tollens F* ⊢ {¬ϕ_n ⇒ ¬∃xP(x, ň)}. Since F* has an axiom ¬ϕ_n by modus ponens F* ⊢ ¬∃xP(x, ň). In this case F* proves that ϕ_n is is not provable in F (and also that F is consistent). This however leads to a proof that F* is also consistent because it contains only F and ¬ϕ_n, and we already know both that F is consistent and that F does not prove ϕ_n. Thus F* proves its own consistency. According to Gödel’s second incompleteness theorem however F* cannot prove its own consistency unless it is inconsistent. Therefore F + ¬ϕ_n must always be an inconsistent theory, and we conclude that F ⊢ ϕ_n. ∎

From other pages I’ve read, I would recap it as:

• Generally, not all true statements are provable. That contradicts the first incompleteness theorem.
• Can we show that some true statements are provable? Löb’s theorem says that you can only do this when it has a proof, in which case it’s trivial. (Because if N is true, then M ⇒ N holds for any M.)
• I love this proof; it more or less shows that except for that trivial case, proving this statement about provability quickly brings you in conflict with the second incompleteness theorem (which is, as Wikipedia puts it, itself basically an arithmetization of the first incompleteness theorem). Other proofs tended to reinvent the wheel by inlining the major incompleteness theorem steps.

The corollary applying it to Henkin sentences, would I guess now go:

If S encodes “S is provable,” then S is true (because otherwise we would violate the second incompleteness theorem).

This still seems… unintuitive? If S is true, it’s provable, and you’d think we’d have an explicit proof of S itself. While the flavour is more like “we can only arrive in this situation in trivial cases.” Though for a Henkin sentence, it doesn’t feel very trivial.