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

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

Еще одним «неудобным» Π₁-высказыванием может оказаться утверждение, устанавливающее истинность теоремы о четырех красках, — теоремы, согласно которой плоскую (или сферическую)карту «мира» можно, используя всего четыре краски, раскрасить так, чтобы любая «страна» получила собственный, отличный от соседей цвет. Теорема о четырех красках была- таки доказана в 1976 году (после 124 лет неудачных попыток) Кеннетом Аппелем и Вольфгангом Хакеном, причем доказательство потребовало использования 1200 часов компьютерного времени. Принимая во внимание то обстоятельство, что существенную часть доказательства составил впечатляющий объем компьютерных вычислений, можно предположить, что полная запись его на бумаге потребовала бы невероятного ее количества. Если же сформулировать эту теорему в виде Π₁- высказывания, то степень сложности такого высказывания будет очень небольшой, хотя, наверное, все же большей, нежели степень сложности Π₁-высказывания, необходимого для выражения гипотезы Гольдбаха. Если бы доказательство Аппеля—Хакена было выдвинуто одним из наших роботов в качестве кандидата на получение ☆-статуса, то его пришлось бы проверять очень и очень тщательно. Для утверждения обоснованности каждого его отдельного фрагмента потребовалось бы участие всего сообщества элитных роботов. И все же, несмотря на сложность доказательства в целом, один лишь объем его чисто вычислительной части вряд ли смог бы явиться сколько-нибудь серьезным затруднением для наших роботов. В конце концов, выполнение точных вычислений — это их работа.

Упомянутые Π₁-высказывания вполне укладываются в пределы степени сложности, устанавливаемые любым достаточно большим значением c, — например, тем, что может быть обусловлено каким-либо правдоподобным набором механизмов M, лежащим в основе поведения наших роботов. Несомненно, найдется множество других Π₁-высказываний, которые будут значительно сложнее приведенных здесь, хотя степень их сложности и не превысит величины c. Некоторые из таких Π₁-высказываний окажутся, скорее всего, особенно неудоборешаемыми, а доказать некоторые из последних, в свою очередь, будет наверняка еще сложнее, чем теорему о четырех красках или даже гипотезу Гольдбаха. Любое из этих Π₁-высказываний, истинность которого может быть однозначно установлена роботами (посредством демонстрации, достаточно убедительной для присвоения высказыванию ☆-статуса и успешного преодоления им всех заграждений, установленных с целью обеспечения безошибочности получаемых роботами результатов), автоматически становится теоремой формальной системы Q*.

Кроме того, возможны и пограничные случаи, приемлемость или неприемлемость (причем грань между этими состояниями весьма тонка) которых определяется строгостью стандартов, необходимых для получения ☆-статуса, или тем, насколько точный характер имеют меры предосторожности, установленные с целью обеспечения безошибочности утверждений, принимаемых в качестве «кирпичей» для построения формальной системы Q*. Точная формулировка системы Q* будет различной в зависимости от того, полагаем мы такое Π₁-высказывание P безошибочным ☆-утверждением либо нет. В обычных обстоятельствах эта разница не имеет большого значения, поскольку различные варианты системы Q*, обусловленные принятием или отклонением высказывания P, являются логически эквивалентными. Такая ситуация может возникнуть в случае Π₁-высказываний, доказательства истинности которых роботы могут счесть сомнительными просто из-за их чрезмерной сложности. Если доказательство высказывания P окажется на деле логическим следствием из других ☆- утверждений, которые уже приняты как безошибочные, то возникнет эквивалентная система Q*, причем вне зависимости от того, принимается высказывание P в качестве ее теоремы или нет. С другой стороны, возможны такие Π₁-высказывания, которые потребуют для своего доказательства каких-то хитроумных логических процедур, выходящих за рамки любых логических следствий из тех ☆-утверждений, которые были приняты как безошибочные ранее, при построении системы Q*. Обозначим получаемую таким образом формальную систему (до включения в нее высказывания P) через Q*₀, а систему, образующуюся после присоединения к системе Q*₀ высказывания P, через Q*₁. Система Q*₁ окажется неэквивалентна системе Q*₀ в том, например, случае, если высказыванием P будет гёделевское предположение G(Q*₀). Однако если роботы, в соответствии с нашим допущением, способны достичь человеческого уровня математического понимания (а то и превзойти его), то они безусловно должны быть способны понять аргументацию Гёделя, так что им ничего не остается, как признать истинность гёделевского предположения для какой угодно системы Q*₀ (присвоив ему гарантирующий безошибочность ☆-статус), коль скоро обоснованность этой системы Q*₀ ими же ☆-