A.N. Kolmogorov’s calculus of problems and homotopy type theory
Philosophy "Mathematical objects, structures and proofs" (thematic issue)
DOI:
https://doi.org/10.17072/2078-7898/2022-3-368-379Keywords:
calculus of problems, intuitionistic logic, homotopy type theory, constructive negationAbstract
In 1932 A.N. Kolmogorov proposed an original version of mathematical intuitionism where the distinction between problems and theorems plays a central role and which differs in its content from the versions of intuitionism developed by A. Heyting and other followers of L. Brouwer. In view of today’s historians and logicians, it remains a controversial point whether this distinction is to be treated as logical or Kolmogorov’s «problems» should be regarded as propositions, provided the latter term is interpreted intuitionistically. The popular BHK semantics of intuitionistic logic, so called after Brouwer, Heyting, and Kolmogorov and supposed to provide a synthesis of ideas of these authors, does not formally distinguish between problems and theorems and treats this distinction as contextual or purely linguistic. We argue that the distinction between problems and theorems is a crucial element of Kolmogorov’s approach and provide a logical interpretation of this distinction using homotopy type theory (HoTT). The notion of homotopy level of a given type in HoTT allows one to distinguish, after Kolmogorov, between problems reduced to proving a sentence and problems that require realization of higher-order constructions. Thus, HoTT provides a support for Kolmogorov’s view on intuitionistic logic in his polemics with Heyting. At the same time, HoTT does not solve the problem of finding a constructive notion of negation applicable to general problems, which is raised by Kolmogorov in the same paper and still remains open.References
Колмогоров А.Н. О принципе tertium non datur // Математический сборник. 1925. Т. 32, вып. 4. С. 646–667.
Колмогоров А.Н. Современные споры о природе математики // Научное слово. 1929. Вып. 6. С. 41–54.
Колмогоров А.Н. К работам по интуиционистской логике // Колмогоров А.Н. Избр. труды. Кн. 1: Математика и механика / отв. ред. С.М. Никольский. М.: Наука, 1985. С. 393.
Колмогоров А.Н. К толкованию интуиционист ской логики / пер. с нем. В.А. Успенского // Колмогоров А.Н. Избр. труды. Кн. 1: Математика и механика / отв. ред. С.М. Никольский. М.: Наука, 1985. С. 142–149.
Плиско В.Е. Исчисление А.Н. Колмогорова как фрагмент минимального исчисления // Успехи математических наук. 1988. Т. 43, вып. 6(264). С. 79–91.
Хинчин А.Я. Идеи интуиционизма и борьба за предмет в современной математике // Вестник коммунистической академии. 1926. Кн. 16. С. 184–192.
Agudelo-Agudelo J.S., Sicard-Ramirez A. Type Theory with Opposite Types: A Paraconsisted Type Theory // Logic Journal of IgPL. 2022. Vol. 30, iss. 5. P. 777–806. DOI: https://doi.org/10.1093/ jigpal/jzab022
Atten M. van. The Development of Intuitionistic Logic // The Stanford Encyclopedia of Philosophy / ed. by E.N. Zalta. 2022. URL: https://plato.stanford.edu/entries/intuitionistic-logic development/ (accwssed: 22.07.2022).
Coquand T. Kolmogorov’s Contribution to Intuitionistic Logic // Kolmogorov’s Heritage in Mathe matics / ed. by E. Charpentier, A. Lesne, N.K. Nikolski. Berlin: Springer, 2007. P. 19–40. DOI: https://doi.org/10.1007/978-3-540-36351-4_2
Dalen M. van. Heyting and Intuitionistic Geometry // Mathematical Logic / ed. by P.P. Petkov. N.Y.: Plenuv Press, 1990. P. 19–27. DOI: https://doi.org/10.1007/978-1-4613-0609-2_2
Griss G.W.C. Sur la Négation (dans les mathé matiques et la logique) // Synthese. 1948–1949. Vol. 7, iss. 1–2. P. 71–74.
Heyting A. Die formalen Regeln der intuition istische Logik // Sitzungsberichte der Preussischen Academie der Wissenshaften. Berlin: Verlag der Akademie der Wissenschaften, 1930. S. 43–56 (I), S. 57–71 (II), S. 158–169 (III).
Homotopy Type Theory: Univalent Foundations of Mathematics. Princeton, NJ: The Univalent Foun dations Program: Institute for Advanced Study, 2013. 480 p.
Kolmogoroff A. Zur Deutung der intuition istischen Logik // Mathematische Zeitschrift. 1932. Bd. 35, ht. 1. S. 58–65. DOI: https://doi.org/ 10.1007/bf01186549
MacLane S., Moerdijk I. Sheaves in Geometry and Logic. N.Y.: Springer, 1994. 642 p. DOI: https://doi.org/10.1007/978-1-4612-0927-0
Martin-Lof P. Intuitionistic Type Theory. Napoli, IT: Bibliopolis, 1984. 91 p.
Odintsov S.P. Constructive Negations and Para consistency. Dordrecht, NL: Springer, 2008. 248 p. DOI: https://doi.org/10.1007/978-1-4020-6867-6
Sanz W. Kolmogorov and the General Theory of Problems // Festschrift for Peter Heister-Schroeder. 2021. URL: https://www.researchgate.net/ publication/349517286_Kolmogorov_and_ The_General_Theory_of_Problems?channel=doi&lin kId=60345796a6fdcc37a846345e&showFulltext=true (accessed: 22.05.2022). DOI: https://doi.org/ 10.13140/RG.2.2.31753.16488
Troelstra A.S. On the Early History of Intuition istic Logic // Mathematical Logic / ed. by P.P. Petkov. N.Y.: Plenuv Press, 1990. P. 3–17. DOI: https://doi.org/10.1007/978-1-4613-0609-2_1
References
Agudelo-Agudelo, J.S. and Sicard-Ramirez, A. (2022). Type theory with opposite types: a paraconsisted type theory. Logic Journal of IgPL. Vol. 30, iss. 5, pp. 777–806. DOI: https://doi.org/ 10.1093/jigpal/jzab022
Atten, M. van (2022). The development of intuitionistic logic. E.N. Zalta (ed.) The Stanford encyclopedia of philosophy. Available at: https://plato.stanford.edu/entries/intuitionistic-logic development/ (accessed 22.07.2022).
Coquand, T. (2007). Kolmogorov’s contribution to intuitionistic logic. E. Charpentier, A. Lesne, N.K. Nikolski (eds.) Kolmogorov’s heritage in mathematics. Berlin: Springer Publ., pp. 19–40. DOI: https://doi.org/10.1007/978-3-540-36351-4_2
Dalen, M. van (1990). Heyting and intuitionistic geometry. P.P. Petkov (ed.) Mathematical Logic. New York: Plenuv Press, pp. 19–27. DOI: https://doi.org/10.1007/978-1-4613-0609-2_2
Griss, G.W.C. (1948–1949). [On negation (in mathematics and logic)]. Synthese. Vol. 7, iss. 1–2, pp. 71–74.
Heyting, A. (1930). [The formal rules of intuitionistic logic]. Sitzungsberichte der Preussischen Acad emie der Wissenshaften [Proceedings of the Prussian Academy of Sciences]. Berlin: Academy of Sciences Publ., pp. 43–56 (I), pp. 57–71 (II), pp. 158–169 (III).
Homotopy type theory: Univalent foundations of mathematics (2013). Princeton, NJ: The Univalent Foundations Program Publ., Institute for Advanced Study Publ., 480 p.
Khinchin, A.Ya. (1926). [Ideas of intuitionism and the struggle concerning the subject matter in the context of modern mathematics]. Vestnik kommunisticheskoy akademii [Bulletin of the Communist Academy]. Book 16, pp. 184–192.
Kolmogorov, A. (1932). [On the interpretation of intuitionistic logic]. Mathematische Zeitschrift [Mathematical Journal]. Vol. 35, iss. 1, pp. 58–65. DOI: https://doi.org/10.1007/bf01186549
Kolmogorov, A.N. (1925). [On the principle of tertium non datur]. Matematicheskii Sbornik. Vol. 32, iss. 4, pp. 646–667.
Kolmogorov, A.N. (1929). [Contemporary debate on the nature of mathematics]. Nauchnoe slovo [Scientific Word]. Iss. 6, pp. 41–54.
Kolmogorov, A.N. (1985). [On the interpretation of intuitionistic logic]. Izbrannye trudy. Kn. 1: Matematika i mekhanika, otv. red. S.M. Nikol’skiy [S.M. Nikolsky (ed.) Selected works. Book 1: Mathematics and mechanics]. Moscow: Nauka Publ., p. 142–149.
Kolmogorov, A.N. (1985). [On the publications on intuitionistic logic]. Izbrannye trudy. Kn. 1: Matematika i mekhanika, otv. red. S.M. Nikol’skiy [S.M. Nikolsky (ed.) Selected works. Book 1: Mathematics and mechanics]. Moscow: Nauka Publ., p. 393.
MacLane, S. and Moerdijk, I. (1994). Sheaves in geometry and logic. New York: Springer Publ., 642 p. DOI: https://doi.org/10.1007/978-1-4612- 0927-0
Martin-Lof, P. (1984). Intuitionistic type theory. Napoli, IT: Bibliopolis Publ., 91 p.
Odintsov, S.P. (2008). Constructive negations and paraconsistency. Dordrecht, NL: Springer Publ., 248 p. DOI: https://doi.org/10.1007/978-1-4020- 6867-6
Plisko, V.E. (1988). [Kolmogorov’s calculus of problems as a fragment of minimal calculus]. Uspekhi matematicheskikh nauk [Successes of Mathematical Sciences]. Vol. 43, iss. 6 (264), pp. 79–91.
Sanz, W. (2021). Kolmogorov and the General Theory of Problems. Festschrift for Peter HeisterSchroeder. Available at: https://www.researchgate.net/publication/349517286 _Kolmogorov_and_The_General_Theory_of_Proble ms?channel=doi&linkId=60345796a6fdcc37a846345 e&showFulltext=true (accessed 22.05.2022). DOI: https://doi.org/10.13140/RG.2.2.31753.16488
Troelstra, A.S. (1990). On the early history of intuitionistic logic. P.P. Petkov (ed.) Mathematical Logic. New York: Plenuv Press, pp. 3–17. DOI: https://doi.org/10.1007/978-1-4613-0609-2_1
Downloads
Published
Issue
Section
License
Copyright (c) 2022 Perm University Herald. Philosophy. Psychology. Sociology
This work is licensed under a Creative Commons Attribution 4.0 International License.
