Constructivism (philosophy of mathematics)
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.
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 CZF 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 logic, which is essentially classical logic without the law 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 an axiom. The law of non-contradiction is still valid.For instance, in Heyting arithmetic, one can prove that for any proposition p that does not contain quantifiers, is a theorem. 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 that 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 numbers. It is possible to test for any particular even number whether it is the sum of two primes, 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 whether either a proof or a disproof of Goldbach's conjecture must exist. 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 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 that classical logic does not have: whenever is proven constructively, then in fact is proven constructively for one particular, often called a witness. Thus the proof of the existence of a mathematical object is tied to the possibility of its construction.
Example from real analysis
In classical real analysis, one way to define a real number is as an equivalence class of Cauchy sequences of rational numbers.In constructive mathematics, one way to construct a real number is as a function ƒ that takes a positive integer and outputs a rational ƒ, together with a function g that takes a positive integer n and outputs a positive integer g such that
so that as n increases, the values of ƒ 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 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. 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 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 numbers.
Cardinality
To take the algorithmic interpretation above would seem at odds with classical notions of cardinality. By enumerating algorithms, we can show that the computable numbers are classically countable. And yet Cantor'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 a bijection 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 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, 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. The classical theorem proving the existence of a bijection in such circumstances, namely the Cantor–Bernstein–Schroeder theorem, is non-constructive. It has recently been shown that the Cantor–Bernstein–Schroeder theorem implies the law of the excluded middle, hence there can be no constructive proof of the theorem.
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 assert that ZF itself is not a constructive system.In intuitionistic theories of type theory, 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 holds, then there is actually a function F such that R 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 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, 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.