Constructivism (mathematics)
Encyclopedia
In the philosophy of mathematics
, constructivism asserts that it is necessary to find (or "construct") a mathematical object to prove that it exists. When one assumes that an object does not exist and derives a contradiction from that assumption
, one still has not found the object and therefore not proved its existence, according to constructivists. This viewpoint involves a verificational interpretation of the existence quantifier, which is at odds with its classical interpretation.
There are many forms of constructivism. These include the program of intuitionism
founded by Brouwer
, the finitism
of Hilbert
and Bernays
, the constructive recursive mathematics of Shanin and Markov
, and Bishop
's program of constructive analysis. Constructivism also includes the study of constructive set theories
such as IZF and the study of topos theory.
Constructivism is often identified with intuitionism, although intuitionism is only one constructivist program. Intuitionism maintains that the foundations of mathematics lie in the individual mathematician's intuition, thereby making mathematics into an intrinsically subjective activity. Other forms of constructivism are not based on this viewpoint of intuition, and are compatible with an objective viewpoint on mathematics.
, which is essentially classical logic
without the law of the excluded middle. This is not to say that the law of the excluded middle is denied entirely; special cases of the law will be provable. It is just that the general law is not assumed as an axiom
. (The law of non-contradiction, on the other hand, is still valid.)
For instance, in Heyting arithmetic
, one can prove that for any proposition p which does not contain quantifiers,
is a theorem (where x, y, z ... are the free variables in the proposition p). In this sense, propositions restricted to the finite are still regarded as being either true or false, as they are in classical mathematics, but this bivalence does not extend to propositions which refer to infinite collections.
In fact, L.E.J. Brouwer, founder of the intuitionist school, viewed the law of the excluded middle as abstracted from finite experience, and then applied to the infinite without justification
. For instance, Goldbach's conjecture
is the assertion that every even number (greater than 2) is the sum of two prime number
s. It is possible to test for any particular even number whether or not it is the sum of two primes (for instance by exhaustive search), so any one of them is either the sum of two primes or it is not. And so far, every one thus tested has in fact been the sum of two primes.
But there is no known proof that all of them are so, nor any known proof that not all of them are so. Thus to Brouwer, we are not justified in asserting "either Goldbach's conjecture is true, or it is not." And while the conjecture may one day be solved, the argument applies to similar unsolved problems; to Brouwer, the law of the excluded middle was tantamount to assuming that every mathematical problem has a solution.
With the omission of the law of the excluded middle as an axiom, the remaining logical system has an existence property which classical logic does not: whenever
is proven constructively, then in fact 
is proven constructively for (at least) one particular 
, often called a witness. Thus the proof of the existence of a mathematical object is tied to the possibility of its construction
.
, one way to define a real number is as an equivalence class of Cauchy sequence
s of rational number
s.
In constructive mathematics, one way to construct a real number is as a function
ƒ that takes a positive integer
and outputs a rational ƒ(n), together with a function g that takes a positive integer n and outputs a positive integer g(n) such that
so that as n increases, the values of ƒ(n) get closer and closer together. We can use ƒ and g together to compute as close a rational approximation as we like to the real number they represent.
Under this definition, a simple representation of the real number e is:
This definition corresponds to the classical definition using Cauchy sequences, except with a constructive twist: for a classical Cauchy sequence, it is required that, for any given distance, there exists (in a classical sense)
a member in the sequence after which all members are closer together than that distance. In the constructive version, it is required that, for any given distance, it is possible to actually specify a point in the sequence where this happens (this required specification is often called the modulus of convergence
). In fact, the standard constructive interpretation
of the mathematical statement
is precisely the existence of the function computing the modulus of convergence. Thus the difference between the two definitions of real numbers can be thought of as the difference in the interpretation of the statement "for all... there exists..."
This then opens the question as to what sort of function
from a countable set to a countable set, such as f and g above, can actually be constructed. Different versions of constructivism diverge on this point. Constructions can be defined as broadly as free choice sequences, which is the intuitionistic view, or as narrowly as algorithms (or more technically, the computable function
s), or even left unspecified. If, for instance, the algorithmic view is taken, then the reals as constructed here are essentially what classically would be called the computable number
s.
. By enumerating algorithms, we can show classically that the computable numbers are countable. And yet Cantor's diagonal argument
shows that real numbers have higher cardinality. Furthermore the diagonal argument seems perfectly constructive. To identify the real numbers with the computable numbers would then be a contradiction.
And in fact, Cantor's diagonal argument is constructive, in the sense that given a bijection
between the real numbers and natural numbers, one constructs a real number which doesn't fit, and thereby proves a contradiction. We can indeed enumerate algorithms to construct a function T, about which we initially assume that it is a function from the natural numbers onto the reals. But, to each algorithm, there may or may not correspond a real number, as the algorithm may fail to satisfy the constraints, or even be non-terminating (T is a partial function
), so this fails to produce the required bijection. In short, one who takes the view that real numbers are effectively computable interprets Cantor's result as showing that the real numbers are not recursively enumerable.
Still, one might expect that since T is a partial function from the natural numbers onto the real numbers, that therefore the real numbers are no more than countable. And, since every natural number can be trivially
represented as a real number, therefore the real numbers are no less than countable. They are, therefore exactly countable. However this reasoning is not constructive, as it still does not construct the required bijection. In fact the cardinality of sets fails to be totally ordered
(see Cantor–Bernstein–Schroeder theorem
).
In intuitionistic theories of type theory
(especially higher-type arithmetic), many forms of the axiom of choice are permitted. For example, the axiom AC11 can be paraphrased to say that for any relation R on the set of real numbers, if you have proved that for each real number x there is a real number y such that R(x,y) holds, then there is actually a function F such that R(x,F(x)) holds for all real numbers. Similar choice principles are accepted for all finite types. The motivation for accepting these seemingly nonconstructive principles is the intuitionistic understanding of the proof that "for each real number x there is a real number y such that R(x,y) holds". According to the BHK interpretation
, this proof itself is essentially the function F that is desired. The choice principles that intuitionists accept do not imply the law of the excluded middle.
However, in certain axiom systems for constructive set theory, the axiom of choice does imply the law of the excluded middle (in the presence of other axioms), as shown by the Diaconescu-Goodman-Myhill theorem. Some constructive set theories include weaker forms of the axiom of choice, such as the axiom of dependent choice
in Myhill's set theory.
s, the existence of the latter being behind such famous results as the Banach–Tarski paradox
, and secondly the hierarchies of notions of measure captured by notions such as Borel algebra
s, which are an important source of intuitions in set theory
. Measure theory provides the foundation for the modern notion of integral
, the Lebesgue integral.
It is possible to rework measure theory on the basis of the computable real line, where the set-theoretic basis for measurability is replaced by notions from order theory
. This constructive measure theory provides the basis for computable analogues for Lebesgue integration.
These views were forcefully expressed by David Hilbert
in 1928, when he wrote in Die Grundlagen der Mathematik, "Taking the principle of excluded middle from the mathematician would be the same, say, as proscribing the telescope to the astronomer or to the boxer the use of his fists".
Errett Bishop
, in his 1967 work Foundations of Constructive Analysis, worked to dispel these fears by developing a great deal of traditional analysis in a constructive framework. Nevertheless, some mathematicians do not accept that Bishop did so successfully, since his book is necessarily more complicated than a classical analysis text would be.
Even though most mathematicians do not accept the constructivist's thesis, that only mathematics done based on constructive methods is sound, constructive methods are increasingly of interest on non-ideological grounds. For example, constructive proofs in analysis may ensure witness extraction, in such a way that working within the constraints of the constructive methods may make finding witnesses to theories easier than using classical methods. Applications for constructive mathematics have also been found in typed lambda calculi
, topos theory
and categorical logic
, which are notable subjects in foundational mathematics and computer science
. In algebra, for such entities as topos
es and Hopf algebra
s, the structure supports an internal language that is a constructive theory; working within the constraints of that language is often more intuitive and flexible than working externally by such means as reasoning about the set of possible concrete algebras and their homomorphism
s.
Physicist Lee Smolin
writes in Three Roads to Quantum Gravity
that topos theory is "the right form of logic for cosmology" (page 30) and "In its first forms it was called 'intuitionistic logic'" (page 31). "In this kind of logic, the statements an observer can make about the universe are divided into at least three groups: those that we can judge to be true, those that we can judge to be false and those whose truth we cannot decide upon at the present time" (page 28).
Philosophy of mathematics
The philosophy of mathematics is the branch of philosophy that studies the philosophical assumptions, foundations, and implications of mathematics. The aim of the philosophy of mathematics is to provide an account of the nature and methodology of mathematics and to understand the place of...
, constructivism asserts that it is necessary to find (or "construct") a mathematical object to prove that it exists. When one assumes that an object does not exist and derives a contradiction from that assumption
Reductio ad absurdum
In logic, proof by contradiction is a form of proof that establishes the truth or validity of a proposition by showing that the proposition's being false would imply a contradiction...
, one still has not found the object and therefore not proved its existence, according to constructivists. This viewpoint involves a verificational interpretation of the existence quantifier, which is at odds with its classical interpretation.
There are many forms of constructivism. These include the program of intuitionism
Intuitionism
In the philosophy of mathematics, intuitionism, or neointuitionism , is an approach to mathematics as the constructive mental activity of humans. That is, mathematics does not consist of analytic activities wherein deep properties of existence are revealed and applied...
founded by Brouwer
Luitzen Egbertus Jan Brouwer
Luitzen Egbertus Jan Brouwer FRS , usually cited as L. E. J. Brouwer but known to his friends as Bertus, was a Dutch mathematician and philosopher, a graduate of the University of Amsterdam, who worked in topology, set theory, measure theory and complex analysis.-Biography:Early in his career,...
, the finitism
Finitism
In the philosophy of mathematics, one of the varieties of finitism is an extreme form of constructivism, according to which a mathematical object does not exist unless it can be constructed from natural numbers in a finite number of steps...
of Hilbert
David Hilbert
David Hilbert was a German mathematician. He is recognized as one of the most influential and universal mathematicians of the 19th and early 20th centuries. Hilbert discovered and developed a broad range of fundamental ideas in many areas, including invariant theory and the axiomatization of...
and Bernays
Paul Bernays
Paul Isaac Bernays was a Swiss mathematician, who made significant contributions to mathematical logic, axiomatic set theory, and the philosophy of mathematics. He was an assistant to, and close collaborator of, David Hilbert.-Biography:Bernays spent his childhood in Berlin. Bernays attended the...
, the constructive recursive mathematics of Shanin and Markov
Andrey Markov (Soviet mathematician)
Andrey Andreyevich Markov Jr. was a Soviet mathematician, the son of the great Russian mathematician Andrey Andreyevich Markov Sr, and one of the key founders of the Russian school of constructive mathematics and logic...
, and Bishop
Errett Bishop
Errett Albert Bishop was an American mathematician known for his work on analysis. He is the father of constructive analysis, because of his 1967 Foundations of Constructive Analysis, where he proved most of the important theorems in real analysis by constructive methods.-Life:Errett Bishop's...
's program of constructive analysis. Constructivism also includes the study of constructive set theories
Constructive set theory
Constructive set theory is an approach to mathematical constructivism following the program of axiomatic set theory. That is, it uses the usual first-order language of classical set theory, and although of course the logic is constructive, there is no explicit use of constructive types...
such as IZF and the study of topos theory.
Constructivism is often identified with intuitionism, although intuitionism is only one constructivist program. Intuitionism maintains that the foundations of mathematics lie in the individual mathematician's intuition, thereby making mathematics into an intrinsically subjective activity. Other forms of constructivism are not based on this viewpoint of intuition, and are compatible with an objective viewpoint on mathematics.
Constructive mathematics
Much constructive mathematics uses intuitionistic logicIntuitionistic logic
Intuitionistic logic, or constructive logic, is a symbolic logic system differing from classical logic in its definition of the meaning of a statement being true. In classical logic, all well-formed statements are assumed to be either true or false, even if we do not have a proof of either...
, which is essentially classical logic
Classical logic
Classical logic identifies a class of formal logics that have been most intensively studied and most widely used. The class is sometimes called standard logic as well...
without the law of the excluded middle. This is not to say that the law of the excluded middle is denied entirely; special cases of the law will be provable. It is just that the general law is not assumed as an axiom
Axiom
In traditional logic, an axiom or postulate is a proposition that is not proven or demonstrated but considered either to be self-evident or to define and delimit the realm of analysis. In other words, an axiom is a logical statement that is assumed to be true...
. (The law of non-contradiction, on the other hand, is still valid.)
For instance, in Heyting arithmetic
Heyting arithmetic
In mathematical logic, Heyting arithmetic is an axiomatization of arithmetic in accordance with the philosophy of intuitionism. It is named after Arend Heyting, who first proposed it....
, one can prove that for any proposition p which does not contain quantifiers,
is a theorem (where x, y, z ... are the free variables in the proposition p). In this sense, propositions restricted to the finite are still regarded as being either true or false, as they are in classical mathematics, but this bivalence does not extend to propositions which refer to infinite collections.In fact, L.E.J. Brouwer, founder of the intuitionist school, viewed the law of the excluded middle as abstracted from finite experience, and then applied to the infinite without justification
Theory of justification
Theory of justification is a part of epistemology that attempts to understand the justification of propositions and beliefs. Epistemologists are concerned with various epistemic features of belief, which include the ideas of justification, warrant, rationality, and probability...
. For instance, Goldbach's conjecture
Goldbach's conjecture
Goldbach's conjecture is one of the oldest unsolved problems in number theory and in all of mathematics. It states:A Goldbach number is a number that can be expressed as the sum of two odd primes...
is the assertion that every even number (greater than 2) is the sum of two prime number
Prime number
A prime number is a natural number greater than 1 that has no positive divisors other than 1 and itself. A natural number greater than 1 that is not a prime number is called a composite number. For example 5 is prime, as only 1 and 5 divide it, whereas 6 is composite, since it has the divisors 2...
s. It is possible to test for any particular even number whether or not it is the sum of two primes (for instance by exhaustive search), so any one of them is either the sum of two primes or it is not. And so far, every one thus tested has in fact been the sum of two primes.
But there is no known proof that all of them are so, nor any known proof that not all of them are so. Thus to Brouwer, we are not justified in asserting "either Goldbach's conjecture is true, or it is not." And while the conjecture may one day be solved, the argument applies to similar unsolved problems; to Brouwer, the law of the excluded middle was tantamount to assuming that every mathematical problem has a solution.
With the omission of the law of the excluded middle as an axiom, the remaining logical system has an existence property which classical logic does not: whenever
is proven constructively, then in fact is proven constructively for (at least) one particular , often called a witness. Thus the proof of the existence of a mathematical object is tied to the possibility of its constructionConstruction
In the fields of architecture and civil engineering, construction is a process that consists of the building or assembling of infrastructure. Far from being a single activity, large scale construction is a feat of human multitasking...
.
Example from real analysis
In classical real analysisReal analysis
Real analysis, is a branch of mathematical analysis dealing with the set of real numbers and functions of a real variable. In particular, it deals with the analytic properties of real functions and sequences, including convergence and limits of sequences of real numbers, the calculus of the real...
, one way to define a real number is as an equivalence class of Cauchy sequence
Cauchy sequence
In mathematics, a Cauchy sequence , named after Augustin-Louis Cauchy, is a sequence whose elements become arbitrarily close to each other as the sequence progresses...
s of rational number
Rational number
In mathematics, a rational number is any number that can be expressed as the quotient or fraction a/b of two integers, with the denominator b not equal to zero. Since b may be equal to 1, every integer is a rational number...
s.
In constructive mathematics, one way to construct a real number is as a function
Function (mathematics)
In mathematics, a function associates one quantity, the argument of the function, also known as the input, with another quantity, the value of the function, also known as the output. A function assigns exactly one output to each input. The argument and the value may be real numbers, but they can...
ƒ that takes a positive integer
and outputs a rational ƒ(n), together with a function g that takes a positive integer n and outputs a positive integer g(n) such thatso that as n increases, the values of ƒ(n) get closer and closer together. We can use ƒ and g together to compute as close a rational approximation as we like to the real number they represent.
Under this definition, a simple representation of the real number e is:
This definition corresponds to the classical definition using Cauchy sequences, except with a constructive twist: for a classical Cauchy sequence, it is required that, for any given distance, there exists (in a classical sense)
Existence theorem
In mathematics, an existence theorem is a theorem with a statement beginning 'there exist ..', or more generally 'for all x, y, ... there exist ...'. That is, in more formal terms of symbolic logic, it is a theorem with a statement involving the existential quantifier. Many such theorems will not...
a member in the sequence after which all members are closer together than that distance. In the constructive version, it is required that, for any given distance, it is possible to actually specify a point in the sequence where this happens (this required specification is often called the modulus of convergence
Modulus of convergence
In real analysis, a branch of mathematics, a modulus of convergence is a function that tells how quickly a convergent sequence converges. These moduli are often employed in the study of computable analysis and constructive mathematics....
). In fact, the standard constructive interpretation
BHK interpretation
In mathematical logic, the Brouwer–Heyting–Kolmogorov interpretation, or BHK interpretation, of intuitionistic logic was proposed by L. E. J. Brouwer, Arend Heyting and independently by Andrey Kolmogorov...
of the mathematical statement
is precisely the existence of the function computing the modulus of convergence. Thus the difference between the two definitions of real numbers can be thought of as the difference in the interpretation of the statement "for all... there exists..."
This then opens the question as to what sort of function
Function (mathematics)
In mathematics, a function associates one quantity, the argument of the function, also known as the input, with another quantity, the value of the function, also known as the output. A function assigns exactly one output to each input. The argument and the value may be real numbers, but they can...
from a countable set to a countable set, such as f and g above, can actually be constructed. Different versions of constructivism diverge on this point. Constructions can be defined as broadly as free choice sequences, which is the intuitionistic view, or as narrowly as algorithms (or more technically, the computable function
Computable function
Computable functions are the basic objects of study in computability theory. Computable functions are the formalized analogue of the intuitive notion of algorithm. They are used to discuss computability without referring to any concrete model of computation such as Turing machines or register...
s), or even left unspecified. If, for instance, the algorithmic view is taken, then the reals as constructed here are essentially what classically would be called the computable number
Computable number
In mathematics, particularly theoretical computer science and mathematical logic, the computable numbers, also known as the recursive numbers or the computable reals, are the real numbers that can be computed to within any desired precision by a finite, terminating algorithm...
s.
Cardinality
To take the algorithmic interpretation above would seem at odds with classical notions of cardinalityCardinal number
In mathematics, cardinal numbers, or cardinals for short, are a generalization of the natural numbers used to measure the cardinality of sets. The cardinality of a finite set is a natural number – the number of elements in the set. The transfinite cardinal numbers describe the sizes of infinite...
. By enumerating algorithms, we can show classically that the computable numbers are countable. And yet Cantor's diagonal argument
Cantor's diagonal argument
Cantor's diagonal argument, also called the diagonalisation argument, the diagonal slash argument or the diagonal method, was published in 1891 by Georg Cantor as a mathematical proof that there are infinite sets which cannot be put into one-to-one correspondence with the infinite set of natural...
shows that real numbers have higher cardinality. Furthermore the diagonal argument seems perfectly constructive. To identify the real numbers with the computable numbers would then be a contradiction.
And in fact, Cantor's diagonal argument is constructive, in the sense that given a bijection
Bijection
A bijection is a function giving an exact pairing of the elements of two sets. A bijection from the set X to the set Y has an inverse function from Y to X. If X and Y are finite sets, then the existence of a bijection means they have the same number of elements...
between the real numbers and natural numbers, one constructs a real number which doesn't fit, and thereby proves a contradiction. We can indeed enumerate algorithms to construct a function T, about which we initially assume that it is a function from the natural numbers onto the reals. But, to each algorithm, there may or may not correspond a real number, as the algorithm may fail to satisfy the constraints, or even be non-terminating (T is a partial function
Partial function
In mathematics, a partial function from X to Y is a function ƒ: X' → Y, where X' is a subset of X. It generalizes the concept of a function by not forcing f to map every element of X to an element of Y . If X' = X, then ƒ is called a total function and is equivalent to a function...
), so this fails to produce the required bijection. In short, one who takes the view that real numbers are effectively computable interprets Cantor's result as showing that the real numbers are not recursively enumerable.
Still, one might expect that since T is a partial function from the natural numbers onto the real numbers, that therefore the real numbers are no more than countable. And, since every natural number can be trivially
Trivial (mathematics)
In mathematics, the adjective trivial is frequently used for objects that have a very simple structure...
represented as a real number, therefore the real numbers are no less than countable. They are, therefore exactly countable. However this reasoning is not constructive, as it still does not construct the required bijection. In fact the cardinality of sets fails to be totally ordered
Total order
In set theory, a total order, linear order, simple order, or ordering is a binary relation on some set X. The relation is transitive, antisymmetric, and total...
(see Cantor–Bernstein–Schroeder theorem
Cantor–Bernstein–Schroeder theorem
In set theory, the Cantor–Bernstein–Schroeder theorem, named after Georg Cantor, Felix Bernstein, and Ernst Schröder, states that, if there exist injective functions and between the sets A and B, then there exists a bijective function...
).
Axiom of choice
The status of the axiom of choice in constructive mathematics is complicated by the different approaches of different constructivist programs. One trivial meaning of "constructive", used informally by mathematicians, is "provable in ZF set theory without the axiom of choice." However, proponents of more limited forms of constructive mathematics would not assert that ZF itself is a constructive system.In intuitionistic theories of type theory
Type theory
In mathematics, logic and computer science, type theory is any of several formal systems that can serve as alternatives to naive set theory, or the study of such formalisms in general...
(especially higher-type arithmetic), many forms of the axiom of choice are permitted. For example, the axiom AC11 can be paraphrased to say that for any relation R on the set of real numbers, if you have proved that for each real number x there is a real number y such that R(x,y) holds, then there is actually a function F such that R(x,F(x)) holds for all real numbers. Similar choice principles are accepted for all finite types. The motivation for accepting these seemingly nonconstructive principles is the intuitionistic understanding of the proof that "for each real number x there is a real number y such that R(x,y) holds". According to the BHK interpretation
BHK interpretation
In mathematical logic, the Brouwer–Heyting–Kolmogorov interpretation, or BHK interpretation, of intuitionistic logic was proposed by L. E. J. Brouwer, Arend Heyting and independently by Andrey Kolmogorov...
, this proof itself is essentially the function F that is desired. The choice principles that intuitionists accept do not imply the law of the excluded middle.
However, in certain axiom systems for constructive set theory, the axiom of choice does imply the law of the excluded middle (in the presence of other axioms), as shown by the Diaconescu-Goodman-Myhill theorem. Some constructive set theories include weaker forms of the axiom of choice, such as the axiom of dependent choice
Axiom of dependent choice
In mathematics, the axiom of dependent choices, denoted DC, is a weak form of the axiom of choice which is still sufficient to develop most of real analysis...
in Myhill's set theory.
Measure theory
Classical measure theory makes deep usage of the axiom of choice, which is fundamental to, first, distinction between measurable and non-measurable setNon-measurable set
In mathematics, a non-measurable set is a set whose structure is so complicated that it cannot be assigned any meaningful measure. Such sets are constructed to shed light on the notions of length, area and volume in formal set theory....
s, the existence of the latter being behind such famous results as the Banach–Tarski paradox
Banach–Tarski paradox
The Banach–Tarski paradox is a theorem in set theoretic geometry which states the following: Given a solid ball in 3-dimensional space, there exists a decomposition of the ball into a finite number of non-overlapping pieces , which can then be put back together in a different way to yield two...
, and secondly the hierarchies of notions of measure captured by notions such as Borel algebra
Borel algebra
In mathematics, a Borel set is any set in a topological space that can be formed from open sets through the operations of countable union, countable intersection, and relative complement...
s, which are an important source of intuitions in set theory
Set theory
Set theory is the branch of mathematics that studies sets, which are collections of objects. Although any type of object can be collected into a set, set theory is applied most often to objects that are relevant to mathematics...
. Measure theory provides the foundation for the modern notion of integral
Integral
Integration is an important concept in mathematics and, together with its inverse, differentiation, is one of the two main operations in calculus...
, the Lebesgue integral.
It is possible to rework measure theory on the basis of the computable real line, where the set-theoretic basis for measurability is replaced by notions from order theory
Order theory
Order theory is a branch of mathematics which investigates our intuitive notion of order using binary relations. It provides a formal framework for describing statements such as "this is less than that" or "this precedes that". This article introduces the field and gives some basic definitions...
. This constructive measure theory provides the basis for computable analogues for Lebesgue integration.
The place of constructivism in mathematics
Traditionally, some mathematicians have been suspicious, if not antagonistic, towards mathematical constructivism, largely because of limitations they believed it to pose for constructive analysis.These views were forcefully expressed by David Hilbert
David Hilbert
David Hilbert was a German mathematician. He is recognized as one of the most influential and universal mathematicians of the 19th and early 20th centuries. Hilbert discovered and developed a broad range of fundamental ideas in many areas, including invariant theory and the axiomatization of...
in 1928, when he wrote in Die Grundlagen der Mathematik, "Taking the principle of excluded middle from the mathematician would be the same, say, as proscribing the telescope to the astronomer or to the boxer the use of his fists".
Errett Bishop
Errett Bishop
Errett Albert Bishop was an American mathematician known for his work on analysis. He is the father of constructive analysis, because of his 1967 Foundations of Constructive Analysis, where he proved most of the important theorems in real analysis by constructive methods.-Life:Errett Bishop's...
, in his 1967 work Foundations of Constructive Analysis, worked to dispel these fears by developing a great deal of traditional analysis in a constructive framework. Nevertheless, some mathematicians do not accept that Bishop did so successfully, since his book is necessarily more complicated than a classical analysis text would be.
Even though most mathematicians do not accept the constructivist's thesis, that only mathematics done based on constructive methods is sound, constructive methods are increasingly of interest on non-ideological grounds. For example, constructive proofs in analysis may ensure witness extraction, in such a way that working within the constraints of the constructive methods may make finding witnesses to theories easier than using classical methods. Applications for constructive mathematics have also been found in typed lambda calculi
Typed lambda calculus
A typed lambda calculus is a typed formalism that uses the lambda-symbol to denote anonymous function abstraction. In this context, types are usually objects of a syntactic nature that are assigned to lambda terms; the exact nature of a type depends on the calculus considered...
, topos theory
Background and genesis of topos theory
This page gives some very general background to the mathematical idea of topos. This is an aspect of category theory, and has a reputation for being abstruse. The level of abstraction involved cannot be reduced beyond a certain point; but on the other hand context can be given...
and categorical logic
Categorical logic
Categorical logic is a branch of category theory within mathematics, adjacent to mathematical logic but more notable for its connections to theoretical computer science. In broad terms, categorical logic represents both syntax and semantics by a category, and an interpretation by a functor...
, which are notable subjects in foundational mathematics and computer science
Computer science
Computer science or computing science is the study of the theoretical foundations of information and computation and of practical techniques for their implementation and application in computer systems...
. In algebra, for such entities as topos
Topos
In mathematics, a topos is a type of category that behaves like the category of sheaves of sets on a topological space...
es and Hopf algebra
Hopf algebra
In mathematics, a Hopf algebra, named after Heinz Hopf, is a structure that is simultaneously an algebra and a coalgebra, with these structures' compatibility making it a bialgebra, and that moreover is equipped with an antiautomorphism satisfying a certain property.Hopf algebras occur naturally...
s, the structure supports an internal language that is a constructive theory; working within the constraints of that language is often more intuitive and flexible than working externally by such means as reasoning about the set of possible concrete algebras and their homomorphism
Homomorphism
In abstract algebra, a homomorphism is a structure-preserving map between two algebraic structures . The word homomorphism comes from the Greek language: ὁμός meaning "same" and μορφή meaning "shape".- Definition :The definition of homomorphism depends on the type of algebraic structure under...
s.
Physicist Lee Smolin
Lee Smolin
Lee Smolin is an American theoretical physicist, a researcher at the Perimeter Institute for Theoretical Physics, and an adjunct professor of physics at the University of Waterloo. He is married to Dina Graser, a communications lawyer in Toronto. His brother is David M...
writes in Three Roads to Quantum Gravity
Three Roads to Quantum Gravity
Three Roads to Quantum Gravity is a 2001 book by theoretical physicist Lee Smolin. He discusses three potential approaches by which a unified theory of quantum gravity, arguably the foremost issue in theoretical physics, may be realized. Approaches discussed include string theory, M-theory, and...
that topos theory is "the right form of logic for cosmology" (page 30) and "In its first forms it was called 'intuitionistic logic'" (page 31). "In this kind of logic, the statements an observer can make about the universe are divided into at least three groups: those that we can judge to be true, those that we can judge to be false and those whose truth we cannot decide upon at the present time" (page 28).
Mathematicians who have contributed to constructivism
- Errett BishopErrett BishopErrett Albert Bishop was an American mathematician known for his work on analysis. He is the father of constructive analysis, because of his 1967 Foundations of Constructive Analysis, where he proved most of the important theorems in real analysis by constructive methods.-Life:Errett Bishop's...
(constructive analysis) - Paul LorenzenPaul LorenzenPaul Lorenzen was a philosopher andmathematician.As a founder of the Erlangen School and the inventor of game semantics he was a famous German philosopher of the 20th century.-Biography:Lorenzen studied with David Hilbert as a schoolboy and he was one of Hasse's...
(constructive logic, analysis and metamathematics) - A. A. MarkovAndrey Markov (Soviet mathematician)Andrey Andreyevich Markov Jr. was a Soviet mathematician, the son of the great Russian mathematician Andrey Andreyevich Markov Sr, and one of the key founders of the Russian school of constructive mathematics and logic...
(constructive mathematics and logic) - Leopold KroneckerLeopold KroneckerLeopold Kronecker was a German mathematician who worked on number theory and algebra.He criticized Cantor's work on set theory, and was quoted by as having said, "God made integers; all else is the work of man"...
(old constructivism) - L. E. J. BrouwerLuitzen Egbertus Jan BrouwerLuitzen Egbertus Jan Brouwer FRS , usually cited as L. E. J. Brouwer but known to his friends as Bertus, was a Dutch mathematician and philosopher, a graduate of the University of Amsterdam, who worked in topology, set theory, measure theory and complex analysis.-Biography:Early in his career,...
(intuitionism) - Arend HeytingArend HeytingArend Heyting was a Dutch mathematician and logician. He was a student of Luitzen Egbertus Jan Brouwer at the University of Amsterdam, and did much to put intuitionistic logic on a footing where it could become part of mathematical logic...
(intuitionistic logic) - Saul KripkeSaul KripkeSaul Aaron Kripke is an American philosopher and logician. He is a professor emeritus at Princeton and teaches as a Distinguished Professor of Philosophy at the CUNY Graduate Center...
(intuitionistic logic) - Per Martin-LöfPer Martin-LöfPer Erik Rutger Martin-Löf is a Swedish logician, philosopher, and mathematical statistician. He is internationally renowned for his work on the foundations of probability, statistics, mathematical logic, and computer science. Since the late 1970s, Martin-Löf's publications have been mainly in...
(constructive type theory, a foundation for Bishop's analysis) - Edward NelsonEdward NelsonEdward Nelson is a professor in the Mathematics Department at Princeton University. He is known for his work on mathematical physics and mathematical logic...
(predicative arithmetic) - Harold EdwardsHarold Edwards (mathematician)Harold Mortimer Edwards, Jr. is an American mathematician working in number theory, algebra, and the history and philosophy of mathematics....
(completed Kronecker's work on divisor theory, published a book of essays on constructivist mathematics) - G. F. C. GrissGeorge F C GrissGeorge François Cornelis Griss , usually cited as G. F. C. Griss, was a Dutch mathematician and philosopher, who was occupied with hegelian idealism and Brouwers intuitionism and stated a negationless mathematics....
(negationless intuitionistic mathematics)
Branches
- Constructive logic
- Constructive type theory
- Constructive analysis
- Constructive non-standard analysisConstructive non-standard analysisIn mathematics, constructive nonstandard analysis is a version of Abraham Robinson's non-standard analysis, developed by Moerdijk , Palmgren , Ruokolainen . Ruokolainen wrote:-References:...
See also
- IntuitionismIntuitionismIn the philosophy of mathematics, intuitionism, or neointuitionism , is an approach to mathematics as the constructive mental activity of humans. That is, mathematics does not consist of analytic activities wherein deep properties of existence are revealed and applied...
- Intuitionistic type theoryIntuitionistic type theoryIntuitionistic type theory, or constructive type theory, or Martin-Löf type theory or just Type Theory is a logical system and a set theory based on the principles of mathematical constructivism. Intuitionistic type theory was introduced by Per Martin-Löf, a Swedish mathematician and philosopher,...
- FinitismFinitismIn the philosophy of mathematics, one of the varieties of finitism is an extreme form of constructivism, according to which a mathematical object does not exist unless it can be constructed from natural numbers in a finite number of steps...
- Game semanticsGame semanticsGame semantics is an approach to formal semantics that grounds the concepts of truth or validity on game-theoretic concepts, such as the existence of a winning strategy for a player, somewhat resembling Socratic dialogues or medieval theory of Obligationes. In the late 1950s Paul Lorenzen was the...
- Constructive proofConstructive proofIn mathematics, a constructive proof is a method of proof that demonstrates the existence of a mathematical object with certain properties by creating or providing a method for creating such an object...