Confusion about Löb's theorem

Question

To quote wikipedia:

Löb's theorem states that in any formal system that includes PA, for any formula P, if it is provable in PA that "if P is provable in PA then P is true", then P is provable in PA.

Now what I don't understand is the following: why isn't the sentence

"if P is provable in PA then P is true"

always provable/true? If a formula is provable it must be by definition true, no? As in: suppose I tell you that the Riemann hypothesis is provable, then you can conclude that the Riemann hypothesis is true, no? Or is there a subtle difference between provability and trueness? I am quite confused and really not familiar with this topic. I came about the paradox through Scott Aaronson's book "Quantum Computing since Democritus" but I found the explanation of the paradox a bit on the short side...

Answer 1

Say that the formal system is $\sf PA + \lnot Con(PA).$ Then the system proves every statement is provable in $\sf PA$, but surely it doesn't prove every statement (unless it is inconsistent, which by Godel's theorem would mean $\sf PA$ is inconsistent).

There is a name for the property "if something is provable in $\sf PA$ then it is true". When this holds we say "$\sf PA$ is sound". Soundness is a stronger property than consistency, so, since $\sf PA$ can't even prove its own consistency, it certainly can't prove its own soundness (in fact, it can't even express its own soundness as a single sentence... the schema "$\operatorname{Prov}(\ulcorner \varphi \urcorner)\to \varphi$" at the center of Lob's theorem is the best we can do, but that's a more technical issue).

So, when we conclude from a proof that something is true, we are assuming the soundness of the system we proved it in. Lob's theorem essentially says that we can't prove anything nontrivial regarding the soundness of a system within the system itself.

---

Addition in response to the comments.

There is certainly a subtle difference between provability and truth. First, neither of these things is something that you can really talk about in an absolute sense. Provability of a given sentence is relative to a particular axiomatic system (e.g. $\sf PA$), and means there is a formal proof the sentence using the axioms and rule of inference. Truth is relative to a particular interpretation of the language the sentence is written in.

For instance, $2+2=4$ is provable in $\sf PA$ (essentially by using the associative property: $(1+1)+(1+1) = 1+1+1+1$, though the exact details are somewhat implementation dependent). And it is also true when we interpret the language of arithmetic in the usual way, as being about $\mathbb N$ with addition and multiplication and $1$ and $0$ meaning what they usually mean.

Relative to a given interpretation, every sentence is either true or false and not both. However, the provability side is not so simple. In a given axiomatic system, a sentence can be provably true, provably false, neither or both.

The "both" option is clearly undesirable... a system where that never happens is called "consistent". As for the "neither" option - which is perhaps undesirable but less catastrophic - a system where that never happens (i.e. every sentence is either provably true or provably false) is called "complete".

There is also the question of how proof in some system relates to truth in some interpretation. When a system only proves true statements relative to a given interpretation, it is called sound (relative to that interpretation). So a sound and complete system would be one where proof and truth align perfectly. It is also something that the incompleteness theorem says we can't have for arithmetic, provided that the axioms of the proof system can be determined algorithmically. Note also no inconsistent system can be sound, since a statement can't be both true and false.

So with all that said, there's one more big layer to the question, and that's that we're not just interested in $\sf PA$ here, but what $\sf PA$ can prove about $\sf PA$. For that to make sense, we need to be able to encode stuff about formal sentences and proofs into the language of arithmetic. This is a big project, but should be plausible given that formal proofs (when the axioms are computably decidable) are computably checkable, and what is a computer doing but a bunch of arithmetic. So we can define in the language of arithmetic a predicate $\sf Prov_{PA}$ where $\sf Prov_{PA}(\ulcorner \varphi\urcorner)$ means that the statement $\varphi$, encoded by the number $\ulcorner \varphi \urcorner$ is provable in $\sf PA.$

What's less clear is the status of truth. When we look at a statement, we determine its truth inductively: first we understand whether an atomic statement like $2+2=5$ is true, then we work up to more complicated statements, like $\varphi \land \psi$ being true iff both $\varphi$ and $\psi$ are true. And finally $\exists x\varphi(x)$ being true if there's some number out there such that $\varphi(n)$ is true. Can we make some induction like that work inside arithmetic itself via some clever encoding? The answer is "almost, but no". The "no" is called Tarski's theorem and is related to the Liar paradox (and I won't even go into the "almost" since I'm already including a lot here and it's out of scope).

