Понятие доказательства в контексте теоретико-типового подхода, II: доказательства теорем

Lev D. Lamberov, Ural Federal University (Yekaterinburg, Russian Federation).

THE CONCEPT OF PROOF IN THE CONTEXT OF A TYPE-THEORETIC APPROACH, II: PROOFS OF THEOREMS

Keywords: foundations of mathematics; proof; type theory; computer science; theorem; computation; four color theorem

This article is a continuation of the study of the epistemological features of the concept of proof in the context of a type-theoretic approach. The previous article was devoted to epistemology of computer program correctness proofs. It addressed the problems of surveyability of this type of proof, the question of their social role. In turn, this article focuses on the use of various computer tools to prove theorems. The article considers the brute force proofs, briefly examines the general structure of the proof of the four color theorem as proposed by Kenneth Appel and Wolfgang Haken. The most interesting comment about the four color theorem was made by Thomas Tymoczko. His argument concerns the notion of surveyability of proof, and one of the central points is the doubts about the concepts of theorem and proof. According to Tymoczko, the use of computers in obtaining mathematical results leads to the introduction of experimental methods in mathematics. Otto Bradley Bassler emphasizes the concept of an intermediate step and the idea of continuity of thinking in Francis Bacon, Renй Descartes and John Locke. According to Bassler, it is reasonable to distinguish between local and global surveyability. The Appel-Haken proof of the four color theorem is globally observable, but not locally observable. It should be noted that not every mathematician checks absolutely all mathematical results in the process of learning and further work. Proof verification is a social process. If even potential local surveyability cannot be guaranteed, then conviction of the proof is akin to believing in inductive generalizations. The mathematician believes in the correctness of the work of the computer, and this belief turns out to be justified in the spirit of reliabilism. The researcher is convinced of the reliability of the computer. However, this conviction is very complex. Paul Teller expresses an alternative point of view regarding the surveyability of proof. According to Teller, the surveyability of proof constitutes human mathematics, but not mathematics in general. Edwin Coleman expresses a close idea. He points out that practically any proof, if we demand full explication and proof of all intermediate results, will be so long that it will completely go beyond the limits of surveyability. Proofs are surveyable only insofar as they are part of the written archive of mathematical results and rely on the set of intermediate lemmas and theorems that are also included in the “World Mathematical Archive”.

Основная часть

Настоящая статья является продолжением исследования эпистемологических особенностей понятия доказательства в рамках теоретико-типового подхода. Предыдущая статья [1] была посвящена эпистемологии доказательства (корректности) программ, в ней рассматривались проблемы обозримости указанного вида доказательств, вопрос об их социальной роли, а также соотношение доказательства с особенностями понимания абстракции в компьютерных науках. В свою очередь, в данной статье внимание обращено на применение различных компьютерных средств к доказательству теорем (т.е. использование вычислительных машин для получения математических результатов). В дальнейшем будут рассмотрены доказательства методом перебора.

Примеров применения вычислительных машин для получения математических результатов методом перебора достаточно. Если останавливаться только на самых известных, то следует указать доказательство К. Лама, Л. Тиля и С. Свирша [2] теоремы о несуществовании конечной плоскости порядка 10, а также доказательство Т. Хэйлса [3] гипотезы Кеплера о плотнейшей упаковке сфер в трехмерном пространстве (позже Т. Хэйлс представил и полное формальное доказательство на языке HOL Light). Тем не менее самым знаменитым остается, безусловно, доказательство теоремы о четырех красках, полученное в конце 1970-х гг. К. Аппелем и В. Хакеном [4, 5], которое и вызвало наиболее жаркие споры по поводу применения компьютеров в деле доказательства теорем. Помимо того, что доказательство всесторонне проверялось математическим сообществом, этот результат был независимо подтвержден еще несколько раз. Во-первых, Ф. Олэйр [6] построил в 1977 г. свое доказательство, применив некоторые другие эвристики, но в целом сохранив общий замысел К. Аппеля и В. Хакена. Во-вторых, Н. Робертсон, Д. Сандерс, П. Сеймур и Р. Томас [7] сформулировали в 1993 г. еще одно доказательство, в первую очередь для того, чтобы гарантировать «теоремность» рассматриваемого результата, поскольку некоторые новые результаты в теории графов зависели от него (использовали теорему о четырех красках в качестве леммы). В-третьих, это чистое формальное доказательство, построенное в 2005 г. Ж. Гонтье [8].

Для того чтобы лучше представить себе доказательство методом перебора, кратко рассмотрим общую структуру доказательства теоремы о четырех красках, как оно предложено К. Аппелем и В. Хакеном. Для начала следует отметить, что их доказательство возникло не на пустом месте, а развивает попытки предыдущих исследователей (прежде всего А. Кэмпе и Г. Хиша). К примеру, несмотря на то, что доказательство А. Кэмпе было опровергнуто, (1) его доказательство для случая 6 и более красок является верным, (2) ряд ключевых идей и общая структура построения доказательства использованы в рассматриваемом доказательстве 1970-х гг.

