Ultrafinitism

Last updated

In the philosophy of mathematics, ultrafinitism (also known as ultraintuitionism, [1] strict formalism, [2] strict finitism, [2] actualism, [1] predicativism, [2] [3] and strong finitism) [2] 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.

Contents

Main ideas

Like other finitists, ultrafinitists deny the existence of the infinite set of natural numbers, on the basis that it can never be completed (i.e., there is a largest natural number).

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 that 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 was led, from 1959 until his death in 2016, 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 Vopěnka, and Johannes Hjelmslev.

Shaughan Lavine has developed a form of set-theoretical ultrafinitism that is consistent with classical mathematics. [4] 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. [4]

Computational complexity theory based restrictions

Other considerations of the possibility of avoiding unwieldy large numbers can be based on computational complexity theory, as in András Kornai's work on explicit finitism (which does not deny the existence of large numbers) [5] and Vladimir Sazonov's notion of feasible numbers.

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 are not philosophies of mathematics but rather the study of restricted forms of reasoning similar to reverse mathematics.

See also

Notes

  1. 1 2 International Workshop on Logic and Computational Complexity, Logic and Computational Complexity, Springer, 1995, p. 31.
  2. 1 2 3 4 St. Iwan (2000), "On the Untenability of Nelson's Predicativism", Erkenntnis 53(1–2), pp. 147–154.
  3. Not to be confused with Russell's predicativism.
  4. 1 2 "Philosophy of Mathematics (Stanford Encyclopedia of Philosophy)". Plato.stanford.edu. Retrieved 2015-10-07.
  5. "Relation to foundations"

Related Research Articles

In the philosophy of mathematics, intuitionism, or neointuitionism, is an approach where mathematics is considered to be purely the result of the constructive mental activity of humans rather than the discovery of fundamental principles claimed to exist in an objective reality. That is, logic and mathematics are not considered analytic activities wherein deep properties of objective reality are revealed and applied, but are instead considered the application of internally consistent methods used to realize more complex mental constructs, regardless of their possible independent existence in an objective reality.

In the philosophy of mathematics, constructivism asserts that it is necessary to find a specific example of a mathematical object in order to prove that an example exists. Contrastingly, in classical mathematics, one can prove the existence of a mathematical object without "finding" that object explicitly, by assuming its non-existence and then deriving a contradiction from that assumption. Such a proof by contradiction might be called non-constructive, and a constructivist might reject it. The constructive viewpoint involves a verificational interpretation of the existential quantifier, which is at odds with its classical interpretation.

Presburger arithmetic is the first-order theory of the natural numbers with addition, named in honor of Mojżesz Presburger, who introduced it in 1929. The signature of Presburger arithmetic contains only the addition operation and equality, omitting the multiplication operation entirely. The theory is computably axiomatizable; the axioms include a schema of induction.

<span class="mw-page-title-main">Set theory</span> Branch of mathematics that studies sets

Set theory is the branch of mathematical logic that studies sets, which can be informally described as collections of objects. Although objects of any kind can be collected into a set, set theory — as a branch of mathematics — is mostly concerned with those that are relevant to mathematics as a whole.

In logic, Richard's paradox is a semantical antinomy of set theory and natural language first described by the French mathematician Jules Richard in 1905. The paradox is ordinarily used to motivate the importance of distinguishing carefully between mathematics and metamathematics.

Finitism is a philosophy of mathematics that accepts the existence only of finite mathematical objects. It is best understood in comparison to the mainstream philosophy of mathematics where infinite mathematical objects are accepted as existing.

Foundations of mathematics is the logical and mathematical framework that allows the development of mathematics without generating self-contradictory theories, and, in particular, to have reliable concepts of theorems, proofs, algorithms, etc. This may also include the philosophical study of the relation of this framework with reality.

Proof theory is a major branch of mathematical logic and theoretical computer science within which proofs are treated as formal mathematical objects, facilitating their analysis by mathematical techniques. Proofs are typically presented as inductively-defined data structures such as lists, boxed lists, or trees, which are constructed according to the axioms and rules of inference of a given logical system. Consequently, proof theory is syntactic in nature, in contrast to model theory, which is semantic in nature.

