3

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?

Thomas Andrews
  • 177,126

2 Answers2

9

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)$.

Burak
  • 3,696
2

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

Carl Mummert
  • 81,604
  • 2
    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.) – Burak Oct 03 '15 at 21:15