On the Constructive and Computational Content of Abstract Mathematics

  • Ulrich BergerEmail author
Part of the Synthese Library book series (SYLI, volume 412)


This essay describes an approach to constructive mathematics based on abstract i.e. axiomatic mathematics. Rather than insisting on structures to be explicitly constructed, constructivity is defined by the sole requirement that proofs have computational content. It is shown that this approach is compatible with restricted forms of classical logic and choice principles.


  1. Bell, J. L. (2008). The axiom of choice. Technical report, The Stanford Encyclopedia of Philosophy.Google Scholar
  2. Berger, U. (2010). Realisability for induction and coinduction with applications to constructive analysis. The Journal of Universal Computer Science, 16(18), 2535–2555.Google Scholar
  3. Berger, U. (2011). From coinductive proofs to exact real arithmetic: Theory and applications. Logical Methods in Computer Science, 7(1), 1–24.CrossRefGoogle Scholar
  4. Berger, U., & Petrovska, O. (2018). Optimized program extraction for induction and coinduction. In CiE 2018 (Volume 10936 of LNCS, pp. 70–80). Berlin/Heidelberg/New York: Springer.Google Scholar
  5. Berger, U., & Seisenberger, M. (2012). Proofs, programs, processes. Theory of Computing Systems, 51(3), 213–329. Scholar
  6. Berger, U., Miyamoto, K., Schwichtenberg, H., & Seisenberger, M. (2011). Minlog – a tool for program extraction for supporting algebra and coalgebra. In CALCO-Tools (Volume 6859 of LNCS, pp. 393–399). Berlin/Heidelberg/New York: Springer.
  7. Bishop, E., & Bridges, D. (1985). Constructive analysis (Grundlehren der mathematischen Wissenschaften 279). Berlin/Heidelberg/NewYork/Tokyo: Springer.Google Scholar
  8. Cohen, P. J. (1963). The independence of the continuum hypothesis. Proceedings of the U.S. National Academy of Sciences, 50, 1143–1148.Google Scholar
  9. Coquand, T., & Lombardi, H. (2006). A logical approach to abstract algebra. Mathematical Structures in Computer Science, 16, 885–900.CrossRefGoogle Scholar
  10. Diaconescu, R. (1975). Axiom of choice and complementation. Proceedings of the American Mathematical Society, 51, 176–178.Google Scholar
  11. Gierz, G., Hofmann, K. H., Keimel, K., Lawson, J. D., Mislove, M., & Scott, D. S. (2003). Continuous lattices and domains (Volume 93 of encyclopedia of mathematics and its applications). Cambridge: Cambridge University Press.CrossRefGoogle Scholar
  12. Gödel, K. (1940). The consistency of the axiom of choice and of the generalized continuum-hypothesis with the axioms of set theory (Annals of mathematics studies, Vol. 3). Princeton: Princeton University Press.Google Scholar
  13. Goodman, N., & Myhill, J. (1978). Choice implies excluded middle. The Zeitschrift für mathematische Logik und Grundlagen der Mathematik, 23, 461.CrossRefGoogle Scholar
  14. Hendtlass, M., & Schuster, P. (2012). A direct proof of Wiener’s theorem. In A. Dawar & B. Löwe (Eds.), CiE 2012: How the World Computes (Volume 7318 of lecture notes in computer science). Springer.Google Scholar
  15. Howard, W. A. (1980). The formulae-as-types notion of construction. In J. P. Seldin & J. R. Hindley (Eds.), To H.B. Curry: Essays on combinatory logic, lambda calculus and formalism (pp. 479–490). London/New York: Academic.Google Scholar
  16. Kleene, S. C. (1945). On the interpretation of intuitionistic number theory. The Journal of Symbolic Logic, 10, 109–124.CrossRefGoogle Scholar
  17. Martin-Löf, P. (1984). Intuitionistic type theory. Napoli: Bibliopolis.Google Scholar
  18. Raoult, J.-C. (1988). Proving open properties by induction. Information Processing Letters, 29, 19–23.CrossRefGoogle Scholar
  19. Richman, F. (2001). Constructive mathematics without choice. In P. Schuster, U. Berger, & H. Osswald (Eds.), Reuniting the Antipodes–Constructive and Nonstandard Views of the Continuum (Volume 306 of synthese library, pp. 199–205). Kluwer.Google Scholar
  20. Rinaldi, D., & Schuster, P. (2016). A universal Krull-Lindenbaum theorem. Journal of Pure and Applied Algebra, 220(9), 3207–3232.CrossRefGoogle Scholar
  21. Schwichtenberg, H. (2006). Minlog. In F. Wiedijk (Ed.), The seventeen provers of the world (Number 3600 in lecture notes in artificial intelligence, pp. 151–157). Berlin/Heidelberg: Springer.Google Scholar
  22. Schwichtenberg, H., & Wainer, S. S. (2012). Proofs and computations. Cambridge: Cambridge University Press.Google Scholar
  23. Troelstra, A. S. (1973). Metamathematical investigation of intuitionistic arithmetic and analysis (Volume 344 of lecture notes in mathematics). Berlin/Heidelberg/New York: Springer.CrossRefGoogle Scholar
  24. Veldman, V. (2001). Brouwer’s real thesis on bars. Philosophia Scientiæ, Constructivism: Mathematics, Logic, Philosophy and Linguistics, 6, 21–42.Google Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.Department of Computer ScienceSwansea UniversitySwanseaUK

Personalised recommendations