To the editors:

In his essay, Graham Priest shows how two very closely related results in logic get two very different treatments. The difference is right there in their names: Martin Löb has furnished a theorem, while Haskell Curry has provided a paradox, even though both are derived in almost exactly the same way, as Priest illustrates. Both results are surprising, but one—Löb’s—is acceptable while the other—Curry’s—is not. Why?

Priest suggests that this imbalance is poorly motivated, philosophically, and that indeed the two results ought to be treated in the same way. I generally agree with his diagnosis and suggestion that, given the similarity, the proofs of both Löb and Curry should fail. I will disagree with him, though, about the way to respond.

Löb seems to force us to accept that the schema

1. If A is provable then A is true

cannot be proven, except for instances in which we already know that the sentence A is provable. This is a disconcerting thing to be asked to accept. Indeed, it seems like the statement “All provable sentences are true” is almost analytic, true by definition of the word “provable.” A way to read the situation is that Löb seems to be pushing us to say that the word “provable” in statement 1 does not mean what we mean when we usually say it—especially when we say that statement 1 itself cannot be proven. Maybe there are two different notions at work, which might be disambiguated:

• It is not provable₁ that all provable₂ sentences are true.

This is less disconcerting. And indeed, this indexed picture is not dissimilar to the picture that emerges from the standard interpretations of Kurt Gödel’s incompleteness theorem.

But, Priest asks, what about the real notion of “provable,” which does seem to obey statement 1 and which does not seem to be somehow indexed? Gödel seems to use this notion in his own incompleteness theorem, leaning heavily on the idea that, indeed, all provable sentences are true—precisely to show that there is some true but unprovable sentence! There seems to be something almost self-defeating in using certain properties of provability to prove that we cannot establish those same properties. Introducing indexing to disambiguate just sends the problem off on an infinite regress to nowhere, without explaining how it is that Gödel’s proof proves anything—with no index.

Priest proposes a reformulation of arithmetic in which statement 1 is true for all A after all. Here is where he uses lessons from Curry’s paradox, to show how we might be able to accept statement 1 and block Löb’s so-called theorem. It is by dropping one of two principles from logic: either contraction,

• If A implies that A implies B, then A implies B,

or modus ponens,

• If A, and A implies B, then B.

As Priest notes, among non-classical logicians, dropping contraction has been the more popular of the two options, though doing so looks like it would deliver an arithmetic that is weaker than we have come to expect. That is, a contraction-free arithmetic will not be able to prove as much as classical arithmetic. Indeed, that is kind of the point, since it is meant not to prove some undesirable results. But assuming we would rather not lose some established arithmetic facts, Priest urges us away from a contraction-free approach and instead toward a modus ponens–free arithmetic, as he has explored elsewhere in his research.

I agree with Priest that there are challenges, maybe insurmountable, with going contraction-free. But I would suggest that the other option, dropping modus ponens, is as problematic—and problematic in much the same way—as the original scenario with Löb to which Priest objects. Let me explain.

Priest states that it is okay to go without modus ponens because “we know that there are axiomatic theories of arithmetic … whose underlying logic is paraconsistent, in which everything true in the Standard Model of arithmetic is provable.” We know this because it is a proven result—proven using modus ponens, among other things. A key result from model theory to which Priest is alluding is called the collapsing lemma. This is proven using an argument by mathematical induction. That is, the principle that, for any property F,

• If F(0) (base case) and if F(n) implies F(n + 1) (induction step), then for all x, F(x).

Priest wants to use mathematical induction to conclude that all truths of the standard model hold in the paraconsistent system. He proves this by establishing the base case and induction step of induction, and arriving at the conclusion using modus ponens.¹

If Priest is advocating giving up modus ponens, then this proof is invalid according to his own account. If it is problematic for Gödel to use the soundness of proof to show we cannot prove soundness, then it is problematic for Priest to use the ponenability of implication to show that we no longer need modus ponens.

A related problem is to ask, what would it mean to say about a modus ponens–free system that everything true in the Standard Model is provable? It would not mean that the system supports proofs in the ordinary sort of sense, like the line-by-line derivations Priest presents in his essay. Rather it would mean that we can see, standing outside the paraconsistent system, that all the standard truths are also true in the paraconsistent system. But within that system there is nothing like the chain of deductive reasoning that people use in normal mathematical practice—precisely because the system in question lacks modus ponens. So the notion of “provable” here is a more specialized notion than one might have thought, given the motivation of capturing the true meaning of “prove.”

I am sympathetic with Priest’s diagnosis of the situation—that the conventional view of Löb and Curry involves some unmotivated distinctions and dubious double-talk. I am also sympathetic to his suggestion that we should not be complacent and should strive for a better outcome using paraconsistent logic. A lot of Priest’s work, along with others’, over the past decades has made tremendous inroads in this mostly uncharted direction, so that future logicians will have easier paths to follow. And Priest is correct that some of the ways forward, like using non-contractive logic, look extremely difficult. But if the aim is to develop an understanding of arithmetic that captures the truths of the subject, in ways that avoid the problems with Löb and Curry that Priest highlights, then there is likely no quick or easy way to carry out this project—especially not ways that disavow their own means.

The fact that there is a lot of honest toil still to be done in arithmetic to revisit concepts from Löb, Curry, and Gödel is not in itself an objection. There was no quick or easy way to get to today’s understanding of arithmetic, or anything else—and it is likely the future will be bumpy, too. To go down the road Priest indicates will be bumpy. The demands of self-consistency mean there is just a lot of hard work that will have to be done, one modus ponens at a time.