Löb's theorem tells us that "if P is provable, then P" is provable, then P is provable.

How can this be true? Wouldn't this imply that all false statements are true, because:

  1. All false statements are unprovable
  2. For all false statements, "if P is provable, then P" is true, because P is not provable
  3. Step 2 is a proof of "if P is provable, then P"
  4. P is provable
  5. P is true

Is there something I'm missing?

  • $\begingroup$ How do you arrive at step 4? $\endgroup$ – Carl Mummert Oct 3 '15 at 12:02
  • $\begingroup$ @CarlMummert: P is provable because "if P is provable, then P" is provable. (Lob's theorem) $\endgroup$ – Runemoro Oct 3 '15 at 16:17

Let us see why your argument is not true by an example. Let $P$ be the sentence $0=1$. If PA could prove $Prov(0=1) \rightarrow 0=1$, then by Löb's theorem it would prove $0=1$.

Obviously PA proves that $0 \neq 1$. You want PA to somehow prove that $\neg Prov(0=1)$ so that PA proves $0 \neq 1 \rightarrow \neg Prov(0=1)$, which is equivalent to the statement $Prov(0=1) \rightarrow 0=1$.

You claim that "false statements are unprovable". How do you know this? Maybe PA is inconsistent and proves everything, or is unsound and proves false statements even though it is consistent. The point is that PA has to prove its own consistency in order for an argument similar to yours to go through within PA. But by Gödel's incompleteness theorem we know that PA cannot prove the statement $Con(PA)$, which is a shorthand for $\neg Prov(0=1)$.


Another way to see that the difficulty there is the each appearance of "provable" in quotes refers to the formal Pvbl relation, which only resembles the real provability relation in certain respects.

In particular, there are consistent theories $T$ that extend PA such that $T \vdash \text{Pvbl}_T(\phi)$ for every formula $\phi$. But of course $T$ does not actually prove every formula $\phi$, because $T$ is consistent.

In the argument in the question, there are several steps that mix real provability with formalized provability. Let's assume that by "false" statement you mean a statement disprovable in the theory.

For example, step 2 begins with the fact that, if $P$ is false, then $P$ is not provable, so by contraposition, if $P$ is provable then $P$ is true. But this does not mean the theory can prove "if $P$ is provable then $P$ is true", which is the formula $\text{Pvbl}(P) \to P$. We cannot expect the theory to prove $\lnot P \to \lnot \text{Pvbl}(P)$, either, because as above there are consistent theories in which $\text{Pvbl}(P)$ is provable for all $P$.

The way to avoid this sort of thing is to be more explicit about writing Pvbl for the formalized provability relation, rather than using "provable" in quotes, which tends to cause confusion.

In particular, Löb's theorem tells us that if $T \vdash \text{Pvbl}(P) \to P$ then $T \vdash P$. That is stronger than the claim that if $T \vdash \text{Pvbl}(P) \to P$ then $T \vdash \text{Pvbl}(P)$. The distinction between these is not nearly as clear when "provable" is used for both "$\vdash$" and "Pvbl".

  • 1
    $\begingroup$ When I was first learning about these subjects, the difference between provability/satisfaction and formalized provability/satisfaction was confusing me a lot. Of course one gets used to this difference in time but it would be really great if basic math logic books emphasized this difference. (I vaguely recall someone suggesting using different colors for different uses of the word "proves" in the theory and the metatheory.) $\endgroup$ – Burak Oct 3 '15 at 21:15

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.