Löb’s Theorem and Curry’s Paradox

The technique of self-reference is very familiar to logicians. How to characterize it precisely is not a simple question, but in essence self-reference occurs when one takes some procedure and uses it, itself, as its own input.

The technique is something of the Dr. Jekyll and Mr. Hyde of logic. It is deployed to prove some of the most profound results in mathematical logic, such as Kurt Gödel’s incompleteness theorems and Alan Turing’s halting theorem. It is also deployed to prove paradoxical contradictions, such as the liar paradox and Russell’s paradox. The results of these two different kinds of problems are as intimately related as Jekyll and Hyde themselves. The difference between profound results and paradox is often razor thin.

One place in which this is the case concerns Löb’s theorem and Curry’s paradox. This pair is perhaps not familiar to people who are not mathematical logicians. The goals of this note are to make it more so and to ponder its significance.

A word on notation for nonlogicians:

• $¬A$ means: it is not the case that A
• $A ∨ B$ means: $A$ or $B$
• $A → B$ means: if $A$ then $B$
• $A ↔ B$ means: $A$ if and only if $B$
• $X ⊢ A$ means: $A$ follows from the premises in $X$

Löb’s Theorem

Löb’s theorem was proved in 1955 by Martin Löb, a German mathematician who worked in the wake of Gödel’s proof of his incompleteness theorems.¹ Those theorems concern axiomatic theories of arithmetic, that is, theories which concern the natural numbers: 0, 1, 2, … . Gödel showed that the symbols, statements, and proofs of such theories can be coded as natural numbers. Now, in an era when computer programs—which, like proofs, are just sequences of statements of a formal language—can be stored in a computer’s memory as a binary number, a sequence of 0s and 1s, this is not an unfamiliar fact.

This coding allowed statements about formulas and proofs themselves to be expressed as purely number-theoretic statements. What Gödel showed next was that if an axiom system, $T$, is sufficiently strong so that it can represent all primitive recursive functions, then there is a formula of arithmetic, ${Prov(x, y)}$, such that if $π$ is a proof of $A$, $T ⊢ Prov(⟨π⟩, ⟨A⟩)$, and if it is not, $T ⊢ ¬Prov(⟨π⟩, ⟨A⟩)$. Here, $⟨π⟩$ is the numeral of the code number of $π$, and $⟨A⟩$ is the numeral of the code of $A$. That $A$ is provable in $T$ can then be expressed by the sentence $∃xProv(x,⟨A⟩)$. This can be written as $𝒫(⟨A⟩)$—or just $𝒫⟨A⟩$: I will omit double brackets to avoid clutter.

Third—and this is the really cunning part—Gödel showed that there was a formula, $G$, such that $T ⊢ G↔ ¬𝒫⟨G⟩$. Effectively, $G$ says: ‘$G$’ is not provable. Here is the self-reference.

Finally, Gödel showed that if $T$ proves $G$, that is, $T ⊢ G$, then $T$ is inconsistent. So if $T$ is consistent, $G$ cannot be proved. At this point, it is not hard to show that if $T$ is consistent, and so $G$ is not provable, $G$ is true. When I talk of truth here and in what follows, I mean what logicians call truth in the Standard Model: that is, the interpretation of the language of arithmetic in which symbols get their standard meaning. Hence there are true sentences that cannot be proved.²

Gödel’s self-referential construction is quite general, and can be used to show that for any formula, $C(x)$, there is a sentence, $A$, such that $T ⊢ A ↔ C⟨A⟩$. Hence arises the question, proposed by the US logician Leon Henkin, of the provability or otherwise of the sentence which says of itself that it is provable—that is, a sentence, $H$, such that $T ⊢ H ↔ 𝒫⟨H⟩$. It was to answer Henkin’s question that Löb proved his theorem, which is as follows:

• For any sentence $A$, if $T ⊢ 𝒫⟨A⟩ → A$ then $T ⊢ A$.

This is a surprising result. After all, if the axioms of the arithmetic are sound, anything provable is true, so every instance of $𝒫⟨A⟩ → A$ is true. But Löb’s theorem shows that you can prove it only for those instances for which you can prove A itself.

Anyway, given the theorem, a solution to Henkin’s problem follows. Since $T⊢P⟨H⟩→H$, $T ⊢ H$.

Löb’s Proof

Against this background, now look at Löb’s proof. This uses three additional statements concerning $𝒫$. Again, if $T$ is sufficiently strong, these can be proved, as was already clear to Gödel. These are

1. If $T ⊢ A$ then $T ⊢ 𝒫⟨A⟩$.

Roughly: if you can prove $A$, you can prove that you can prove it.

2. $T ⊢ 𝒫⟨A→B⟩→(𝒫⟨A⟩→𝒫⟨B⟩)$.

Roughly: if you can prove $A→B$ and $A$ then you can prove $B$.

