Advertisement

From Mathesis Universalis to Provability, Computability, and Constructivity

  • Klaus MainzerEmail author
Chapter
Part of the Synthese Library book series (SYLI, volume 412)

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

Keywords

Mathesis universalis Proof mining Program extraction Reverse mathematics Constructivity Intuitionistic type theory Program assistant Univalent foundations program Machine learning Theoria cum praxis 

References

  1. 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.CrossRefGoogle Scholar
  2. Aigner, M., & Ziegler, G.M. (2001). Proofs from The Book (2nd ed.). Berlin: Springer.Google Scholar
  3. Awodey, S., & Warren, M. A. (2009). Homotopy theoretic models of identity type. Mathematical Proceedings of the Cambridge Philosophical Society, 146(1), 45–55.CrossRefGoogle Scholar
  4. Berger, J., & Ishahara, H. (2005). Brouwer’s fan theorem and unique existence in constructive analysis. Mathematical Logic Quarterly, 51, 360–364.CrossRefGoogle Scholar
  5. Bertot, Y., & Castéran, P. (2004). Interactive theorem proving and program development. Coq’Art: The calculus of inductive constructions. Springer: New York.CrossRefGoogle Scholar
  6. 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
  7. Bishop, E. (1967). Foundations of constructive analysis. New York: McGraw-Hill.Google Scholar
  8. 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).
  9. Brouwer, L. E. J. (1907). Over de Grondslagen der Wiskunde [On the foundations of mathematics]. Amsterdam: Maas & Van Suchtelen.Google Scholar
  10. Chaitin, G. J. (1998). The limits of mathematics. Singapore: Springer.Google Scholar
  11. Churchland, P. S., & Sejnowski, T. J. (1992). The computational brain. Cambridge, MA: MIT Press.CrossRefGoogle Scholar
  12. Coquand, T., & Huet, G. (1988). The calculus of constructions. Information and Computation, 76(2–3), 95–120.CrossRefGoogle Scholar
  13. Davis, M. (1958). Computability & unsolvability. New York: McGraw-Hill.Google Scholar
  14. Davis, M., Putnam, H., & Robinson, J. (1961). The decision problem for exponential Diophantine equations. Annals of Mathematics II, 74, 425–436.CrossRefGoogle Scholar
  15. 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.
  16. 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
  17. 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
  18. 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).CrossRefGoogle Scholar
  19. Eilenberg, S., & Cartan, H. (1956). Homological algebra. Princeton University Press: Princeton.Google Scholar
  20. Euclid. (1782). The elements of Euclid (with Dissertations). J. Williamson (translator and commentator). Clarendon Press: Oxford.Google Scholar
  21. Feferman, S. (1964). Systems of predicative analysis. Journal of Symbolic Logic, 29, 1–30.CrossRefGoogle Scholar
  22. Feferman, S. (1968). Systems of predicative analysis II: Representations of ordinals. Journal of Symbolic Logic, 53, 193–213.CrossRefGoogle Scholar
  23. 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
  24. 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
  25. 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).CrossRefGoogle Scholar
  26. 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.CrossRefGoogle Scholar
  27. Gödel, K. (1958). Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes. Dialectica, 12, 280–287.CrossRefGoogle Scholar
  28. Gonthier, G. (2008). Formal proof – The four-color theorem. Notices of the American Mathematical Society, 55(11), 1382–1393.Google Scholar
  29. Grothendieck, A., et al. (1971–1977). Séminaire de Géométrie Algébrique (Vol. 1–7). Berlin: Springer.Google Scholar
  30. Hazewinkel, M. (2001). Homotopy. In M. Hazewinkel (Ed.), Encyclopedia of mathematics. New York: Springer.Google Scholar
  31. Herken, R. (Ed.). (1995). The universal Turing machine. A half-century survey. Wien: Springer.Google Scholar
  32. Hermes, H. (1969a). Ideen von Leibniz zur Grundlagenforschung: Die ars inveniendi und die ars iudicandi. In: Studia Leibnitiana. Suppl. III (pp. 92–102). Wiesbaden: SteinerGoogle Scholar
  33. Hermes, H. (1969b). Enumerability, decidability, computability. Berlin: Springer.CrossRefGoogle Scholar
  34. Heyting, A. (1934). Mathematische Grundlagenforschung. Intuitionismus. Beweistheorie. Berlin: Springer. reprint 1974.Google Scholar
  35. 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
  36. Hintikka, J., & Remes, U. (1974). The method of analysis – Its geometrical origin and its general significance. Dordrecht: North-Holland.Google Scholar
  37. 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
  38. 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
  39. Ishahara, H. (2006). Reverse mathematics in Bishop’s constructive mathematics. Philosophia Scientiae, 6, 43–59.CrossRefGoogle Scholar
  40. Ishihara, H. (2005). Constructive reverse mathematics. Compactness properties (Oxford Logic Guides 48) (pp. 245–267). Oxford: Oxford University Press.Google Scholar
  41. Jäger, G., & Sieg, W. (Eds.). (2017). Feferman on foundations: Logic, mathematics, philosophy. New York: Springer.Google Scholar
  42. Joyal, A. (2002). Quasi-categories and Kan complexes. Journal of Pure and Applied Algebra, 175, 207–222.CrossRefGoogle Scholar
  43. 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
  44. Kleene, S. C. (1974). Introduction to metamathematics (7th ed.). Amsterdam: North Holland.Google Scholar
  45. 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
  46. Knobloch, E. (1987). Theoria cum Praxi. Leibniz und die Folgen für Wissenschaft und Technik. Studia Leibnitiana, 19, 129–147.Google Scholar
  47. Kohlenbach, U. (2008). Applied proof theory: Proof interpretations and their use in mathematics. Berlin: Springer.Google Scholar
  48. Kolmogorov, A. N. (1932). Zur Deutung der intuitionistischen Logik. Mathematische Zeitschrift, 35, 58–65.CrossRefGoogle Scholar
  49. 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
  50. 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
  51. Lorenzen, P. (1955). Einführung in die operative Logik und Mathematik. Berlin: Springer.CrossRefGoogle Scholar
  52. Lorenzen, P. (1965). Differential und Integral. Eine konstruktive Einführung in die klassische Analysis. Frankfurt: Akademische Verlagsgesellschaft.Google Scholar
  53. Mainzer, K. (1970). Der Konstruktionsbegriff in der Mathematik. Philosophia Naturalis, 12, 367–412.Google Scholar
  54. Mainzer, K. (1973). Mathematischer Konstruktivismus. Münster: Ph.D. U.Google Scholar
  55. Mainzer, K. (1980). Geschichte der Geometrie. Mannheim: B.I. Wissenschaftsverlag.Google Scholar
  56. Mainzer, K. (1994). Computer – Neue Flügel des Geistes? Berlin/New York: De Gruyter.CrossRefGoogle Scholar
  57. Mainzer, K. (1997). Gehirn, Computer, Komplexität. Berlin: Springer.CrossRefGoogle Scholar
  58. Mainzer, K. (2007). Thinking in complexity. The computational dynamics of matter, mind, and mankind (5th ed.). Berlin: Springer.Google Scholar
  59. Mainzer, K. (2016). Künstliche Intelligenz. Wann übernehmen die Maschinen? Springer: Berlin.CrossRefGoogle Scholar
  60. Mainzer, K. (2018a). The digital and the real world. Computational foundations of mathematics, science, technology and philosophy. Singapore: World Scientific Singapore.CrossRefGoogle Scholar
  61. 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
  62. Mainzer, K., & Chua, L. O. (2011). The universe as automaton. From simplicity and symmetry to complexity. Springer: Berlin.Google Scholar
  63. Mainzer, K., & Chua, L. (2013). Local activity principle. London: Imperial College Press.CrossRefGoogle Scholar
  64. Mainzer, K., Schuster, P., & Schwichtenberg, H. (Eds.). (2018). Proof and computation. Digitization in mathematics, computer science, and philosophy. Singapore: World Scientific Singapore.Google Scholar
  65. 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
  66. Martin-Löf, P. (1971b). A theory of types (Technical report 71-3). Stockholm: University of Stockholm.Google Scholar
  67. 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
  68. 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
  69. 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
  70. 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.CrossRefGoogle Scholar
  71. Matiyasevich, Y. V. (1970). Enumerable sets are diophantic. Soviet Mathematics: Doklady, 11, 345–357.Google Scholar
  72. Matiyasevich, Y. V. (1993). Hilbert’s tenth problem. Cambridge, MA: The MIT Press.Google Scholar
  73. 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.CrossRefGoogle Scholar
  74. Mitchell, T. M. (1997). Machine learning. New York: McGraw-Hill.Google Scholar
  75. 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
  76. 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
  77. Pappi Alexandrini collectionis quae supersunt 3 vols. (ed. F.O. Hultsch). Berlin 1876-1878.Google Scholar
  78. Pfeifer, R., & Scheier, C. (2001). Understanding intelligence. Cambridge, MA: The MIT Press.CrossRefGoogle Scholar
  79. Pinasco, J. P. (2009). New proofs of Euclid’s and Euler’s theorems. American Mathematical Monthly, 116(2), 172–173.CrossRefGoogle Scholar
  80. Pomerleau, D. A. (1989). An autonomous land vehicle in a neural network (Technical Report CMU-CS-89-107.). Pitsburgh: Carnegie Mellon University.Google Scholar
  81. Post, E. L. (1936). Finite combinatory processes – Formulation I. Symbolic Logic, 1, 103–105.CrossRefGoogle Scholar
  82. 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.CrossRefGoogle Scholar
  83. Russell, B. (1908). Mathematical logic as based on the theory of types. Amer. Journal of Mathematics, 30, 222–262.CrossRefGoogle Scholar
  84. 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
  85. 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.CrossRefGoogle Scholar
  86. Schwichtenberg, H., & Wainer, S. S. (2012). Proofs and computations. Cambridge: Cambridge University Press.Google Scholar
  87. Setzer, A. (2000). Extending Martin-Löf type theory by one Mahlo-universe. Archive for Mathematical Logic, 39, 155–181.CrossRefGoogle Scholar
  88. Sheperdson, J. C., & Sturgis, H. E. (1963). Computability of recursive functions. Journal of the Association for Computing Machinery, 10, 217–255.CrossRefGoogle Scholar
  89. Shoenfield, J. R. (1967). Mathematical logic. Reading: Addison-Wesley.Google Scholar
  90. Simpson, S. G. (1999). Subsystems of second order arithmetic. Perspectives in mathematical logic. Springer: Berlin.CrossRefGoogle Scholar
  91. Simpson, S. G. (2005). Reverse mathematics. Lecture notes in logic 21. The Association of Symbolic Logic 2005.Google Scholar
  92. Soare, R. I. (2016). Turing-computability. Theory and applications. New York: Springer.Google Scholar
  93. Spanier, E. H. (1966). Algebraic topology. Berlin: Springer.Google Scholar
  94. The Univalent Foundations Program. (2013). Homotopy type theory: Univalent foundations of mathematics. Princeton: Institute for Advanced Study.Google Scholar
  95. Troelstra, A. S., & van Dalen, D. (1988). Constructivism in mathematics. An introduction. 2 vols. Amsterdam: North-Holland.Google Scholar
  96. 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
  97. Voevodsky, V. (2012). A universe polymorphic type system. http://uf-ias-2012.wikispaces.com/file/view/Universe+polymorphic+type+sytem.pdf
  98. 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
  99. Weyl, H. (1918). Das Kontinuum. Kritische Untersuchungen über die Grundlagen der Analysis. De Gruyter: Leipzig.Google Scholar
  100. Weyl, H. (1921). Über die neue Grundlagenkrise der Mathematik. Mathematische Zeitschrift, 10, 39–79.CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.Technical University of Munich (TUM)MunichGermany

Personalised recommendations