3.25. Сложность в математических доказательствах 309

ющей вычислительную проверку, - то мы снова окажемся в ситуации формальной системы, над которой грозно нависает гёделевское доказательство, явным образом демонстрируя, что любая точная формализация подобного рода не может представлять всю совокупность аргументов, пригодных, в принципе, для установления истинности -высказываний. Гёделевское доказательство показывает - к добру ли, к худу ли, - что никаким допускающим вычислительную проверку способом невозможно охватить все приемлемые человеком методы математического рассуждения.

Читатель, возможно, уже беспокоится, что все мои рассуждения здесь затеяны с целью получить точное определение понятия "роботово доказательство" посредством хитрого трюка с "безошибочными -утверждениями". В самом деле, при введении гёделевского рассуждения необходимым предварительным условием было как раз получение точного определения этого понятия. Возникшее же в результате противоречие просто послужило еще одним подтверждением того факта, что человеческое понимание математической истины невозможно полностью свести к процедурам, допускающим вычислительную проверку. Главной целью всех представленных рассуждений было показать, посредством reductio ad absurdum, что человеческое представление о восприятии неопровержимой истинности высказываний невозможно реализовать в рамках какой бы то ни было вычислительной системы, будь она точной или какой-либо иной. В этом нет никакого парадокса, хотя кому-то полученные выводы могут показаться весьма и весьма тревожными. Получение противоречивых выводов является вполне естественным и даже единственно возможным завершением любого доказательства, построенного на reductio ad absurdum, кажущаяся парадоксальность этих выводов служит лишь для того, чтобы полностью исключить из рассмотрения то самое предположение, с которого доказательство, собственно, и начиналось.

3.25. Сложность в математических доказательствах

Существует, однако, еще одно немаловажное соображение, о котором необходимо упомянуть. Суть его заключается в том, что, хотя количество -высказываний, которые необходи-

310 Глава 3

мо принимать в рассмотрение в рамках приведенного в §3.20 рассуждения, является конечным, нет никакого явного ограничения на объем доказательств, необходимых роботам для реализации -демонстрации истинности всех этих -высказываний. Даже если ограничить степень сложности принимаемых в рассмотрение -высказываний самым скромным пределом с, то все равно придется учитывать и некоторые весьма громоздкие и сложные случаи. Например, гипотезу Гольдбаха (см. §2.3), согласно которой каждое четное число, большее 2, является суммой двух простых чисел, можно сформулировать в виде высказывания очень небольшой степени сложности, и в то же время она представляет собой настолько сложный случай, что все попытки математиков-людей однозначно установить ее истинность до сих пор не увенчались успехом. Учитывая подобные обстоятельства, можно предположить, что если кому-то в конце концов удастся отыскать доказательство действительной истинности Гольдбахова -высказывания, то это доказательство неизбежно окажется весьма и весьма сложным и изощренным. Если такое доказательство выдвинет в качестве кандидата на -утверждение один из наших роботов, то прежде, чем его таковым признают, оно непременно будет подвергнуто чрезвычайно тщательному исследованию (возможно, даже силами всего роботского общества, ответственного за присвоение -статуса). В случае гипотезы Гольдбаха нам неизвестно, является ли это высказывание действительно истинным, - а если является, то возможно ли его доказательство в рамках известных и общепринятых методов математического доказательства. Иначе говоря, это -высказывание может входить в формальную систему , а может и не входить.

Еще одним "неудобным" -высказыванием может оказаться утверждение, устанавливающее истинность теоремы о четырех красках, - теоремы, согласно которой плоскую (или сферическую)карту "мира" можно, используя всего четыре краски, раскрасить так, чтобы любая "страна" получила собственный, отличный от соседей цвет. Теорема о четырех красках была-таки доказана в 1976 году (после 124 лет неудачных попыток) Кеннетом Аппелем и Вольфгангом Хакеном, причем доказательство потребовало использования 1200 часов компьютерного времени. Принимая во внимание то обстоятельство, что существенную часть доказательства составил впечатляющий объем ком-