In analysis, constructive problems arise instantly because we start with the real numbers, and there is no finite procedure for deciding whether two given real numbers are equal (the real numbers are not discrete). The main thrust of constructive mathematics was in the direction of analysis, although several mathematicians, including Kronecker and van der Waerden, made important contributions to constructive algebra. Heyting, working in intuitionistic algebra, concentrated on issues raised by considering algebraic structures over the real numbers, and so developed a handmaiden of analysis rather than a theory of discrete algebraic structures. Paradoxically, it is in algebra where we are most likely to meet up with wildly nonconstructive arguments such as those that establish the existence of maximal ideals, and the existence of more than two automorphisms of the field of complex numbers.
It is important to realize that constructive algebra is algebra; in fact it is a generalization of classical algebra in that we do not assume the law of excluded middle, just as group theory is a generalization of abelian group theory in that the commutative law is not assumed. A constructive proof of a theorem is, in particular, a proof of that theorem. Every theorem in constructive mathematics can be understood as referring to the conventional universe of mathematical discourse, and the proofs are acceptable within that universe. We do not limit ourselves to a restricted class of "constructive objects," as recursive function theorists do, nor do we introduce classically false principles, as the intuitionists do.
[from the preface of A course in constructive algebra ]
In Memoriam, Errett Bishop
NMSU seminar in constructive mathematics
In the present context, the characteristic property is the rejection of the law of excluded middle. It is somewhat remarkable how this one metamathematical move embodies the essence of constructivism. Constructivism suggests rejection of the law of excluded middle because there is generally no computational basis for asserting "p or not p". For example, consider the statement, provable using the law of excluded middle, that some digit appears infinitely often in the decimal expansion of pi. Here the existence of an integer is claimed to be proved, but no method for its computation is indicated by the proof. It is less clear, but born out by experience and theoretical constructions such as recursive realizability, that theorems proved without the law of excluded middle automatically have a computational interpretation.
Contemporary constructive mathematics can be regarded as arising from the philosophical impact of the computer on pure mathematics. The computer is changing the very way we regard mathematical objects. Our growing experience with programming makes the idea of computation-in-principle quite real to us, and this idea is the motivating force behind doing constructive mathematics. We now have an immediate feeling for the distinction between a very large but finite process, and an infinite process. While there are a number of logical systems that do not incorporate the law of excluded middle, so-called intuitionistic logic is the accepted standard in all constructive schools. This logic, first made explicit by A. Heyting, was based on the mathematical practice of L.E.J. Brouwer and his intuitionistic school. Intuitionistic logic can be thought of as a fragment of classical logic, so anything proved within it is simultaneously proved classically. The full-blown intuitionism of Brouwer embraced principles which are false under the classical interpretation: for example, that every function defined on all the real numbers is continuous. These principles can be thought of as flowing from a more detailed philosophical analysis of the nature of mathematical objects and our relation to them.
The Russian school of constructive mathematics, initiated by A.A. Markov and continued by N.A. Shanin, G.S. Tseitin, B.A. Kushner and others, is probably best thought of as constructive recursive mathematics. The underlying logic is intuitionistic, but the mathematical objects are restricted to finite objects---including algorithms represented by finite strings of symbols. Historically, but perhaps not necessarily, this school adopted Markov's principle: to show that an algorithm halts at some stage, it suffices to prove that it cannot possibly run forever. Brouwer held Markov's principle to be false, and in certain formalizations of his thinking it is refutable. However, as it is classically true, it is not refutable in basic constructive mathematics.
I identify basic constructive mathematics with the constructive mathematical practice of Errett Bishop, although there is a bit more to this than simply adopting intuitionistic logic. The most salient addition is the axiom of dependent choices, a strong countable choice axiom. This axiom conforms with the practice of the Russian school and of the intuitionists. Bishop also uses the notion of an operation, which is a completely informal analogue of an algorithm in recursive mathematics. While this is probably interpretable in intuitionism, it is confusing, at best, in classical mathematics. With the possible exception of Tennenbaum's constructive development of Noetherian rings, all of Bishop's mathematics can be rephrased to avoid talking about operations.
There are a number of books on constructive mathematics available. Heyting's charming introduction to intuitionism is unique. The others divide roughly according to whether they emphasize mathematics or logic. Examples of the former are Aberth, Bishop, Bishop-Bridges, Bridges, Bridges-Richman, and Mines-Richman-Ruitenburg; examples of the latter are Dummett, Beeson, and Troelstra-van Dalen. I am inclined to classify Kushner and Shanin with the latter because, like texts that emphasize logic, they deal with conventional mathematics at one remove, studying a symbolism for algorithms rather than the objects of ordinary mathematical discourse themselves. Aberth, although he also is presenting Russian constructivism, has much more of the flavor of a conventional mathematical text---for the novice this is a good introduction to the Russian school.
Troelstra and van Dalen's book---actually a two-volume set---is the first comprehensive book on constructive mathematics written by mathematicians raised in the tradition of intuitionism---direct descendants of Brouwer, as it were. The introduction can be read with profit by anyone wishing to get an idea of what constructive mathematics is about.
[from a review of Constructivism in mathematics, an introduction,
by A.S. Troelstra and D. van Dalen. North-Holland, 1988]