Ultrafinitism is (I believe) a philosophy of mathematics that is not only constructive, but does not admit the existence of arbitrarily large natural numbers. According to wikipedia, it has been primarily studied by Alexander Esenin-Volpin. On his opinions page, Doron Zeilberger has often expressed similar opinions.

Wikipedia also says that Troelstra said in 1988 that there were no satisfactory foundations for ultrafinitism. Is this still true? Even if so, are there any aspects of ultrafinitism that you can get your hands on coming from a purely classical perspective?

Edit: Neel Krishnaswami in his answer gave a link to a paper by Vladimir Sazonov (non-Springer link) that seems to go a ways towards giving a formal foundation to ultrafinitism.

First, Sazonov references a result of Parikh's which says that Peano Arithmetic can be consistently extended with a set variable $F$ and axioms $0\in F$, $1\in F$, $F$ is closed under $+$ and $\times$, and $N\notin F$, where $N$ is an exponential tower of $2^{1000}$ twos.

Then, he gives his own theory, wherein there is no cut rule and proofs that are too long are disallowed, and shows that the axiom $\forall x\ \log \log x < 10$ is consistent.

Ultrafinitism is (I believe) a philosophy of mathematics that is not only constructive, but does not admit the existence of arbitrarily large natural numbers. According to wikipedia, it has been primarily studied by Alexander Esenin-Volpin. On his opinions page, Doron Zeilberger has often expressed similar opinions.

Wikipedia also says that Troelstra said in 1988 that there were no satisfactory foundations for ultrafinitism. Is this still true? Even if so, are there any aspects of ultrafinitism that you can get your hands on coming from a purely classical perspective?

Edit: Neel Krishnaswami in his answer gave a link to a paper by Vladimir Sazonov (non-Springer link) that seems to go a ways towards giving a formal foundation to ultrafinitism.

First, Sazonov references a result of Parikh's which says that Peano Arithmetic can be consistently extended with a set variable $F$ and axioms $0\in F$, $1\in F$, $F$ is closed under $+$ and $\times$, and $N\notin F$, where $N$ is an exponential tower of $2^{1000}$ twos.

Then, he gives his own theory, wherein proofs that are too long are disallowed, and shows that the axiom $\forall x\ \log \log x < 10$ is consistent.

Ultrafinitism is (I believe), believe) a philosophy of mathematics that is not only constructive, but does not admit the existence of arbitrarily large natural numbers. According to wikipedia, it has been primarily studied by Alexander Esenin-Volpin. On his opinions page, Doron Zeilberger has often expressed similar opinions.

Wikipedia also says that Troelstra said in 1988 that there were no satisfactory foundations for ultrafinitism. Is this still true? Even if so, are there any aspects of ultrafinitism that you can get your hands on coming from a purely classical perspective?

Ultrafinitism is (I believe), a philosophy of mathematics that is not only constructive, but does not admit the existence of arbitrarily large natural numbers. According to wikipedia, it has been primarily studied by Alexander Esenin-Volpin. On his opinions page, Doron Zeilberger has often expressed similar opinions.

Wikipedia also says that Troelstra said in 1988 that there were no satisfactory foundations for ultrafinitism. Is this still true? Even if so, are there any aspects of ultrafinitism that you can get your hands on coming from a purely classical perspective?