A model-theoretic question re: Nelson and exponentiation EDIT: I am not asking about the validity of exponentiation, or PA. My question  is about a specific technical claim which Nelson makes in this article (pp. 9-12): that a certain theory does not prove a certain sentence, and more generally that that theory does not prove any of a certain class of sentences. I am not interested in the mathematical quality, philosophical validity, literary value, font choice, overall moral rectitude, or shoe size of the article as a whole. I hope my edits have clarified this, and it is now apparent that the philosophical context of this question is merely that: context.
Let's suppose we are skeptical that PA is in fact consistent; perhaps we are convinced that addition "makes sense," pretty sure multiplication "makes sense," but dubious that exponentiation "makes sense" (this appears to not be too far from Nelson's own opinions, based on the article linked above). It now becomes valuable to have a notion of relative finitism: if we accept that one operation makes sense finitistically, what other operations can we argue are acceptable on that basis alone?
Informally, we want to ask:

Given definable functions $f, g$ (growthwise in the neighborhood of the "usual arithmetic functions"), can we prove that, if there is a "natural number series" closed under $f$, then there is also a "natural number series" closed under $g$?

Of course, the word "prove" is a dangerous one there: if we mean prove in PA, we're trivializing everything right from the outset even if we're confident PA is consistent. On the other hand, replacing PA with a weaker theory seems to beg the question of how to justify the finitistic acceptability of that theory. 
Nelson suggests the following approach: start with PA, but somehow modify it so that it can imagine proper initial segments of the universe which are closed under successor. Now we can ask nontrivial questions about the existence of "well-behaved initial segments" - intuitively, "notions of number" that permit the operations we care about to make sense - and we can do so from the perspective of PA even without accepting PA!
Specifically, Nelson considers the theory PA', in the language of arithmetic + a new unary predicate symbol $C$ (counting number), consisting of PA together with the statement "$C$ is downwards-closed, contains $0$, and $\forall x(C(x)\implies C(x+1))$."
Although PA' contains PA, it is still extremely weak in a sense: since we haven't extended the induction scheme to include formulas involving $C$, PA' can't prove the "obvious" statement $\forall x(C(x))$," or even that $C$ is closed under addition! So we're in a very interesting situation: on the one hand, we have a lot of deductive power at our disposal from the "ambient PA-ness," but on the other hand we've also given ourselves tools for creating contexts in which arithmetic breaks very badly.
Nelson uses this as a platform for asking the above question in a rigorous form.


*

*Claim 1: There is a definable initial segment of $C$ which PA' proves is closed under addition (and successor).


*

*Proof: Let $A=\{x\in C: \forall y\in C(y+x\in C)\}$. Downwards closure and closure under successor are easy to prove. For closure under addition, note that if $x_1,x_2\in A$ and $y\in C$, we have $y+(x_1+x_2)=(y+x_1)+x_2$, and $y+x_1\in C$ since $x_1\in A$, so $(y+x_1)+x_2\in C$ since $x_2\in A$; that is, $x_1,x_2\in A\implies x_1+x_2\in A$.


*Claim 2: There is a definable initial segment of $C$ which PA' proves is closed under multiplication (and addition and successor).


*

*Proof: Let $M=\{x\in A: \forall y\in A(y\cdot x\in A)\}$. Downwards closure and closure under successor and addition are easy to prove. For closure under multiplication, note that if $x_1,x_2\in M$ and $y\in A$, we have $y\cdot (x_1\cdot x_2)=(y\cdot x_1)\cdot x_2$, and $y\cdot x_1\in A$ since $x_1\in M$, so $(y\cdot x_1)\cdot x_2\in A$ since $x_2\in M$; that is, $x_1,x_2\in M\implies x_1\cdot x_2\in M$.



Note that in each case we've used associativity (which is proved in PA for all numbers, not just those in $C$; this is how PA provides "useful context" for our finitistic concerns, the point being that "addition is associative" is clearly acceptable relative to the claim that addition makes sense in the first place). This breaks down for exponentiation, of course. Here Nelson makes two claims, one explicit and the other implicit.
The claim Nelson makes explicitly is:

Weak claim: PA' cannot prove that the set $E=\{x\in M: \forall y\in M(y^x\in M)\}$ is closed under exponentiation.

It seems, however, that his real point is that this is a fundamental obstacle, that in some sense the definition of $E$ above is the only "reasonable" candidate. In other words, I think the following stronger claim is implicit in Nelson's critique of arithmetic:

Strong claim: PA' cannot prove that there is a definable initial segment of $C$ closed under exponentiation. (More precisely: there is no formula $\varphi$ in the language of PA' such that PA' proves that $\varphi$ defines an initial segment of $C$ which is closed under exponentiation.)

My question is:

Question: Are these claims correct?

I'm specifically interested in the stronger claim, since that seems to be the more significant one and a positive answer would have plausible foundational value; however, the weaker claim is probably easier to analyze, and is also the only claim Nelson explicitly made.

Let me mention, for additional motivation, two possible "spin-off" questions which may be of interest:


*

*First, we could replace PA with a different theory of arithmetic. This would have the effect of changing what arithmetic results we could use in establishing the existence of a definable cut below $C$ with certain closure properties. The arguments above only require the most basic bits of arithmetic, but conceivably a more complicated argument could require a nontrivial amount of induction. If indeed replacing PA with a different theory of arithmetic would change the situation, that would be really cool, even if the foundational significance is not obvious.

*Second, we can "relativize" Nelson's construction. Say that a definable (in the language of PA) function $f$ is finitistic relative to another definable function $g$ if there is a formula $\varphi$ in the language of PA$_g$ - which is the theory consisting of PA together with a unary predicate symbol $G$, and axioms saying that $G$ names a downwards-closed set closed under successor and $g$ - which PA$_g$ proves defines a downwards-closed set closed under successor and $f$. Relative finitism seems potentially interesting (and possibly connected with bounded arithmetic), even from a non-finitistic point of view, especially if per the above bulletpoint the "ambient arithmetic" can meaningfully affect the situation.
 A: Here is a proof of the weak claim.  Let $X$ be any nonstandard model of PA with an initial segment $I$ containing all standard numbers which is closed under addition and multiplication but not exponentiation.  Let $C$ be the set of $x\in X$ such that $x\leq n^i$ for some standard $n$ and some $i\in I$.  Note that $C$ is closed under addition and multiplication: if $x\leq n^i$ and $y\leq m^j$, then $xy$ and $x+y$ are both at most $(m+n)^{i+j}$.  So, we can take $X$ as a model of PA' with this $C$, and your set $M$ will be $C$.
Note also that $C$ is closed under exponentiation to elements of $I$, since if $x\leq n^i$ then $x^j\leq (n^i)^j=n^{ij}$.  It follows that your set $E$ contains $I$.  On the other hand, if $e\in E$, then in particular $2^e\in C$ so $2^e\leq n^i$ for some standard $n$ and some $i\in I$.  But we have $(2^m)\geq n$ for some standard $m$, and so $n^i\leq 2^{mi}$ and so $e\leq mi$.  Thus $e\in I$.
Thus your set $E$ for this model is just $I$.  Since $I$ was chosen to not be closed under exponentiation, this proves the weak claim.
