Skip to main content
SpringerLink
Log in

From Mathesis Universalis to Provability, Computability, and Constructivity

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

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

  • 219 Accesses

Abstract

This paper advocates for a revival of Leibniz’ mathesis universalis as proof theory together with his claim for theoria cum praxi under the conditions of modern foundational research of mathematics and computer science. After considering the development from Leibniz’ mathesis universalis to Turing computability (Chap. 1), current foundational research programs are analyzed. They connect proof theory with computational applications - proof mining with program extraction (Chap. 2), reverse mathematics with constructivity (Chap. 3) and intuitionistic type theory with proof assistants (Chap. 4). The foundational program of univalent mathematics is inspired by the idea of a proof-checking software to guarantee correctness, trust and security in mathematics (Chap. 5). In the age of digitalization, correctness, security and trust in algorithms turn out to be general problems of computer technology with deep societal impact. They should be tackled by mathesis universalis as proof theory (Chap. 6).

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.

    Mackensen (1974).

  2. 2.

    Leibniz (1666).

  3. 3.

    An interpretation of ars iudicandi as effective decidability and ars inveniendi as effective enumerability was discussed by Hermes (1969a).

  4. 4.

    Scholz (1961).

  5. 5.

    Turing (1936).

  6. 6.

    Minsky (1961), Sheperdson and Sturgis (1963).

  7. 7.

    Turing (1936).

  8. 8.

    Post (1936).

  9. 9.

    A survey on the interdisciplinary influence of this concept was given in Herken (1995).

  10. 10.

    Kleene (1974) and Shoenfield (1967).

  11. 11.

    Davis (1958), Soare (2016).

  12. 12.

    Hermes (1969b).

  13. 13.

    Gödel (1931).

  14. 14.

    Chaitin (1998).

  15. 15.

    Hilbert (1900).

  16. 16.

    Matiyasevich (1970, 1993).

  17. 17.

    Davis et al. (1961).

  18. 18.

    Euclid (1782), 63; Aigner, Ziegler (2001), 3.

  19. 19.

    Pinasco (2009).

  20. 20.

    Feferman (1996).

  21. 21.

    Kohlenbach (2008), 13.

  22. 22.

    Kohlenbach (2008), 14.

  23. 23.

    Mainzer (1970).

  24. 24.

    Heyting (1934) and Kolmogorov (1932).

  25. 25.

    Gödel (1958).

  26. 26.

    Moschovakis (1997).

  27. 27.

    Schwichtenberg, Wainer (2012), 389 f.

  28. 28.

    Schwichtenberg (2006).

  29. 29.

    Pappos (1876–1878 II, 634 ff).

  30. 30.

    Hintikka and Remes (1974) and Mainzer (1980, 1994, 120 ff).

  31. 31.

    Friedman (1975, 2000).

  32. 32.

    Simpson (1999, 2005).

  33. 33.

    Bishop (1967).

  34. 34.

    Ebbinghaus et al. (1991), chapter 2.

  35. 35.

    Weyl (1918).

  36. 36.

    Lorenzen (1955, 1965).

  37. 37.

    Feferman (1964, 1968), Mainzer (1973) and Jäger and Sieg (2017).

  38. 38.

    Ishihara (2005, 2006).

  39. 39.

    Brouwer (1907).

  40. 40.

    Berger and Ishahara (2005).

  41. 41.

    Troelstra and van Dalen (1988, 220).

  42. 42.

    Howard (1969).

  43. 43.

    Dybjer and Palmgren (2016).

  44. 44.

    Martin-Löf (1971a, b, 1998).

  45. 45.

    Martin-Löf (1975).

  46. 46.

    Grothendieck et al. (1971–1977).

  47. 47.

    Martin-Löf (2009).

  48. 48.

    Martin-Löf (1975).

  49. 49.

    Martin-Löf (1982).

  50. 50.

    Aczel (1978).

  51. 51.

    Palmgren (1998), Rathjen et al. (1998) and Setzer (2000)

  52. 52.

    Coquand and Huet (1988).

  53. 53.

    Bertot, Castéran (2004).

  54. 54.

    Gonthier (2008).

  55. 55.

    Di Risi (2015).

  56. 56.

    Leibniz (1679).

  57. 57.

    Spanier (1966).

  58. 58.

    Eilenberg and Cartan (1956).

  59. 59.

    Hazewinkel (2001).

  60. 60.

    Awodey and Warren (2009).

  61. 61.

    Hofmann and Streicher (1998).

  62. 62.

    The Univalent Foundations Program (2013).

  63. 63.

    Bezem et al. (2014).

  64. 64.

    Voevodsky (2012) and Joyal (2002).

  65. 65.

    Knobloch (1987).

  66. 66.

    Durkheim (1893).

  67. 67.

    obituary of Vladimir Voevodsky 1966–2017, Institute for Advanced Study October 04 2017, 5 (https://www.ias.edu/news/2017/vladimir-voevodsky-obituary).

  68. 68.

    Weyl (1921).

  69. 69.

    Churchland, Sejnowski (1992) and Mainzer (1994, 1997).

  70. 70.

    Mainzer (2007) and Mainzer and Chua (2011, 2013).

  71. 71.

    Mainzer (2016, 2018b).

  72. 72.

    Mitchell (1997).

  73. 73.

    Bojarski et al. (2017).

  74. 74.

    Pomerleau (1989) and Pfeifer and Scheier (2001).

  75. 75.

    Kalra and Paddock (2016).

  76. 76.

    Knight (2017, 4)

  77. 77.

    Mainzer et al. (2018) and Mainzer (2018a, b).

References

  • Aczel, P. (1978). The type theoretic interpretation of constructive set theory. In A. Macintyre, L. Pacholski, & J. Paris (Eds.), Logic Colloquium ‘77 (pp. 55–66). Amsterdam/New York: North-Holland.

    Google Scholar 

  • Aigner, M., & Ziegler, G.M. (2001). Proofs from The Book (2nd ed.). Berlin: Springer.

    Google Scholar 

  • Awodey, S., & Warren, M. A. (2009). Homotopy theoretic models of identity type. Mathematical Proceedings of the Cambridge Philosophical Society, 146(1), 45–55.

    Google Scholar 

  • Berger, J., & Ishahara, H. (2005). Brouwer’s fan theorem and unique existence in constructive analysis. Mathematical Logic Quarterly, 51, 360–364.

    Google Scholar 

  • Bertot, Y., & Castéran, P. (2004). Interactive theorem proving and program development. Coq’Art: The calculus of inductive constructions. Springer: New York.

    Google Scholar 

  • Bezem, M., Coquand, T., & Huber, S. (2014). A model of type theory in cubical sets. In R. Matthes & A. Schubert (Eds.), 19th international conference on types for proofs and programs (TYPES 2013) (pp. 107–128). Dagstuhl: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik.

    Google Scholar 

  • Bishop, E. (1967). Foundations of constructive analysis. New York: McGraw-Hill.

    Google Scholar 

  • Bojarski, M., Yeres, P., Choromanska, A., Xhoromanski, K., Firner, B., Jackel, L., & Müller, U. (2017). Explaining how a deep learning network trained with end-to-end learning steers a car. https://arxiv.org/abs/1704.07911 (2018/01/26).

  • Brouwer, L. E. J. (1907). Over de Grondslagen der Wiskunde [On the foundations of mathematics]. Amsterdam: Maas & Van Suchtelen.

    Google Scholar 

  • Chaitin, G. J. (1998). The limits of mathematics. Singapore: Springer.

    Google Scholar 

  • Churchland, P. S., & Sejnowski, T. J. (1992). The computational brain. Cambridge, MA: MIT Press.

    Google Scholar 

  • Coquand, T., & Huet, G. (1988). The calculus of constructions. Information and Computation, 76(2–3), 95–120.

    Google Scholar 

  • Davis, M. (1958). Computability & unsolvability. New York: McGraw-Hill.

    Google Scholar 

  • Davis, M., Putnam, H., & Robinson, J. (1961). The decision problem for exponential Diophantine equations. Annals of Mathematics II, 74, 425–436.

    Google Scholar 

  • De Risi, V. (2015). Analysis situs, the foundations of Mathematics and a geometry of space. In The Oxford’s handbook of Leibniz. Online publication: e-ISBN: 9780199984060. https://doi.org/10.1093/oxfordhb/9780199744725.013.22.

  • Durkheim, E. (1893). De la division du travail social. Étude sur l’organisation des sociétés supérieures. Félix Alcan: Paris.

    Google Scholar 

  • Dybjer, P., & Palmgren, E. (2016). Intuitionistic type theory. In The Stanford encyclopedia of philosophy, the metaphysics research lab (CSLI). Stanford: Stanford University. (open access).

    Google Scholar 

  • Ebbinghaus, H.-D., Hermes, H., Hirzebruch, F., Koecher, M., Mainzer, K., Neukirch, J., Prestel, A., & Remmert, R. (1991). Numbers. Berlin: Springer. (German 1983 3rd edition).

    Google Scholar 

  • Eilenberg, S., & Cartan, H. (1956). Homological algebra. Princeton University Press: Princeton.

    Google Scholar 

  • Euclid. (1782). The elements of Euclid (with Dissertations). J. Williamson (translator and commentator). Clarendon Press: Oxford.

    Google Scholar 

  • Feferman, S. (1964). Systems of predicative analysis. Journal of Symbolic Logic, 29, 1–30.

    Google Scholar 

  • Feferman, S. (1968). Systems of predicative analysis II: Representations of ordinals. Journal of Symbolic Logic, 53, 193–213.

    Google Scholar 

  • Feferman, S. (1996). Kreisel’s “unwinding” program. In P. Odifreddi (Ed.), Kreisleriana. About and around Georg Kreisel. Review of modern logic, A.K. Peters/CRC Press, (pp. 247–273).

    Google Scholar 

  • Friedman, H. (1975). Some systems of second order arithmetic and their use. In Proceedings of the international congress of mathematicians (Vancouver, BC, 1974), (Vol. 1, pp. 235–242). Montreal: Canadian Mathematical Congress.

    Google Scholar 

  • Friedman, H., & Simpson, S. G. (2000). Issues and problems in reverse mathematics. In Computability theory and its applications. Contemporary mathematics (Vol. 257, pp. 127–144).

    Google Scholar 

  • Gödel, K. (1931). Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I. Monatshefte für Mathematik und Physik, 38(1), 173–198.

    Google Scholar 

  • Gödel, K. (1958). Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes. Dialectica, 12, 280–287.

    Google Scholar 

  • Gonthier, G. (2008). Formal proof – The four-color theorem. Notices of the American Mathematical Society, 55(11), 1382–1393.

    Google Scholar 

  • Grothendieck, A., et al. (1971–1977). Séminaire de Géométrie Algébrique (Vol. 1–7). Berlin: Springer.

    Google Scholar 

  • Hazewinkel, M. (2001). Homotopy. In M. Hazewinkel (Ed.), Encyclopedia of mathematics. New York: Springer.

    Google Scholar 

  • Herken, R. (Ed.). (1995). The universal Turing machine. A half-century survey. Wien: Springer.

    Google Scholar 

  • Hermes, H. (1969a). Ideen von Leibniz zur Grundlagenforschung: Die ars inveniendi und die ars iudicandi. In: Studia Leibnitiana. Suppl. III (pp. 92–102). Wiesbaden: Steiner

    Google Scholar 

  • Hermes, H. (1969b). Enumerability, decidability, computability. Berlin: Springer.

    Google Scholar 

  • Heyting, A. (1934). Mathematische Grundlagenforschung. Intuitionismus. Beweistheorie. Berlin: Springer. reprint 1974.

    Google Scholar 

  • Hilbert, D. (1900). Mathematische Probleme. In: Nachrichten der Königlichen Gesellschaft der Wissenschaften zu Göttingen, mathematisch-physikalische Klasse. Heft, 3, 253–297.

    Google Scholar 

  • Hintikka, J., & Remes, U. (1974). The method of analysis – Its geometrical origin and its general significance. Dordrecht: North-Holland.

    Google Scholar 

  • Hofmann, M., & Streicher, T. (1998). The groupoid interpretation of type theory. In G. Sambin & J. M. Smith (Eds.), Twenty five years of constructive type theory (pp. 83–112). Oxford: Clarendon Press.

    Google Scholar 

  • Howard, W. A. (1969). 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). Boston: Academic. 1980.

    Google Scholar 

  • Ishahara, H. (2006). Reverse mathematics in Bishop’s constructive mathematics. Philosophia Scientiae, 6, 43–59.

    Google Scholar 

  • Ishihara, H. (2005). Constructive reverse mathematics. Compactness properties (Oxford Logic Guides 48) (pp. 245–267). Oxford: Oxford University Press.

    Google Scholar 

  • Jäger, G., & Sieg, W. (Eds.). (2017). Feferman on foundations: Logic, mathematics, philosophy. New York: Springer.

    Google Scholar 

  • Joyal, A. (2002). Quasi-categories and Kan complexes. Journal of Pure and Applied Algebra, 175, 207–222.

    Google Scholar 

  • Kalra, N., & Paddock, S. M. (2016). Driving to safety: How many miles of driving would it take to demonstrate autonomous vehicle reliability? Santa Monica: RAND Corporation. (ISBN 9780833095299).

    Google Scholar 

  • Kleene, S. C. (1974). Introduction to metamathematics (7th ed.). Amsterdam: North Holland.

    Google Scholar 

  • Knight, W. (2017, April 11). The dark secret at the heart of AI. MIT Technology Review, 1–22. https://www.technologyreview.com/s/604087/the-dark-secret-at-the-heart-of-AI

  • Knobloch, E. (1987). Theoria cum Praxi. Leibniz und die Folgen für Wissenschaft und Technik. Studia Leibnitiana, 19, 129–147.

    Google Scholar 

  • Kohlenbach, U. (2008). Applied proof theory: Proof interpretations and their use in mathematics. Berlin: Springer.

    Google Scholar 

  • Kolmogorov, A. N. (1932). Zur Deutung der intuitionistischen Logik. Mathematische Zeitschrift, 35, 58–65.

    Google Scholar 

  • Leibniz, G. W. (1666). Dissertation on the art of combinations. In Philosophical papers and letters (L. E. Loemker, Ed. and Trans., pp. 73–84).

    Google Scholar 

  • Leibniz, G. W. (1679). Studies in a geometry of situation with a letter to Christian Huygens. In: Philosophical papers and letters (L. E. Loemker, Ed. and Trans., Vol. I). Chicago 1956, pp. 381–396.

    Google Scholar 

  • Lorenzen, P. (1955). Einführung in die operative Logik und Mathematik. Berlin: Springer.

    Google Scholar 

  • Lorenzen, P. (1965). Differential und Integral. Eine konstruktive Einführung in die klassische Analysis. Frankfurt: Akademische Verlagsgesellschaft.

    Google Scholar 

  • Mainzer, K. (1970). Der Konstruktionsbegriff in der Mathematik. Philosophia Naturalis, 12, 367–412.

    Google Scholar 

  • Mainzer, K. (1973). Mathematischer Konstruktivismus. Münster: Ph.D. U.

    Google Scholar 

  • Mainzer, K. (1980). Geschichte der Geometrie. Mannheim: B.I. Wissenschaftsverlag.

    Google Scholar 

  • Mainzer, K. (1994). Computer – Neue Flügel des Geistes? Berlin/New York: De Gruyter.

    Google Scholar 

  • Mainzer, K. (1997). Gehirn, Computer, Komplexität. Berlin: Springer.

    Google Scholar 

  • Mainzer, K. (2007). Thinking in complexity. The computational dynamics of matter, mind, and mankind (5th ed.). Berlin: Springer.

    Google Scholar 

  • Mainzer, K. (2016). Künstliche Intelligenz. Wann übernehmen die Maschinen? Springer: Berlin.

    Google Scholar 

  • Mainzer, K. (2018a). The digital and the real world. Computational foundations of mathematics, science, technology and philosophy. Singapore: World Scientific Singapore.

    Google Scholar 

  • Mainzer, K. (2018b). Artificial intelligence and machine learning – Algorithmic foundations and philosophical perspectives. Journal of Shanghai Normal University (Philosophy & Social Sciences Edition)., 48(3).

    Google Scholar 

  • Mainzer, K., & Chua, L. O. (2011). The universe as automaton. From simplicity and symmetry to complexity. Springer: Berlin.

    Google Scholar 

  • Mainzer, K., & Chua, L. (2013). Local activity principle. London: Imperial College Press.

    Google Scholar 

  • Mainzer, K., Schuster, P., & Schwichtenberg, H. (Eds.). (2018). Proof and computation. Digitization in mathematics, computer science, and philosophy. Singapore: World Scientific Singapore.

    Google Scholar 

  • Martin-Löf, P. (1971a). On the strength of intuitionistic reasoning (Contribution to the Symposium on Perspectives in the Philosophy of Mathematics at the IVth International congress of Logic, Methodology, and Philosophy of Science, Bucharest, August 29–September 4). (Unpublished typed paper).

    Google Scholar 

  • Martin-Löf, P. (1971b). A theory of types (Technical report 71-3). Stockholm: University of Stockholm.

    Google Scholar 

  • Martin-Löf, P. (1975). An intuitionistic theory of types: Predicative part. In H. E. Rose & J. Shepherdson (Eds.), Logic Colloquium ‘73 (pp. 73–118). Amsterdam: North-Holland.

    Google Scholar 

  • Martin-Löf, P. (1982). Constructive mathematics and computer programming. In L. J. Cohen, J. Los, H. Pfeiffer, & K.-P. Podewski (Eds.), Logic, methodology and philosophy of science VI, proceedings of the 1979 international congress at Hannover, Germany (pp. 153–175). Amsterdam: North- Holland Publishing Company.

    Google Scholar 

  • Martin-Löf, P. (1998). An intuitionistic theory of types. Twenty-five years of constructive type theory (Venice, 1995). In Oxford logic guides (Vol. 36, pp. 127–172). New York: Oxford University Press.

    Google Scholar 

  • Martin-Löf, P. (2009). 100 years of Zermelo’s axiom of choice: What was the problem with it? In S. Lindström, E. Palmgren, K. Segerberg, & V. Stoltenberg-Hansen (Eds.), Logicism, intuitionism, and formalism: What has become of them? (pp. 209–219). Dordrecht: Springer.

    Google Scholar 

  • Matiyasevich, Y. V. (1970). Enumerable sets are diophantic. Soviet Mathematics: Doklady, 11, 345–357.

    Google Scholar 

  • Matiyasevich, Y. V. (1993). Hilbert’s tenth problem. Cambridge, MA: The MIT Press.

    Google Scholar 

  • Minsky, M. L. (1961). Recursive unsolvability of Post’s problem of “tag” and other topics in the theory of turing machines. Annals of Mathematics, 74, 437–454.

    Google Scholar 

  • Mitchell, T. M. (1997). Machine learning. New York: McGraw-Hill.

    Google Scholar 

  • Moschovakis, Y. (1997). The logic of functional recursion. In Logic and scientific methods. 10th international congress logic, methodology and philosophy of science (pp. 179–208). Dordrecht: Kluwer Academic Publishers.

    Google Scholar 

  • Palmgren, E. (1998). On universes in type theory. In G. Sambin & J. M. Smith (Eds.), Twenty-five years of constructive type theory (pp. 191–204). Oxford: Clarendon Press.

    Google Scholar 

  • Pappi Alexandrini collectionis quae supersunt 3 vols. (ed. F.O. Hultsch). Berlin 1876-1878.

    Google Scholar 

  • Pfeifer, R., & Scheier, C. (2001). Understanding intelligence. Cambridge, MA: The MIT Press.

    Google Scholar 

  • Pinasco, J. P. (2009). New proofs of Euclid’s and Euler’s theorems. American Mathematical Monthly, 116(2), 172–173.

    Google Scholar 

  • Pomerleau, D. A. (1989). An autonomous land vehicle in a neural network (Technical Report CMU-CS-89-107.). Pitsburgh: Carnegie Mellon University.

    Google Scholar 

  • Post, E. L. (1936). Finite combinatory processes – Formulation I. Symbolic Logic, 1, 103–105.

    Google Scholar 

  • Rathjen, M., Griffor, E. R., & Palmgren, E. (1998). Inaccessibility in constructive set theory and type theory. Annals of Pure and Applied Logic, 94, 181–200.

    Google Scholar 

  • Russell, B. (1908). Mathematical logic as based on the theory of types. Amer. Journal of Mathematics, 30, 222–262.

    Google Scholar 

  • Scholz, H. (1961). Mathesis Universalis. Abhandlungen zur Philosophie als strenger Wissenschaft, hrsg. von H. Hermes, F. Kambartel, J. Ritter. Basel: Benno Schwabe & Co.

    Google Scholar 

  • Schwichtenberg, H. (2006). Minlog. In F. Wiedijk (Ed.), The seventeen provers of the world (Lecture Notes in Artificial Intelligence vol. 3600) (pp. 151–157). Berlin: Springer.

    Google Scholar 

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

    Google Scholar 

  • Setzer, A. (2000). Extending Martin-Löf type theory by one Mahlo-universe. Archive for Mathematical Logic, 39, 155–181.

    Google Scholar 

  • Sheperdson, J. C., & Sturgis, H. E. (1963). Computability of recursive functions. Journal of the Association for Computing Machinery, 10, 217–255.

    Google Scholar 

  • Shoenfield, J. R. (1967). Mathematical logic. Reading: Addison-Wesley.

    Google Scholar 

  • Simpson, S. G. (1999). Subsystems of second order arithmetic. Perspectives in mathematical logic. Springer: Berlin.

    Google Scholar 

  • Simpson, S. G. (2005). Reverse mathematics. Lecture notes in logic 21. The Association of Symbolic Logic 2005.

    Google Scholar 

  • Soare, R. I. (2016). Turing-computability. Theory and applications. New York: Springer.

    Google Scholar 

  • Spanier, E. H. (1966). Algebraic topology. Berlin: Springer.

    Google Scholar 

  • The Univalent Foundations Program. (2013). Homotopy type theory: Univalent foundations of mathematics. Princeton: Institute for Advanced Study.

    Google Scholar 

  • Troelstra, A. S., & van Dalen, D. (1988). Constructivism in mathematics. An introduction. 2 vols. Amsterdam: North-Holland.

    Google Scholar 

  • Turing, A. M. (1936–1937). On computable numbers, with an application to the Entscheidungsproblem. Proceedings of the London Mathematical Society Series 2, 42(1), 230–265. On computable numbers, with an application to the Entscheidungsproblem: A correction. Proceedings of the London Mathematical Society 2 (published 1937), 43(6), 544–546.

    Google Scholar 

  • Voevodsky, V. (2012). A universe polymorphic type system. http://uf-ias-2012.wikispaces.com/file/view/Universe+polymorphic+type+sytem.pdf

  • von Mackensen, L. (1974). Leibniz als Ahnherr der Kybernetik – ein bisher unbekannter Vorschlag einer „„Machina arithmetica dyadicae“). Akten des II Internationalen Leibniz-Kongresses 1972 Bd. 2 (pp. 255–268). Wiesbaden: Steiner.

    Google Scholar 

  • Weyl, H. (1918). Das Kontinuum. Kritische Untersuchungen über die Grundlagen der Analysis. De Gruyter: Leipzig.

    Google Scholar 

  • Weyl, H. (1921). Über die neue Grundlagenkrise der Mathematik. Mathematische Zeitschrift, 10, 39–79.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Technical University of Munich (TUM), Munich, Germany

    Klaus Mainzer

Authors
  1. Klaus Mainzer
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Klaus Mainzer .

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

Mainzer, K. (2019). From Mathesis Universalis to Provability, Computability, and Constructivity. 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_12

Download citation

Publish with us

Policies and ethics

Search

Navigation