Практика компьютерных доказательств и человеческое понимание: эпистемологическая проблематика: Философия

Лев Дмитриевич Ламберов

doi:10.17072/2078-7898/2021-1-5-19

Авторы

Лев Дмитриевич Ламберов Уральский федеральный университет им. первого Президента России Б.Н. Ельцина 620002, Екатеринбург, ул. Мира, 19

DOI:

https://doi.org/10.17072/2078-7898/2021-1-5-19

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

доказательство, понимание, обозримость, основания математики, практика

Аннотация

В последние десятилетия в математике особую остроту приобрели эпистемологические проблемы, связанные со слишком большой длиной доказательства важных математических результатов, а также с большим и постоянно возрастающим количеством публикаций по математике. Предполагается, что эти затруднения могут быть разрешены (хотя бы частично) путем обращения к компьютерным доказательствам. Однако и компьютерные доказательства оказываются проблематичными с эпистемологической точки зрения. И относительно доказательств в обычной (неформальной) математике, и относительно компьютерных доказательств в равной степени актуальна проблема их обозримости. Исходя из традиционного понимания доказательства оно обязательно должно быть обозримым, иначе оно не будет достигать своей основной цели — формирования убежденности в правильности доказываемого математического результата. Около 15 лет назад начал развиваться новый подход к основаниям математики, сочетающий в себе конструктивистские, структуралистские черты и ряд преимуществ классического подхода к математике. Этот подход выстраивается на основе гомотопической теории типов и носит название унивалентных оснований математики. Благодаря мощному понятию равенства этот подход позволяет значительно сократить длину формализованных доказательств, что намечает путь к разрешению возникших эпистемологических затруднений.

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

Лев Дмитриевич Ламберов , Уральский федеральный университет им. первого Президента России Б.Н. Ельцина 620002, Екатеринбург, ул. Мира, 19

кандидат философских наук, доцент,доцент кафедры онтологии и теории познания

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

Доманов О.А. Структурализм и конструктивизм в гуманитарных науках и математике // Сибирский философский журнал. 2017. Т. 15, № 3. С. 39–50. DOI: https://doi.org/10.25205/2541-7517-2017-15-3-39-50

Ламберов Л.Д. Основания математики: теория множеств vs. теория типов // Философия науки. 2017. № 1. С. 41–60. DOI: https://doi.org/10.15372/ps20170104

Ламберов Л.Д. Понятие доказательства в контексте теоретико-типового подхода, I: доказательство программ // Вестник Томского государственного университета. Философия. Социология. Политология. 2018. № 46. С. 49–57. DOI: https://doi.org/10.17223/1998863x/46/6

Ламберов Л.Д. Понятие доказательства в контексте теоретико-типового подхода, II: доказательства теорем // Вестник Томского государственного университета. Философия. Социология. Политология. 2019. № 49. С. 34–41. DOI: https://doi.org/10.17223/1998863x/49/4

Ламберов Л.Д. Понятие доказательства в контексте теоретико-типового подхода, III: доказательства как (некоторые) типы // Вестник Томского государственного университета. Философия. Социология. Политология. 2020. № 57. С. 25–32. DOI: https://doi.org/10.17223/1998863Х/57/3

Ламберов Л.Д. Унивалентность и понятие структуры в философии математики // Сибирский философский журнал. 2018. Т. 16, № 1. С. 20–32. DOI: https://doi.org/10.25205/2541-7517-2018-16-1-20-32

Родин А.В. Делать и показывать // Доказательство: очевидность, достоверность и убедительность в математике / под ред. В.А. Бажанова, А.Н. Кричевца, В.А. Шапошникова. М.: Либроком, 2014. С. 219–255.

Хлебалин А.В. Интерактивное доказательство: верификация и генерирование нового математического знания // Философия науки. 2020. № 1. С. 87–95. DOI: https://doi.org/10.15372/ps20200105

Целищев В.В. Интуиция, финитизм и рекурсивное мышление. Новосибирск: Параллель, 2007. 220 с.

Целищев В.В. Эпистемология математического доказательства. Новосибирск: Параллель, 2006. 212 с.

