# Löb's theorem

https://arbital.com/p/lobs_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].