Skip to main content
SpringerLink
Log in

On the Constructive and Computational Content of Abstract Mathematics

  • Chapter
  • First Online:
Mathesis Universalis, Computability and Proof

Part of the book series: Synthese Library ((SYLI,volume 412))

  • 220 Accesses

Abstract

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.

This work was supported by the International Research Staff Exchange Scheme (IRSES) Nr. 612638 CORCON and Nr. 294962 COMPUTAL of the European Commission and the Marie Curie RISE project CID (H2020-MSCA-RISE-2016-731143).

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 99.00
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 129.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 129.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    The BHK interpretation identifies proofs with computations or procedures. We prefer to speak of a correspondence.

References

  • Bell, J. L. (2008). The axiom of choice. Technical report, The Stanford Encyclopedia of Philosophy.

    Google Scholar 

  • 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 

  • Berger, U. (2011). From coinductive proofs to exact real arithmetic: Theory and applications. Logical Methods in Computer Science, 7(1), 1–24.

    Article  Google Scholar 

  • 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 

  • Berger, U., & Seisenberger, M. (2012). Proofs, programs, processes. Theory of Computing Systems, 51(3), 213–329. https://doi.org/10.1007/s00224-011-9325-8.

    Article  Google Scholar 

  • 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. https://doi.org/10.1007/978-3-642-22944-2_29.

  • Bishop, E., & Bridges, D. (1985). Constructive analysis (Grundlehren der mathematischen Wissenschaften 279). Berlin/Heidelberg/NewYork/Tokyo: Springer.

    Google Scholar 

  • Cohen, P. J. (1963). The independence of the continuum hypothesis. Proceedings of the U.S. National Academy of Sciences, 50, 1143–1148.

    Google Scholar 

  • Coquand, T., & Lombardi, H. (2006). A logical approach to abstract algebra. Mathematical Structures in Computer Science, 16, 885–900.

    Article  Google Scholar 

  • Diaconescu, R. (1975). Axiom of choice and complementation. Proceedings of the American Mathematical Society, 51, 176–178.

    Google Scholar 

  • 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.

    Book  Google Scholar 

  • 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 

  • Goodman, N., & Myhill, J. (1978). Choice implies excluded middle. The Zeitschrift für mathematische Logik und Grundlagen der Mathematik, 23, 461.

    Article  Google Scholar 

  • 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 

  • 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 

  • Kleene, S. C. (1945). On the interpretation of intuitionistic number theory. The Journal of Symbolic Logic, 10, 109–124.

    Article  Google Scholar 

  • Martin-Löf, P. (1984). Intuitionistic type theory. Napoli: Bibliopolis.

    Google Scholar 

  • Raoult, J.-C. (1988). Proving open properties by induction. Information Processing Letters, 29, 19–23.

    Article  Google Scholar 

  • 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 

  • Rinaldi, D., & Schuster, P. (2016). A universal Krull-Lindenbaum theorem. Journal of Pure and Applied Algebra, 220(9), 3207–3232.

    Article  Google Scholar 

  • 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 

  • Schwichtenberg, H., & Wainer, S. S. (2012). Proofs and computations. Cambridge: Cambridge University Press.

    Google Scholar 

  • The Minlog System. http://www.mathematik.uni-muenchen.de/$sim$minlog/

  • Troelstra, A. S. (1973). Metamathematical investigation of intuitionistic arithmetic and analysis (Volume 344 of lecture notes in mathematics). Berlin/Heidelberg/New York: Springer.

    Book  Google Scholar 

  • Veldman, V. (2001). Brouwer’s real thesis on bars. Philosophia Scientiæ, Constructivism: Mathematics, Logic, Philosophy and Linguistics, 6, 21–42.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Swansea University, Swansea, UK

    Ulrich Berger

Authors
  1. Ulrich Berger
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Ulrich Berger .

Editor information

Editors and Affiliations

  1. Institute of Philosophy, Technical University of Berlin, Berlin, Germany

    Stefania Centrone

  2. Department of Philosophy, University of Helsinki, Helsinki, Finland

    Sara Negri

  3. University of Hamburg, Hamburg, Germany

    Deniz Sarikaya

  4. Dipartimento di Informatica, Università degli Studi di Verona, Verona, Italy

    Peter M. Schuster

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Berger, U. (2019). On the Constructive and Computational Content of Abstract Mathematics. In: Centrone, S., Negri, S., Sarikaya, D., Schuster, P.M. (eds) Mathesis Universalis, Computability and Proof. Synthese Library, vol 412. Springer, Cham. https://doi.org/10.1007/978-3-030-20447-1_6

Download citation

Publish with us

Policies and ethics

Search

Navigation