Для начала необходимо дать определение нормальной карты. Нормальной картой называется карта, на которой ни одна «внутренняя» страна не охватывает целиком никакую другую страну, а также нет такой точки, в которой бы встречалось более трех стран. Любая карта может быть преобразована в нормальную карту при помощи специальной процедуры. Если для раскрашивания получившейся нормальной карты достаточно N цветов, то для раскрашивания оригинальной карты также достаточно N цветов. В своей работе А. Кэмпе показал, что любая нормальная карта должна содержать страну с менее чем шестью соседями. Таким образом, можно выделить несколько типов неизбежных наборов конфигураций: страна с двумя соседями, страна с тремя соседями, страна с четырьмя соседями, страна с пятью соседями. Далее требуется показать редуцируемость различных неизбежных наборов конфигураций. Контрпример П.Дж. Хивуда опровергал доказательство редуцируемости случая страны с пятью соседями в доказательстве А. Кэмпе, а в начале XX в. вопрос редуцируемости на графах был подробно разработан Дж. Биркгофом. Редуцируемость предполагает, что если имеется нормальная карта, для раскрашивания которой требуется, допустим, пять цветов, содержащая одну из неизбежных конфигураций, то должна существовать карта с меньшим числом стран, для которой также требуется пять красок. Тем не менее поскольку не может существовать минимальная нормальная карта, для раскрашивания которой требуется пять красок, то не может существовать карта, для которой требуется пять красок.

Для доказательства требуется (1) выделить неизбежный набор конфигураций и (2) показать его редуцируемость. Для этого К. Аппелем и В. Хакеном и был использован метод перебора. По сути, их доказательство представляет собой доказательство методом индукции с (1) тривиальным случаем, (2) случаем, предполагающим несколько подслучаев, и (3) случаем, предполагающим более тысячи подслучаев. Индукция проводится по числу вершин карты (карта преобразуется в граф), демонстрируется, что для определенного набора редуцируемых конфигураций раскрашивание может быть выполнено с помощью чертырех красок, а затем показывается, что набор редцуируемых конфигураций является неизбежным (т.е. любая карта содержит хотя бы одну такую конфигурацию). Другими словами, с помощью вычислительных машин были сформированы неизбежные наборы конфигураций и продемонстрирована их редуцируемость. Всего было затрачено более 1 200 часов машинного времени на трех разных машинах, потребовалось провести машинный анализ более 2 000 конфигураций, в финальном доказательстве используется редукция 1 482 конфигураций, ручная проверка которых, по словам авторов, просто невозможна [9. P. 121].

Помимо амбивалентной реакции со стороны математического сообщества, доказательство теоремы о четырех красках методом перебора, не предполагающего человеческой проверки за разумное обозримое время, вызвало реакцию философов математики. Наиболее яркий и провокативный комментарий по поводу теоремы о четырех красках высказал Т. Тимошко [10]. Его аргументация касается понятия обозримости доказательства, а один из центральных моментов состоит в сомнении по поводу понятий теоремы и доказательства. С точки зрения Т. Тимошко, использование компьютеров при получении математических результатов приводит к введению в математику экспериментальных методов. В определенном смысле идеи Т. Тимошко оказываются весьма близки философии математики И. Лакатоса, который, надо сказать, упоминается в приведенной статье. Здесь имеются в виду фаллибилистское или квазиэмпиристское истолкование математики и процесса уточнения математических понятий, описываемые в «Доказательствах и опровержениях».

Итак, доказательство может быть понято (1) как средство достижения убежденности, (2) как обозримая конструкция, (3) как конструкция, которая может быть формализована. Причем доказательство обладает убедительной силой в том случае, если оно обозримо и формализуемо. Убедительность математического доказательства зависит от понимания общей структуры доказательства, а также от понимания каждого отдельного шага и перехода между элементарными шагами.

Вслед за Б. Бэсслером [11, 12] можно обратить внимание на выделение понятия промежуточного шага и идеи непрерывности мышления у Ф. Бэкона, Р. Декарта и Дж. Локка. Соответственно, можно выделить обозримость в смысле интуитивной понятности перехода между элементарными шагами доказательства, которая вероятнее всего обеспечивается использованием достаточно элементарных правил и гарантируется прежде всего при формализации доказательств (т.е. при обращении к механической процедуре), а также интуитивное постижение сложной цепочки рассуждений целиком. С точки зрения Б. Бэсслера, разумно выделить локальную и глобальную обозримости, предполагающие соответственно обозримость отдельных шагов доказательства в некотором порядке и обозримость всего доказательства целиком.

