This is a file in the archives of the Stanford Encyclopedia of Philosophy.

Stanford Encyclopedia of Philosophy

A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z

Constructive Mathematics

Constructive mathematics is distinguished from its traditional counterpart, classical mathematics, by the strict interpretation of the phrase ‘there exists’ as ‘we can construct’. In order to work constructively, we need to re-interpret not only the existential quantifier but all the logical connectives and quantifiers as instructions on how to construct a proof of the statement involving these logical expressions.

Although certain individuals--most notably Kronecker--had expressed disapproval of the ‘idealistic’, nonconstructive methods used by some of their nineteenth century contemporaries, it is in the polemical writings of L.E.J. Brouwer (1881-1966), beginning with his Amsterdam doctoral thesis (Brouwer [1907]) and continuing over the next forty-seven years, that the foundations of a precise, systematic approach to constructive mathematics were laid. In Brouwer’s philosophy, known as intuitionism, mathematics is a free creation of the human mind, and an object exists if and only if it can be (mentally) constructed.

The Basis of Constructive Mathematics
Recasting Classical Results
Bishop to K1
Recent Developments
Bibliography
Other Internet Resources
Related Entries

The Basis of Constructive Mathematics

Constructive mathematics is based on the idea that the logical connectives and the existential quantifier are to be interpreted as instructions on how to construct a proof of the statement involving these logical expressions. Specifically, the interpretation proceeds as follows:

To prove p or q (‘p q’), we must have either a proof of p or a proof of q.
To prove p and q (‘p & q’), we must have both a proof of p and a proof of q.
A proof of p implies q (‘p q’) is an algorithm that converts a proof of p into a proof of q.
To prove it is not the case that p (‘p’), we must show that p implies a contradiction.
To prove there exists something with property P (‘ xP(x)’), we must construct an object x and prove that P(x) holds.
A proof of everything has property P (‘xP(x)’) is an algorithm that, applied to any object x, proves that P(x) holds.

Careful analysis of the logical principles actually used in constructive proofs led Heyting (in his [1930]) to the axioms for intuitionistic logic. In this logic, the proposition:

n P(n) n P(n)

need not hold even when P(n) is a decidable property of natural numbers n. So, in turn, the Law of Excluded Middle (LEM):

p p

does not hold. As a result, many classical results cannot be proved constructively, since they would imply LEM or some other manifestly nonconstructive principle. One such principle is the Limited Principle of Omniscience (LPO):

a {0,1}^N (a=0 a0),

where a = (a₀,a₁,a₂,...), N is the set of natural numbers, and

a = 0 n (a_n = 0),
a 0 n (a_n = 1)

In words, LPO states that for each binary sequence (a_n), either a_n = 0 for all n or else there exists n such that a_n = 1. There are several reasons for regarding LPO as an essentially nonconstructive principle. First, its recursive interpretation is provably false within recursive function theory, even with classical logic (see Bridges and Richman [1987], Chapter 3); so if we want to allow a recursive interpretation of our constructive mathematics, then we cannot use LPO. Secondly, there is a model theory (namely, Kripke models) in which it can be shown that LPO is not derivable with intuitionistic logic (see Bridges and Richman [1987], Chapter 7).

Recasting Classical Results

Among the many classical results which, in their traditional forms, entail LPO and are therefore essentially nonconstructive are

the decidability of equality in the real line R;
the least-upper-bound principle;
the field Z₂ is Noetherian.

Fortunately, such results usually can be re-cast, sometimes with additional hypotheses that are trivially satisfied in classical mathematics, to produce constructive versions. For example, we have the following very useful constructive least-upper-bound principle:

Let S be a nonempty^[1] subset of R that is bounded above. Then supS exists if and only if for all real numbers , (with < ), we have:
x S (x < ) x S (x > ).

It might be suspected that, since we cannot prove constructively that Z₂ is Noetherian, there will be no constructive version of the Hilbert Basis Theorem. This suspicion is doubtless reinforced by recollection of the furore that arose after Hilbert’s original, highly nonconstructive proof of that theorem: witness Gordan’s famous remark, ‘Das ist nicht Mathematik. Das ist Theologie’. However, the real constructive problem lies with the definition of ‘Noetherian’. Mines et al. [1988] define a ring R to be Noetherian if for each ascending chain:

