17
$\begingroup$

Edward Nelson advocated weak versions of arithmetic (called predicative arithmetic) that couldn't prove the totality of exponentiation. Since his theory extends Robinson arithmetic, the incompleteness theorems apply to it. But if the incompleteness theorems are proven in theories stronger than those he accepts, he could presumably reject them. So my questions are first, did Nelson doubt either of the incompleteness theorems? And second, can the incompleteness theorems be proved in weak systems of arithmetic that don't prove the totality of exponentiation?

The closest thing I can find to an answer is an excerpt from his book Predicative Arithmetic, in which he says on page 81 "at least one of these two pillars of finitary mathematical logic, the Hilbert-Ackermann Consistency Theorem and Gödel's Second Theorem, makes an appeal to impredicative concepts."

$\endgroup$
3
  • $\begingroup$ The first question seems like the sort of thing that could only be answered by Nelson. Is it a reference request? $\endgroup$
    – LSpice
    Commented Dec 13, 2020 at 0:46
  • 1
    $\begingroup$ Isn't Edward Nelson the guy who claims arithmetic is inconsistent? Doesn't the incompleteness theorem say something like "if arithmetic is consistent, then a certain statement is unprovable"? So isn't it automatically true if arithmetic is inconsistent? (I don't know anything about logic so I'm probably talking nonsense.) $\endgroup$
    – bof
    Commented Dec 13, 2020 at 1:24
  • 8
    $\begingroup$ bof, Nelson published a mistaken proof of an inconsistency in Peano arithmetic some years back, but he withdrew it when Terry Tao pointed out the error. He did believe for a long time that PA was inconsistent. I don't know why he thought that: I can understand believing that PA is false or meaningless, but "inconsistent" is a stronger claim. The stuff on his web site doesn't really explain this. LSpice, we lost Ed Nelson in 2014 so we unfortunately don't have a way to receive any new answers from him. $\endgroup$
    – none
    Commented Dec 13, 2020 at 3:36

3 Answers 3

22
$\begingroup$

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

$\endgroup$
7
  • $\begingroup$ I am still confused about something. I looked again at Buss's thesis, where he proves the incompleteness theorems for $S^1_2$ in the familiar form $S^1_2 \not\vdash \phi$ where $\phi$ is a consistency statement. But his proof appeals to Gentzen's cut-elimination theorem, which he says is not provable in bounded arithmetic. Is there a better reference than Buss's thesis? Or is the issue that we should instead be focusing on what you called the real incompleteness theorem, which is a statement about interpretability and not a direct statement about the unprovability of consistency? $\endgroup$ Commented Dec 14, 2020 at 4:09
  • 1
    $\begingroup$ I had a look at the thesis. He actually proves the incompleteness theorem in the stronger form that $S^1_{2,\alpha}$ (which is a notation for $S^1_2$ extended with axioms in the range of a $PV$-function $\alpha$) does not prove its own free-cut-free consistency; that’s why the proof also refers to free-cut-free proofs. You can just ignore that if you want the result for ordinary provability. But anyway, the formalized version of the second incompleteness theorem for free-cut-free provability would need to refer to it everywhere: ... $\endgroup$ Commented Dec 15, 2020 at 14:37
  • 1
    $\begingroup$ ... $S^1_2\vdash\mathrm{ThmFCF}^1_\alpha(\ulcorner\mathrm{FCFCon}^1_\alpha\urcorner)\to\neg\mathrm{FCFCon}^1_\alpha$. $\endgroup$ Commented Dec 15, 2020 at 14:37
  • $\begingroup$ Ah, thanks...that makes sense. I have been poking around some of the usual sources (e.g., Pudlák and Hájek's book, Cook and Nguyen's book) and they don't seem to say explicitly that the incompleteness theorems are provable in "bounded reverse mathematics." I guess you're just expected to examine the proofs and "see" that they don't use superpolynomial reasoning? $\endgroup$ Commented Dec 15, 2020 at 16:06
  • $\begingroup$ Generally speaking, for variants of the second incompleteness theorem proved by reasoning with appropriate analogues of the Hilbert–Bernays–Löb provability conditions (as is the case here), the formalized version of the incompleteness theorem (in the “schema” formulation) follows by a simple extension of the proof of the non-formalized version, still using the same provability conditions. See e.g. the usual proof of Löb’s axiom. $\endgroup$ Commented Dec 15, 2020 at 16:37
15
$\begingroup$

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

$\endgroup$
11
  • 3
    $\begingroup$ The Bezboruah and Shepherdson result (which basically exploits the fact that Q doesn't prove much of anything to show that in particular, it doesn't prove anything of a syntactic form similar to a consistency statement) is a red herring. The real second incompleteness theorem for weak theories says that if $T$ is any consistent recursively axiomatized theory, then $T$ cannot interpret $Q+Con(T)$. (Pudlák, Cuts, consistency statements, and interpretations, JSL 1985, proves an even stronger form with restricted consistency statements.) Since an interpretation of $Q+Con(T)$ can be assumed ... $\endgroup$ Commented Dec 13, 2020 at 8:20
  • 1
    $\begingroup$ ... to actually interpret, say, $I\Delta_0+\Omega_1+Con(T)$ by passing to a definable cut if necessary, there is no question whether the statement really "means" the consistency of $T$ (or rather, this is no more in question than it is when applied in PA). Sequence encoding and formalization of the various syntactic notions used in the consistency statements are perfectly well-behaved in $I\Delta_0+\Omega_1$. $\endgroup$ Commented Dec 13, 2020 at 8:27
  • 3
    $\begingroup$ After a closer look at the book, it turns out that arithmetizing syntax, including consistency statement, in $I\Delta_0+\Omega_1$, is exactly what Nelson is doing in the second part of the book! So, assuming we can take at face value that he accepts as valid everything that he put in the book, there is no doubt that he finds arithmetization of consistency statements (including the formulation of Gödel’s second incompleteness theorem) as meaningful, and he even developed himself in the book more or less all the tools needed to actually prove the incompleteness theorem. $\endgroup$ Commented Dec 13, 2020 at 10:49
  • 1
    $\begingroup$ @EmilJeřábek : I understand that syntax can be arithmetized in weak theories but how exactly are you stating "T is recursively axiomatized theory" in a weak system? Also, as I explained, although Nelson surely accepts that all the reasoning in his book is valid, it does not follow that he believes the theorem statements in the sense that he regards the theorems as making meaningful assertions that he actually believes. $\endgroup$ Commented Dec 13, 2020 at 14:07
  • 2
    $\begingroup$ Yes, though I guess the $\Sigma^b_1$ version can be made into a single statement using the existence of a universal $\Sigma^b_1$ formula in a fragment of $I\Delta_0+\Omega_1$. $\endgroup$ Commented Dec 13, 2020 at 16:47
8
$\begingroup$

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.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .