Löb's theorem

[summary: If $~$PA\vdash Prv_{PA}(A)\implies A$~$ then $~$PA\vdash A$~$]

We trust Peano Arithmetic to correctly capture certain features of the [ standard model of arithmetic]. Furthermore, we know that Peano Arithmetic is expressive enough to talk about itself in meaningful ways. So it would certainly be great if Peano Arithmetic asserted what now is an intuition: that everything it proves is certainly true.

In formal notation, let $~$Prv$~$ stand for the Standard provability predicate of $~$PA$~$. Then, $~$Prv(T)$~$ is true if and only if there is a proof from the axioms and rules of inference of $~$PA$~$ of $~$T$~$. Then what we would like $~$PA$~$ to say is that $~$Prv(S)\implies S$~$ for every sentence $~$S$~$.

But alas, $~$PA$~$ suffers from a problem of self-trust.

Löb's theorem states that if $~$PA\vdash Prv(S)\implies S$~$ then $~$PA\vdash S$~$. This immediately implies that if $~$PA$~$ is consistent, the sentences $~$PA\vdash Prv(S)\implies S$~$ are not provable when $~$S$~$ is false, even though according to our intuitive understanding of the standard model every sentence of this form must be true.

Thus, $~$PA$~$ is incomplete, and fails to prove a particular set of sentences that would increase massively our confidence in it.

Notice that [godels_second_incompleteness_theorem Gödel's second incompleteness theorem] follows immediately from Löb's theorem, as if $~$PA$~$ is consistent, then by Löb's $~$PA\nvdash Prv(0= 1)\implies 0= 1$~$, which by the propositional calculus implies $~$PA\nvdash \neg Prv(0= 1)$~$.

It is worth remarking that Löb's theorem does not only apply to the standard provability predicate, but to every predicate satisfying the [ Hilbert-Bernais derivability conditions].