Reverse mathematics is a program in mathematical logic that seeks to determine which axioms are required to prove theorems of mathematics. Its defining method can briefly be described as "going backwards from the theorems to the axioms", in contrast to the ordinary mathematical practice of deriving theorems from axioms. It can be conceptualized as sculpting out necessary conditions from sufficient ones.

<span class="mw-page-title-main">Edward Nelson</span> American mathematician (1932–2014)

Edward Nelson was an American mathematician. He was professor in the Mathematics Department at Princeton University. He was known for his work on mathematical physics and mathematical logic. In mathematical logic, he was noted especially for his internal set theory, and views on ultrafinitism and the consistency of arithmetic. In philosophy of mathematics he advocated the view of formalism rather than platonism or intuitionism. He also wrote on the relationship between religion and mathematics.

In mathematical logic, the Brouwer–Heyting–Kolmogorov interpretation, or BHK interpretation, of intuitionistic logic was proposed by L. E. J. Brouwer and Arend Heyting, and independently by Andrey Kolmogorov. It is also sometimes called the realizability interpretation, because of the connection with the realizability theory of Stephen Kleene. It is the standard explanation of intuitionistic logic.

Alexander Sergeyevich Esenin-Volpin was a Russian-American poet and mathematician.

Primitive recursive arithmetic (PRA) is a quantifier-free formalization of the natural numbers. It was first proposed by Norwegian mathematician Skolem (1923), as a formalization of his finitistic conception of the foundations of arithmetic, and it is widely agreed that all reasoning of PRA is finitistic. Many also believe that all of finitism is captured by PRA, but others believe finitism can be extended to forms of recursion beyond primitive recursion, up to ε0, which is the proof-theoretic ordinal of Peano arithmetic. PRA's proof theoretic ordinal is ωω, where ω is the smallest transfinite ordinal. PRA is sometimes called Skolem arithmetic, although that has another meaning, see Skolem arithmetic.

Markov's principle, named after Andrey Markov Jr, is a conditional existence statement for which there are many equivalent formulations, as discussed below. The principle is logically valid classically, but not in intuitionistic constructive mathematics. However, many particular instances of it are nevertheless provable in a constructive context as well.

In intuitionistic mathematics, a choice sequence is a constructive formulation of a sequence. Since the Intuitionistic school of mathematics, as formulated by L. E. J. Brouwer, rejects the idea of a completed infinity, in order to use a sequence, we must have a formulation of a finite, constructible object that can serve the same purpose as a sequence. Thus, Brouwer formulated the choice sequence, which is given as a construction, rather than an abstract, infinite object.

<span class="mw-page-title-main">Mathematical object</span> Anything with which mathematical reasoning is possible

A mathematical object is an abstract concept arising in mathematics. In the usual language of mathematics, an object is anything that has been formally defined, and with which one may do deductive reasoning and mathematical proofs. Typically, a mathematical object can be a value that can be assigned to a variable, and therefore can be involved in formulas. Commonly encountered mathematical objects include numbers, sets, functions, expressions, geometric objects, transformations of other mathematical objects, and spaces. Mathematical objects can be very complex; for example, theorems, proofs, and even theories are considered as mathematical objects in proof theory.

Geoffrey Hellman is an American professor and philosopher. He is Professor of Philosophy at the University of Minnesota in Minneapolis, Minnesota. He obtained his B.A. (1965) and Ph.D. (1972) degrees in philosophy from Harvard University. He was elected to the American Academy of Arts and Sciences in 2007.

In proof theory, a branch of mathematical logic, elementary function arithmetic (EFA), also called elementary arithmetic and exponential function arithmetic, is the system of arithmetic with the usual elementary properties of 0, 1, +, ×, , together with induction for formulas with bounded quantifiers.

Bounded arithmetic is a collective name for a family of weak subtheories of Peano arithmetic. Such theories are typically obtained by requiring that quantifiers be bounded in the induction axiom or equivalent postulates. The main purpose is to characterize one or another class of computational complexity in the sense that a function is provably total if and only if it belongs to a given complexity class. Further, theories of bounded arithmetic present uniform counterparts to standard propositional proof systems such as Frege system and are, in particular, useful for constructing polynomial-size proofs in these systems. The characterization of standard complexity classes and correspondence to propositional proof systems allows to interpret theories of bounded arithmetic as formal systems capturing various levels of feasible reasoning.

References