Löb's theorem


by Jaime Sevilla Molina Jul 6 2016 updated Jul 30 2016

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].


Patrick Stevens

Something I learnt from Mietek Bak is that Löb's Theorem is kind of more subtle than this. In provability theory, it's fine to have a "box" operator that we informally read as "is provable"; but what Löb's theorem tells us that we can't simply interpret it literally as "is provable" without difficulties. One should define the "provability" predicate formally, to avoid getting confused (or one should specify that it is simply a formal symbol to which we have not assigned any semantic meaning, although that is somewhat against the point of the angle taken by the parent article); for example, the provability predicate could be defined by a certain first-order formula which unpacks a Gödel number, checks it's encoding a proof and verifies each step of the encoded proof.