Constructive Mathematics

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.

• 1. Introduction
• 2. The Constructive Interpretation of Logic
• 3. Varieties of Constructive Mathematics
• 4. Concluding Remarks
• Bibliography
• Other Internet Resources
• Related Entries

1. Introduction

Before mathematicians assert something they are supposed to have proved it true. What, then, do mathematicians mean when they assert a disjunction P  Q, where P and Q are syntactically correct statements in some (formal or informal) language that a mathematician can use? A natural -- although, as we shall see, not the unique -- interpretation of this disjunction is that not only does (at least) one of the statements P, Q hold, but also we can decide which one holds. Thus just as mathematicians will assert that P only when they have decided that P by proving it, they may assert P  Q only when they either can decide -- that is, prove -- that P or decide (prove) that Q.

With this interpretation, however, mathematicians run into a serious problem in the special case where Q is the negation, P, of P. To decide that P is to show that P implies a contradiction (such as 0=1). But it will often be that mathematicians have neither decided that P nor decided that P. To see this, we need only reflect on the following:

Goldbach Conjecture:
Every even integer > 2 can be written as a sum of two primes,

which remains neither proved nor disproved despite the best efforts of many of the leading mathematicians since it was first raised in a letter from Goldbach to Euler in 1742. We are forced to conclude that, under the very natural interpretation of P Q just canvassed, only an optimist can retain a belief in the law of excluded middle, P  P.

Traditional, or classical, mathematics gets round this by widening the interpretation of disjunction: it interprets P  Q as (PQ), or in other words, “it is contradictory that both P and Q be false”. In turn, this leads to the idealistic interpretation of existence, in which xP(x) means xP(x) (“it is contradictory that P(x) be false for every x”). It is on these interpretations of disjunction and existence that mathematicians have built the grand, and apparently impregnable, edifice of classical mathematics which serves a foundation for the physical, the social, and (increasingly) the biological sciences. However, the wider interpretations come at a cost: for example, when we pass from our initial, natural interpretation of P  Q to the unrestricted use of the idealistic one, (PQ), the resulting mathematics cannot generally be interpreted within computational models such as recursive function theory.

This point is illustrated by a well-worn example, the proposition:

There exists irrational numbers a, b such that a^b is rational.

A slick classical proof goes as follows. Either is rational, in which case we take a = b = ; or else is irrational, in which case we take a = and b = (See Dummett 1977, 10). But as it stands, this proof does not enable us to pinpoint which of the two choices of the pair (a,b) has the required property. In order to determine the correct choice of (a,b), we would need to decide whether is rational or irrational, which is precisely to employ our initial interpretation of disjunction with P the statement “ is rational”.

Here is another illustration of the difference between interpretations. Consider the following simple statement about the set of real numbers:

(*) x (x = 0 x 0),

where, for reasons that we divulge shortly, x 0 means that we can find a rational number r with 0 < r < |x|. A natural computational interpretation of (*) is that we have a procedure which, applied to any real number x, either tells us that x=0 or else tells us that x 0. (For example, such a procedure might output 0 if x=0, and output 1 if x 0.) However, because the computer can handle real numbers only by means finite rational approximations, we have the problem of underflow, in which a sufficiently small positive number can be misread as 0 by the computer; so there cannot be a decision procedure that justifies the statement (*). In other words, we cannot expect (*) to hold under our natural computational interpretation of the quantifier and the connective .

Let's examine this from another angle. Let G(n) act as shorthand for the statement “2n + 2 is a sum of two primes”, where n ranges over the positive integers, and define an infinite binary sequence a = (a₁,a₂,…) as follows:

an =

0 1

if G(n) holds for all k n if G(n) holds for some k n

There is no question that a is a computationally well-defined sequence, in the sense that we have an algorithm for computing a_n for each n: check the even numbers 4,6,8,…,2n+2 to determine whether each of them is a sum of two primes; in that case, set a_n=0; in the contrary case, set a_n=1. Now consider the real number whose n^th binary digit is a_n:

x	=	(0a1a2a2)2
	=	2-1a1 + 2-2a2 +
	=	n=1 2-nan.

If (*) holds under our computational interpretation, then we can decide between the following two alternatives:

• 2^-1a₁ + 2^-2a₂ + = 0, which implies that a_n = 0 for every n;
• we can find a positive integer N such that 2^-1a₁ + 2^-2a₂ + > 2^-N.