3. $T ⊢ 𝒫⟨A⟩→𝒫⟨𝒫⟨A⟩⟩$.

Roughly: you can prove that, if $A$ is provable, then it is provable that it is provable.

Löb’s proof can be put in a few different ways, but they all come to much the same thing. One way of putting it goes as follows. The proof uses a few assumptions about the underlying logic of $T$. I will note these as we go along. Modus ponens is the inference $\{A,A→B\}⊢B$. Contraction is the inference $\{A→(A→B)\}⊢A→B$.

Suppose that $T⊢𝒫⟨A⟩→A$. By Gödel’s self-referential construction, we can find a sentence, $L$, such that

• $T⊢L↔(𝒫⟨L⟩→A)$.

Take $C(x)$ to be $𝒫(x)→A$. So

• $T⊢L→(𝒫⟨L⟩→A)$.

By statement 1,

• $T⊢𝒫⟨L→(𝒫⟨L⟩→A)⟩$,

and so by statement 2 and modus ponens,

• $T⊢𝒫⟨L⟩→𝒫⟨(𝒫⟨L⟩→A)⟩$.

Hence by statement 2 again and the transitivity of →,

• $T⊢𝒫⟨L⟩→(𝒫⟨(𝒫⟨L⟩)⟩→𝒫⟨A⟩)$.

But $\{B→(C→D)\}⊢C→(B→D)$. Hence,

• $T⊢𝒫⟨𝒫⟨L⟩⟩→(𝒫⟨L⟩→⟨A⟩)$.

So by statement 3 and the transitivity of → it follows that

• $T⊢𝒫⟨L⟩→(𝒫⟨L⟩→𝒫⟨A⟩)$.

By contraction,

• $T⊢𝒫⟨L⟩→𝒫⟨A⟩$,

and by the supposition about $A$ and transitivity again,

• $T⊢𝒫⟨L⟩→A$.

By the original characterization of $L$,

• $T⊢(𝒫⟨L⟩→A)→L$.

So by modus ponens,

• $T⊢L$.

By statement 1 again,

• $T⊢𝒫⟨L⟩$.

So by a final application of modus ponens,

• $T⊢A$,

as required.

Curry’s Paradox

Curry’s paradox was published in 1942 by the American logician Haskell Curry—though paradoxes in the same family were known to some medieval logicians.³ It can be formulated using the notions of set, property, or truth; here, I give the version that uses truth. Like the liar paradox, it appeals to the apparently obvious principle that a sentence is true just if things are the way it says. Logicians, following Alfred Tarski, often call this the $T$-schema. So, for any sentence, $A$, provided it does not use context-dependent words such as “you” and “now,”

• $𝒯$⟨A⟩$↔A$.

Here, $𝒯x$ is the predicate “$x$ is true,” and $⟨A⟩$ is a name for $A$. It need not be obtained by arithmetic coding, but it could be.

The liar paradox concerns the sentence, $S$, such that $S↔¬𝒯⟨S⟩$; that is, it says of itself that it is not true, and deduces both $S$ and $¬S$. If one appeals to the principle of explosion—$\{B,¬B\}⊢A$, for arbitrary $A$ and $B$—then an arbitrary conclusion follows. Curry’s paradox establishes an arbitrary conclusion $A$, but without explicit mention of negation or the use of explosion. Again, it can be formulated in several different ways, though these all come to much the same thing. Here is one standard way.

Given $A$, we form the sentence which says of itself that if it is true then $A$. In other words, by some form of self-reference, we form a sentence, $C$, of the form $𝒯⟨C⟩→A$. The $T$-schema for $C$ then gives

• $𝒯⟨C⟩↔(𝒯⟨C⟩→A)$

and so

• $𝒯⟨C⟩→(𝒯⟨C⟩→A)$.

By contraction, we get

• $𝒯⟨C⟩→A$.

From the $T$-schema for $C$ in the other direction, we get

• $(𝒯⟨C⟩→A)→𝒯⟨C⟩$.

By modus ponens,

• $𝒯⟨C⟩$.

And by modus ponens again,

• $A$.

Since $A$ may be obviously absurd—e.g., “Julius Caesar was a frog”—this cannot be the case. And even if it is true—e.g., “Julius Caesar was Roman”—one ought not to be able to prove it like this.

And So?

It is not hard to see that the same thing is going on structurally in the proof of Löb’s theorem and Curry’s paradox.⁴ Write $𝒬$ for either $𝒫$ or $𝒯$. Then by self-reference we form a sentence, $S$, of the form $𝒬⟨S⟩→A$. Using the properties of $𝒬$, we then show that $𝒬⟨S⟩→(𝒬⟨S⟩→A)$, and so by contraction, $𝒬⟨S⟩→A$. A couple of applications of modus ponens then deliver A. In one case the reasoning delivers a theorem. In the other it delivers something unacceptable. What is going on here?

