×

From mathesis universalis to provability, computability, and constructivity. (English) Zbl 1469.03113

Centrone, Stefania (ed.) et al., Mathesis universalis, computability and proof. Based on the Humboldt-Kolleg “Proof theory as mathesis universalis”, held at the German-Italian Centre for European Excellence, Villa Vigoni, Loveno di Menaggio, Como, Italy, July 24–28, 2017. Cham: Springer. Synth. Libr. 412, 203-234 (2019).
Summary: 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).
For the entire collection see [Zbl 1431.03011].

MSC:

03D10 Turing machines and related notions
03D35 Undecidability and degrees of sets of sentences
03F35 Second- and higher-order arithmetic and fragments
03F60 Constructive and recursive analysis
03B30 Foundations of classical theories (including reverse mathematics)
03F25 Relative consistency and interpretations
68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
03B38 Type theory
55U40 Topological categories, foundations of homotopy theory

Software:

Coq
PDFBibTeX XMLCite
Full Text: DOI

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. · Zbl 0481.03035 · doi:10.1016/S0049-237X(08)71989-X
[2] Aigner, M., & Ziegler, G.M. (2001). Proofs from The Book (2nd ed.). Berlin: Springer. · Zbl 0978.00002
[3] Awodey, S., & Warren, M. A. (2009). Homotopy theoretic models of identity type. Mathematical Proceedings of the Cambridge Philosophical Society, 146(1), 45-55. · Zbl 1205.03065 · doi:10.1017/S0305004108001783
[4] Berger, J., & Ishahara, H. (2005). Brouwer’s fan theorem and unique existence in constructive analysis. Mathematical Logic Quarterly, 51, 360-364. · Zbl 1079.03059 · doi:10.1002/malq.200410038
[5] Bertot, Y., & Castéran, P. (2004). Interactive theorem proving and program development. Coq’Art: The calculus of inductive constructions. Springer: New York. · Zbl 1069.68095 · doi:10.1007/978-3-662-07964-5
[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. · Zbl 1359.03009
[7] Bishop, E. (1967). Foundations of constructive analysis. New York: McGraw-Hill. · Zbl 0183.01503
[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. · JFM 38.0081.04
[10] Chaitin, G. J. (1998). The limits of mathematics. Singapore: Springer. · Zbl 0955.68046
[11] Churchland, P. S., & Sejnowski, T. J. (1992). The computational brain. Cambridge, MA: MIT Press. · Zbl 0872.92003 · doi:10.7551/mitpress/2010.001.0001
[12] Coquand, T., & Huet, G. (1988). The calculus of constructions. Information and Computation, 76(2-3), 95-120. · Zbl 0654.03045 · doi:10.1016/0890-5401(88)90005-3
[13] Davis, M. (1958). Computability & unsolvability. New York: McGraw-Hill. · Zbl 0080.00902
[14] Davis, M., Putnam, H., & Robinson, J. (1961). The decision problem for exponential Diophantine equations. Annals of Mathematics II, 74, 425-436. · Zbl 0111.01003 · doi:10.2307/1970289
[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. · doi: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.
[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).
[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). · Zbl 0543.00001 · doi:10.1007/978-1-4612-1005-4
[19] Eilenberg, S., & Cartan, H. (1956). Homological algebra. Princeton University Press: Princeton. · Zbl 0075.24305
[20] Euclid. (1782). The elements of Euclid (with Dissertations). J. Williamson (translator and commentator). Clarendon Press: Oxford.
[21] Feferman, S. (1964). Systems of predicative analysis. Journal of Symbolic Logic, 29, 1-30. · Zbl 0134.01101 · doi:10.2307/2269764
[22] Feferman, S. (1968). Systems of predicative analysis II: Representations of ordinals. Journal of Symbolic Logic, 53, 193-213. · Zbl 0162.02201 · doi:10.2307/2269866
[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). · Zbl 0889.03045
[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. · Zbl 0344.02022
[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). · Zbl 0967.03050 · doi:10.1090/conm/257/04031
[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. · JFM 57.0054.02 · doi:10.1007/BF01700692
[27] Gödel, K. (1958). Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes. Dialectica, 12, 280-287. · Zbl 0090.01003 · doi:10.1111/j.1746-8361.1958.tb01464.x
[28] Gonthier, G. (2008). Formal proof - The four-color theorem. Notices of the American Mathematical Society, 55(11), 1382-1393. · Zbl 1195.05026
[29] Grothendieck, A., et al. (1971-1977). Séminaire de Géométrie Algébrique (Vol. 1-7). Berlin: Springer.
[30] Hazewinkel, M. (2001). Homotopy. In M. Hazewinkel (Ed.), Encyclopedia of mathematics. New York: Springer.
[31] Herken, R. (Ed.). (1995). The universal Turing machine. A half-century survey. Wien: Springer. · Zbl 0820.68043
[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: Steiner
[33] Hermes, H. (1969b). Enumerability, decidability, computability. Berlin: Springer. · Zbl 0179.01801 · doi:10.1007/978-3-642-46178-1
[34] Heyting, A. (1934). Mathematische Grundlagenforschung. Intuitionismus. Beweistheorie. Berlin: Springer. reprint 1974. · JFM 60.0019.01
[35] Hilbert, D. (1900). Mathematische Probleme. In: Nachrichten der Königlichen Gesellschaft der Wissenschaften zu Göttingen, mathematisch-physikalische Klasse. Heft, 3, 253-297. · JFM 31.0068.03
[36] Hintikka, J., & Remes, U. (1974). The method of analysis - Its geometrical origin and its general significance. Dordrecht: North-Holland. · Zbl 0344.01002
[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. · Zbl 0930.03089
[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.
[39] Ishahara, H. (2006). Reverse mathematics in Bishop’s constructive mathematics. Philosophia Scientiae, 6, 43-59. · doi:10.4000/philosophiascientiae.406
[40] Ishihara, H. (2005). Constructive reverse mathematics. Compactness properties (Oxford Logic Guides 48) (pp. 245-267). Oxford: Oxford University Press. · Zbl 1095.03075
[41] Jäger, G., & Sieg, W. (Eds.). (2017). Feferman on foundations: Logic, mathematics, philosophy. New York: Springer. · Zbl 1394.03005
[42] Joyal, A. (2002). Quasi-categories and Kan complexes. Journal of Pure and Applied Algebra, 175, 207-222. · Zbl 1015.18008 · doi:10.1016/S0022-4049(02)00135-4
[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).
[44] Kleene, S. C. (1974). Introduction to metamathematics (7th ed.). Amsterdam: North Holland. · Zbl 0875.03002
[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.
[47] Kohlenbach, U. (2008). Applied proof theory: Proof interpretations and their use in mathematics. Berlin: Springer. · Zbl 1158.03002
[48] Kolmogorov, A. N. (1932). Zur Deutung der intuitionistischen Logik. Mathematische Zeitschrift, 35, 58-65. · Zbl 0004.00201 · doi:10.1007/BF01186549
[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).
[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.
[51] Lorenzen, P. (1955). Einführung in die operative Logik und Mathematik. Berlin: Springer. · Zbl 0068.00801 · doi:10.1007/978-3-662-01539-1
[52] Lorenzen, P. (1965). Differential und Integral. Eine konstruktive Einführung in die klassische Analysis. Frankfurt: Akademische Verlagsgesellschaft. · Zbl 0171.27102
[53] Mainzer, K. (1970). Der Konstruktionsbegriff in der Mathematik. Philosophia Naturalis, 12, 367-412.
[54] Mainzer, K. (1973). Mathematischer Konstruktivismus. Münster: Ph.D. U. · Zbl 0249.02003
[55] Mainzer, K. (1980). Geschichte der Geometrie. Mannheim: B.I. Wissenschaftsverlag. · Zbl 0485.01001
[56] Mainzer, K. (1994). Computer - Neue Flügel des Geistes? Berlin/New York: De Gruyter. · Zbl 0921.00004 · doi:10.1515/9783110886849
[57] Mainzer, K. (1997). Gehirn, Computer, Komplexität. Berlin: Springer. · Zbl 0864.68079 · doi:10.1007/978-3-642-60524-6
[58] Mainzer, K. (2007). Thinking in complexity. The computational dynamics of matter, mind, and mankind (5th ed.). Berlin: Springer. · Zbl 1163.37001
[59] Mainzer, K. (2016). Künstliche Intelligenz. Wann übernehmen die Maschinen? Springer: Berlin. · doi:10.1007/978-3-662-48453-1
[60] Mainzer, K. (2018a). The digital and the real world. Computational foundations of mathematics, science, technology and philosophy. Singapore: World Scientific Singapore. · Zbl 1411.68007 · doi:10.1142/10583
[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).
[62] Mainzer, K., & Chua, L. O. (2011). The universe as automaton. From simplicity and symmetry to complexity. Springer: Berlin. · Zbl 1237.37002
[63] Mainzer, K., & Chua, L. (2013). Local activity principle. London: Imperial College Press. · Zbl 1294.37001 · doi:10.1142/p882
[64] Mainzer, K., Schuster, P., & Schwichtenberg, H. (Eds.). (2018). Proof and computation. Digitization in mathematics, computer science, and philosophy. Singapore: World Scientific Singapore. · Zbl 1400.03005
[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). · Zbl 0231.02040
[66] Martin-Löf, P. (1971b). A theory of types (Technical report 71-3). Stockholm: University of Stockholm.
[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. · Zbl 0334.02016
[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. · Zbl 0541.03034
[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. · Zbl 0931.03070
[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. · Zbl 1167.03033 · doi:10.1007/978-1-4020-8926-8_10
[71] Matiyasevich, Y. V. (1970). Enumerable sets are diophantic. Soviet Mathematics: Doklady, 11, 345-357.
[72] Matiyasevich, Y. V. (1993). Hilbert’s tenth problem. Cambridge, MA: The MIT Press. · Zbl 0790.03009
[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. · Zbl 0105.00802 · doi:10.2307/1970290
[74] Mitchell, T. M. (1997). Machine learning. New York: McGraw-Hill. · Zbl 0913.68167
[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. · Zbl 0903.03020
[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. · Zbl 0930.03090
[77] Pappi Alexandrini collectionis quae supersunt 3 vols. (ed. F.O. Hultsch). Berlin 1876-1878.
[78] Pfeifer, R., & Scheier, C. (2001). Understanding intelligence. Cambridge, MA: The MIT Press. · doi:10.7551/mitpress/6979.001.0001
[79] Pinasco, J. P. (2009). New proofs of Euclid’s and Euler’s theorems. American Mathematical Monthly, 116(2), 172-173. · Zbl 1214.11012 · doi:10.4169/193009709X469931
[80] Pomerleau, D. A. (1989). An autonomous land vehicle in a neural network (Technical Report CMU-CS-89-107.). Pitsburgh: Carnegie Mellon University.
[81] Post, E. L. (1936). Finite combinatory processes - Formulation I. Symbolic Logic, 1, 103-105. · JFM 62.1060.01 · doi:10.2307/2269031
[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. · Zbl 0926.03074 · doi:10.1016/S0168-0072(97)00072-9
[83] Russell, B. (1908). Mathematical logic as based on the theory of types. Amer. Journal of Mathematics, 30, 222-262. · JFM 39.0085.03 · doi:10.2307/2369948
[84] Scholz, H. (1961). Mathesis Universalis. Abhandlungen zur Philosophie als strenger Wissenschaft, hrsg. von H. Hermes, F. Kambartel, J. Ritter. Basel: Benno Schwabe & Co. · Zbl 0111.00503
[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. · doi:10.1007/11542384_19
[86] Schwichtenberg, H., & Wainer, S. S. (2012). Proofs and computations. Cambridge: Cambridge University Press. · Zbl 1294.03006
[87] Setzer, A. (2000). Extending Martin-Löf type theory by one Mahlo-universe. Archive for Mathematical Logic, 39, 155-181. · Zbl 0943.03046 · doi:10.1007/s001530050140
[88] Sheperdson, J. C., & Sturgis, H. E. (1963). Computability of recursive functions. Journal of the Association for Computing Machinery, 10, 217-255. · Zbl 0118.25401 · doi:10.1145/321160.321170
[89] Shoenfield, J. R. (1967). Mathematical logic. Reading: Addison-Wesley. · Zbl 0155.01102
[90] Simpson, S. G. (1999). Subsystems of second order arithmetic. Perspectives in mathematical logic. Springer: Berlin. · Zbl 0909.03048 · doi:10.1007/978-3-642-59971-2
[91] Simpson, S. G. (2005). Reverse mathematics. Lecture notes in logic 21. The Association of Symbolic Logic 2005.
[92] Soare, R. I. (2016). Turing-computability. Theory and applications. New York: Springer. · Zbl 1350.03001
[93] Spanier, E. H. (1966). Algebraic topology. Berlin: Springer. · Zbl 0145.43303
[94] The Univalent Foundations Program. (2013). Homotopy type theory: Univalent foundations of mathematics. Princeton: Institute for Advanced Study. · Zbl 1298.03002
[95] Troelstra, A. S., & van Dalen, D. (1988). Constructivism in mathematics. An introduction. 2 vols. Amsterdam: North-Holland. · Zbl 0661.03047
[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. · JFM 63.0823.02
[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. · Zbl 0291.01015
[99] Weyl, H. (1918). Das Kontinuum. Kritische Untersuchungen über die Grundlagen der Analysis. De Gruyter: Leipzig. · JFM 46.0312.01
[100] Weyl, H. · JFM 48.0220.01 · doi:10.1007/BF02102305
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.