Целищев В.В., Хлебалин А.В. Формальные средства в математике и концепция понимания // Философия науки. 2020. № 2. С. 45–58. DOI: https://doi.org/10.15372/ps20200204

Шапошников В.А. Распределенное познание и математическая практика в цифровом обществе: от формализации доказательств к пересмотру оснований // Эпистемология и философия науки. 2018. Т. 55, № 4. С. 160–173. DOI: https://doi.org/10.5840/eps201855474

Almgren’s Big Regularity Paper: Q-Valued Functions Minimizing Dirichlet’s Integral and the Regularity of Area-Minimizing Rectifiable Currents up to Codimension 2 / ed. by V. Scheffer, J.E. Taylor. Singapore: World Scientific, 2000. 972 p. DOI: https://doi.org/10.1142/4253

Appel K., Haken W. Every Planar Map is Four Colorable. I. Discharging // Illinois Journal of Mathematics. 1977. Vol. 21, iss. 3. P. 429–490. DOI: https://doi.org/10.1215/ijm/1256049011

Appel K., Haken W., Koch J. Every Planar Map is Four Colorable. II. Reducibility // Illinois Journal of Mathematics. 1977. Vol. 21, iss. 3. P. 491–567. DOI: https://doi.org/10.1215/ijm/1256049012

Aschbacher M. Highly Complex Proofs and Implications of Such Proofs // Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences. 2005. Vol. 363, iss. 1835. P. 2401–2406. DOI: https://doi.org/10.1098/rsta.2005.1655

Aschbacher M. The Status of the Classification of the Finite Simple Groups // Notices of the American Mathematical Society. 2004. Vol. 51, no. 7. P. 736–740.

Athreya J.S., Aulicino D., Hooper W.P. Platonic Solids and High Genus Covers of Lattice Surfaces // Experimental Mathematics. 2020. URL: https://www.tandfonline.com/doi/full/10.1080/10586458.2020.1712564 (accessed: 07.10.2020). DOI: https://doi.org/10.1080/10586458.2020.1712564

Bassler O.B. The Surveyability of Mathematical Proof: A Historical Perspective // Synthese. 2006. Vol. 148, iss. 1. P. 99–133. DOI: https://doi.org/10.1007/s11229-004-6221-7

Boyer R.S., Kaufmann M., Moore J.S. The Boyer-Moore Theorem Prover and Its Interactive Enhancement // Computers & Mathematics with Applications. 1995. Vol. 29, iss. 2. P. 27–62. DOI: https://doi.org/10.1016/0898-1221(94)00215-7

Church A. A Formulation of the Simple Theory of Types // The Journal of Symbolic Logic. 1940. Vol. 5, iss. 2. P. 56–68. DOI: https://doi.org/10.2307/2266170

Church A. A Set of Postulates for the Foundation of Logic // Annals of Mathematics (2nd Series). 1932. Vol. 33, no. 2. P. 346–366. DOI: https://doi.org/10.2307/1968337

Davies B. Whither Mathematics? // Notices of the American Mathematical Society. 2005. Vol. 52, no. 11. P. 1350–1356.

Davis M. A Computer Program for Presburger’s Algorithm // Automation of Reasoning. Vol. 1: Classical Papers on Computational Logic, 1957–1966 / ed. by J. Sielmann, G. Wrightson. Berlin; Heidelberg: Springer-Verlag, 1983. P. 41–48. DOI: https://doi.org/10.1007/978-3-642-81952-0_3

Davis M. The Prehistory and Early History of Automated Deduction // Automation of Reasoning. Vol. 1: Classical Papers on Computational Logic, 1957–1966 / ed. by J. Sielmann, G. Wrightson. Berlin; Heidelberg: Springer-Verlag, 1983. P. 1–28. DOI: https://doi.org/10.1007/978-3-642-81952-0_1

De Bruijn N. Automath, a Language for Mathematics // Automation of Reasoning. Vol. 2: Classical Papers on Computational Logic, 1967–1970 / ed. by J. Sielmann, G. Wrightson. Berlin; Heidelberg: Springer-Verlag, 1983. P. 159–200. DOI: https://doi.org/10.1007/978-3-642-81955-1_11