In the latter case, by testing a₁,…,a_N, we can find n N such that a_n = 1. Thus the computational interpretation of (*) enables us to decide whether there exists n such that a_n = 1; in other words, it enables us to decide the status of the Goldbach Conjecture.

The use of the Goldbach Conjecture here is purely dramatic. To avoid it, we define a function f on the set of binary sequences as follows:

f(a) =

0 1

if an = 0 for all n if an = 1 for some n.

The argument of the preceding paragraph can then be modified to show that, under our computational interpretation, (*) provides us with a procedure for calculating f(a) for any computationally well-defined binary sequence f(a). Now, the computability of the function f can be expressed informally by the following:

Limited Principle of Omniscience (LPO):
For each binary sequence (a₁,a₂,…) either a_n = 0 for all n or else there exists n such that a_n = 1,

which is generally regarded as an essentially nonconstructive principle, for several reasons. First, its recursive interpretation,

There is a recursive algorithm which, applied to any recursively defined binary sequence (a₁,a₂,…), outputs 0 if a_n = 0 for all n, and outputs 1 if a_n = 1 for some n,

is provably false within recursive function theory, even with classical logic (see Bridges & Richman 1987, Chapter 3); so if we want to allow a recursive interpretation of all our mathematics, then we cannot use LPO. Secondly, there is a model theory (involving the use of Kripke models) in which it can be shown that LPO is not derivable in Peano arithmetic using the computational interpretation of the connectives and quantifiers that we state in more detail in the next section (Bridges & Richman 1987, Chapter 7).

2. Constructive Interpretation of Logic

It should, by now, be clear that a full-blooded computational development of mathematics disallows the idealistic interpretations of disjunction and existence upon which most classical mathematics depends. In fact, in order to work constructively, we need to return from the classical interpretations back to the natural, constructive ones, as follows.

(or):	to prove P Q we must have either a proof of P or a proof of Q.
(and):	to prove P Q we must have a proof of P and a proof of Q.
(implies):	a proof of P Q is an algorithm that converts a proof of P into a proof of Q.
(not):	to prove P we must show that P implies 0 = 1.
(there exists):	to prove xP(x) we must construct an object x and prove that P(x) holds.
(for each/all):	a proof of xP(x) is an algorithm that, applied to any object x, proves that P(x) holds.

These computational interpretations can be made more precise using Kleene's notion of realizability; see (Dummett 1977, 318-335; Beeson 1985, Chapter VII).

Why would we want to do this? First, there is the desire to retain, as far as possible, computational interpretations of our mathematics. Ideally, we are trying to develop mathematics in such a way that if a theorem asserts the existence of an object x with a property P, then the proof of the theorem embodies algorithms for constructing x and for demonstrating, by whatever calculations are necessary, that x has the property P. Here are some examples of theorems, each followed by an informal description of the requirements for its constructive proof.

(A)	For each real number x, either x = 0 or x 0.
	Proof requirement: An algorithm which, applied to a given real number x, would decide whether x = 0 or x 0. Note that, in order to make this decision, the algorithm might use not only the data describing x but also the data showing that x is actually a real number.
(B)	Each nonempty subset S of R that is bounded above has a least upper bound.
	Proof requirement: An algorithm which, applied to a set S of real numbers, a member s of S, and an upper bound for S, computes an object b and shows that b is a real number; shows that x b for each x S; and given a real number b < b, computes an element x of S such that x > b.
(C)	If f is a continuous real-valued mapping on the closed interval [0,1] such that f(0)f(1) < 0, then there exists x such that 0 < x < 1 and f(x) = 0.
	Proof requirement: An algorithm which, applied to the function f, a modulus of continuity for f, and the values f(0) and f(1), computes an object x and shows that x is a real number between 0 and 1, and shows that f(x) = 0.
(D)	If f is a continuous real-valued mapping on the closed interval [0,1] such that f(0)f(1) < 0, then for each > 0 there exists x such that 0 < x < 1 and |f(x)| < .
	Proof requirement: An algorithm which, applied to the function f, a modulus of continuity for f, the values f(0) and f(1), and a positive number , computes an object x and shows that x is a real number between 0 and 1, and shows that |f(x)| < .

We already have reasons for doubting that (A) has a constructive proof. If the proof requirements for (B) can be fulfilled, then, given a binary sequence (a₁,a₂,…), we can apply our proof of (B) to the set {a₁,a₂,…} in order to determine its supremum . Computing with an error < 1/2, we then determine whether = 0 or = 1; in the first case, a_n = 0 for all n, whereas in the second, we can easily find N such that a_N = 1. Thus (B) implies LPO and is therefore essentially nonconstructive. However, in Bishop's constructive theory of the real numbers, based on Cauchy sequences with a preassigned convergence rate, we can prove the following:

