Did Edward Nelson accept the incompleteness theorems?

Gödel’s second incompleteness theorem requires neither exponentiation nor “impredicative concepts”. The systems Nelson works in are fragments of arithmetic interpretable on definable cuts in $Q$; one such fragment is the bounded arithmetic $I\Delta_0+\Omega_1$ (this appears to be what Nelson calls $Q_4$ in the Predicative arithmetic book). The theory $I\Delta_0+\Omega_1$ (and even weak fragments of it with more restricted induction, such as $PV_1$) is perfectly capable of proving the second incompleteness theorem (for theories with a polynomial-time set of axioms, which is not a real constraint).


(EDIT: I have substantially rewritten this answer in light of what I have learned from Emil Jeřábek and from reading some of the relevant references more carefully.)

As Emil Jeřábek has said, the short answer to your second question is yes, but there are some caveats to note.

First of all, it is perhaps not immediately obvious even how to state Gödel’s incompleteness theorems in such a weak system, let alone prove them, since the usual statements quantify over sets of computable axioms. A set of axioms for which axiomhood is decidable only by an inordinately expensive computation is going to be difficult to talk about meaningfully in a very weak system. We can sidestep this problem by restricting attention to “tame” sets of axioms, since that includes all sets of axioms that are of practical interest in the foundations of mathematics. Even with this restriction, there is a technical difficulty with quantifying over sets of axioms, but we can sidestep that, too, by talking about the incompleteness theorem schema; i.e., for each set of axioms of interest, we write down a formula of (bounded) arithmetic to express axiomhood, and we have a separate instance of the incompleteness theorem schema for each such formula.

A second difficulty is that for very weak systems, there arises the question of whether the incompleteness theorems even mean what we want them to mean. For example, Bezboruah and Shepherdson proved Gödel’s second incompleteness theorem for Q, where Q is Robinson’s arithmetic. But Q is so weak that it cannot even properly formalize basic properties of syntax, so the fact that Q does not prove Con(Q) arguably does not mean much.

However, on the positive side, exponentiation is not required for the arithmetization of syntax. For example, in his Ph.D. thesis Bounded Arithmetic, Samuel Buss carried out the arithmetization of syntax in detail using a weak system called $S^1_2$, and proved a version of Gödel’s second incompleteness theorem for $S^1_2$. (Indeed, Nelson’s own book shows how to arithmetize basic syntax using his own system of “predicative arithmetic”.)

Buss’s proof still does not quite answer your question as posed, because you wanted to know not only whether the incompleteness theorems hold for weak systems; you asked whether the proofs of the incompleteness theorems can be formalized in a system that does not prove that exponentiation is a total function. This point confused me for a while because Buss’s proof actually appeals to Gentzen’s cut-elimination theorem, which is not provable in bounded arithmetic. However, as Emil Jeřábek pointed out, this is because Buss is proving a somewhat stronger version of the second incompleteness theorem than usual. If we consider the usual incompleteness theorem then an expert can see “by inspection” that the proof does not exceed the abilities of bounded arithmetic.

I still have not seen an explicit statement in the literature that the incompleteness theorems are provable in bounded arithmetic; this seems to be “folklore.” It is a result in an area called bounded reverse mathematics. One book that explicitly pursues the program of bounded reverse mathematics is Logical Foundations of Proof Complexity by Stephen Cook and Phuong Nguyen, but they do not prove the incompleteness theorems. Another book that discusses the incompleteness theorems for weak systems is Metamathematics of First-Order Arithmetic by Pavel Pudlák and Petr Hájek, but I could not find an explicit statement there either.

(EDIT: I asked on the Foundations of Mathematics mailing list for a published reference, and Richard Heck pointed me to On the scheme of induction for bounded arithmetic formulas by A. J. Wilkie and J. B. Paris, Ann. Pure Appl. Logic 35 (1987), 261–302. This paper gives a pretty detailed proof that the incompleteness theorems can be proved on the basis of the system $I\Delta_0 + \Omega_1$ for bounded arithmetic.)


Now for some comments about your first question. It is important to recognize that it was not always easy to ascertain exactly what Nelson believed, even when he was still alive. Even a weak system of arithmetic admits arbitrarily large numbers, but Nelson said things that indicated that he was suspicious of numbers that cannot actually be written down in unary. Following up on a comment in his book Predicative Arithmetic about the number $80^{5000}$, I once asked Nelson about the number $80\cdot 80 \cdots 80$ where we explicitly write down $5000$ copies of $80$. He was skeptical that this was an actual number, despite the fact that no exponentiation is involved. Under such circumstances, I am not even sure whether Nelson believed that $\sqrt{2}$ is irrational in the same sense that you and I believe that. If Nelson and I were to walk through the proof together, then of course he would agree that every step of the proof was formally correct, but what would the conclusion of the proof “say”? You and I think it says something about arbitrarily large natural numbers but Nelson might not. And if he did not, why should he even believe that the correctness of a short sequence of formal manipulations should tell us anything about (for example) whether a computer search for positive integers $a$ and $b$ such that $a^2 = 2b^2$ would succeed or fail? In short, I do not think it is particularly fruitful to try to understand exactly what Nelson personally believed or doubted, because he simply did not give a sufficiently detailed and coherent account of those beliefs.

There is an interesting discussion of Nelson’s “predicativism” in the paper Interpretability in Robinson’s Q, by Fernando Ferreira and Gilda Ferreira. What Nelson seemed to be arguing in Predicative Arithmetic was that we should not regard a mathematical statement as meaningful unless it can be interpreted in Q. Ferreira and Ferreira point out that it has been shown (by Wilkie) that the totality of exponentiation cannot be interpreted in Q, whereas the negation of the totality of exponentiation can be interpreted in Q (the latter is a result of Solovay). This would seem to vindicate Nelson’s view that exponentiation presents an “impassable barrier” to the committed predicativist. On the other hand, Ferreira and Ferreira also present arguments that Nelson’s view suffers from a certain “instability,” since for example it is not closed under taking conjunctions. I refer the reader to their paper for a more detailed discussion. In any case, it would seem that a necessary condition for Nelson to accept the incompleteness theorems would be that they are interpretable in Q. I would guess that this is true, but again I do not know of an explicit reference.


Your second question has been properly answered by Emil Jerabek, I would say. Reading some of the comments, I feel I should write the following about your first question:

From talking to Ed Nelson and to people who knew him well, I can say that Ed Nelson has for a long time been firmly convinced that the exponential function somehow leads to inconsistency (and therefore PA is inconsistent). He has written about this at length and has pointed out some motivation for this view, like the Bellantoni-Cook characterisation of function complexity and his writings on predicativity.

Ed Nelson's deeper motivation for his view seems to have been the following: he had a feeling that somehow fixed point constructions (like an enumeration of all partial recursive functions or Goedel's incompleteness theorems) could be 'internalised' or 'made total' to produce a contradiction like '0=1'. Such a contradiction would only be possible given the exponential function. At the most fundamental level, Ed Nelson did not believe that the notion of completed infinite set was formally consistent.