Five stages of accepting constructive mathematics

Bauer, Andrej

doi:10.1090/bull/1556

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.