Homotopy Type Theory: Univalent Foundations of Mathematics. 2013. URL: https://homotopytypetheory.org/book/ (accessed: 01.11.2020).

Lawvere F.W. Quantifiers and sheaves // Actes du congres international des mathematiciens / ed. by M. Berger, J. Dieudonne et al. Nice: Gauthier-Villars, 1971. Vol. 1. P. 329–334.

Martin-Löf P. Intuitionistic Type Theory. Napoli: Bibliopolis, 1984. 100 p.

Mercer J. Functions of Positive and Negative Type and Their Connection with the Theory of Integral Equations // Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences. 1909. Vol. 209, iss. 441–458. P. 415–446. DOI: https://doi.org/10.1098/rsta.1909.0016

Milner R. LCF: A Way of Doing Proofs with a Machine // Mathematical Foundations of Computer Science 1979. Lecture Notes in Computer Science. Berlin; Heidelberg: Springer, 1979. Vol. 74. P. 146–159. DOI: https://doi.org/10.1007/3-540-09526-8_11

Newel A., Shaw J.C., Simon H.A. Empirical Explorations with the Logic Theory Machine: A Case Study in Heuristics // Automation of Reasoning. Vol. 1: Classical Papers on Computational Logic, 1957–1966 // ed. by J. Sielmann, G. Wrightson. Berlin; Heidelberg: Springer-Verlag, 1983. P. 49–73. DOI: https://doi.org/10.1007/978-3-642-81952-0_4

Polanyi M. Personal Knowledge: Towards a Post-Critical Philosophy. Chicago, IL: University of Chicago Press, 1958. 428 p.

Robertson N., Seymour P. Graph Minors. I. Excluding a Forest // Journal of Combinatorial Theory. Series B. 1983. Vol. 35, iss. 1. P. 39–61. DOI: https://doi.org/10.1016/0095-8956(83)90079-5

Robertson N., Seymour P. Graph Minors. XX. Wagner’s Conjecture // Journal of Combinatorial Theory. Series B. 2004. Vol. 92, iss. 2. P. 325–357. DOI: https://doi.org/10.1016/j.jctb.2004.08.001

Rodin A. Formal Proof-Verification and Mathematical Intuition: the Case of Univalent Foundations // 16th International Congress on Logic, Methodology and Philosophy of Science and Technology (Prague, August 5–10, 2019): Book of Abstracts. Prague, 2019. P. 418.

Russell B. The Principles of Mathematics. Cambridge, MA: Cambridge University Press, 1903. 534 p.

Shanker S. Wittgenstein and the Turning Point in the Philosophy of Mathematics. Albany: Croom Helm, 1987. 358 p.

Solomon R. The Classification of Finite Simple Groups: A Progress Report // Notices of the American Mathematical Society. 2018. Vol. 65, no. 6. P. 646–651. DOI: https://doi.org/10.1090/noti1689

Studies in Logic and the Foundations of Mathematics. Vol. 136: Admissibility of Logical Inference Rules / ed. by V.V. Rybakov. Amsterdam: Elsevier Science B.V., 1997. 616 p. DOI: https://doi.org/10.1016/s0049-237x(97)x8001-2

Teller P. Computer Proof // The Journal of Philosophy. 1980. Vol. 77, iss. 12. P. 797–803. DOI: https://doi.org/10.2307/2025805

The QED Manifesto // Automated Deduction – CADE 12 / ed. by A. Bundy. Berlin, Heidelberg: Springer-Verlag, 1994. P. 238–251.

Tymoczko T. The Four-Color Theorem and Its Philosophical Significance // The Journal of Philosophy. 1979. Vol. 76, iss. 2. P. 57–83. DOI: https://doi.org/10.2307/2025976

Weiss I. The QED Manifesto after Two Decades – Version 2.0 // Journal of Software. 2016. Vol. 11, no. 8. P. 803–815. DOI: https://doi.org/10.17706/jsw.11.8.803-815

Wiedijk F. Formal Proof — Getting Started // Notices of the American Mathematical Society. 2008. Vol. 55, no. 11. P. 1408–1414.

Wiedijk F. The QED Manifesto Revisited // Studies in Logic, Grammar and Rhetoric. 2007. Vol. 10, iss. 23. P. 121–133.