J₁ J₂ J₃ ...

of finitely generated left ideals in R there exists n such that J_n = J_n+1.

This definition of ‘Noetherian’ is classically equivalent to the standard classical one (see, for example, page 35 of Cohn [19??]), is satisfied by the ring Z₂ and leads to the following constructive version of the Hilbert Basis Theorem:

If R is a coherent Noetherian ring, then so is R[x],

where, as usual, R[x] is the ring of polynomials over R. (We omit the details of coherence; suffice it to say that it is a property that automatically holds for a Noetherian ring in classical mathematics.)

Bishop to K1

Unfortunately--and perhaps inevitably, in the face of opposition from mathematicians of such stature as Hilbert--Brouwer’s intuitionist school of mathematics and philosophy became more and more involved in what, at least to classical mathematicians, appeared to be quasi-mystical speculation about the nature of constructive thought, to the detriment of the practice of constructive mathematics itself. On the other hand, in the 1930s the Russian mathematician A.A. Markov began a the development of a form of recursive constructive mathematics Kushner [1985], which was, essentially, recursive function theory with intuitionistic logic. The disadvantage of Markov’s approach was that the strict rules of recursive function theoretic language made it difficult to carry out, for example, analysis in a manner that was either natural or easily readable for traditional analysts. So progress in recursive analysis was both relatively slow and inaccessible compared with its classical counterpart.

What was needed was a top-ranking classical mathematician to show that a thoroughgoing constructive development of constructive mathematics was possible without a commitment to Brouwer’s eccentric principles or to the machinery of recursive function theory. This need was fulfilled in 1967, with the appearance of Errett Bishop’s monograph Foundations of Constructive Analysis(Bishop [1967]; see also Bishop and Bridges [1985]), the product of an astonishing couple of years in which, working in the informal but rigorous style used by normal analysts, Bishop provided a constructive development of a large part of twentieth-century analysis, including the Stone-Weierstrass Theorem, the Hahn-Banach and separation theorems, the spectral theorem for selfadjoint operators on a Hilbert space, the Lebesgue convergence theorems for abstract integrals, Haar measure and the abstract Fourier transform, ergodic theorems, and the elements of Banach algebra theory. Thus, at a stroke, he gave the lie to the commonly-held view, expressed so forcefully by Hilbert:

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. (Hilbert [1928])

Not only did Bishop’s mathematics (BISH) have the advantage of readability--if you open Bishop’s book at any page, what you see is recognisably analysis (even if, from time to time, his moves in the course of a proof may appear strange to one schooled in the use of LEM)---but, unlike intuitionistic or recursive mathematics, it admits many different interpretations. Intuitionistic mathematics, Markov’s recursive constructive mathematics, and even classical mathematics all provide models of BISH. In fact, the results and proofs in BISH can be interpreted, with at most minor amendments, in any reasonable model of computable mathematics, such as, for example, Weihrauch’s TTE (Weihrauch [1987], [1996]).

How is this multiple interpretability achieved? At least in part by Bishop’s refusal to pin down his primitive notion of ‘algorithm’ or ‘finite routine’. This refusal on his part has led to some criticism of the foundation of his approach, as lacking the precision that a logician would normally expect of a foundational system. However, this criticism can be overcome by looking more closely at what practitioners of BISH actually do, as distinct from what Bishop may have thought he was doing, when they prove theorems: in practice, they are doing mathematics with intuitionistic logic. Experience shows that the restriction to intuitionistic logic always forces mathematicians to work in a manner that, at least informally, can be described as algorithmic; so algorithmic mathematics appears to be equivalent to mathematics that uses only intuitionistic logic. If that is the case, then we can practice constructive mathematics using intuitionistic logic on any reasonably defined mathematical objects, not just some class of ‘constructive objects’.

This view, more or less, appears to have first been put forward by Richman (Richman [1990], Richman [1996]), but was also hinted at in Bridges [1975]. Taking the logic as the characteristic of constructive mathematics, it does not, of course, reflect the primacy of mathematics over logic that was part of the belief of Brouwer, Heyting, Markov, Bishop, and other pioneers of constructivism.

