(<b>EDIT:</b> 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 <i>state</i> 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 <i>schema</i>; 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 <i>very</i> 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 <A href="https://doi.org/10.2307/2272251">Gödel’s second incompleteness theorem for <i>Q</i></a>, where <i>Q</i> is Robinson’s arithmetic. But <i>Q</i> is so weak that it cannot even properly formalize basic properties of syntax, so the fact that <i>Q</i> does not prove Con(<i>Q</i>) 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 <a href="http://www.math.ucsd.edu/~sbuss/ResearchWeb/BAthesis/Buss_Thesis_OCR.pdf"><i>Bounded Arithmetic</i></a>, 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 <i>hold</i> 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 <i>bounded reverse mathematics</i>. One book that explicitly pursues the program of bounded reverse mathematics is <i>Logical Foundations of Proof Complexity</i> 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 <i>Metamathematics of First-Order Arithmetic</i> by Pavel Pudlák and Petr Hájek, but I could not find an explicit statement there either. <hr> 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 <i>Predicative Arithmetic</i> about the number $80^{5000}$, <a href="https://mathoverflow.net/questions/142669/illustrating-edward-nelsons-worldview-with-nonstandard-models-of-arithmetic/146523#comment377806_146523">I once asked Nelson</a> 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 <a href="https://projecteuclid.org/euclid.bsl/1389017495">Interpretability in Robinson’s <i>Q</i></a>, by Fernando Ferreira and Gilda Ferreira. What Nelson seemed to be arguing in <i>Predicative Arithmetic</i> was that we should not regard a mathematical statement as meaningful unless it can be <i>interpreted in Q</i>. Ferreira and Ferreira point out that it has been shown (by Wilkie) that the totality of exponentiation cannot be interpreted in <i>Q</i>, whereas the negation of the totality of exponentiation can be interpreted in <i>Q</i> (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 <i>Q</i>. I would guess that this is true, but again I do not know of an explicit reference.