Abstract
The goal of this paper is to discuss the following question: is the theory of recursive functions needed for a rigorous development of constructive mathematics? I will try to present the point of view of constructive mathematics on this question. The plan is the following: I first explain the gradual loss of appreciation of constructivity after 1936, clearly observed by Heyting and Skolem, in connection with the development of recursivity. There is an important change in 1967, publication of Bishop’s book, and the (re)discovery that the theory of recursive functions is actually not needed for a rigorous development of constructive mathematics. I then end with a presentation of the current view of constructive mathematics: mathematics done using intuitionistic logic, view which, surprisingly, does not rely on any explicit notion of algorithm.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
As is well known, there are several different equivalent form of this definition, but the discussion that follows apply for these variants as well.
- 2.
We stress that we limit our discussion to the notion of total recursive functions, and do not consider partial recursive functions, introduced by Kleene. Only total recursive functions are relevant for an explanation of the notion of functions in constructive mathematics, which are total by definition Bishop (1967) and Richman (1990).
- 3.
This problem does not appear using a constructive meta-level, since, in this case, we can only consider f to be a function when we can decide, for each n, whether or not there is n consecutive 7 in the decimal development of π.
- 4.
As noticed in Heyting’s paper (1961), and as is also stressed in Kreisel’s review of this paper, such infinitary notions are naturally and elegantly expressed using generalised inductive definitions in an intuitionistic metatheory.
References
Bishop, E. (1967). Foundations of constructive mathematics (xiii+370pp). New York/Toronto/ Ont.-London: McGraw-Hill.
Borel, E. (1908). Les “Paradoxes” de la théorie des ensembles. Ann. Sci. Ecole Norm Sup, 25, 443–338.
Bridges, D.S. (1999). Constructive mathematics: a foundation for computable analysis. Theoretical Computer Science, 219, 95–109.
Brouwer, L. (1918). Begründung der Mengenlehre unabhängig vom logish‘chen Satz vom ausgeschlossenen Dritten. Ester Teil. Verh. Nederl. Akad. Wetensch. Afd. Natuurk., Sct. I, 12(5), 3–43.
Coquand, Th., & Lombardi, H. (2006). A logical approach to abstract algebra. Mathematical Structures in Computer Science, 16(5), 885–900.
Church, A. (1946). Review of Novikoff’s (1943). Journal of Symbolic Logic, 11(4), 129–131.
Van Heijenoort, J. (1977). From Frege to Gödel: a source book in mathematical logic, 1879–1931 (Vol. 9). Cambridge: Harvard University Press.
Heyting, A. (1930). Die formalen Regeln der intuitionistischen Logik. I, II, III. Sitzungsberichte Akad. Berlin (pp. 42–56, 57–71, 158–169).
Heyting, A. (1957). Some remarks on intuitionism. In Proceedings of colloquium on constructivity in mathematics, Amsterdam, pp. 69–71.
Heyting, A. (1958). Intuitionism in mathematics. In R. Klibansky (Ed.), Philosophy in the mid-century: A survey (Vol. 1, pp. 101–115). Logic and philosophy of science. Florenc: La Nuova Italia Editrice.
Heyting, A. (1961). Infinitistic methods from a finitist point of view. Proceedings of the symposium on foundations of mathematics on infinitistic methods, Warsaw, 1959 (pp. 185–192). Oxford/London/New York/Paris: Pergamon.
Heyting, A. (1962). After thirty years. In Logic, methodology and philosophy of science (pp. 194–197). Stanford: Stanford University Press.
Heyting, A. (1962). After thirty years. In N. Ernest, S. Patrick, T. Alfred (Eds.), Proceedings of the 1960 international congress on logic, methodology and philosophy of science (pp. 194–197). Stanford: Stanford University Press.
Kleene, S. C. (1936). General recursive functions on natural numbers. Mathematische Annalen, 112, 727–742.
Kleene, S. C. (1952). Introduction to metamathematics (x+550pp). New York: D. Van Nostrand.
Lorenzen, P. (1951). Algebraische und logistische Untersuchungen über freie Verbände. Journal of Symbolic Logic, 16, 81–106.
Martin-Löf, P. (1970). Notes on constructive mathematics (109pp). Stockholm: Almqvist and Wiksell.
Martin-Löf, P. (1984). Intuitionistic type theory. Bibliopolis: Napoli.
Mines, R., Richman, W., & Ruitenburg, W. (1988). A course in constructive algebra. Heidelberg: Springer.
Mints, G. (1991). Proof theory in the USSR: 1925–1969. Journal of Symbolic Logic, 56(2), 385–424.
Novikoff, P. S. (1943). On the consistency of certain logical calculus. Rec. Math. [Mat. Sbornik] N.S., 12(54), 231–261.
Rathjen, M. (2005). The constructive Hilbert program and the limits of Martin-Löf type theory. Synthese, 147(1), 81–120.
Richman, F. (1990). Intuitionism as a generalisation. Philosophia Mathematica (2), 5, 124–128.
Sambin, G. (1987). Intuitionistic formal spaces—a first communication. Mathematical logic and its applications (Druzhba, 1986) (pp. 187–204). New York: Plenum.
Sanin. (1958). A constructive interpretation of mathematical judgments (Russian). Trudy Mat. Inst. Steklov., 52, 226–311.
Shoenfield, J. R. (1967). Mathematical logic. Reading: Addison-Wesley.
Skolem, T. (1955). A critical remark on foundational research. Norske Vid. Selsk. Forh., Trondheim, 28, 100–105.
Stolzenberg, G. (1970). Review: Foundations of constructive analysis by Errett Bishop. Bulletin of the American Mathematical Society, 76, 301–323.
Wang, H. (1951). Review of P. Lorenzen Algebraische und logistische Untersuchungen über freie Verbände. Journal of Symbolic Logic, 16, 269–272.
Acknowledgements
I would like to thank Göran Sundholm for interesting discussions on the topic of this paper and for sending me the references (Heyting 1957).
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer Science+Business Media Dordrecht
About this chapter
Cite this chapter
Coquand, T. (2014). Recursive Functions and Constructive Mathematics. In: Dubucs, J., Bourdeau, M. (eds) Constructivity and Computability in Historical and Philosophical Perspective. Logic, Epistemology, and the Unity of Science, vol 34. Springer, Dordrecht. https://doi.org/10.1007/978-94-017-9217-2_6
Download citation
DOI: https://doi.org/10.1007/978-94-017-9217-2_6
Published:
Publisher Name: Springer, Dordrecht
Print ISBN: 978-94-017-9216-5
Online ISBN: 978-94-017-9217-2
eBook Packages: Humanities, Social Sciences and LawPhilosophy and Religion (R0)