Применение предложенного Б. Бэсслером различия к доказательству теоремы о четырех красках К. Аппеля и В. Хакена показывает, что само по себе доказательство является глобально обозримым, поскольку его общая логическая структура вполне понятна. Тем не менее следует признать, что несмотря на логическую простоту, это доказательство обладает высокой комбинаторной сложностью (в смысле сложности вычислений). Последнее обстоятельство не позволяет доказательству теоремы о четырех красках быть локально обозримым. При построении неизбежного набора конфигураций К. Аппелем и В. Хакеном было использовано около 500 правил, что дало, как уже указывалось, 1 482 конфигурации. Хотя в общем смысле принципы построения и вообще концепция неизбежных наборов конфигураций могут быть понятны, сам процесс их формирования в данном конкретном случае никоим образом не является локально обозримым. В нем присутствует непрерывность рассуждения в смысле философов Нового времени, в нем присутствуют промежуточные шаги в том отношении, в каком можно выделить промежуточные шаги в вычислении в противовес логическому рассуждению. Однако сложность и (в первую очередь) длительность этой процедуры не позволяют ни одному живому человеку фактически проследить каждый шаг и каждое применение правила. Доказательство теоремы о четырех красках в лучшем случае может претендовать на потенциальную локальную обозримость (применение около 500 правил, конечно, вызывает определенные сомнения даже в потенциальной локальной обозримости). В этом случае получается, что глобальная обозримость не зависит от локальной обозримости.

Однако является ли обозримость неотъемлемым свойством доказательства? Необходимо отметить, что далеко не каждый математик проверяет абсолютно все математические результаты в процессе своего обучения и дальнейшей работы. Проверка доказательств является социальным процессом, о чем речь шла в предыдущей статье [1]. Правда, даже несмотря на своего рода «распределенность» требования обозримости по всему математическому сообществу, доказательства, подобные рассматриваемому доказательству теоремы о четырех красках, вряд ли могут считаться обозримыми в локальном смысле. Если не может быть гарантирована даже потенциальная локальная обозримость, то убежденность в правильности доказательства оказывается сродни вере в индуктивные обобщения. Так, в процитированной статье Т. Тимошко, как было указано ранее, проблематизирует понятия теоремы и доказательства и в конечном счете склоняется к точке зрения, что традиционного понятия доказательства недостаточно, поскольку оно исключает всяческие эмпирические элементы из математических результатов. По его мнению, доказательство теоремы о четырех красках, предложенное К. Аппелем и В. Хакеном, является математическим доказательством, а сама «теорема» полноценной математической теоремой. Дело лишь в том, что математика, по мнению Т. Тимошко, представляет собой фаллибилистское предприятие сродни естественным наукам. Комбинаторная сложность, сложность вычислений, используемых для получения и обоснования некоторых математических результатов, оказывается сродни эмпирическим элементам и экспериментам в естественных науках. Необходимо также отметить, что сам Т. Тимошко проводит различие, оказывающееся весьма близким различию локальной и глобальной обозримости и состоящее в разграничении собственно доказательства и описания доказательства. Представляется, что разграничение Б. Бэсслером локальной и глобальной обозримости перестает служить средством проблематизации эпистемологических вопросов касательно математических доказательств в духе вопроса о том, почему и в каких случаях глобальная обозримость не зависит от локальной обозримости. Последнее не вызывает проблем в связи с доказательством теоремы о четырех красках, поскольку то, что является в нем глобально обозримым, по сути, является описанием общей структуры доказательства, а для описания общей структуры доказательства вполне разумно абстрагироваться от мелких деталей, представляющих собой отдельно взятые шаги, сохраняя лишь связность общей «картины».

Однако не оказывается ли эпистемологическое затруднение с доказательством теоремы о четырех красках еще более радикальным? Заметьте, исследователь верит в корректность работы вычислительной машины, и эта вера оказывается обоснованной в духе релайабилизма. Исследователь убежден в надежности работы вычислительной машины. Тем не менее эта убежденность весьма сложного вида: она предполагает убежденность в проекте вычислительной машины (включая всю теоретическую базу такого проекта), убежденность в правильности реализации проекта в конкретном железе, убежденность в том, что в момент запуска соответствующей вычислительной процедуры машина находится в «нормальном» состоянии (например, на нее не оказывается какое-либо физическое воздействие, способное изменить результат вычислений), убежденность в правильности вычислительной процедуры, убежденность в корректности реализации этой процедуры в виде компьютерной программы, убежденность в правильности работы операционной системы и ее компонентов и т.д. Таким образом, убежденность в надежности компьютерных вычислений не сильно отличается от убежденности в результатах работы черного ящика в словах гениального марсианского математика Саймона или в прозрениях Рамануджана. Безусловно, надежность работы вычислительной машины потенциально может быть проверена, что, правда, абсолютно не исключает возможности ошибки в силу каких-либо неучтенных даже при самой тщательной проверке факторов. Однако уже этого достаточно, чтобы доказательство теоремы о четырех красках не могло быть воздвигнуто на пантеон «традиционных» априорных математических доказательств.

А так ли важна обозримость для доказательства? Какую роль играет эта «интеллектуальная добродетель» в математической практике? В связи с этим вопросом можно обратиться к философии математики Л. Витгенштейна [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.