Mathematics and Statistics

Related Links

• Beginners’ References
• FAQ
• Links

Constructive Mathematics

Frequently Asked Questions

Note: Some of the symbols used on this page may not display correctly with certain web browsers (usually indicated with either a question mark or box). If this is the case with your browser you can view the intended character(s) by clicking of the symbols. Problem browsers include Internet Explorer and older versions of Netscape.

1. What is constructive mathematics?

   A general answer to this question is that constructive mathematics is mathematics which, at least in principle, can be implemented on a computer.

   There are at least two ways of developing mathematics constructively. In the first way one uses classical (that is, traditional) logic. Unfortunately, that logic allows us to prove theorems that no computer can implement, so in order to do things constructively, we have to work within a strict algorithmic framework such as recursive function theory [22] or Weihrauch’s Type Two Effectivity theory [35]. This can make the resulting mathematics appear rather hard to read and certainly different from normal analysis, algebra, or the like.

   The second way of approaching constructivity is to replace classical logic by intuitionistic logic, which neatly captures the proof processes used when you work in a rigorously computational manner. This way has the advantage that, once you get used to a logic which does not allow, for example, the application of the law of excluded middle (LEM)

   P∨¬P,

   you find yourself working in the style of a traditional algebraist, analyst, and so on, without referring continually to a special algorithmic language and symbolism.

   In these comments I will use constructive mathematics (CM for short) to mean mathematics with intuitionistic logic. (Actually, we need a bit more than just a change of logic: namely, some kind of number–theoretic or set–theoretic foundation that does not conflict with that logic. One such foundation is constructive Zermelo–Fraenkel set theory [3].)

   Top of page

2. Why chose CM at all? Why would a constructive approach interest people?

   Why did I choose to do CM? Because I found it interesting, and because the idea of actually finding objects, instead of merely showing that they could not possibly fail to exist, was one that appealed to me. When I first came across Errett Bishop’s book, in 1968, I had been working on von Neumann algebra theory as a graduate student, and had been vaguely—and certainly inarticulately—dissatisfied with the prevailing style of existence proofs in my reading in that subject. Such proofs typically either proceeded by assuming the non–existence of the desired object and deducing a contradiction, or else applying Zorn’s lemma to ‘construct’ a maximal family of projections with some property or other. Somehow, beautiful though those proofs were, they left me with a feeling that I had been cheated. What did those objects whose existence was proved really look like? How could they be described explicitly? It was only on reading Errett’s book that I understood what was bothering me and that it was possible to give satisfactory answers to those questions.

   Now, don't get me wrong. Just because I find CM particularly appealing it is not the case that I dislike classical (that is, traditional) mathematics, let alone that I am advocating that classical mathematics is somehow not a proper activity for mathematicians to be engaged in. I find most classical mathematics (at least, what I can understand of it) very interesting and a worthy scientific/cultural pursuit. However, if, as I am, you are interested in computability/constructivity within pure mathematics (as distinct from, say, numerical analysis), then you should seriously investigate constructive mathematics. By working constructively—that is, with intuitionistic logic—you will learn to appreciate the distinction between idealistic existence (the impossibility of non–existence) and constructive existence. This distinction is one that, in my view, should be heeded and appreciated far more than it is. As Bishop wrote,

   Meaningful distinctions deserve to be maintained [6]

   If, however, you are not interested in questions of computability, then you should stick to classical logic. There are even areas of mathematics where the content is so highly nonconstructive that it would make little sense to give up classical logic; the higher reaches of modern set theory would seem to be just such an area.

   To summarise: CM should interest people who would like to understand better the distinction between classical and constructive existence, and who are interested in pushing beyond the former to a real construction of the object whose existence is asserted.

   Top of page

