Даглас Хофштадтер - ГЕДЕЛЬ, ЭШЕР, БАХ: эта бесконечная гирлянда

«Я не могу быть доказано в формальной системе ТТЧ + 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 видно, что у ТТЧ могут быть самые разные разветвления:

Рис. 75. Разветвление ТТЧ. У каждого нового варианта ТТЧ — своя Гёделева строчка; эта строчка или ее отрицание могут быть добавлены к системе, так что из каждой системы могут родиться два новых варианта; этот процесс может продолжаться до бесконечности.

Разумеется, это только начало. Представьте себе, что мы движемся вниз по самой левой ветви этого дерева, всегда добавляя саму Гёделеву строчку (а не ее отрицание). Это большее, что мы можем сделать, чтобы избавиться от супернатуральных чисел. После добавления G мы добавляем G'; затем G'', G''' и так далее. Каждый раз, когда мы производим новый вариант ТТЧ, ее уязвимость против Черепашьего метода — простите, я имею в виду Гёделева метода — позволяет вывести новую строчку, интерпретируемую как:

«Я не могу быть доказана в формальной системе X».

Разумеется, через некоторое время весь этот процесс начинает казаться привычным и легко предсказуемым — ведь все эти «дырки» делаются при помощи одной и той же техники! Это означает, что, как типографские объекты, они все сделаны по одному и тому же эталону — что, в свою очередь, означает, что они могут быть представлены с помощью одной-единственной схемы аксиом. Так почему бы нам не попытаться заткнуть все дырки одним махом, чтобы раз и навсегда избавиться от этой противной неполноты? Вместо того, чтобы добавлять по одной аксиоме, мы можем добавить к ТТЧ схему аксиом . Эта схема аксиом будет тем эталоном, по которому будут изготовляться G, G', G'', G''' и так далее. Может быть, что путем добавления этой схемы аксиом (назовем ее «G ω.») нам удастся перехитрить метод «Гёделизации». Действительно, кажется совершенно ясным, что добавление G ω, к ТТЧ будет последним шагом , необходимым для полной аксиоматизации всех истин теории чисел.

Этот момент соответствует тому месту «Акростиконтрапунктуса», где Черепаха рассказывает о создании Крабом патефона «Омега». Однако читатели были оставлены в неизвестности по поводу судьбы этого аппарата, поскольку усталая Черепаха решила поползти домой спать (но прежде, чем уйти, хитрое животное сделало тонкий намек на Теорему Гёделя о неполноте). Теперь, наконец, у нас дошли руки до того, чтобы прояснить ту ситуацию… Возможно, что, прочтя Диалог «Праздничная Кантататата», вы уже подозреваете, каков будет ответ.

Как вы, наверное, и подозревали, даже это фантастическое улучшение ТТЧ не может избежать той же судьбы. Странно, что происходит это по той же причине, что и раньше. Схема аксиом недостаточно мощна, и к ней снова приложимо Гёделево построение. Постараюсь это объяснить. (Существует более строгое объяснение, чем то, которое я приведу здесь.) Если бы удалось описать все строчки G, G', G'', G''', … при помощи одной-единственной типографской схемы, это означало бы, что существует способ описать Гёделевы номера этих строчек при помощи одной-единственной арифметической схемы. И этот арифметический портрет бесконечного класса чисел может быть представлен в ТТЧ + G' при помощи некоей формулы АКСИОМА-ОМЕГА{а}, которая интерпретируется следующим образом: « а — это Гёделев номер одной из аксиом, получающихся из G ω». Когда a заменяется на какой-либо определенный символ числа, получившаяся формула будет теоремой ТТЧ + G ωтогда и только тогда, когда этот символ представляет собой Гёделев номер аксиомы, принадлежащей этой схеме.

С помощью этой новой формулы становится возможным представить даже такое сложное понятие как пара-доказательства-ТТЧ + G ωвнутри ТТЧ + G ω:

ПАРА-ДОКАЗАТЕЛЬСТВА-(ТТЧ + G ω){a,a'}

Используя эту формулу, мы можем построить нового «дядю» и затем приступить к его арифмоквайнированию уже знакомым нам способом, производя таким образом еще одну неразрешимую строчку, которую мы назовем «ТТЧ + G ω+1». Вы, наверное, спросите, почему ТТЧ + G ω+1не находится среди аксиом, порожденных нашей схемой аксиом ТТЧ + G ω? Ответом является то, что ТТЧ + G ωоказалась недостаточно хитра, чтобы предусмотреть возможность своего собственного включения в теорию чисел.