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.
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 Markov, and Bishop's program of constructive analysis. Constructivism also includes the study of constructive set theories such as IZF.
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.
Much constructive mathematics uses intuitionistic logic, 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.
Full article ▸