3. Are our proofs complicated? Is there any estimate of the complexity of these proofs?

   Generally, constructive proofs are quite complicated. This is hardly surprising, since they produce more (computational) information than their classical counterparts (if the latter have any). Consider, for example, the constructive proofs of Picard’s theorem in the following two classically equivalent forms.

   PT_p

   Let ƒ be a holomorphic function on the punctured disc D (0,1) := {z ∈ C : 0 < |z| < 1} that omits two complex values from its range. Then ƒ has a pole of determinate order at 0.

   PT_s

   Let ƒ be a holomorphic function on D(0,1) that has an essential singularity at 0, and let ζ, ζ′ be two distinct complex numbers. Then either there exists z ∈ D(0,1) with ƒ (z) = ζ or else there exists z ∈ D(0,1) with ƒ (z) = ζ′

   These two theorems, although classically equivalent, are totally different from a constructive point of view. In PT_p we use the data comprising the function ƒ and the two complex values omitted from its range, to construct an integer ν, show that the ν^th Laurent coefficient of ƒ is 0, and to show that all Laurent coefficients with index less than ν are zero. In PT_s our data consist of the holomorphic function ƒ and the two distinct complex numbers ζ, ζ′, and the constructive proof embodies an algorithm converting those data to solution z of one of the equations ƒ (z) = ζ, ƒ (z) = ζ′; moreover, the proof shows which equation is actually solved.

   Now, it is hardly surprising that the constructive proofs of both PT_p and PT_s are rather complicated. For one thing, they rely on delicate estimates involving winding numbers and requiring a number of preliminaries that the classical proof of Picard’s theorem does not require. In addition, those algorithms could actually be extracted from the proofs and implemented on a computer. So we pay more in terms of effort and complexity of proof, but we get more for our money as well.

   The complexity of constructive proofs, other than those that use the Church–Markov–Turing thesis as an additional hypothesis (see [21]) is still largely untouched terrain. However, anecdotal evidence from Bas Spitters suggests that, perhaps contrary to one’s initial expectations, many of the proofs in Bishop’s book are remarkably efficient when implemented on a computer.

   Top of page

4. Are the practitioners of CM just rewriting classical results? Has anybody produced a brand new result in CM that hasn't been proved classically?

   It all depends on what you mean by “brand new result”. If you take the classical viewpoint that every statement is either true or false and hence that once proved, a result is no longer new, then much of what we are doing will look like rewriting classical results. However, if you interpret a constructive theorem and its proof properly, then it is quite clear that, even if the statement of the theorem looks like something that is well known classically, both the properly–interpreted theorem and its proof are brand new.

   Consider yet again the Picard theorems discussed above. The full constructive interpretation of PT_p is this:

   There is an algorithm which, applied to a holomorphic function ƒ on D(0,1) and to two complex values omitted from the domain of ƒ, computes the order ν of the pole that ƒ has at 0.

   I know of no proof of this statement other than the constructive one in [12] the theorem, as presented in my statement, is brand new. Moreover, that proof, while drawing on a classical proof of the classical Picard theorem for inspiration, is also new.

   Similarly, we have the constructive interpretation of PT_s:

   There is an algorithm which, applied to a holomorphic function ƒ on D(0,1) , the data showing that ƒ has an essential singularity at 0 (that is, the sequence of Laurent coefficients of ƒ which contains infinitely many negatively indexed terms), and two distinct complex numbers ζ and ζ′, computes a complex number z and shows that either ƒ (z) = ζ or ƒ (z) = ζ′.

   Once again, this is a brand new theorem, nowhere found (to my knowledge) in the classical literature; and once again, its proof is also new.

   There are aspects of constructive mathematics that are clearly new, in that the classical mathematician would see nothing to prove where the constructive mathematicians does. For example, many theorems of constructive analysis require a certain subset S of a metric space X to be located, in the sense that the distance

   ρ(x,S) := inf { ρ(x,s) : ∈ S }

   exists (is computable). Proving that S is located may be a nontrivial matter. This is related to the failure of the classical least–upper–bound principle. For the constructive existence of the least upper bound of a nonempty subset S of R that is bounded above we need the additional condition (it is both necessary and sufficient) that S be order located: that is, for all real α, β with α < β, either β is an upper bound of S or else there exists s ∈ S with s > α. (Note that the “or” here is decidable: in constructive mathematics, to prove the disjunction p ∨ q, we must either produce a proof of p or else produce a proof of q.)

   Top of page