So when wikipedia writes "if $\varphi$ is provable in $\sf PA$, then $\varphi$ is true" what they mean is the sentence $\sf Prov_{PA}(\ulcorner \varphi \urcorner)\to \varphi$ (i.e. the "is true" is not really there, what they mean is asserting the statement itself).

So, with all that background about a) the difference between proof and truth and b) the subtleties of $\sf PA$ talking about its own proofs, we can return to your question. Lob's theorem says the only instances of $\sf Prov_{PA}(\ulcorner \varphi \urcorner)\to \varphi$ that $\sf PA$ can prove are the trivial ones where $\sf PA$ already proves $\varphi$, i.e. in a sense, it has no insight into its own soundness. This shouldn't be that surprising in light of Godel's second incompleteness theorem (which is extremely related to / any easy corollary of Lob's theorem) which says that $\sf PA$ can't prove its own consistency.

(This was the purpose of my original example in the answer: $\sf PA + \lnot Con(PA)$ is a consistent extension of $\sf PA$ that proves its own inconsistency... so it can prove every instance of $\sf Prov_{PA+\lnot Con(PA)}(\ulcorner \varphi\urcorner)$, so any proof of an instance of $\sf Prov_{PA+\lnot Con(PA)}(\ulcorner \varphi\urcorner)\to \varphi$ would immediately lead to a proof of $\varphi$.)

The bottom line is even if we take it for granted that $\sf PA$ is sound with respect to the usual interpretation of arithmetic (most do), there's no reason to expect $\sf PA$ to have this kind of insight into itself. Lob's (and Godel's and Tarski's) theorems are all limitative results about this precise sort of thing.

Answer 2

To answer the specific question you asked, consider the formula

$\phi:=Prov (\ulcorner 0=1 \urcorner) \to 0=1$.

Given that $\neg A$ is defined as $A \to 0=1$ in $\sf PA$, it follows that $\phi$ is just saying $\neg Prov (0=1)$. The only way that could be is if $\sf PA$ is consistent, since the Principle of Explosion holds.

So, if $\sf PA$ proves $\sf \phi$, then it has proven its own consistency, which contradicts Gödel’s Second Incompleteness Theorem. This is why soundness cannot be proven for arbitrary formulas in theories at least as strong as $\sf PA$.

Answer 3

If you prove the Riemann hypothesis, then before believing that the Riemann hypothesis is true, I'd ask you what assumptions (axioms) you used in the proof. If you used any false assumptions, I won't believe that RH is true. If you used only true assumptions (and your proof was carefully checked) then I'd believe that RH is true.

In the case at hand, you're discussing the situation where the axioms used are PA. Since I know that those axioms are true, your proof would convince me that RH is true.

Unlike me, PA doesn't "know" that all of the axioms of PA are true. In fact, the concept of "true" can't even be expressed in the language of PA; this is an instance of Tarski's "undefinability of truth" theorem. The language of PA can express the concept of "consistent", but PA can't prove that PA is consistent; this is an instance Gödel's second incompleteness theorem.

The bottom line here is that PA cannot imitate ("formalize") the argument above whereby your proof of RH would convince me that RH is true. In this respect, I'm smarter than PA! Even though I know that everything proved by PA is true, PA can't even express that knowledge, and can't prove that "0=1" isn't provable in PA (even though it can express the latter).