Wos L., Henschen L. Automated Theorem Proving, 1965–1970 // Automation of Reasoning. Vol. 2: Classical Papers on Computational Logic, 1967–1970 / ed. by J. Sielmann, G. Wrightson. Berlin; Heidelberg: Springer-Verlag, 1983. P. 1–24. DOI: https://doi.org/10.1007/978-3-642-81955-1_1

References

Appel, K. and Haken, W. (1977). Every planar map is four colorable. I. Discharging. Illinois Journal of Mathematics. Vol. 21, iss. 3, pp. 429–490. DOI: https://doi.org/10.1215/ijm/1256049011

Appel, K., Haken, W. and Koch, J. (1977). Every planar map is four colorable. II. Reducibility. Illinois Journal of Mathematics. Vol. 21, iss. 3, pp. 491–567. DOI: https://doi.org/10.1215/ijm/1256049012

Aschbacher, M. (2004). The status of the classification of the finite simple groups. Notices of the American Mathematical Society. Vol. 51, no. 7, pp. 736–740.

Aschbacher, M. (2005). Highly complex proofs and implications of such proofs. Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences. Vol. 363, iss. 1835, pp. 2401–2406. DOI: https://doi.org/10.1098/rsta.2005.1655

Athreya, J.S., Aulicino, D. and Hooper, W.P. (2020). Platonic solids and high genus covers of lattice surfaces. Experimental Mathematics. Available at: https://www.tandfonline.com/doi/full/10.1080/10586458.2020.1712564 (accessed 07.10.2020). DOI: https://doi.org/10.1080/10586458.2020.1712564

Bassler, O.B. (2006). The surveyability of mathematical proof: a historical perspective. Synthese. Vol. 148, iss. 1, pp. 99–133. DOI: https://doi.org/10.1007/s11229-004-6221-7

Boyer, R.S., Kaufmann, M. and Moore, J.S. (1995). The Boyer-Moore theorem prover and its interactive enhancement. Computers & Mathematics with Applications. Vol. 29, iss. 2, pp. 27–62. DOI: https://doi.org/10.1016/0898-1221(94)00215-7

Bundy, A. (ed.) (1994). The QED Manifesto. Automated Deduction – CADE 12. Berlin, Heidelberg: Springer-Verlag Publ., pp. 238–251.

Church, A. (1932). A set of postulates for the foundation of logic. Annals of Mathematics (Second Series). Vol. 33, no. 2, pp. 346–366. DOI: https://doi.org/10.2307/1968337

Church, A. (1940). A formulation of the simple theory of types. The Journal of Symbolic Logic. Vol. 5, iss. 2, pp. 56–68. DOI: https://doi.org/10.2307/2266170

Davies, B. (2005). Whither mathematics? Notices of the American Mathematical Society. Vol. 52, no. 11, pp. 1350–1356.

Davis, M. (1983). A computer program for presburger’s algorithm. Automation of Reasoning. Vol. 1: Classical Papers on Computational Logic, 1957–1966, ed. by J. Sielmann, G. Wrightson. Berlin, Heidelberg: Springer-Verlag Publ., pp. 41–48. DOI: https://doi.org/10.1007/978-3-642-81952-0_3

Davis, M. (1983). The prehistory and early history of automated deduction. Automation of Reasoning. Vol. 1: Classical Papers on Computational Logic, 1957–1966, ed. by J. Sielmann, G. Wrightson. Berlin, Heidelberg: Springer-Verlag Publ., pp. 1–28. DOI: https://doi.org/10.1007/978-3-642-81952-0_1

De Bruijn, N. (1983). Automath, a language for mathematics. Automation of Reasoning. Vol. 2: Classical Papers on Computational Logic, 1967–1970, ed. by J. Sielmann, G.. Wrightson. Berlin, Heidelberg: Springer-Verlag Publ., pp. 159–200. DOI: https://doi.org/10.1007/978-3-642-81955-1_11

Domanov, O.A. (2017). [Structuralism and constructivism in human sciences and mathematics]. Sibirskiy filosofskiy zhurnal [Siberian Journal of Philosophy]. Vol. 15, no. 3, pp. 39–50. DOI: https://doi.org/10.25205/2541-7517-2017-15-3-39-50

