Proving theorems via Löb's theorem

Question

Löb's theorem states that a mathematical formula which (metamathematically) asserts its own provability is indeed provable. More precisely, if a sufficiently strong system T (e.g. PA or ZFC) proves $Prov_T(\varphi) \rightarrow \varphi$, then T actually proves $\varphi$.

If one analyzes the proof, one sees that the proof works for any formalized provability predicate satisfying certain conditions (that are listed in the Wikipedia page). My question is the following:

Has anyone tried to prove some natural mathematical statement $\varphi$ using Löb's theorem, by constructing a provability predicate for which one has $Prov_T(\varphi) \rightarrow \varphi$ and which satisfies the necessary conditions?

I am aware that it sounds like an impossible mission. But surely someone must have tried to "reverse engineer" a predicate at least for certain number-theoretic statements?

Answer 1

I wouldn't expect that to yield anything useful.

Löb's theorem is fundamentally a negative result. What it does is to pull the rug under this otherwise intriguing proof strategy:

I want to prove $\psi$ (within $T$), but that seems to be hard. Instead I will use some kind of non-constructive meta-reasoning (that is formalizable in $T$) to show that a proof of $\psi$ must exist (even though I may not learn how that proof works), and then also prove $\operatorname{Prov}_T(\varphi)\to \varphi$ for a class of statements that includes my $\psi$. Then, combining those two parts, I will have proved $\psi$.

Löb's theorem tells us that this strategy is fundamentally flawed, because if you manage to complete the "easy" part $\operatorname{Prov}_T(\varphi)\to \varphi$, then you actually don't even need the non-constructive meta-reasoning that looked like the clever shortcut at first.

The lesson we learn is that proving $\operatorname{Prov}_T(\varphi)\to\varphi$ is harder than it looks -- you can't prove this for some nice general syntactically recognizable class of $\varphi$s unless it's because every $\varphi$ in that class is true (in which case having a particular proof in your hands is not very exciting).

In other words, proving $\operatorname{Prov}_T(\varphi)\to\varphi$ inescapably needs to involve reasoning about the particular thing that makes $\varphi$ true, rather than just things that would make us trust a separately given proof of $\varphi$. And if you're doing that kind of reasoning anyway, the argument goes, you might as well be proving $\varphi$ directly. That doesn't look like the makings of a shortcut.

(There are some "unnatural" exceptions to this where $\varphi$ is something you construct using the fixpoint theorem with the express goal of making $\operatorname{Prov}_T(\varphi)\to\varphi$ necessarily true. But that's explicitly not what you're asking).