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

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

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

- 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.

need not hold even whenn P(n)n P(n)

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):pp

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

In words, LPO states that for each binary sequence (a= 0n(a_{n}= 0),

a0n(a_{n}= 1)

- the decidability of equality in the real line
**R**; - the least-upper-bound principle;
- the field
**Z**_{2}is Noetherian.

It might be suspected that, since we cannot prove constructively thatLetSbe a nonempty^{1}subset ofRthat is bounded above. ThensupSexists if and only if for all real numbers, (with < ),we have:xS(x< )xS(x> ).

of finitely generated left ideals inJ_{1}J_{2}J_{3}...

where, as usual,IfRis a coherent Noetherian ring, then so isR[x],

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.

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, Constable [19??] and Hayashi [1988]).

- 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), - Constable, R.
- 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.

Douglas Bridges

*First published: November 18,1997*

*Content last modified: November 18, 1997 *