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).
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 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.
Berger, U. (2010). Realisability for induction and coinduction with applications to constructive analysis. The Journal of Universal Computer Science, 16(18), 2535–2555.
Berger, U. (2011). From coinductive proofs to exact real arithmetic: Theory and applications. Logical Methods in Computer Science, 7(1), 1–24.
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.
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.
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.
Cohen, P. J. (1963). The independence of the continuum hypothesis. Proceedings of the U.S. National Academy of Sciences, 50, 1143–1148.
Coquand, T., & Lombardi, H. (2006). A logical approach to abstract algebra. Mathematical Structures in Computer Science, 16, 885–900.
Diaconescu, R. (1975). Axiom of choice and complementation. Proceedings of the American Mathematical Society, 51, 176–178.
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.
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.
Goodman, N., & Myhill, J. (1978). Choice implies excluded middle. The Zeitschrift für mathematische Logik und Grundlagen der Mathematik, 23, 461.
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.
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.
Kleene, S. C. (1945). On the interpretation of intuitionistic number theory. The Journal of Symbolic Logic, 10, 109–124.
Martin-Löf, P. (1984). Intuitionistic type theory. Napoli: Bibliopolis.
Raoult, J.-C. (1988). Proving open properties by induction. Information Processing Letters, 29, 19–23.
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.
Rinaldi, D., & Schuster, P. (2016). A universal Krull-Lindenbaum theorem. Journal of Pure and Applied Algebra, 220(9), 3207–3232.
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.
Schwichtenberg, H., & Wainer, S. S. (2012). Proofs and computations. Cambridge: Cambridge University Press.
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.
Veldman, V. (2001). Brouwer’s real thesis on bars. Philosophia Scientiæ, Constructivism: Mathematics, Logic, Philosophy and Linguistics, 6, 21–42.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this chapter
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
DOI: https://doi.org/10.1007/978-3-030-20447-1_6
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-20446-4
Online ISBN: 978-3-030-20447-1
eBook Packages: Religion and PhilosophyPhilosophy and Religion (R0)