Исчисление задач А.Н. Колмогорова и гомотопическая теория типов: Философия «Математические объекты, структуры и доказательства» (тематический выпуск)

Андрей Вячеславович Родин

doi:10.17072/2078-7898/2022-3-368-379

Авторы

Андрей Вячеславович Родин Русское общество истории и философии науки, 109240, Москва, Гончарная, 12/1

DOI:

https://doi.org/10.17072/2078-7898/2022-3-368-379

Ключевые слова:

исчисление задач, интуиционистская логика, гомотопическая теория типов, конструктивное отрицание

Аннотация

А.Н. Колмогоров в 1932 г. предложил оригинальный вариант математического интуиционизма Л. Бауэра, в котором центральную роль играет различие задач и теорем, отличающихся по своему содержанию от интуиционизма А. Гейтинга и других последователей. У современных историков и логиков существуют разные мнения по вопросу о том, следует ли считать различие между задачами и теоремами у А.Н. Колмогорова логическим или же в интуиционистской интерпретации высказываний можно считать «проблемы» А.Н. Колмогорова просто альтернативным термином для теорем. В популярной ВНК-интерпретации интуиционистской логики, названной так по именам Л. Брауэра, А. Гейтинга и А.Н. Колмогорова, предлагается синтез подходов этих трех авторов, в котором различие между задачами выносится за пределы логики и трактуется как контекстуальное или чисто лингвистическое. В статье показывается, что различие между задачами и теоремами играет ключевую роль в подходе А.Н. Колмогорова, и приводится логическая интерпретация этого различия с использованием гомотопической теории типов (ГТТ). Используемое в этой теории понятие гомотопического уровня позволяет вслед за А.Н. Колмогоровым различать задачи, которые сводятся к доказательству утверждений, и задачи на реализацию конструкций более высоких уровней. Таким образом, ГТТ соотносится с точкой зрения А.Н. Колмогорова в его полемике с А. Гейтингом. В то же время в ГТТ не решается поставленная А.Н. Колмогоровым задача поиска конструктивного понятия отрицания, применимого к задачам общего вида, которая на сегодняшний день остается по-прежнему открытой.

Биография автора

Андрей Вячеславович Родин , Русское общество истории и философии науки, 109240, Москва, Гончарная, 12/1

доктор философских наук, научный сотрудник

Библиографические ссылки

Колмогоров А.Н. О принципе 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