Let's come back to Löb's theorem. The point of the preceding explanation is that, although I know (and, better yet, you found it obvious) that "If PA proves $p$ then $p$ is true", that knowledge is beyond the proof capabilities of PA (even for the special case where $p$ is "0=1"). So the hypothesis in Löb's theorem, that "If PA proves $p$ then $p$ is true" is provable in PA, is nontrivial; it's not always correct. [To be accurate, I shouldn't use the word "true" where PA-provability is under discussion, because of Tarski's theorem. The sentence in quotation marks should be simply "If PA proves $p$ then $p$."]

Indeed, Gödel's second incompleteness theorem tells us that this hypothesis fails when $p$ is "0=1". Löb upgrades this by saying that this hypothesis "almost always" fails; the only sentences $p$ for which it holds are those that PA by itself could prove.

Answer 4

The question suggests that the distinction between expressibility of truth and provability ought to be addressed. It may conceptually add some light to the present discussion to take into consideration Tarski's theorem of undefinability of a truth predicate. This highly significant theorem had been formulated before Gödel's incompleteness theorems, however, was overshadowed by them.

Recall that a truth predicate tells a statement is true whenever it is true, and a provability predicate tells a statement is provable whenever it is provable. The crucial point here is that though no truth predicate can be intra-lingually encoded for a large class of formal languages, a smaller class among them can encode provability for themselves.

A plain proof of Tarski's theorem in essentials is given by Bruno Poizat in his A Course in Model Theory: An Introduction to Contemporary Mathematical Logic (2000, Springer-Verlag, p. 123). I record it here for future reference, if needed:

Theorem 7.9 (Tarski's Theorem). The set of codes of true sentences of arithmetic is not definable by an arithmetic formula.

Proof. Suppose that there is a formula $V(x)$, in one free variable $x$, such that the numbers $n$ satisfying it are exactly the codes of true sentences.

The set $A$ of codes of formulas whose only free variable is $x$ is definable, as is the function $\phi$ that sends the pair $(n, m)$, where $n$ is in $A$, to the code of the sentence obtained by replacing the variable $x$ by the number $m$ in the formula coded by $n$.

Now let $V(x, y)$ denote the formula $V(\phi(x, y))$; we can see that this formula is satisfied by those pairs $(n, m)$ for which $n$ is the code of a formula having $x$ as its only free variable, such that the sentence obtained from it by replacing $x$ with $m$ is true.

Now let $n_{o}$ be the code of the formula $\neg V(x, x)$; we cannot avoid the following dilemma:

• If $V(no, no)$ is true, then $\neg V(no, no)$ is true.

• If $V(n_{o}, n_{o})$ is false, then $\neg V(n_{o}, n_{o})$ is false.

Another aspect of Löb's theorem worth a remark is that Hilbert–Bernays provability conditions are assumed.

For a “soft” discussion on the theorem in a broader setting, I'd recommend the philosopher Graham Priest's article Löb’s Theorem and Curry’s Paradox.

Answer 5

In essence, Löb's theorem deals with a pretty mind-bending idea in formal logic. You're right to think, "If something is provable, then it's true, right?" But here's the kicker: in the world of formal systems like PA (Peano Arithmetic), saying "if P is provable, then P is true" isn't as straightforward as it sounds.

This isn't just about proving specific statements like a math problem; it's about the system trying to talk about its own proofs. Löb's theorem shows that for a statement to be provable in PA, PA itself must prove that "if this statement is provable, then it's true." It's a bit like the system needing to check its own work before it can confidently say something is true.

The twist is, due to Gödel's incompleteness theorems, a system can't outright prove its own consistency (or, in simpler terms, can't 100% back up its own reliability). So, when we're in the realm of statements about the system's own proofs, things get trickier.

In casual terms, it's like saying, "If I can show my work is always right, then this particular piece of work is right." But the catch is proving that first part – showing your work is always right, especially when your work involves checking your own work! Löb's theorem navigates these tricky waters, showing us the limitations and capabilities of formal systems in proving statements about themselves.