In thephilosophy of mathematics,constructivism asserts that it is necessary to find (or "construct") a specific example of a mathematical object in order to prove that an example exists. Contrastingly, in classical mathematics, one can prove theexistence of a mathematical object without "finding" that object explicitly, by assuming its non-existence and then deriving acontradiction from that assumption. Such aproof by contradiction might be called non-constructive, and a constructivist might reject it. The constructive viewpoint involves a verificational interpretation of theexistential quantifier, which is at odds with its classical interpretation.
There are many forms of constructivism.[1] These include the program ofintuitionism founded byBrouwer, thefinitism ofHilbert andBernays, the constructive recursive mathematics ofShanin andMarkov, andBishop's program ofconstructive analysis.[2] Constructivism also includes the study ofconstructive set theories such asCZF and the study oftopos 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.[3] Other forms of constructivism are not based on this viewpoint of intuition, and are compatible with an objective viewpoint on mathematics.
Much constructive mathematics usesintuitionistic logic, which is essentiallyclassical logic without thelaw of the excluded middle. This law states that, for any proposition, either that proposition is true or its negation is. 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 anaxiom. Thelaw of non-contradiction (which states that contradictory statements cannot both be true at the same time) is still valid.
For instance, inHeyting arithmetic, one can prove that for any propositionp thatdoes not containquantifiers, is a theorem (wherex,y,z ... are thefree variables in the propositionp). In this sense, propositions restricted to thefinite are still regarded as being either true or false, as they are in classical mathematics, but thisbivalence does not extend to propositions that refer toinfinite 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 withoutjustification. For instance,Goldbach's conjecture is the assertion that every even number greater than 2 is the sum of twoprime numbers. It is possible to test for any particular even number whether 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; nor is it even known whethereither a proofor a disproof of Goldbach's conjecture must exist (the conjecture may beundecidable in traditional ZF set theory). 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 is tantamount to assuming thatevery mathematical problem has a solution.
With the omission of the law of the excluded middle as an axiom, the remaininglogical system has anexistence property that classical logic does not have: whenever is proven constructively, then in fact is proven constructively for (at least) one particular, often called awitness. Thus the proof of the existence of a mathematical object is tied to the possibility of its construction.
In classicalreal analysis, one way todefine a real number is as anequivalence class ofCauchy sequences ofrational numbers.
In constructive mathematics, one way to construct a real number is as afunctionƒ that takes a positive integer and outputs a rationalƒ(n), together with a functiong that takes a positive integern and outputs a positive integerg(n) such that
so that asn increases, the values ofƒ(n) get closer and closer together. We can useƒ andg 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 numbere 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 themodulus of convergence). In fact, thestandard 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 offunction from acountableset to a countable set, such asf andg above, can actually be constructed. Different versions of constructivism diverge on this point. Constructions can be defined as broadly asfree choice sequences, which is the intuitionistic view, or as narrowly as algorithms (or more technically, thecomputable functions), 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 thecomputable numbers.
To take the algorithmic interpretation above would seem at odds with classical notions ofcardinality. By enumerating algorithms, we can show that thecomputable numbers are classically countable. And yetCantor's diagonal argument here shows that real numbers have uncountable cardinality. To identify the real numbers with the computable numbers would then be a contradiction. Furthermore, the diagonal argument seems perfectly constructive.
Indeed Cantor's diagonal argument can be presented constructively, in the sense that given abijection between the natural numbers and real numbers, one constructs a real number not in the functions range, and thereby establishes a contradiction. One can enumerate algorithms to construct a functionT, about which we initially assume that it is a function from the natural numbersonto 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 apartial function), so this fails to produce the required bijection. In short, one who takes the view that real numbers are (individually) effectively computable interprets Cantor's result as showing that the real numbers (collectively) are notrecursively enumerable.
Still, one might expect that sinceT is a partial function from the natural numbers onto the real numbers, that therefore the real numbers areno more than countable. And, since every natural number can betrivially represented as a real number, therefore the real numbers areno less than countable. They are, thereforeexactly countable. However this reasoning is not constructive, as it still does not construct the required bijection. The classical theorem proving the existence of a bijection in such circumstances, namely theCantor–Bernstein–Schroeder theorem, is non-constructive. It has recently been shown that theCantor–Bernstein–Schroeder theorem implies thelaw of the excluded middle, hence there can be no constructive proof of the theorem.[4]
The status of theaxiom 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 inZF set theory without the axiom of choice." However, proponents of more limited forms of constructive mathematics would assert that ZF itself is not a constructive system.
In intuitionistic theories oftype 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 relationR on the set of real numbers, if you have proved that for each real numberx there is a real numbery such thatR(x,y) holds, then there is actually a functionF such thatR(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 numberx there is a real numbery such thatR(x,y) holds". According to theBHK interpretation, this proof itself is essentially the functionF that is desired. The choice principles that intuitionists accept do not imply thelaw 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 theDiaconescu-Goodman-Myhill theorem. Some constructive set theories include weaker forms of the axiom of choice, such as theaxiom of dependent choice in Myhill's set theory.
Classicalmeasure theory is fundamentally non-constructive, since the classical definition ofLebesgue measure does not describe any way how to compute the measure of a set or the integral of a function. In fact, if one thinks of a function just as a rule that "inputs a real number and outputs a real number" then there cannot be any algorithm to compute the integral of a function, since any algorithm would only be able to call finitely many values of the function at a time, and finitely many values are not enough to compute the integral to any nontrivial accuracy. The solution to this conundrum, carried out first inBishop (1967), is to consider only functions that are written as the pointwise limit of continuous functions (with known modulus of continuity), with information about the rate of convergence. An advantage of constructivizing measure theory is that if one can prove that a set is constructively of full measure, then there is an algorithm for finding a point in that set (again seeBishop (1967)).
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 byDavid Hilbert in 1928, when he wrote inGrundlagen 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".[5]
Errett Bishop, in his 1967 workFoundations of Constructive Analysis,[2] worked to dispel these fears by developing a great deal of traditional analysis in a constructive framework.
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.[citation needed] 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.[citation needed] Applications for constructive mathematics have also been found intyped lambda calculi,topos theory andcategorical logic, which are notable subjects in foundational mathematics andcomputer science. In algebra, for such entities astopoi andHopf algebras, the structure supports aninternal 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 theirhomomorphisms.[citation needed]
PhysicistLee Smolin writes inThree 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).
{{cite book}}: CS1 maint: publisher location (link){{cite book}}: CS1 maint: bot: original URL status unknown (link)| International | |
|---|---|
| National | |
| Other | |
