There are formal systems that can’t construct exponentiation but still have weak versions of induction. in mainstream language, they have proof-theoretic ordinal ω^2. That exponentiation leads to proof theoretic ordinal ω^3 gives a precise way of saying that this is a natural place to stop. Ultrafinitists like Nelson appear to want something even more restrictive, but they refuse to talk in this language, so it’s hard to tell. I don’t blame them for wanting their own axiomatization, but their failure to even mention these systems makes me suspicious of them. Here is a Math Overflow discussion of ultrafinitist foundations.
There are formal systems that can’t construct exponentiation but still have weak versions of induction. in mainstream language, they have proof-theoretic ordinal ω^2. That exponentiation leads to proof theoretic ordinal ω^3 gives a precise way of saying that this is a natural place to stop. Ultrafinitists like Nelson appear to want something even more restrictive, but they refuse to talk in this language, so it’s hard to tell. I don’t blame them for wanting their own axiomatization, but their failure to even mention these systems makes me suspicious of them. Here is a Math Overflow discussion of ultrafinitist foundations.
The Buss axiom mentioned on Math Overflow is very cool.