This article includes a list of general references, but it remains largely unverified because it lacks sufficient corresponding inline citations. (October 2015) (Learn how and when to remove this template message)
In the philosophy of mathematics, ultrafinitism (also known as ultraintuitionism, strict formalism, strict finitism, actualism, predicativism, and strong finitism) is a form of finitism and intuitionism. There are various philosophies of mathematics that are called ultrafinitism. A major identifying property common among most of these philosophies is their objections to totality of number theoretic functions like exponentiation over natural numbers.
In addition, some ultrafinitists are concerned with acceptance of objects in mathematics that no one can construct in practice because of physical restrictions in constructing large finite mathematical objects. Thus some ultrafinitists will deny or refrain from accepting the existence of large numbers, for example, the floor of the first Skewes's number, which is a huge number defined using the exponential function as exp(exp(exp(79))), or
The reason is that nobody has yet calculated what natural number is the floor of this real number, and it may not even be physically possible to do so. Similarly, (in Knuth's up-arrow notation) would be considered only a formal expression which does not correspond to a natural number. The brand of ultrafinitism concerned with physical realizability of mathematics is often called actualism.
Edward Nelson criticized the classical conception of natural numbers because of the circularity of its definition. In classical mathematics the natural numbers are defined as 0 and numbers obtained by the iterative applications of the successor function to 0. But the concept of natural number is already assumed for the iteration. In other words, to obtain a number like one needs to perform the successor function iteratively, in fact exactly times to 0.
Some versions of ultrafinitism are forms of constructivism, but most constructivists view the philosophy as unworkably extreme. The logical foundation of ultrafinitism is unclear; in his comprehensive survey Constructivism in Mathematics (1988), the constructive logician A. S. Troelstra dismissed it by saying "no satisfactory development exists at present." This was not so much a philosophical objection as it was an admission that, in a rigorous work of mathematical logic, there was simply nothing precise enough to include.
People associated with ultrafinitism
Serious work on ultrafinitism has been led, since 1959, by Alexander Esenin-Volpin, who in 1961 sketched a program for proving the consistency of Zermelo–Fraenkel set theory in ultrafinite mathematics. Other mathematicians who have worked in the topic include Doron Zeilberger, Edward Nelson, Rohit Jivanlal Parikh, and Jean Paul Van Bendegem. The philosophy is also sometimes associated with the beliefs of Ludwig Wittgenstein, Robin Gandy, Petr Vopenka, and J. Hjelmslev.
Shaughan Lavine has developed a form of set-theoretical ultrafinitism that is consistent with classical mathematics. Lavine has shown that the basic principles of arithmetic such as "there is no largest natural number" can be upheld, as Lavine allows for the inclusion of "indefinitely large" numbers.
Computational complexity theory based restrictions
Other considerations of the possibility of avoiding unwieldy large numbers can be based on computational complexity theory, as in Andras Kornai's work on explicit finitism (which does not deny the existence of large numbers) and Vladimir Sazonov's notion of feasible number.
There has also been considerable formal development on versions of ultrafinitism that are based on complexity theory, like Samuel Buss's Bounded Arithmetic theories, which capture mathematics associated with various complexity classes like P and PSPACE. Buss's work can be considered the continuation of Edward Nelson's work on predicative arithmetic as bounded arithmetic theories like S12 are interpretable in Raphael Robinson's theory Q and therefore are predicative in Nelson's sense. The power of these theories for developing mathematics is studied in Bounded reverse mathematics as can be found in the works of Stephen A. Cook and Phuong The Nguyen. However these researches are not philosophies of mathematics but rather the study of restricted forms of reasoning similar to reverse mathematics.
- International Workshop on Logic and Computational Complexity, Logic and Computational Complexity, Springer, 1995, p. 31.
- St. Iwan (2000), "On the Untenability of Nelson's Predicativism", Erkenntnis 53(1–2), pp. 147–154.
- Not to be confused with Russell's predicativism.
- "Philosophy of Mathematics (Stanford Encyclopedia of Philosophy)". Plato.stanford.edu. Retrieved 2015-10-07.
- "Relation to foundations"
- Ésénine-Volpine, A. S. (1961), "Le programme ultra-intuitionniste des fondements des mathématiques", Infinitistic Methods (Proc. Sympos. Foundations of Math., Warsaw, 1959), Oxford: Pergamon, pp. 201–223, MR 0147389 Reviewed by Kreisel, G.; Ehrenfeucht, A. (1967), "Review of Le Programme Ultra-Intuitionniste des Fondements des Mathematiques by A. S. Ésénine-Volpine", The Journal of Symbolic Logic, Association for Symbolic Logic, 32 (4): 517, doi:10.2307/2270182, JSTOR 2270182
- Lavine, S., 1994. Understanding the Infinite, Cambridge, MA: Harvard University Press.
- Explicit finitism by Andras Kornai
- On feasible numbers by Vladimir Sazonov
- "Real" Analysis Is A Degenerate Case Of Discrete Analysis by Doron Zeilberger
- Discussion on formal foundations on MathOverflow
- History of constructivism in the 20th century by A. S. Troelstra
- Predicative Arithmetic by Edward Nelson
- Logical Foundations of Proof Complexity by Stephen A. Cook and Phuong The Nguyen
- Bounded Reverse Mathematics by Phuong The Nguyen
- Reading Brian Rotman’s “Ad Infinitum…” by Charles Petzold
- Computational Complexity Theory