Homotopy type theory: univalent foundations of mathematics (2013). Available at: https://homotopytypetheory.org/book/ (accessed 01.11.2020).

Khlebalin, A.V. (2020). [Interactive proof: verification and generation of new mathematical knowledge]. Filosofiya nauki [Philosophy of Sciences]. No. 1, pp. 87–95. DOI: https://doi.org/10.15372/ps20200105

Lamberov, L.D. (2017). [Foundations of mathematics: set theory vs. type theory]. Filosofiya nauki [Philosophy of Sciences]. No. 1, pp. 41–60. DOI: https://doi.org/10.15372/ps20170104

Lamberov, L.D. (2018). [The concept of proof in the context of a type-theoretic approach, I: proof of computer program correctness]. Vestnik Tomskogo gosudarstvennogo universiteta. Filosofiya. Sotsiologiya. Politologiya [Tomsk State University Journal of Philosophy, Sociology and Political Science]. No. 46, pp. 49–57. DOI: https://doi.org/10.17223/1998863x/46/6

Lamberov, L.D. (2018). [Univalence and the concept of structure in the philosophy of mathematics]. Sibirskii filosofskii zhurnal [Siberian Journal of Philosophy]. Vol. 16, no. 1, pp. 20–32. DOI: https://doi.org/10.25205/2541-7517-2018-16-1-20-32

Lamberov, L.D. (2019). [The concept of proof in the context of type-theoretic approach, II: proofs of theorems]. Vestnik Tomskogo gosudarstvennogo universiteta. Filosofiya. Sotsiologiya. Politologiya [Tomsk State University Journal of Philosophy, Sociology and Political Science]. No. 49, pp. 34–41. DOI: https://doi.org/10.17223/1998863x/49/4

Lamberov, L.D. (2020). [The concept of proof in the context of type-theoretic approach, III: proofs as (some) types]. Vestnik Tomskogo gosudarstvennogo universiteta. Filosofiya. Sotsiologiya. Politologiya [Tomsk State University Journal of Philosophy, Sociology and Political Science]. No. 57, pp. 25–32. DOI: https://doi.org/10.17223/1998863Х/57/3

Lawvere, F.W. (1971). Quantifiers and sheaves. Actes du congres international des mathematiciens, ed. by M. Berger, J. Dieudonne et al. [Proceedings of the International Congress of mathematicians, ed. by M. Berger, J. Dieudonne et al.]. Nice: Gauthier-Villars Publ., vol. 1, pp. 329–334.

Martin-Löf, P. (1984). Intuitionistic type theory. Napoli: Bibliopolis Publ., 100 p.

Mercer, J. (1909). Functions of positive and negative type and their connection with the theory of integral equations. Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences. Vol. 209, iss. 441–458, pp. 415–446. DOI: https://doi.org/10.1098/rsta.1909.0016

Milner, R. (1979). LCF: a way of doing proofs with a machine. Mathematical Foundations of Computer Science 1979. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer Publ., vol. 74, pp. 146–159. DOI: https://doi.org/10.1007/3-540-09526-8_11

Newel, A., Shaw, J.C. and Simon, H.A. (1983). Empirical explorations with the logic theory machine: a case study in heuristics. Automation of Reasoning. Vol. 1: Classical Papers on Computational Logic, 1957–1966, ed. by J. Sielmann, G. Wrightson. Berlin, Heidelberg: Springer-Verlag Publ., pp. 49–73. DOI: https://doi.org/10.1007/978-3-642-81952-0_4

Polanyi, M. (1958). Personal knowledge: towards a post-critical philosophy. Chicago, IL: University of Chicago Press, 428 p.

Robertson, N. and Seymour, P. (1983). Graph minors. I. Excluding a forest. Journal of Combinatorial Theory. Series B. Vol. 35, iss. 1, pp. 39–61. DOI: https://doi.org/10.1016/0095-8956(83)90079-5

Robertson, N. and Seymour, P. (2004). Graph minors. XX. Wagner’s conjecture. Journal of Combinatorial Theory. Series B. Vol. 92, iss. 2, pp. 325–357. DOI: https://doi.org/10.1016/j.jctb.2004.08.001

