Черепаха: О, Боже мой! Какая честь для меня — оказаться обладательницей такой мощной Схемы Ответов! Мне кажется, что человеческая мысль редко изобретала что-либо подобное. Я восхищена ее гигантской мощью! Вы не возражаете, если я дам имя вашему подарку?
Ахилл: Конечно, нет.
Черепаха: Тогда я назову его «Схемой Ответов ω2.» И мы сможем перейти к другим темам — как только вы скажете мне, что обладание Схемой Ответов ω2 позволит мне заключить, что сегодня ваш день рождения.
Ахилл: Увы мне, увы!.. Кончатся ли когда-нибудь эти мученья? Что еще меня ожидает?
Черепаха: С удовольствием скажу вам. Дело в том, что после вашей Схемы Ответов ω2 идет ответ ω2 + 1, затем ω2 + 2… Разумеется, вы можете собрать их в кучу под названием Схема Ответов ω2 + ω, после чего могут последовать несколько других «куч», как, например, ω2 + 2ω, ω2 + Зω и так далее. Рано или поздно вы придете к Схеме Ответов 2ω2, затем Зω2, 4ω2 и так далее. Существуют также дальнейшие Схемы Ответов, такие, как ω3, ω4, ω5 Так может продолжаться довольно долго.
Ахилл: Могу себе представить. Наверное, через некоторое время так можно дойти до Схемы Ответов ωω.
Черепаха: Разумеется.
Ахилл: А затем ωωω и так далее?
Черепаха: Вы довольно быстро ухватили мою идею. Если не возражаете, хочу вам кое-что предложить. Почему бы вам не соединить их все в одну-единственную Схему Ответов?
Ахилл: Хорошо, хотя я начинаю сомневаться, есть ли от этого какая-нибудь польза.
Черепаха: Мне кажется, что нам будет трудненько найти имя для этой Схемы. Может быть, нам придется просто назвать ее Схема Ответов ε.
Ахилл: Черт побери! Каждый раз, когда вы даете очередной Схеме Ответов, имя это разбивает мои надежды на то, что мой ответ вас, наконец, удовлетворит. Почему бы нам просто не оставить Схему безымянной?
Черепаха: Никак невозможно, Ахилл. Как же мы будем говорить об этой схеме, если у нее не будет имени? Кроме того, именно в этой Схеме есть что-то особенно завершенное и прекрасное. Было бы некрасиво оставить ее безымянной! А вы не хотели бы совершать некрасивых поступков, особенно в день вашего рождения не правда ли? Неужели сегодня ваш день рождения? Кстати о днях рождения, сегодня мой день рождения!
Ахилл: Неужели?
Черепаха: Да. Вообще-то, на самом деле, сегодня день рождения моего дяди, но это почти одно и то же. Как насчет того, чтобы пригласить меня на шикарный праздничный ужин?
Ахилл: Подождите минутку г-жа Ч! Сегодня МОЙ день рождения, и это Вы должны меня приглашать!
Черепаха: Но вам так и не удалось убедить меня в том, что вы говорите правду! Вы развели страшную путаницу, выдумали какие-то Схемы Ответов… Я всего-навсего хотела узнать, не день рождения ли у вас сегодня, но вам удалось меня совершенно сбить с толку. Как вам только не стыдно? Так или иначе я была бы счастлива, если бы вы пригласили меня на ужин сегодня вечером.
Ахилл: Ну что ж. Я знаю одно местечко. Там готовят самые экзотические супы, и я точно знаю какого супчика мне бы сейчас хотелось!
ГЛАВА XV: Прыжок из системы
Более мощная формальная система
РАЗМЫШЛЯЯ над доказательством Гёделя, вдумчивый критик мог бы задаться вопросом, насколько оно обще. Он мог бы подумать, что Гёделю удалось найти недостаток лишь в одной формальной системе — в ТТЧ. Если бы это было так, то, возможно, удалось бы найти какую-нибудь лучшую систему, в которой Гёделев трюк был бы невозможен — и, таким образом, Теорема Гёделя потеряла бы значительную часть своей мощи. В этой главе мы подробно рассмотрим те характеристики ТТЧ, которые сделали ее уязвимой для аргументов, изложенных ранее.
Естественно подумать, что если проблема в том, что в ТТЧ есть «дырка» — иными словами, неразрешимое суждение G — то почему бы нам не заткнуть эту дырку? Почему бы не добавить G к ТТЧ в качестве шестой аксиомы? Конечно, по сравнению с остальными аксиомами, G — неуклюжий великан, и получившаяся система ТТЧ + G выглядела бы довольно комично из-за диспропорции ее аксиом. Тем не менее, это предложение имеет смысл. Представим себе, что перед нами ТТЧ + G — высшая формальная система. Мы надеемся, что она не только свободна от супернатуральных чисел, но и полна. Безусловно то, что ТТЧ + G лучше ТТЧ по крайней мере в одном, строчка G больше не является в ней неразрешимой, поскольку теперь она превратилась в теорему.
В чем же была причина недостатков ТТЧ? Ее уязвимость объяснялась тем, что она была способна говорить о себе самой. В частности, источником неприятностей было высказывание:
«Я не могу быть доказано в формальной системе ТТЧ»
или, более подробно,
«Не существует такого натурального числа, которое составляло бы пару доказательства ТТЧ с Гёделевым номером этой строчки.»
Есть ли у нас причина ожидать, что ТТЧ + G будет неуязвима для Гёделева доказательства? На самом деле, нет. Наша новая система может выразить ничуть не меньше, чем ТТЧ. Поскольку Гёделево доказательство основывается, прежде всего, на выразительной мощи формальной системы, будет неудивительно, если наша новая система окажется подверженной тому же недугу, как и ТТЧ. Для этого нужно будет найти строчку, выражающую высказывание:
«Я не могу быть доказано в формальной системе ТТЧ + G»
После того, как мы проделали подобное в ТТЧ, это совсем несложно. Принципы здесь те же самые, только контекст слегка изменен (Образно говоря, это все равно, что пропеть известную нам мелодию тоном выше.) Как и раньше, нужная нам строчка — назовем ее G' — строится при посредстве «дяди». Но теперь, вместо пары доказательства ТТЧ, она основывается на похожем, но немного более сложном понятии пары доказательства ТТЧ + G. Понятие пар доказательства ТТЧ + G — всего лишь небольшое расширение понятия пар доказательства ТТЧ.
Можно представить себе подобное расширение для системы MIU. Мы имели дело с неизмененной формой пар доказательства MIU. Если бы мы теперь добавили MU в качестве второй аксиомы, у нас получилась бы новая система — MIU + MU. Деривация в такой расширенной системе выглядела бы так:
MU аксиома
MUU правило 2
Существует пара доказательства MIU + MU, соответствующая этой деривации: m = ЗОЗОО, n = 300. Разумеется, эта пара чисел не является парой доказательства MIU, а всего лишь парой доказательства MIU + MU. Добавление дополнительной аксиомы ненамного усложнило арифметические свойства пар доказательства. Самое главное их свойство, примитивно-рекурсивность, сохраняется и в новой системе.
Метод Гёделя используется еще раз
Вернувшись к ТТЧ, мы находим похожую ситуацию. Пары доказательства ТТЧ + G, как и их предшественницы, примитивно рекурсивны. Они представимы в ТТЧ + G с помощью формулы, которую мы сократим следующим очевидным образом:
ПАРА-ДОКАЗАТЕЛЬСТВА-(ТТЧ + G){a,a'}
Теперь мы должны повторить знакомую процедуру. Чтобы сконструировать строчку, соответствующую G, начнем снова с «дяди»:
~Eа:Eа':<ПАРА-ДОКАЗАТЕЛЬСТВА-(ТТЧ + G){a,a'}
ΛARITHMOQUINE {а'',а'}>
Предположим, что Гёделев номер этой строчки — d'. Теперь мы арифмоквайнируем самого дядю. Это даст нам G':
~Eа:Eа':<ПАРА-ДОКАЗАТЕЛЬСТВА-(ТТЧ + G){a,a'}
ΛARITHMOQUINE {SSS.... SSSO/a'',a'}>
. |______|
. S повторяется d' раз
Интерпретация этой строчки такова:
«Меня нельзя доказать в формальной системе ТТЧ + G».
Разветвление
После этого остаются лишь технические детали. G' в ТТЧ + G — то же самое, чем G была в ТТЧ. Оказывается, что либо G, либо G' может быть добавлена к ТТЧ + G, и что результатом этого является дальнейшее разветвление теории чисел. Если вы думаете, что подобное происходит только с «положительными типами», то вы ошибаетесь: точно такой же трюк можно сыграть с ТТЧ + ~G, то есть, с нестандартным вариантом теории чисел, полученным путем добавления к ТТЧ отрицания G. Из рис. 75 видно, что у ТТЧ могут быть самые разные разветвления:
