Mathematician Edward Nelson is known for his extreme views on the foundations of mathematics, variously described as "ultrafintism" or "strict finitism" (Nelson's preferred term), which came into the split light recently because of his claim, quickly recanted, of proving $PA$ inconsistent (but he's still working on it). He believes in Robinson Arithmetic, but not the induction schema of Peano Arithmetic (although he does accept weak forms of induction interpretable in Robinson's $Q$, like induction for bounded formulas; see his book Predicative Arithmetic). He even believes that exponentiation is not total! Here is a quote explaining his viewpoint:
“The intuition that the set of all subsets of a finite set is finite—or more generally, that if $A$ and $B$ are finite sets, then so is the set $B^A$ of all functions from $A$ to $B$—is a questionable intuition. Let $A$ be the set of some $5000$ spaces for symbols on a blank sheet of typewriter paper, and let $B$ be the set of some $80$ symbols of a typewriter; then perhaps $B^A$ is infinite. Perhaps it is even incorrect to think of $B^A$ as being a set. To do so is to postulate an entity, the set of all possible typewritten pages, and then to ascribe some kind of reality to this entity—for example, by asserting that one can in principle survey each possible typewritten page. But perhaps it is simply not so. Perhaps there is no such number as $80^{5000}$; perhaps it is always possible to write a new and different page.”
He believes that finite numbers are closed under addition and multiplication, but not exponentiation: he thinks you can have two numbers, like $80$ and $5000$, which are both finite, but where $80^{5000}$ in infinitely large!
My question is, can we illustrate this view using a nonstandard model of arithmetic? Specifically, how would we construct a nonstandard model of $Q$, containing an initial segment closed under successor, addition, and multiplication, but not exponentiation? Preferably, I'd like a computable nonstandard model.
Any help would be greatly appreciated.
Thank You in Advance.
EDIT: As @JoelDavidHamkins pointed out, exponentiation need not be total in a model of $Q$, so such a model wouldn't illustrate the phenomenon Edward Nelson believes is possible, of the exponentiation of finite numbers being infinite. So let me clarify: I'm looking for a computable nonstandard model of $Q$ + "exponentiation is total", such that the model has an initial segment closed under successor, addition, and multiplication, but not exponentiation.
EDIT 2: @EmilJeřábek has pointed out that different formulations of "exponentiation is total" in the language of arithmetic aren't provably equivalent in $Q$. How you formalize this assertion doesn't really concern me, so rather than talk about models of $Q$ + "exponentiation is total", let me talk about models $M$ of $Q$ equipped with a binary operation on $M$ that satisfies the basic properties of exponentiation: $a^{b+c} = a^b a^c$, $(a^b)^c = a^{bc}$, $a^1 = a$, $a^{0} = 1$, and $0^b = 0$. I also want addition and multiplication to be commutative and associative, multiplication to distribute over addition, and addition to obey the cancellation property that $a + c = b + c$ implies $a = b$. An example of a computable nonstandard model of $Q$ that satisfies at least these properties of addition and multiplication is the set of polynomials $\{P = a_nx^n + \ldots + a_0 \in \Bbb Z[x] , a_n > 0 \}$, together with $0$, with polynomial addition and multiplication, and the successor just involving adding $1$.
Best Answer
Thanks to Timothy Chow for informing me of this discussion.
To avoid vagueness, let Q* be Q with the usual relativization schemata adjoined. Construct a formal system F by adjoining an unary predicate symbol $\psi$, the axiom $\psi(0)$, and the rule of inference: from $\rm\psi(a)$ infer $\rm\psi(Sa)$ (for any term a). I think this is an adequate formalization of the concept of an "actual number". Is $\psi(80^{5000})$ a theorem of F? I see no reason to believe so. Of course, one can arithmetize F in various theories, even Q*, and prove a formula $\exists p[p \hbox{ is an arithmetized proof in F of } `\psi(80^{5000})\hbox{'}]$, but to conclude from this that there is a proof in F itself of $\psi(80^{5000})$ appears to me to be unjustified.
Contrast F with the theory T obtained by adjoining to Q* a unary predicate symbol $\phi$ and the two axioms $\phi(0)$ and $\phi(0)\;\&\;\forall x'[\phi(x')\to\phi({\rm S}x')]\to\phi(x)$. Then one can easily prove in T $\phi(80^{5000})$ or even $\phi(80^{5000...^{5000}})$. The ellipsis means that the iterated exponential term is actually written down.