Однако не оказывается ли эпистемологическое затруднение с доказательством теоремы о четырех красках еще более радикальным? Заметьте, исследователь верит в корректность работы вычислительной машины, и эта вера оказывается обоснованной в духе релайабилизма. Исследователь убежден в надежности работы вычислительной машины. Тем не менее эта убежденность весьма сложного вида: она предполагает убежденность в проекте вычислительной машины (включая всю теоретическую базу такого проекта), убежденность в правильности реализации проекта в конкретном железе, убежденность в том, что в момент запуска соответствующей вычислительной процедуры машина находится в «нормальном» состоянии (например, на нее не оказывается какое-либо физическое воздействие, способное изменить результат вычислений), убежденность в правильности вычислительной процедуры, убежденность в корректности реализации этой процедуры в виде компьютерной программы, убежденность в правильности работы операционной системы и ее компонентов и т.д. Таким образом, убежденность в надежности компьютерных вычислений не сильно отличается от убежденности в результатах работы черного ящика в словах гениального марсианского математика Саймона или в прозрениях Рамануджана. Безусловно, надежность работы вычислительной машины потенциально может быть проверена, что, правда, абсолютно не исключает возможности ошибки в силу каких-либо неучтенных даже при самой тщательной проверке факторов. Однако уже этого достаточно, чтобы доказательство теоремы о четырех красках не могло быть воздвигнуто на пантеон «традиционных» априорных математических доказательств.
А так ли важна обозримость для доказательства? Какую роль играет эта «интеллектуальная добродетель» в математической практике? В связи с этим вопросом можно обратиться к философии математики Л. Витгенштейна [13, 14], по мнению которого доказательства представляют собой грамматические конструкции, позволяющие «схватывать» смысл математических терминов, и определяют правила их употребления. Очевидно, что если доказательство не является обозримым, то мы не можем научиться употреблению определяемых им математических терминов. Следует отметить, что близкое затруднение связывается Л. Витгенштейном с изучением слов, обозначающих цвета. Суть затруднения состоит в разграничении доказательства и эксперимента в том отношении, что доказательство предполагает обозримость своих элементарных шагов, т.е. предполагает очевидные логические, концептуальные или нормативные отношения между отдельными шагами. Тем не менее следует отметить, что в отличие от рассмотрения слов, обозначающих цвета, при рассмотрении понятия доказательства Л. Витгенштейн более не использует идею «феноменологической обозримости» [15]. Необходимо обратить внимание на то, что описание операции (например, построения бесконечного ряда натуральных чисел) вполне может быть «схвачено». Тем не менее вопрос соотношения доказательства и эксперимента, парадигмы и шаблона в философии математики Л. Витгенштейна в настоящее время далек от ясности и требует отдельного обстоятельного исследования.
Заключение
Таким образом, несмотря на, казалось бы, экспериментальный характер некоторых частей доказательства теоремы о четырех красках, оно вполне может выполнять роль грамматической конструкции, определяющей правила употребления соответствующих математических терминов, поскольку у нас имеется вполне обозримое описание доказательства, которое позволяет воспроизводить это доказательство, повторять процедуру доказывания .
Альтернативную точку зрения по поводу обозримости доказательства высказывает П. Теллер [17], согласно которому обозримые доказательства составляют человеческую математику, но не математику вообще. Обозримость требуется людям для выполнения проверки доказательств, но никакие обстоятельства не запрещают представить себе некоторые другие организмы, рассуждающие сходным с компьютерами образом, которые могут оказаться способными выполнить проверку комбинаторно сложных частей доказательства теоремы о четырех красках. Почему же в этом случае математика должна ограничиваться только тем, что доступно для проверки людьми? И тем не менее такая гипотетическая ситуация не обязательно будет схожа со случаем марсианского математика Саймона или Рамануджана, так как в конце концов надежность работы вычислительной машины может быть проверена, а сами комбинаторно сложные вычисления воспроизведены при наличии соответствующих ресурсов. Другими словами, вычислительная машина все же имеет более высокую степень надежности, чем оракул. Близкую идею высказывает Э. Коулмэн [18], указывая на то, что практически любое доказательство, если требовать полной экспликации и доказательства всех промежуточных результатов, на которых оно основывается, будет настолько длинным, что вполне выйдет за границы обозримости. Доказательства оказываются обозримыми лишь постольку, поскольку они являются частью записанного архива математических результатов и опираются без предъявления доказательств на множество промежуточных лемм и теорем, также входящих во «всемирный математический архив». Можно допустить, что даже комбинаторно сложные части некоторого доказательства могут быть представлены в виде некоторого количества промежуточных результатов, доступных для проверки не отдельно взятым математиком, но по частям всем математическим сообществом.
математика доказательство обозримость теорема
Литература
1. Ламберов Л.Д. Понятие доказательства в контексте теоретико-типового подхода, I: доказательство программ // Вестник Томского государственного университета. Философия. Социология. Политология. 2018. № 6. С. 49-57.
2. Lam C. W.H., ThielL., Swiercz S. The Non-Existence of Finite Projective Planes of Order 10 // Canadian Journal of Mathematics. 1989. № 41. P. 1117-1123.
3. Hales T.C. A Proof of the Kepler Conjecture // Annals of Mathematics, Second Series. 2005. Vol. 162, № 3. P. 1065-1185.
4. Appel K., Haken W. Every Planar Map is Four Colorable. I. Discharging // Illinois Journal of Mathematics. 1977. Vol. 21, № 3. P. 429-490.
5. Appel K., Haken W., Koch J. Every Planar Map is Four Colorable. II. Reducibility // Illinois Journal of Mathematics. 1977. Vol. 21, № 3. P. 491-567.
6. Allaire F. Another Proof of the Four Colour Theorem Part I // Proceedings of the 7th Manitoba Conference on Numerical Mathematics and Computing / ed. by D. McCarthy; H.C. Williams. Winnipeg : Utilitas Mathematica Pub., 1977. P. 3-72. 1
7. Robertson N., Sanders D., Seymour P., Thomas R. The Four-Colour Theorem // Journal of Combinatorial Theory, series B. 1997. Vol. 70. P. 2-44.
8. Gonthier G. Formal Proof The Four-Color Theorem // Notices of the American Mathematical Society. 2008. Vol. 55, № 11. P. 1382-1393.
9. Appel K., Haken W. The Solution of the Four-Color-Map Problem // Scientific American.1977 Vol. 237. P. 108-121.
10. Tymoczko T. The Four-Color Theorem and Its Philosophical Significance // The Journal of Philosophy. 1979. Vol. 76, № 2. P. 57-83.
11. Bassler O.B. The Surveyability of Mathematical Proof: A Historical Perspective // Synthese. 2006. Vol. 148, № 1. P. 99-133.
12. Целищее В.В. Эпистемология математического доказательства. Новосибирск : Параллель, 2006. 212 с.
13. Wittgenstein L. Remarks on the Foundations of Mathematics. Cambridge, MA : MIT Press,
1977. 444 p.
14. Shanker S. Wittgenstein and the Turning Point in the Philosophy of Mathematics. London : Croom Helm, 1987. 358 p.
15. Secco G.D., PereiraL. C. Proofs Versus Experiments: Wittgensteinian Themes Surrounding the Four-Color Theorem // How Colors Matter to Philosophy / ed. by M. Silva. Cham : Springer International Publishing, 2017. P. 289-307.
16. Wittgenstein L. Tractatus Logico-Philosophicus. London : Routledge, 2004. 108 p.
17. TellerP. Computer Proof // The Journal of Philosophy. 1980. Vol. 77, № 12. P. 797-803.
18. Coleman E. The Surveyability of Long Proofs // Foundations of Science. 2009. Vol. 14. P. 27-43.
References
1. 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. 46. pp. 49-57. (In Russian). DOI: 10.17223/1998863Kh/46/6
2. Lam, C.W.H., Thiel, L. & Swiercz, S. (1989) The Non-Existence of Finite Projective Planes of Order 10. Canadian Journal of Mathematics. 41. pp. 1117-1123.
3. Hales, T.C. (2005) A Proof of the Kepler Conjecture. Annals of Mathematics, Second Series. 162(3). pp. 1065-1185.
4. Appel, K. & Haken, W. (1977) Every Planar Map is Four Colorable. I. Discharging. Illinois Journal of Mathematics. 21(3). pp. 429-490.
5. Appel, K., Haken, W. & Koch, J. (1977) Every Planar Map is Four Colorable. II. Reducibility. Illinois Journal of Mathematics. 21(3). pp. 491-567. DOI: 10.1215/ijm/1256049012
6. Allaire, F. (1977) Another Proof of the Four Colour Theorem Part I. In: McCarthy, D. & Williams, H.C. (eds) Proceedings of the 7th Manitoba Conference on Numerical Mathematics and Computing. Winnipeg: Utilitas Mathematica. 3-72.
7. Robertson, N., Sanders, D., Seymour, P. & Thomas, R. (1997) The Four-Colour Theorem. Journal of Combinatorial Theory, series B. 70. pp. 2-44.
8. Gonthier, G. (2008) Formal Proof The Four-Color Theorem. Notices of the American Mathematical Society. 55(11). pp. 1382-1393.
9. Appel, K. & Haken, W. (1977) The Solution of the Four-Color-Map Problem. Scientific American. 237. pp. 108-121.
10. Tymoczko, T. (1979) The Four-Color Theorem and Its Philosophical Significance. The Journal of Philosophy. 76(2). pp. 57-83.
11. Bassler, O.B. (2006) The Surveyability of Mathematical Proof: A Historical Perspective. Synthese. 148(1). pp. 99-133.
12. Tselishchev, V.V. (2006) Epistemologiya matematicheskogo dokazatel'stva [Epistemology of mathematical evidence]. Novosibirsk: Parallel'.
13. Wittgenstein, L. (1978) Remarks on the Foundations of Mathematics. Cambridge, Mass.: MIT Press.
14. Shanker, S. (1987) Wittgenstein and the Turning Point in the Philosophy of Mathematics. London: Croom Helm.
15. Secco, G.D. &Pereira, L.C. (2017) Proofs Versus Experiments: Wittgensteinian Themes Surrounding the Four-Color Theorem. In: Silva, M. (ed.) How Colors Matter to Philosophy. Cham: Springer International Publishing. pp. 289-307.
16. Wittgenstein, L. (2004) TractatusLogico-Philosophicus. London: Routledge.
17. Teller, P. (1980) Computer Proof. The Journal of Philosophy. 77(12). pp. 797-803.
18. Coleman, E. (2009) The Surveyability of Long Proofs. Foundations of Science. 14. pp. 27-43.