Представьте себе, что вы не знали заранее, что ТТЧ окажется неполной — напротив, вы ожидали, что она полна, то есть, что любое истинное высказывание, которое можно выразить в нотации ТТЧ, является теоремой. В таком случае вы могли бы иметь разрешающую процедуру для всей теории чисел. Ваш метод был бы прост; если вы хотите знать, истинно ли высказывание X теории чисел, вы должны закодировать его в строчку x ТТЧ. Теперь, если X — истинно, то полнота говорит нам, что x — теорема. С другой стороны, если не-X — истинно, тогда ~x — теорема. Таким образом, либо x, либо ~x должны оказаться теоремами, поскольку либо X, либо не-X истинны. Теперь вы должны систематически пронумеровать все теоремы ТТЧ, так же как мы сделали это для систем MIU и pr. Какое-то время спустя, вы наткнетесь либо на x, либо на ~x, и, таким образом, узнаете, какое из двух высказываний — X или не-X — истинно. (Следите ли вы за ходом рассуждения? Очень важно держать в голове разницу между формальной системой ТТЧ и ее неформальным соответствием — теорией чисел; читатель должен постараться хорошо понять эту разницу.) Так что в принципе, если бы ТТЧ была полной, специалисты по теории чисел остались бы без работы: со временем любую проблему можно было бы решить чисто механическим путем. Оказывается, однако, что это невозможно; по этому поводу можно радоваться или огорчаться, в зависимости от вашей точки зрения.
Последний вопрос, который мы рассмотрим в этой главе, таков: должны ли мы так же верить в непротиворечивость ТТЧ, как мы верили в непротиворечивость исчисления высказываний? И если нет, то возможно ли укрепить нашу веру в ТТЧ, доказав, что она непротиворечива? Для начала можно утверждать, подобно тому, как Неосторожность утверждала об исчислении высказываний, что непротиворечивость ТТЧ «очевидна» — а именно, что каждое правило воплощает принцип логических рассуждений, в который мы верим безоговорочно; следовательно, ставить под вопрос непротиворечивость ТТЧ, это все равно, что сомневаться в собственном здравом уме. Этот аргумент все еще имеет некоторый вес, но уже не такой, как раньше. Дело в том, что теперь у нас слишком много правил вывода, и в какие-то из них могла вкрасться ошибка. Более того, откуда мы знаем, что наша мысленная модель неких абстрактных единиц под названием «натуральные числа» последовательна? Может быть, наши собственные мыслительные процессы, те неформальные процессы, которые мы пытались выразить в правилах формальной системы, сами по себе непоследовательны! Конечно, мы не ожидаем подобного подвоха. Тем не менее, можно представить, что чем сложнее объект нашей мысли, тем легче в нем запутаться; а натуральные числа — объект совсем не тривиальный. Так что в этом случае мы должны серьезнее воспринимать аргументы Осторожности, когда она требует доказательства непротиворечивости. Не то, чтобы мы действительно сомневались в непротиворечивости ТТЧ — но у нас все же есть малюсенькое сомнение, тень сомнения, и доказательство помогло бы эту тень рассеять.
Какой же метод доказательства нам бы хотелось использовать? Здесь мы снова сталкиваемся с проблемой порочного круга. Если мы будем использовать в доказательстве факта о системе те же инструменты, какие используются внутри самой системы, то чего мы таким образом добьемся? Если бы нам удалось убедиться в непротиворечивости ТТЧ, используя более слабую систему рассуждений, чем сама ТТЧ, мы избежали бы этого порочного круга! Подумайте о том, как протягивают тяжелый канат между двумя кораблями (по крайней мере, я читал об этом, когда был мальчишкой): сначала с одного из кораблей пускается стрела, которая перетаскивает через промежуток между кораблями веревку, затем при помощи этой веревки перетягивается канат. Если бы нам удалось использовать «легкую» систему, Чтобы показать непротиворечивость «тяжелой» системы, тогда мы могли бы считать, что действительно чего-то добились.
С первого взгляда может показаться, что у нас есть такая веревка. Наша цель — доказать, что в ТТЧ есть некоторое типографское свойство (непротиворечивость): в ней не встречаются одновременно теоремы формы x и ~x. Это похоже на доказательство того, что MU не является теоремой системы MIU. В обоих случаях мы имеем дело с утверждениями о типографских свойствах си стем, манипулирующих символами. Наше сравнение с веревкой основано на предположении о том, что факты теории чисел не нужны для доказательства некоего типографского свойства. Иными словами, если не использовать свойства целых чисел вообще — или использовать только несколько простейших свойств — мы можем доказать непротиворечивость ТТЧ, используя способы, более простые, чем наша внутренняя система рассуждений.
Именно на это надеялась школа математиков и логиков начала века; главой этой влиятельной школы был Давид Гильберт. Их целью было доказать непротиворечивость формализации теории чисел, подобных ТТЧ, используя весьма ограниченный набор логических принципов рассуждения, называемых финитными. Эти принципы были бы их «веревкой». Среди финитных методов — все методы исчисления высказываний, и некоторые методы численных рассуждений. Однако труды Гёделя показали, что любые усилия протащить через про пасть канат непротиворечивости ТТЧ, пользуясь веревкой финитных методов, обречены на провал. Гёдель показал, что для того, чтобы перетащить этот канат, невозможно пользоваться более легкой веревкой — просто нет настолько крепкой веревки, чтобы она выдержала такую нагрузку. Выражаясь менее метафорично, можно сказать: любая система, достаточно мощная, чтобы доказать непротиворечивость ТТЧ, по крайней мере так же мощна, как сама ТТЧ. Поэтому порочного круга здесь не избежать.
Приношение «МУ» [16]
Черепаха и Ахилл только что вернулись с лекции о происхождении Генетического Кода; они сидят у Ахилла и пьют чай.
Ахилл: Я должен кое в чем признаться, г-жа Ч.
Черепаха: Что такое?
Ахилл: Несмотря на интереснейшую тему, я пару раз задремал… Но даже во сне я кое-что слышал. Вот какая странная мысль всплыла из глубины моего сознания: «А» и «Т» могут обозначать не «аденин» и «тимин», а мое и ваше имена! Ведь вас зовут Тортилла! Кроме того, в моем полусне вдоль остова двойной спирали ДНК были подвешены крохотные Ахиллы и Тортиллы, всегда в парах, как аденин и тимин. Правда, странный образ?
Черепаха: Фу! Кто верит в подобные глупости? К тому же, что вы скажете о «С» и «G»?
Ахилл: Что ж, цитозин мог бы обозначать г-на Краба — ведь его имя пишется «Crab». Насчет «G» я не знаю, но уверен, что можно было бы что-нибудь придумать. Так или иначе, было забавно вообразить мою ДНК, полную ваших малюсеньких копий — и моих, конечно. Только подумайте, к какой бесконечной регрессии это бы привело!
Черепаха: Вижу, что вы не очень-то внимательно слушали лекцию.
Ахилл: Неправда — я старался изо всех сил. Просто было очень трудно отделить мои фантазии от фактов. В конце концов, молекулярные биологи изучают такой необыкновенный нижний мир…
Черепаха: Что вы имеете в виду?
Ахилл: Молекулярная биология полна странных спиральных петель, которые я как следует не понимаю. Например, белки, закодированные в ДНК, могут «провернуться назад» и повлиять на саму ДНК — даже разрушить ее. Подобные странные петли меня всегда запутывают. В них есть что-то пугающее.
Черепаха: Я нахожу их весьма привлекательными.
Ахилл: Разумеется — они вполне в вашем вкусе. Но мне иногда хочется прекратить весь этот анализ и просто помедитировать немного, в качестве противоядия. Это очищает голову от путаницы странных петель и всех этих невероятных сложностей, о которых мы сегодня услышали.