## Five stages of accepting constructive mathematics

HTML articles powered by AMS MathViewer

- by Andrej Bauer PDF
- Bull. Amer. Math. Soc.
**54**(2017), 481-498 Request permission

## Abstract:

On the odd day, a mathematician might wonder what constructive mathematics is all about. They may have heard arguments in favor of constructivism but are not at all convinced by them, and in any case they may care little about philosophy. A typical introductory text about constructivism spends a great deal of time explaining the principles and contains only trivial mathematics, while advanced constructive texts are impenetrable, like all unfamiliar mathematics. How then can a mathematician find out what constructive mathematics feels like? What new and relevant ideas does constructive mathematics have to offer, if any? I shall attempt to answer these questions.## References

- Steve Awodey and Michael A. Warren,
*Homotopy theoretic models of identity types*, Math. Proc. Cambridge Philos. Soc.**146**(2009), no. 1, 45–55. MR**2461866**, DOI 10.1017/S0305004108001783 - Stefan Banach and Alfred Tarski,
*Sur la décomposition des ensembles de points en parties respectivement congruentes*, Fundamenta Mathematicae**6**(1924), 244–277. - Andrej Bauer,
*An injection from the Baire space to natural numbers*, Math. Structures Comput. Sci.**25**(2015), no. 7, 1484–1489. MR**3391059**, DOI 10.1017/S0960129513000406 - Michael J. Beeson,
*Foundations of constructive mathematics*, Ergebnisse der Mathematik und ihrer Grenzgebiete (3) [Results in Mathematics and Related Areas (3)], vol. 6, Springer-Verlag, Berlin, 1985. Metamathematical studies. MR**786465**, DOI 10.1007/978-3-642-68952-9 - Errett Bishop,
*Foundations of constructive analysis*, McGraw-Hill Book Co., New York-Toronto, Ont.-London, 1967. MR**0221878** - Paul Cohen,
*The independence of the continuum hypothesis*, Proc. Nat. Acad. Sci. U.S.A.**50**(1963), 1143–1148. MR**157890**, DOI 10.1073/pnas.50.6.1143 - Paul J. Cohen,
*The independence of the continuum hypothesis. II*, Proc. Nat. Acad. Sci. U.S.A.**51**(1964), 105–110. MR**159745**, DOI 10.1073/pnas.51.1.105 - Radu Diaconescu,
*Axiom of choice and complementation*, Proc. Amer. Math. Soc.**51**(1975), 176–178. MR**373893**, DOI 10.1090/S0002-9939-1975-0373893-X - Eduardo J. Dubuc,
*$C^{\infty }$-schemes*, Amer. J. Math.**103**(1981), no. 4, 683–690. MR**623133**, DOI 10.2307/2374046 - Ryszard Engelking,
*General topology*, 2nd ed., Sigma Series in Pure Mathematics, vol. 6, Heldermann Verlag, Berlin, 1989. Translated from the Polish by the author. MR**1039321** - Paul R. Halmos,
*Naive set theory*, The University Series in Undergraduate Mathematics, D. Van Nostrand Co., Princeton, N.J.-Toronto-London-New York, 1960. MR**0114756** - J. M. E. Hyland,
*The effective topos*, The L.E.J. Brouwer Centenary Symposium (Noordwijkerhout, 1981) Studies in Logic and the Foundations of Mathematics, vol. 110, North-Holland, Amsterdam-New York, 1982, pp. 165–216. MR**717245** - Thomas Jech,
*Set theory*, Springer Monographs in Mathematics, Springer-Verlag, Berlin, 2003. The third millennium edition, revised and expanded. MR**1940513** - Peter T. Johnstone,
*The point of pointless topology*, Bull. Amer. Math. Soc. (N.S.)**8**(1983), no. 1, 41–53. MR**682820**, DOI 10.1090/S0273-0979-1983-15080-2 - Peter T. Johnstone,
*Stone spaces*, Cambridge Studies in Advanced Mathematics, vol. 3, Cambridge University Press, Cambridge, 1986. Reprint of the 1982 edition. MR**861951** - André Joyal,
*Une théorie combinatoire des séries formelles*, Adv. in Math.**42**(1981), no. 1, 1–82 (French, with English summary). MR**633783**, DOI 10.1016/0001-8708(81)90052-9 - Elisabeth Kübler-Ross,
*On death and dying*, New York, Routledge, 1969. - Saunders Mac Lane and Ieke Moerdijk,
*Sheaves in geometry and logic: A first introduction to topos theory*, Springer-Verlag, 1992. - F. William Lawvere,
*Qualitative distinctions between some toposes of generalized graphs*, Categories in computer science and logic (Boulder, CO, 1987) Contemp. Math., vol. 92, Amer. Math. Soc., Providence, RI, 1989, pp. 261–299. MR**1003203**, DOI 10.1090/conm/092/1003203 - Andrew M. Pitts,
*Nominal sets*, Cambridge Tracts in Theoretical Computer Science, vol. 57, Cambridge University Press, Cambridge, 2013. Names and symmetry in computer science. MR**3113350**, DOI 10.1017/CBO9781139084673 - Fred Richman,
*Intuitionism as generalization*, Philos. Math. (2)**5**(1990), no. 1-2, 124–128. MR**1061335**, DOI 10.1093/philmat/s2-5.1-2.124 - Giuseppe Rosolini,
*Un modello per la teoria intuizionista degli insiemi*, Atti degli Incontri di Logica Matematica (Siena) (C. Bernardi and P. Pagli, eds.), 1982, pp. 227–230. - Alex Simpson,
*Measure, randomness and sublocales*, Ann. Pure Appl. Logic**163**(2012), no. 11, 1642–1659. MR**2959665**, DOI 10.1016/j.apal.2011.12.014 - Raymon M. Smullyan,
*This book needs no title: A budget of living paradoxes*, Prentice-Hall, 1980. - Robert M. Solovay,
*A model of set-theory in which every set of reals is Lebesgue measurable*, Ann. of Math. (2)**92**(1970), 1–56. MR**265151**, DOI 10.2307/1970696 - Ernst Specker,
*Nicht konstruktiv beweisbare Sätze der Analysis*, J. Symbolic Logic**14**(1949), 145–158 (German). MR**31447**, DOI 10.2307/2267043 - Paul Taylor,
*A lambda calculus for real analysis*, J. Log. Anal.**2**(2010), Paper 5, 115. MR**2678927**, DOI 10.4115/jla.2010.2.5 - Anne S. Troelstra and Dirk van Dalen,
*Constructivism in mathematics, an introduction*, Studies in Logic and the Foundations of Mathematics., no. 121 and 123, North-Holland, 1988. - A. Tychonoff,
*Über die topologische Erweiterung von Räumen*, Math. Ann.**102**(1930), no. 1, 544–561 (German). MR**1512595**, DOI 10.1007/BF01782364 - The Univalent Foundations Program,
*Homotopy type theory: Univalent foundations of mathematics*, Institute for Advanced Study, 2013. - Jean van Heijenoort (ed.),
*From Frege to Gödel*, Harvard University Press, Cambridge, MA, 2002. A source book in mathematical logic, 1879–1931; Reprint of the third printing of the 1967 original [ MR0209111 (35 #15)]. MR**1890980** - Steven Vickers,
*Some constructive roads to Tychonoff*, From sets and types to topology and analysis, Oxford Logic Guides, vol. 48, Oxford Univ. Press, Oxford, 2005, pp. 223–238. MR**2188646**, DOI 10.1093/acprof:oso/9780198566519.003.0014 - Giuseppe Vitali,
*Sul problema della misura dei gruppi di punti di una retta*, Tech. report, Bologna, 1905. - Vladimir Voevodsky,
*The equivalence axiom and univalent models of type theory*(talk at CMU on February 4, 2010), ArXiv e-print 1402.5556 (2010). - Vladimir Voevodsky,
*Univalent foundations*(talk notes), https://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimir/files/2011_UPenn.pdf, September 2011. - Philip Wadler,
*Propositions as types*, Communications of the ACM**58**(2015), no. 12, 75–84.

## Additional Information

**Andrej Bauer**- Affiliation: Faculty of Mathematics and Physics, University of Ljubljana, Jadranska 19, SI-1000 Ljubljana, Slovenia
- MR Author ID: 640857
- Email: Andrej.Bauer@andrej.com
- Received by editor(s): July 1, 2016
- Published electronically: October 3, 2016
- Additional Notes: This material is based upon work supported by the Air Force Office of Scientific Research, Air Force Materiel Command, USAF under Award No. FA9550-14-1-0096
- © Copyright 2016 American Mathematical Society
- Journal: Bull. Amer. Math. Soc.
**54**(2017), 481-498 - MSC (2010): Primary 03F65
- DOI: https://doi.org/10.1090/bull/1556
- MathSciNet review: 3662915