Douglas_Knight comments on Exponentiation goes wrong first - Less Wrong

10 [deleted] 14 December 2010 04:13AM

You are viewing a comment permalink. View the original post to see all comments and the full post content.

Comments (81)

You are viewing a single comment's thread.

Comment author: Douglas_Knight 14 December 2010 06:19:58PM *  3 points [-]

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.

Comment author: [deleted] 14 December 2010 06:44:20PM 1 point [-]

The Buss axiom mentioned on Math Overflow is very cool.