My understanding is that Nelson doesn't necessarily believe in exponentiation either although his work here doesn't have the direct potential to wreck that.

I know this isn't the main point of your comment but I got carried away looking this stuff up.

In his 1986 book, he defines a predicate exp(x,k,f) which basically means "f is a function defined for i < k and f(i) = x^i". And he defines another predicate epsilon(k) which is "for all x there exists f such that exp(x,k,f)". I think you can give a proof of epsilon(k) in his regime in O(log log k) steps. In standard arithmetic that takes O(1) steps using induction, but O(log log k) is pretty cheap too if you're not going to iterate exponentiation. So that's a sense in which Nelson does believe in exponentiation.

On the other hand I think it's accurate to say that Nelson doesn't believe that exponentiation is total, i.e. that for all n, epsilon(n). Here's an extract from Nelson's "Predicative Arithmetic" (Princeton U Press 1986). Chapter heading: "Is exponentiation total?"

Why are mathematicians so convinced that exponentiation is total (everywhere defined)? Because they believe in the existence of abstract objects called numbers. What is a number? Originally, sequences of tally marks were used to count things. Then positional notation -- the most powerful achievement of mathematics -- was invented. Decimals (i.e. numbers written in positional notation) are simply canonical forms for variable-free terms of arithmetic. It has universally assumed, on the basis of scant evidence, that decimals are the same kind of thing as sequences of tally marks, only expressed in a more practical and efficient notation. This assumption is based on the semantic view of mathematics, in which mathematical expressions, such as decimals and sequences of tally marks, are regarded as denoting abstract objects. But to one who takes a formalist view of mathematics, the subject matter of mathematics is the expressions themselves together with the rules for manipulating them -- nothing more. From this point of view, the invention of positional notation was the creation of a new kind of number.

How is it then that we can continue to think of the numbers as being 0, S0, SS0, SSS0, ...? The relativization scheme of Chapter 5 [heading: "Induction by relativization"] explains this to some extent. But now let us adjoin exponentiation to the symbols of arithmetic. Have we again created a new kind of number? Yes. Let b be a variable-free term of arithmetic. To say that the expression 2^b is just another way of expressing the variable-free term of arithmetic, SS0 SS0 ... SS0 with b occurrences of SS0, is to assume that b denotes something that is also denoted by a sequence of tally marks. (The notorious three dots are a direct carry-over from tally marks.) The situation is worse for expressions of the form 2^2^b -- then we need to assume that 2^b itself denotes something that is also denoted by a sequence of tally marks.

Mathematicians have always operated on the unchallenged assumption that it is possible in principle to express 2^b as a numeral by performing the recursively indicated computations. To say that it is possible in principle is to say that the recursion will terminate in a certain number of steps -- and this use of the word "numbers" can only refer to the primitive notion; the steps are things that are counted by a sequence of tally marks. In what number of steps will the recursion terminate? Why, in somewhat more that 2^b steps. The circularity in the argument is glaringly obvious.