Constructive Least-Upper-Bound Principle:
Let S be a nonempty subset of R that is bounded above. Then S has a least upper bound if and only if it is located, in the sense that for all real numbers , with < , either is an upper bound for S or else there exists x in> S with x > (Bishop & Bridges 1985, p. 37, Proposition (4.3))

Each of statements (C) and (D), which are classically equivalent, is a version of the Intermediate Value Theorem. In these statements, a modulus of continuity for f is a set of ordered pairs ( ,) of positive real numbers with the following two properties:

• for each > 0 there exists > 0 such that (,) ;
• for each (,) , and for all x,y [0,1] such that |x - y| < , we have |f(x) - f(y)| < .

Statement (C) is essentially nonconstructive, since it entails the following nonconstructive principle:

Lesser Limited Principle of Omniscience (LLPO):
For each binary sequence (a₁,a₂,…) with at most one term equal to 1, either a_n = 0 for all even n or else a_n = 0 for all odd n.

Statement (D), a weak form of (C), can be proved constructively, using an interval-halving argument of a standard type. The following stronger constructive intermediate value theorem, which suffices for most practical purposes, is proved using an approximate interval-halving argument:

Let f be a continuous real-valued mapping on the closed interval [0,1] such that f(0) and f(1) have opposite signs. Suppose also that f is locally nonzero, in the sense that for each x [0,1] and each r > 0, there exists y such that |x - y| < r and f(y) 0. Then there exists x such that 0 < x < 1 and f(x)=0.

The situation of the intermediate value theorem is typical of many in constructive analysis, where we find one classical theorem with several constructive versions, some or all of which may be equivalent under classical logic. (See also, for example, Bridges et al. 1982.)

There is one omniscience principle whose constructive status is less clear than that of LPO and LLPO, namely, the following:

Markov's Principle (MP):
For each binary sequence (a_n), if it is contradictory that all the terms a_n equal 0, then there exists a term equal to 1.

This principle is equivalent to a number of simple classical propositions, including the following:

• For each real number x, if it is contradictory that x equal 0, then x 0 (in the sense we mentioned earlier).
• For each real number x, if it is contradictory that x equal 0, then there exists y such that xy = 1.
• For each one-one continuous mapping f : [0,1] , if x y, then f(x) f(y).

Markov's Principle represents an unbounded search: if you have a proof that all terms a_n being 0 leads to a contradiction, then, by testing the terms a₁,a₂,a₃,… in turn, you are ‘guaranteed’ to come across a term equal to 1; but this guarantee does not extend to an assurance that you will find the desired term before the end of the universe. Most practitioners of constructive mathematics view Markov's Principle with at least suspicion, if not downright disbelief. Such views are reinforced by the observation that there is a Kripke Model showing that MP is not derivable in Peano arithmetic under our computational interpretation of logic. (See Bridges & Richman 1987, 137-138.)

3. Varieties of Constructive Mathematics

The desire to retain the possibility of a computational interpretation is one motivation for using the constructive reinterpretations of the logical connective and quantifiers that we gave above; but it is not exactly the motivation of the pioneers of constructivism in mathematics.

In the late nineteenth century, certain individuals -- most notably Kronecker and Poincaré -- had expressed doubts, or even disapproval, of the idealistic, nonconstructive methods used by some of their contemporaries; but it is in the polemical writings of L.E.J. Brouwer (1881-1966), beginning with his Amsterdam doctoral thesis in 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. If one takes that philosophical stance, then one is inexorably drawn to the foregoing constructive interpretation of the logical connectives and quantifiers: for how could a proof of the impossibility of the non-existence of a certain object x -- an idealistic proof of the existence of x -- describe a mental construction of x? Brouwer was not the clearest expositor of his ideas, as is shown by the following quotation:

Mathematics arises when the subject of two-ness, which results from the passage of time, is abstracted from all special occurrences. The remaining empty form [the relation of n to n+1] of the common content of all these two-nesses becomes the original intuition of mathematics and repeated unlimitedly creates new mathematical subjects. (quoted in Kline 1972, pp. 1199-2000)