The standard story is something like this. The proof of Löb’s theorem is fine. The result is perhaps surprising, but then so are many mathematical results. The proof of Curry’s paradox is fallacious. That, at least, is impossible to gainsay. The liar paradox delivers a contradiction. If one is a dialetheist, one can simply accept the argument and its conclusion. The use of paraconsistent logic, not validating explosion, prevents the contradiction from spreading where it should not go.⁵ With Curry’s paradox it is impossible to accept the argument: we have a direct proof of everything. Given that all the logical moves in the paradoxical argument are in the proof of Löb’s theorem, and so correct, the only other possibility is that the $T$-schema must be rejected in full generality. This view about truth is buttressed by appeal to a construction of Tarski, according to which there is a hierarchy of languages. There is a $T$-schema at every level of the hierarchy—except the first—but the schema at any level is guaranteed to hold only for sentences of the level below.⁶

The $T$-schema—for all $A: 𝒯⟨A⟩ ↔ A$—is not, then, a property of truth. It holds only for a certain class of $A$s. It is well known that there are consistent theories of arithmetic plus a truth predicate in which the schema holds for certain syntactically defined classes of sentences.⁷ In the same way, the provability of the Löb schema—for all $A: 𝒫⟨A⟩ → A$—is not a property of provability. It holds only for a certain class of $A$s, namely, those that are themselves provable.

This analysis is problematic. The analogy between $𝒯$ and $𝒫$ is not as straightforward as it might appear. Those who hold the view concerning truth in question hold that not all instances of the $T$-schema are true. By contrast, all instances of the Löb schema are true. They are just not provable. In one sense, this is just a version of Gödel’s incompleteness theorem; but matters are more significant than that.

As is clear to anyone familiar with Gödel’s proof, the heuristic it uses is a paradox for provability analogous to the liar paradox for truth. Specifically, let $G$ be a sentence of the form $¬𝒫⟨G⟩$. Since $𝒫⟨G⟩$ → $G$, $𝒫⟨G⟩$ → $¬𝒫⟨G⟩$. Hence $¬𝒫⟨G⟩$, that is, $G$; and we have just proved this, i.e., $𝒫⟨G⟩$. So there is a paradox. Clearly, this uses the Löb schema, and in particular its instance for $G$, at the first step. If this is not provable in a formal arithmetic, then this argument cannot be reproduced in the formal system to show that it is inconsistent. What is left of the argument just shows that the arithmetic is incomplete.

But the instances of the Löb schema are true; indeed, since “prove” means something like “establish,” they would seem to be true by the very meaning of “prove.” And since the aim of an axiom system is to capture the truths of some subject, one should expect to be able to have an axiom system for arithmetic in which they are provable. If this system is not to be trivial, i.e., such that everything is provable, then the proof of Löb’s theorem must fail. Given the structural parallel between the proof of Löb’s theorem and that of Curry’s paradox, it would seem that same thing must account for the failure of the argument there. There are only two possible suspects: the principles of modus ponens and contraction—for the conditional involved. The more dubious of the two would appear to be contraction. There has been little investigation of arithmetics based on logics in which contraction fails—so far. But given what is known about proofs in formal arithmetic, there is a definite suspicion that many of the standard number-theoretic results would not be provable in such theories. Though initially less promising, the failure of modus ponens is actually more so. In paraconsistent logics, explosion fails. That is, there can be situations where for some $A$ and $B$, $B$ and $¬B$ hold, but $A$ does not. But then the disjunctive syllogism $\{B, ¬B∨A\} ⊢ A$ also fails. $¬B∨A$ holds since its first disjunct does. In standard mathematics $A→B$ is understood as $¬B∨A$. In other words, modus ponens fails.

Moreover, we know that there are axiomatic theories of arithmetic, $T$, whose underlying logic is paraconsistent, in which everything true in the Standard Model of arithmetic is provable.⁸ So, in particular, $T$ is complete: for any $A$, either $T⊢A$ or $T⊢ ¬A$. The theories are inconsistent, but contradictions do not spread everywhere because of the failure of explosion.⁹ Modus ponens seems such an integral part of reasoning that it would naturally be thought to be virtually impossible without it. What these results show is that this is not so. All arithmetic truths—and so all the standard results of number theory—are provable in such theories without it.

In these inconsistent arithmetics, all instances of the Löb schema $𝒫⟨A⟩→A$ are provable; so, as might be expected, are the Gödel undecidable sentence $G$—that is, $¬P⟨G⟩$—and its negation. The proof of Löb’s theorem fails, as it must, since the theory is nontrivial. Whether the Henkin sentence $H$—that is $𝒫⟨H⟩$—is provable in these arithmetics is currently unknown. In that sense, Henkin’s original question is still open.¹⁰