Douglas_Knight comments on Exponentiation goes wrong first - Less Wrong
You are viewing a comment permalink. View the original post to see all comments and the full post content.
You are viewing a comment permalink. View the original post to see all comments and the full post content.
Comments (81)
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.