Skip to main content
Added link to paper by Wilkie and Paris
Source Link
Timothy Chow
  • 82.7k
  • 26
  • 363
  • 587

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

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

Major rewrite
Source Link
Timothy Chow
  • 82.7k
  • 26
  • 363
  • 587

(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 clear how to state Gödel’s incompleteness theorems in such a weak system, let alone prove itthem, since the usual statements make referencequantify over sets of computable axioms. A set of axioms for which axiomhood is decidable only by an inordinately expensive computation is going to computably enumerable axiomatic systemsbe difficult to talk about meaningfully in a very weak system.

One We can sidestep that issuethis problem by focusing on a specific systemrestricting attention to “tame” sets of axioms, since that includes all sets of axioms that are of practical interest. For example you might ask if Robinson’s arithmetic Q can prove Con(Q) in the foundations of mathematics. You might think that Even with this restriction, there is just a special casetechnical difficulty with quantifying over sets of Gödel’s second theoremaxioms, but weirdly enough,we can sidestep that is not quite true, at least not the waytoo, by talking about the incompleteness theorem is usually provedschema; i.e., because the arithmetizationfor each set of syntax is usually carried out inaxioms of interest, we write down a way that assumes various factsformula of elementary number theory that in turn assume that exponentiation is total(bounded) arithmetic to express axiomhood, and we have a separate instance of the incompleteness theorem schema for each such formula. However

A second difficulty is that for very weak systems, these difficulties can be circumventedthere arises the question of whether the incompleteness theorems even mean what we want them to mean. For example, and Bezboruah and Shepherdson did proveproved Gödel’s second incompleteness theorem for Q, where Q is Robinson’s arithmetic. ItBut Q is questionable, howeverso weak that it cannot even properly formalize basic properties of syntax, what such a statement really “means” for someone whoso the fact that Q does not believe that exponentiation is total. The stringprove Con(Q) arguably does not mean much.

However, taken literallyon the positive side, exponentiation is some kindnot required for the arithmetization of complicated algebraic statementsyntax. 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 ifproved 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 harbor serious doubts aboutwanted to know not only whether the totalityincompleteness 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, then itwhich is not clear thatprovable in bounded arithmetic. However, as Emil Jeřábek pointed out, this complicated algebraicis 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 really “expresses”in the consistencyliterature 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 QLogical 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.

 

AsNow for exactly what Nelson believed,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$ and he. 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.

First of all it is not even clear how to state Gödel’s incompleteness theorems in such a weak system, let alone prove it, since the usual statements make reference to computably enumerable axiomatic systems.

One can sidestep that issue by focusing on a specific system of interest. For example you might ask if Robinson’s arithmetic Q can prove Con(Q). You might think that this is just a special case of Gödel’s second theorem, but weirdly enough, that is not quite true, at least not the way the theorem is usually proved, because the arithmetization of syntax is usually carried out in a way that assumes various facts of elementary number theory that in turn assume that exponentiation is total. However, these difficulties can be circumvented, and Bezboruah and Shepherdson did prove Gödel’s second incompleteness theorem for Q. It is questionable, however, what such a statement really “means” for someone who does not believe that exponentiation is total. The string Con(Q), taken literally, is some kind of complicated algebraic statement, and if you harbor serious doubts about the totality of exponentiation, then it is not clear that this complicated algebraic statement really “expresses” the consistency of Q.

As for exactly what Nelson believed, that was not always easy to ascertain 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.  I once asked Nelson about the number $80\cdot 80 \cdots 80$ where we explicitly write down $5000$ copies of $80$ and 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.

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

 

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.

Source Link
Timothy Chow
  • 82.7k
  • 26
  • 363
  • 587

First of all it is not even clear how to state Gödel’s incompleteness theorems in such a weak system, let alone prove it, since the usual statements make reference to computably enumerable axiomatic systems.

One can sidestep that issue by focusing on a specific system of interest. For example you might ask if Robinson’s arithmetic Q can prove Con(Q). You might think that this is just a special case of Gödel’s second theorem, but weirdly enough, that is not quite true, at least not the way the theorem is usually proved, because the arithmetization of syntax is usually carried out in a way that assumes various facts of elementary number theory that in turn assume that exponentiation is total. However, these difficulties can be circumvented, and Bezboruah and Shepherdson did prove Gödel’s second incompleteness theorem for Q. It is questionable, however, what such a statement really “means” for someone who does not believe that exponentiation is total. The string Con(Q), taken literally, is some kind of complicated algebraic statement, and if you harbor serious doubts about the totality of exponentiation, then it is not clear that this complicated algebraic statement really “expresses” the consistency of Q.

As for exactly what Nelson believed, that was not always easy to ascertain 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. I once asked Nelson about the number $80\cdot 80 \cdots 80$ where we explicitly write down $5000$ copies of $80$ and 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.