The primary concern of mathematics is number, and this means the positive integers. We feel about number the way Kant felt about space. The positive integers and their arithmetic are presupposed by the very nature of our intelligence and, we are tempted to believe, by the very nature of intelligence in general. The development of the positive integers from the primitive concept of the unit, the concept of adjoining a unit, and the process of mathematical induction carries complete conviction. In the words of Kronecker, the positive integers were created by God.

According to [Brouwer's] view and reading of history, classical logic was abstracted from the mathematics of finite sets and their subsets. ... Forgetful of this limited origin, one afterwards mistook that logic for something above and prior to all mathematics, and finally applied it, without justification, to the mathematics of infinite sets. This is the Fall and original sin of set theory, for which it is justly punished by the antinomies. It is not that such contradictions showed up that is surprising, but that they showed up at such a late stage of the game. (quoted in Kline 1972, p. 2001)

In order to describe the logic used by the intuitionist mathematician, it was necessary first to analyse the mathematical processes of the mind, from which analysis the logic could be extracted. In 1930, Brouwer's most famous pupil, Arend Heyting, published a set of formal axioms which so clearly characterise the logic used by the intuitionist that they have become universally known as the axioms for intuitionistic logic (Heyting 1930). These axioms captured the informal computational interpretations of the connectives and quantifiers that we gave earlier. Over the years, Brouwer added principles, suggested by his introspective analysis of the nature of the continuum, which made intuitionistic mathematics diverge dramatically from its classical counterpart. The reader is referred to the entry on intuitionistic logic for more information about such matters.

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 late 1940s the Russian mathematician A.A. Markov (Markov 1954) began the development of a form of recursive constructive mathematics (RUSS), which was, essentially, recursive function theory with intuitionistic logic (see Kushner 1985). In this variety the objects are defined by means of Gödel-numberings, and the procedures are all recursive; the main distinction between RUSS and the classical recursive analysis developed after, in 1936, the work of Turing, Church, and others clarified the nature of computable processes, is that the logic used in RUSS is intuitionistic. Thus RUSS may be described as ‘recursive mathematics with intuitionistic logic’.

One obstacle faced by the mathematician attempting to come to grips with RUSS is that, expressed in the language of recursion theory, it is not easily readable; indeed, on opening a page of Kushner's excellent lectures, one might be forgiven for wondering whether this is analysis or logic. Fortunately, one can get to the heart of RUSS by an axiomatic approach, as shown in Richman 1983.

Progress in all varieties of constructive mathematics was relatively slow throughout the next decade and a half. What was needed to raise the profile of constructivism in mathematics was a top-ranking classical mathematician to show that a thoroughgoing constructive development of mathematics was possible without a commitment to Brouwer's non-classical 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), 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 self-adjoint 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. (See also Bishop & Bridges 1985.) 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)

How is this multiple interpretability achieved? At least in part by Bishop's refusal to pin down his primitive notion of ‘algorithm’ or, in his words, ‘finite routine’. This refusal has led to the criticism that his approach lacks 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 (1990, 1996). Taking the logic as the primary characteristic of constructive mathematics, it does not reflect the primacy of mathematics over logic that was part of the belief of Brouwer, Heyting, Markov, Bishop, and other pioneers of constructivism. On the other hand, it does capture the essence of constructive mathematics in practice.

Thus one might distinguish between the ontological constructivism of Brouwer and others who are led to constructive mathematics through a belief that mathematical objects are mental creations, and the epistemological constructivism of Richman and those who see constructive mathematics as characterised by its methodology, based on the use of intuitionistic logic. Of course, the former approach to constructivism inevitably leads to the latter; and the latter is certainly not inconsistent with a Brouwerian ontology.

4. Conclusion

Bibliography

References

• Beeson, Michael, 1985, Foundations of Constructive Mathematics, Heidelberg: Springer-Verlag.
• Bishop, Errett, 1967, Foundations of Constructive Analysis, New York: McGraw-Hill.
• Bishop, Errett, 1973, Schizophrenia in Contemporary Mathematics, Amer. Math. Soc. Colloquium Lectures, Missoula: University of Montana; reprinted in Errett Bisop: Reflections on Him and His Research, Amer. Math. Soc. Memoirs 39.
• Bishop, E. and Bridges, D., 1985, , Grundlehren der math. Wissenschaften 279, Heidelberg: Springer-Verlag.
• Bridges, D., Calder, A., Julian, W., Mines. R. and Richman, F., 1982, "Picard's Theorem", Trans. Amer. Math. Soc., 269(2), 513-520.
• Bridges, D. and Richman, F., 1987, Varieties of Constructive Mathematics, London Math. Soc. Lecture Notes 97, Cambridge: Cambridge University Press.
• Brouwer, L.E.J., 1907, Over de Grondslagen der Wiskunde, Doctoral Thesis, University of Amsterdam, 1907; reprinted with additional material, D. van Dalen (ed.), by Matematisch Centrum, Amsterdam, 1981.
• Dummett, Michael, 1977, Elements of Intuitionism, Oxford: Clarendon Press.
• 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.
• Kline, Morris, 1972. Mathematical Thought from Ancient to Modern Times , vol 3, Oxford: Clarendon Press.
• Kushner, B., 1985, Lectures on Constructive Mathematical Analysis, Providence RI: Amer. Math. Soc.
• Markov, A.A., 1954, Theory of Algorithms, Trudy Mat. Istituta imeni V.A. Steklova, 42, Moskva: Izdatel'stvo Akademii Nauk SSSR.
• Richman, Fred, 1983, "Church's Thesis Without Tears", J. Symbolic Logic, 48, 797-803.
• -----, 1990, "Intuitionism as Generalization", Philosophia Math, 5, 124-128.
• -----, 1996, "Interview with a Constructive Mathematician", Modern Logic, 6, 247-271.
• Weihrauch, Klaus, 1996, "A Foundation for Computable Analysis", in Combinatorics, Complexity, & Logic, D. Bridges, C. Calude, J. Gibbons, S. Reeves, and I. Witten (eds.), Singapore: Springer-Verlag.
• -----, 2000, Computable Analysis, EATCS Texts in Theoretical Computer Science, Heidelberg: Springer-Verlag.

Related Literature

• Bridges, Douglas, 1998, "Constructive Truth in Practice", in Truth in Mathematics, H. Dales and G. Oliveri (eds.), Oxford: Clarendon Press.
• Brouwer, L.E.J., 1908, "De onbetrouwbaarheid der logische principes", Tijdschrift voor Wijsbegeerte, 2, 152-158.
• Goodman, N.D., and Myhill, J., "Choice Implies Excluded Middle", Zeit. Logik und Grundlagen der Math, 24, 461.
• Hayashi, S., and Nakano, H., 1988, PX: A Computational Logic, MIT Press, Cambridge MA.
• Heijenoort, Jean van, 1967, From Frege to Gödel: A Source Book in Mathematical Logic 1879-1931, Harvard University Press, Cambridge, Mass.
• Heyting, A., 1971, Intuitionism -- An Introduction, 3rd edition, Amsterdam: North Holland.
• Hilbert, D., 1925, "Über das Unendliche", Mathematische Annalen, 95, 161-190; translation, "On the Infinite", by E. Putnam and G. Massey, in Philosophy of Mathematics: Selected Readings, P. Benacerraf and H. Putnam (eds.), 134-151, Englewood Cliffs, NJ: Prentice Hall, 1964.
• Mines, R., Richman, F., and Ruitenburg, W., 1988, A Course in Constructive Algebra, Universitext, Heidelberg: Springer-Verlag.
• Myhill, John, 1973, "Some Properties of Intuitionistic Zermelo-Fraenkel Set Theory", in Cambridge Summer School in Mathematical Logic, A. Mathias and H. Rogers (eds.), Lecture Notes in Mathematics, 337, Heidelberg: Springer-Verlag, 206-231.
• -----, 1975, "Constructive Set Theory", J. Symbolic Logic, 40/3, 347-382.
• 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.
• Richman, Fred, 2000, "The Fundamental Theorem of Algebra: A Constructive Treatment Without Choice", Pacific J. Math., 196, 213-230.
• Troelstra, A.S., 1978, "Aspects of Constructive Mathematics", in Handbook of Mathematical Logic, J. Barwise (ed.), Amsterdam: North-Holland.
• Troelstra, A.S., and van Dalen, D., 1988, Constructivity in Mathematics: An Introduction (two volumes), Amsterdam: North Holland.
• van Dalen, D., 1981, Brouwer's Cambridge Lectures on Intuitionism, Cambridge: Cambridge University Press.
• -----, 1999, Mystic, Geometer and Intuitionist: The Life of L.E.J. Brouwer, vol. I, Oxford: Clarendon Press.
• van Stigt, W.P., 1990, Brouwer's Intuitionism, Amsterdam: North-Holland.

Other Internet Resources

Related Entries

Table of Contents

First published: November 18, 1997
Content last modified: March 26, 2002