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).
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
Mackensen (1974).
- 2.
Leibniz (1666).
- 3.
An interpretation of ars iudicandi as effective decidability and ars inveniendi as effective enumerability was discussed by Hermes (1969a).
- 4.
Scholz (1961).
- 5.
Turing (1936).
- 6.
- 7.
Turing (1936).
- 8.
Post (1936).
- 9.
A survey on the interdisciplinary influence of this concept was given in Herken (1995).
- 10.
- 11.
- 12.
Hermes (1969b).
- 13.
Gödel (1931).
- 14.
Chaitin (1998).
- 15.
Hilbert (1900).
- 16.
- 17.
Davis et al. (1961).
- 18.
- 19.
Pinasco (2009).
- 20.
Feferman (1996).
- 21.
Kohlenbach (2008), 13.
- 22.
Kohlenbach (2008), 14.
- 23.
Mainzer (1970).
- 24.
- 25.
Gödel (1958).
- 26.
Moschovakis (1997).
- 27.
Schwichtenberg, Wainer (2012), 389 f.
- 28.
Schwichtenberg (2006).
- 29.
Pappos (1876–1878 II, 634 ff).
- 30.
- 31.
- 32.
- 33.
Bishop (1967).
- 34.
Ebbinghaus et al. (1991), chapter 2.
- 35.
Weyl (1918).
- 36.
- 37.
- 38.
- 39.
Brouwer (1907).
- 40.
Berger and Ishahara (2005).
- 41.
Troelstra and van Dalen (1988, 220).
- 42.
Howard (1969).
- 43.
Dybjer and Palmgren (2016).
- 44.
- 45.
Martin-Löf (1975).
- 46.
Grothendieck et al. (1971–1977).
- 47.
Martin-Löf (2009).
- 48.
Martin-Löf (1975).
- 49.
Martin-Löf (1982).
- 50.
Aczel (1978).
- 51.
- 52.
Coquand and Huet (1988).
- 53.
Bertot, Castéran (2004).
- 54.
Gonthier (2008).
- 55.
Di Risi (2015).
- 56.
Leibniz (1679).
- 57.
Spanier (1966).
- 58.
Eilenberg and Cartan (1956).
- 59.
Hazewinkel (2001).
- 60.
Awodey and Warren (2009).
- 61.
Hofmann and Streicher (1998).
- 62.
The Univalent Foundations Program (2013).
- 63.
Bezem et al. (2014).
- 64.
- 65.
Knobloch (1987).
- 66.
Durkheim (1893).
- 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.
Weyl (1921).
- 69.
- 70.
- 71.
- 72.
Mitchell (1997).
- 73.
Bojarski et al. (2017).
- 74.
- 75.
Kalra and Paddock (2016).
- 76.
Knight (2017, 4)
- 77.
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.
Aigner, M., & Ziegler, G.M. (2001). Proofs from The Book (2nd ed.). Berlin: Springer.
Awodey, S., & Warren, M. A. (2009). Homotopy theoretic models of identity type. Mathematical Proceedings of the Cambridge Philosophical Society, 146(1), 45–55.
Berger, J., & Ishahara, H. (2005). Brouwer’s fan theorem and unique existence in constructive analysis. Mathematical Logic Quarterly, 51, 360–364.
Bertot, Y., & Castéran, P. (2004). Interactive theorem proving and program development. Coq’Art: The calculus of inductive constructions. Springer: New York.
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.
Bishop, E. (1967). Foundations of constructive analysis. New York: McGraw-Hill.
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.
Chaitin, G. J. (1998). The limits of mathematics. Singapore: Springer.
Churchland, P. S., & Sejnowski, T. J. (1992). The computational brain. Cambridge, MA: MIT Press.
Coquand, T., & Huet, G. (1988). The calculus of constructions. Information and Computation, 76(2–3), 95–120.
Davis, M. (1958). Computability & unsolvability. New York: McGraw-Hill.
Davis, M., Putnam, H., & Robinson, J. (1961). The decision problem for exponential Diophantine equations. Annals of Mathematics II, 74, 425–436.
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.
Dybjer, P., & Palmgren, E. (2016). Intuitionistic type theory. In The Stanford encyclopedia of philosophy, the metaphysics research lab (CSLI). Stanford: Stanford University. (open access).
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).
Eilenberg, S., & Cartan, H. (1956). Homological algebra. Princeton University Press: Princeton.
Euclid. (1782). The elements of Euclid (with Dissertations). J. Williamson (translator and commentator). Clarendon Press: Oxford.
Feferman, S. (1964). Systems of predicative analysis. Journal of Symbolic Logic, 29, 1–30.
Feferman, S. (1968). Systems of predicative analysis II: Representations of ordinals. Journal of Symbolic Logic, 53, 193–213.
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).
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.
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).
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.
Gödel, K. (1958). Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes. Dialectica, 12, 280–287.
Gonthier, G. (2008). Formal proof – The four-color theorem. Notices of the American Mathematical Society, 55(11), 1382–1393.
Grothendieck, A., et al. (1971–1977). Séminaire de Géométrie Algébrique (Vol. 1–7). Berlin: Springer.
Hazewinkel, M. (2001). Homotopy. In M. Hazewinkel (Ed.), Encyclopedia of mathematics. New York: Springer.
Herken, R. (Ed.). (1995). The universal Turing machine. A half-century survey. Wien: Springer.
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
Hermes, H. (1969b). Enumerability, decidability, computability. Berlin: Springer.
Heyting, A. (1934). Mathematische Grundlagenforschung. Intuitionismus. Beweistheorie. Berlin: Springer. reprint 1974.
Hilbert, D. (1900). Mathematische Probleme. In: Nachrichten der Königlichen Gesellschaft der Wissenschaften zu Göttingen, mathematisch-physikalische Klasse. Heft, 3, 253–297.
Hintikka, J., & Remes, U. (1974). The method of analysis – Its geometrical origin and its general significance. Dordrecht: North-Holland.
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.
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.
Ishahara, H. (2006). Reverse mathematics in Bishop’s constructive mathematics. Philosophia Scientiae, 6, 43–59.
Ishihara, H. (2005). Constructive reverse mathematics. Compactness properties (Oxford Logic Guides 48) (pp. 245–267). Oxford: Oxford University Press.
Jäger, G., & Sieg, W. (Eds.). (2017). Feferman on foundations: Logic, mathematics, philosophy. New York: Springer.
Joyal, A. (2002). Quasi-categories and Kan complexes. Journal of Pure and Applied Algebra, 175, 207–222.
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).
Kleene, S. C. (1974). Introduction to metamathematics (7th ed.). Amsterdam: North Holland.
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.
Kohlenbach, U. (2008). Applied proof theory: Proof interpretations and their use in mathematics. Berlin: Springer.
Kolmogorov, A. N. (1932). Zur Deutung der intuitionistischen Logik. Mathematische Zeitschrift, 35, 58–65.
Leibniz, G. W. (1666). Dissertation on the art of combinations. In Philosophical papers and letters (L. E. Loemker, Ed. and Trans., pp. 73–84).
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.
Lorenzen, P. (1955). Einführung in die operative Logik und Mathematik. Berlin: Springer.
Lorenzen, P. (1965). Differential und Integral. Eine konstruktive Einführung in die klassische Analysis. Frankfurt: Akademische Verlagsgesellschaft.
Mainzer, K. (1970). Der Konstruktionsbegriff in der Mathematik. Philosophia Naturalis, 12, 367–412.
Mainzer, K. (1973). Mathematischer Konstruktivismus. Münster: Ph.D. U.
Mainzer, K. (1980). Geschichte der Geometrie. Mannheim: B.I. Wissenschaftsverlag.
Mainzer, K. (1994). Computer – Neue Flügel des Geistes? Berlin/New York: De Gruyter.
Mainzer, K. (1997). Gehirn, Computer, Komplexität. Berlin: Springer.
Mainzer, K. (2007). Thinking in complexity. The computational dynamics of matter, mind, and mankind (5th ed.). Berlin: Springer.
Mainzer, K. (2016). Künstliche Intelligenz. Wann übernehmen die Maschinen? Springer: Berlin.
Mainzer, K. (2018a). The digital and the real world. Computational foundations of mathematics, science, technology and philosophy. Singapore: World Scientific Singapore.
Mainzer, K. (2018b). Artificial intelligence and machine learning – Algorithmic foundations and philosophical perspectives. Journal of Shanghai Normal University (Philosophy & Social Sciences Edition)., 48(3).
Mainzer, K., & Chua, L. O. (2011). The universe as automaton. From simplicity and symmetry to complexity. Springer: Berlin.
Mainzer, K., & Chua, L. (2013). Local activity principle. London: Imperial College Press.
Mainzer, K., Schuster, P., & Schwichtenberg, H. (Eds.). (2018). Proof and computation. Digitization in mathematics, computer science, and philosophy. Singapore: World Scientific Singapore.
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).
Martin-Löf, P. (1971b). A theory of types (Technical report 71-3). Stockholm: University of Stockholm.
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.
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.
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.
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.
Matiyasevich, Y. V. (1970). Enumerable sets are diophantic. Soviet Mathematics: Doklady, 11, 345–357.
Matiyasevich, Y. V. (1993). Hilbert’s tenth problem. Cambridge, MA: The MIT Press.
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.
Mitchell, T. M. (1997). Machine learning. New York: McGraw-Hill.
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.
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.
Pappi Alexandrini collectionis quae supersunt 3 vols. (ed. F.O. Hultsch). Berlin 1876-1878.
Pfeifer, R., & Scheier, C. (2001). Understanding intelligence. Cambridge, MA: The MIT Press.
Pinasco, J. P. (2009). New proofs of Euclid’s and Euler’s theorems. American Mathematical Monthly, 116(2), 172–173.
Pomerleau, D. A. (1989). An autonomous land vehicle in a neural network (Technical Report CMU-CS-89-107.). Pitsburgh: Carnegie Mellon University.
Post, E. L. (1936). Finite combinatory processes – Formulation I. Symbolic Logic, 1, 103–105.
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.
Russell, B. (1908). Mathematical logic as based on the theory of types. Amer. Journal of Mathematics, 30, 222–262.
Scholz, H. (1961). Mathesis Universalis. Abhandlungen zur Philosophie als strenger Wissenschaft, hrsg. von H. Hermes, F. Kambartel, J. Ritter. Basel: Benno Schwabe & Co.
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.
Schwichtenberg, H., & Wainer, S. S. (2012). Proofs and computations. Cambridge: Cambridge University Press.
Setzer, A. (2000). Extending Martin-Löf type theory by one Mahlo-universe. Archive for Mathematical Logic, 39, 155–181.
Sheperdson, J. C., & Sturgis, H. E. (1963). Computability of recursive functions. Journal of the Association for Computing Machinery, 10, 217–255.
Shoenfield, J. R. (1967). Mathematical logic. Reading: Addison-Wesley.
Simpson, S. G. (1999). Subsystems of second order arithmetic. Perspectives in mathematical logic. Springer: Berlin.
Simpson, S. G. (2005). Reverse mathematics. Lecture notes in logic 21. The Association of Symbolic Logic 2005.
Soare, R. I. (2016). Turing-computability. Theory and applications. New York: Springer.
Spanier, E. H. (1966). Algebraic topology. Berlin: Springer.
The Univalent Foundations Program. (2013). Homotopy type theory: Univalent foundations of mathematics. Princeton: Institute for Advanced Study.
Troelstra, A. S., & van Dalen, D. (1988). Constructivism in mathematics. An introduction. 2 vols. Amsterdam: North-Holland.
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.
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.
Weyl, H. (1918). Das Kontinuum. Kritische Untersuchungen über die Grundlagen der Analysis. De Gruyter: Leipzig.
Weyl, H. (1921). Über die neue Grundlagenkrise der Mathematik. Mathematische Zeitschrift, 10, 39–79.
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
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
DOI: https://doi.org/10.1007/978-3-030-20447-1_12
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)