Note that Richman’s philosophy is one of the practice of constructive mathematics, and is certainly compatible with a more radical constructive philosophy of mathematics itself, such as Brouwer’s intuitionism, in which the objects of mathematics are mental constructs. It is a philosophy of epistemology, rather than ontology.

Recent Developments

In the thirty years since the appearance of Bishop’s book there have been substantial developments in constructive analysis and algebra. Some of these developments--notably, those in the theory of the integral and the Riemann Mapping Theorem--are described (although not necessarily for the first time) in Bishop and Bridges [1985]; others can be found in the original papers of Richman, Bridges, and others. Good sources of information about the foundations of constructive mathematics are the books Beeson [1985] and Troelstra & van Dalen [1988].

Formal systems for BISH have found interesting applications in computer programming. The basic idea in these applications is that from each proof in BISH we can extract a programme whose correctness is provided by the proof from which it is extracted. The pioneering work in this area was by Martin-Löf ([1975]), in his theory of types; but there are now several research groups of computer scientists around the world who are working in this promising area of automatic theorem-proving (see, for example, Hayashi and Nakano [1988]).

Bibliography

Beeson, Michael, 1985, Foundations of Constructive Mathematics, Springer-Verlag, Heidelberg.
Bishop, Errett, 1967, Foundations of Constructive Analysis, McGraw-Hill, New York.
Bishop, E. and Bridges, D., 1985, Constructive Mathematics, Grundlehren der math. Wissenschaften 279, Springer-Verlag, Heidelberg.
Bridges, Douglas, 1975, Constructive Mathematics--Its Set Theory and Practice, D.Phil. thesis, Oxford University.
Bridges, D. and Richman, F., 1987, Varieties of Constructive Mathematics, London Math. Soc. Lecture Notes 97, Cambridge University Press.
Brouwer, L.E.J., 1981, Over de Grondslagen der Wiskunde, Doctoral Thesis, University of Amsterdam, 1907. Reprinted with additional material (D. van Dalen, ed.) by Matematisch Centrum, Amsterdam.
Cohn, P.M., Algebra (Vol. 2),
Hayashi, S., and Nakano, H., 1988, PX: A Computational Logic, MIT Press, Cambridge MA.
van Heijenoort, Jean, 1967, From Frege to Gödel: A Source Book in Mathematical Logic 1879-1931, Harvard University Press, Cambridge, Mass.
Heyting, A., 1930, "Die formalen Regeln der intuitionistischen Logik", Sitzungsber. preuss. Akad. Wiss. Berlin, 42-56.
Hilbert, David, 1928, "Die Grundlagen der Mathematik", Hamburger Mathematische Einzelschriften 5, Teubner, Leipzig. Reprinted in English translation in van Heijenoort [1967], in which the exact quotation appears on page 476.
B.A. Kushner, 1985, Lectures on Constructive Mathematical Analysis, Amer. Math. Soc., Providence RI.
Martin-Löf, P., 1975, "An intuitionistic theory of types: predicative part", in Logic Colloquium 1973 (H.E. Rose and J.C. Shepherdson, eds), 73-118, North-Holland, Amsterdam.
Mines, R., Richman, F., and Ruitenburg, W., 1988, A Course in Constructive Algebra, Universitext, Springer-Verlag, Heidelberg.
Richman, F., 1990, "Intuitionism as generalization", Philosophia Math. 5, 124-128, (MR #91g:03014).
Richman, F., 1996, "Interview with a constructive mathematician", Modern Logic 6, 247-271.
Troelstra, A.S., and van Dalen, D., 1988, Constructivity in Mathematics: An Introduction (two volumes). North Holland, Amsterdam
Weihrauch, Klaus, 1987, Computability, Springer-Verlag, Heidelberg.
Weihrauch, Klaus, 1996, "A foundation for computable analysis", in Combinatorics, Complexity, & Logic (Proceedings of Conference in Auckland, 9-13 December 1996), D.S. Bridges, C.S. Calude, J. Gibbons, S. Reeves, I.H. Witten, eds., Springer-Verlag, Singapore, 1996.

Other Internet Resources

[Please contact the author with suggestions.]

Related Entries

A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z

Table of Contents

First published: November 18,1997
Content last modified: November 18, 1997