5. Does CM have any final products?

   Yuk! I hate those management jargon words like “final products”. However, since people use them in questioning what we do, we’d better deal with them, like it or not.

   What is the final product of any branch of pure mathematics? Do, for example, set theorists like Hugh Woodin, working with extremely high–level abstractions, have a final product? If the questioner means “something that has applications in the real world”, then it seems totally unreasonable to expect constructive analysis to justify itself by the production of such a final product when that justification is not required of classical pure mathematics. If pushed, however, I would say that the final product of all pure mathematics, constructive and nonconstructive, is a body of results, proofs and techniques that contribute to the higher levels of human culture and that may, (as history shows) frequently will, have significant applications in the future.

   Top of page

6. Is program extraction from constructive proofs a real thing?

   Yes, it is. Research groups in Japan, the States, the United Kingdom, Sweden and Germany have been active in this area for many years [14, 18, 23, 30] A constructive proof of (let's use this one again) Picard‘s Theorem PT_s really does contain an extractable algorithm for computing the point z with the properties stated in the conclusion of that theorem. Moreover, the proof is itself a proof that the program is correct—that is, meets its specifications. So the constructive result gives us two things for the price of one: an algorithm and a proof of its correctness. That's a real bargain!

   Top of page

7. What's the status of the Axiom of Choice?

   On one level, this one is relatively easy to answer: the full Axiom of Choice (AC),

   (1)

   ∀_x∈X ∃_y∈Y   P(x,y)   ⇒   ∃_{ƒ ∈Y ^X} ∀_x∈X   P(x,ƒ (x)),

   implies the Law of Excluded Middle (LEM), as was shown by Diaconescu [15] and later by Goodman–Myhill [17]. Contrary to a popular misconception that a dislike of, or disbelief in, AC is the reason why people do constructive mathematics, it is not AC, but LEM, that is the primary object of suspicion; However the fact that AC implies LEM confirms one’s instinct that AC is nonconstructive.

   In view of the Diaconescu–Goodman–Myhill theorem, what did Bishop mean when he said that under the hypotheses of (1),

   A choice function exists … because a choice is implied by the very meaning of existence?

   I believe that he meant that the constructive interpretation of the hypothesis in (1) is that there is an algorithm which leads us from elements x of X to elements y of Y such that P(x,y) holds. However, to compute the y from a given x, the algorithm will use not just the data describing x itself, but also the data proving that x satisfies the conditions for membership of the set A. Thus the algorithm will not be a function of x but a function of both x and its certificate of membership of A. The value at x of a genuine function from X to Y would depend only on x and not on its membership certificate.

   At a deeper level, the question is tricker to answer, at least if recast in the form, “What, if any, choice axioms are permissible in constructive mathematics?”. Some constructive mathematicians, notably Fred Richman, doubt the constructive validity of even countable choice (and hence of dependent choice). The argument in favour of countable choice is that one has to do no work to show that a natural number x belongs to the set N of natural numbers: each natural number is, as it were, its own certificate of membership of N. Thus in the case X = N, the choice algorithm implied “by the very meaning of existence” in (1) is, in fact, a genuine function on N. Needless to say, those who distrust even countable choice as a constructive principle do not buy into this argument.

   Top of page

090805

References

1. O. Aberth, Computable Analysis, McGraw–Hill, New York, 1980.
2. O. Aberth, Computable Calculus, Academic Press, San Diego, CA, 2001.
3. P. Aczel and M. Rathjen, Notes on Constructive Set Theory, Report No. 40, Institut Mittag–Leffler, Royal Swedish Academy of Sciences, 2001.
4. M.J. Beeson, Foundations of Constructive Mathematics, Springer–Verlag, Heidelberg, 1985.
5. E.A. Bishop, Foundations of Constructive Analysis, McGraw–Hill, New York, 1967.
6. E.A. Bishop, Schizophrenia in Contemporary Mathematics, Amer. Math. Soc. Colloquium Lectures, Univ. of Montana, Missoula; reprinted in: Contemporary Mathematics 39, 1–32, Amer. Math. Soc., 1985.
7. E.A. Bishop and D.S. Bridges, Constructive Analysis, Grundlehren der math. Wissenschaften 279, Springer–Verlag, 1985.
8. D.S. Bridges, “Constructive truth in practice”, in: Truth in Mathematics (Proceedings of the conference held at Mussomeli, Sicily, 13–21 September 1995, H.G. Dales and G. Oliveri, eds), 53–69, Oxford University Press, Oxford, 1997.
9. D.S. Bridges, “Constructive Mathematics: a Foundation for Computable Analysis”, Theor. Comp. Sci. 219 (1–2), 95-109, 1999.
10. D.S. Bridges and S. Reeves, “Constructive mathematics, in theory and programming practice”, Phil. Math. 7(1), 65–104, 1999.
11. D.S. Bridges and F. Richman, Varieties of Constructive Mathematics, London Math. Soc. Lecture Notes 97, Cambridge University Press, 1987.
12. D.S. Bridges, A. Calder, W. Julian, R. Mines, and F. Richman, “Picard's theorem”, Trans. Amer. Math. Soc. 269(2), 513–520, 1982.
13. L.E.J. Brouwer, “De onbetrouwbaarheid der logische principes”, Tijdschrift voor Wijsbegeerte 2, 152–158, 1908.
14. R.L. Constable et al., Implementing Mathematics with the Nuprl Proof Development System, Prentice–Hall, Englewood Cliffs, New Jersey, 1986.
15. R. Diaconescu, “Axiom of choice and complementation”, Proc. Amer. Math. Soc. 51, 176–178, 1975.
16. M.A.E. Dummett, Elements of Intuitionism (2/e), Oxford Logic Guides 28, Clarendon Press, Oxford, 2000.
17. N. D. Goodman and J. Myhill, “Choice Implies Excluded Middle”, Zeit. Math. Logik und Grundlagen der Math. 24, 461, 1975.
18. S. Hayashi and H. Nakano, PX: A Computational Logic, MIT Press, Cambridge MA, 1988.
19. A. Heyting, “Die formalen Regeln der intuitionistischen Logik”, Sitzungsber. preuss. Akad. Wiss. Berlin, 42–56, 1930.
20. A. Heyting, Intuitionism—An Introduction (Third Edition), North Holland, 1971.
21. Ker–I Ko,Complexity Theory of Real Functions, Birkhäuser, Boston, 1991.
22. B. Kushner, Lectures on Constructive Mathematical Analysis, Amer. Math. Soc., Providence RI, 1985.
23. P. Martin–Löf, “Constructive mathematics and computer programming”, in Proc. 6th. Int. Congress for Logic, Methodology and Philosophy of Science (L. Jonathan Cohen, ed.), North–Holland, Amsterdam, 1980.
24. R. Mines, F. Richman and W. Ruitenburg, A Course in Constructive Algebra, Universitext, Springer–Verlag, Heidelberg, 1988.
25. J. Myhill, “Constructive set theory”, J. Symbolic Logic 40(3), 347–382, 1975.
26. F. Richman (ed.), Constructive Mathematics (Proceedings of the Conference at Las Cruces, New Mexico, August 1980), Lecture Notes in Mathematics 873, Springer–Verlag, Heidelberg, 1981.
27. F. Richman, “Constructive mathematics without choice”, in: Reuniting the Antipodes—Constructive and Nonstandard Views of the Continuum (P. Schuster et al., eds), Synthèse Library 306, 199–205, Kluwer Academic Publishers, Amsterdam, 2001.
28. F. Richman, “Intuitionism as Generalization”, Philosophia Math. 5, 124–128, 1990.
29. F. Richman, “Interview with a Constructive Mathematician”, Modern Logic 6, 247–271, 1996.
30. H. Schwichtenberg, http://www.mathematik.uni-muenchen.de/~schwicht/.
31. G. Stolzenberg, Review of “Foundations of Constructive Analysis” [5], Bull, Amer. Math. Soc. 76, 301–323, 1970.
32. A.S. Troelstra, “Aspects of constructive mathematics”, in Handbook of Mathematical Logic (J. Barwise, ed.), 973–1052, North–Holland, Amsterdam, 1978.
33. A.S. Troelstra and D. van Dalen, Constructivism in Mathematics: An Introduction (two volumes), North–Holland, Amsterdam, 1988.
34. S. Warschawski, “Errett Bishop—In Memoriam”, Contemporary Mathematics 39, 33–39, Amer. Math. Soc., 1985.
35. K. Weihrauch, Computable Analysis, Springer–Verlag, Heidelberg, 2000.

070305