Rodin, A.V. (2014). [To do and to show]. Dokazatel’stvo: ochevidnost’, dostovernost’ i ubeditel’nost’ v matematike, pod red. V.A. Bazhanova, A.N. Krichevts, V.A. Shaposhnikova [Proof: evidence, certainty, conclusiveness in mathematics, ed. by. V.A. Bazhanov, A.N. Krichevts, V.A. Shaposhnikov]. Moscow: Librokom Publ., pp. 219–255.

Rodin, A. (2019). Formal proof-verification and mathematical intuition: the case of univalent foundations. 16th International Congress on Logic, Methodology and Philosophy of Science and Technology (Prague, August 5–10, 2019): Book of Abstracts. Prague, p. 418.

Russell, B. (1903). The principles of mathematics. Cambridge, MA: Cambridge University Press, 534 p.

Rybakov, V.V. (ed.) (1997). Studies in Logic and the Foundations of Mathematics. Vol. 136: Admissibility of Logical Inference Rules. Amsterdam: Elsevier Science Publ., 616 p. DOI: https://doi.org/10.1016/s0049-237x(97)x8001-2

Shanker, S. (1987). Wittgenstein and the turning point in the philosophy of mathematics. Albany: Croom Helm Publ., 358 p.

Shaposhnikov, V.A. (2018). [Distributed cognition and mathematical practice in the digital society: from formalized proofs to revisited foundations]. Epistemologiya i filosofiya nauki [Epistemology and Philosophy of Science]. Vol. 55, no. 4, pp. 160–173. DOI: https://doi.org/10.5840/eps201855474

Scheffer, V. and Taylor, J.E. (eds.) (2000). Almgren’s big regularity paper: q-valued functions minimizing dirichlet’s integral and the regularity of area-minimizing rectifiable currents up to codimension. Singapore: World Scientific Publ., 972 p. DOI: https://doi.org/10.1142/4253

Solomon, R. (2018). The classification of finite simple groups: a progress report. Notices of the American Mathematical Society. Vol. 65, no. 6, pp. 646–651. DOI: https://doi.org/10.1090/noti1689

Teller, P. (1980). Computer proof. The Journal of Philosophy. Vol. 77, iss. 12, pp. 797–803. DOI: https://doi.org/10.2307/2025805

Tselischev, V.V. (2006). Epistemologiya matematicheskogo dokazatel’stva [Epistemology of mathematical proof]. Novosibirsk: Parallel’ Publ., 212 p.

Tselischev, V.V. (2007). Intuitsiya, finitizm i rekursivnoe myshlenie [Intuition, finitism, and human understanding]. Novosibirsk: Parallel’ Publ., 220 p.

Tselischev, V.V. and Khlebalin, A.V. (2020). [Formalism in mathematics and conception of understanding]. Filosofiya nauki [Philosophy of Sciences]. No. 2, pp. 45–58. DOI: https://doi.org/10.15372/ps20200204

Tymoczko, T. (1979). The four-color theorem and its philosophical significance. The Journal of Philosophy. Vol. 76, iss. 2, pp. 57–83. DOI: https://doi.org/10.2307/2025976

Weiss, I. (2016). The QED manifesto after two decades – Version 2.0. Journal of Software. Vol. 11, no. 8, pp. 803–815. DOI: https://doi.org/10.17706/jsw.11.8.803-815

Wiedijk, F. (2007). The QED manifesto revisited. Studies in Logic, Grammar and Rhetoric. Vol. 10, iss. 23, pp. 121–133.

Wiedijk, F. (2008). Formal proof — getting started. Notices of the American Mathematical Society. Vol. 55, no. 11, pp. 1408–1414.

Wos, L. and Henschen, L. (1983). Automated theorem proving, 1965–1970. Automation of Reasoning. Vol. 2: Classical Papers on Computational Logic, 1967–1970, ed. by J. Sielmann, G. Wrightson. Berlin, Heidelberg: Springer-Verlag Publ., pp. 1–24. DOI: https://doi.org/10.1007/978-3-642-81955-1_1