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

ПАРА-ДОКАЗАТЕЛЬСТВА-ТТЧ{а, а'}

(Эта сокращенная формула ТТЧ читается так: «Натуральные числа а и а' являются парой доказательства».) Следующим шагом является перевод нашего высказывания в теорию чисел, следуя модели МУМОН. Получается высказывание «существует некое число а, которое составляет пару доказательства с 666,111,666 в качестве второго элемента». Это выражается следующей формулой ТТЧ:

Ea:ПАРА-ДОКАЗАТЕЛЬСТВА-ТТЧ{a, SSSSS … SSSSS0/а'}

. |________|

. (Очень много S - целых 666,111.666!)

Это — закрытое высказывание ТТЧ. (Давайте назовем его Джошу — скоро узнаете, почему.) Мы убедились, что возможно говорить не только о примитивно рекурсивном понятии пар доказательства ТТЧ, но и о родственном, хотя и более сложном понятии чисел-теорем ТТЧ.

Чтобы убедиться, насколько хорошо вы поняли эти идеи, попробуйте перевести в ТТЧ следующие высказывания мета-ТТЧ:

(1) 0=0не является теоремой ТТЧ.

(2) ~0=0— теорема ТТЧ.

(3) ~0=0не является теоремой ТТЧ.

Каким образом решения отличаются от примеров, данных выше, и друг от друга? Вот еще несколько упражнений на перевод:

(4) ДЖОШУ — теорема ТТЧ. (Получившуюся строчку ТТЧ назовите МЕТА-ДЖОШУ.)

(5) МЕТА-ДЖОШУ — теорема ТТЧ. (Получившуюся строчку ТТЧ назовите МЕТА-МЕТА-ДЖОШУ.)

(6) МЕТА-МЕТА-ДЖОШУ — теорема ТТЧ.

(7) МЕТА-МЕТА-МЕТА-ДЖОШУ — теорема ТТЧ.

(и т. д., и т. п.)

Пример (5) показывает, что высказывания мета-мета-ТТЧ могут быть переведены в нотацию ТТЧ; пример (6) показывает то же самое для мета-мета-мета-ТТЧ, и т. д.

Важно помнить о разнице между выражением свойства, и его представлением . Например, свойство численно-теоремности ТТЧ выражено следующей формулой:

Eа: ПАРА-ДОКАЗАТЕЛЬСТВА-ТТЧ {а, а'}

Перевод: «а' — число-теорема ТТЧ». Однако у нас нет гарантии того, что эта формула действительно представляет данное понятие, поскольку у нас нет гарантии того, что это свойство примитивно рекурсивно — на самом деле, у нас есть некоторые основания полагать, что это не так! (Наши подозрения вполне обоснованы. Свойство являться числом-теоремой ТТЧ — НЕ примитивно рекурсивно, и такой формулы ТТЧ, которая могла бы его выразить, не существует!) С другой стороны, свойство являться парой доказательства, являясь примитивно рекурсивным, одновременно выразимо и представимо с помощью формулы, данной выше.

Предыдущее обсуждение показало нам, как ТТЧ может «анализировать» понятие теоремности ТТЧ. Это — основа первой части доказательства. Перейдем теперь ко второй идее доказательства, путем развития понятия, позволяющего сконцентрировать этот «самоанализ» в одной единственной формуле. Для этого давайте посмотрим, что случается с Гёделевым номером какой-либо формулы, когда ее структура слегка меняется. Рассмотрим следующее изменение:

замена всех свободных переменных на определенные символы чисел.

Ниже, в левой колонке, даны два примера этой операции; в правой колонке показаны параллельные изменения в Гёделевых номерах.

Формула Геделев номер

a=a 262,111,262

теперь заменим все свободные переменные на символ числа 2

SS0=SS0 123,123,666,111,123,123,666

*******

~Ea:Ea':Ea''=(SSa*SSa') 223,333,262,636,333,262,163,636,

. 262,163,163,111,362,123,123,262,

. 236,123,123,262,163,323

теперь заменим заменим свободные переменные на символ числа 4

~Ea:Ea':SSSS0=(SSa*SSa') 223,333,262,636,333,262,163,636,

. 123,123,123,123,666,111,362,123,

. 123,262,236,123,123,262,163,323,

В правой колонке происходит изоморфный арифметический процесс, в котором один большой номер превращается в другой, еще больший номер. Функцию, которая производит этот новый номер из старого, несложно описать арифметически в терминах сложения, умножения, возведения в десятую степень и так далее — но нам это не нужно. Важно здесь то, что отношения между (1) первоначальным Гёделевым номером, (2) номером, чей символ мы вставили и (3) Гёделевым номером, при этом получающимся — это примитивно рекурсивные отношения. Это значит, что на Блупе может быть написана программа-тест, которая, если мы введем в нее эти три номера, сможет ответить ДА. если между ними существуют такие отношения, и НЕТ — в противном случае. Вы можете проверить себя на способность проводить такие тесты (и в то же время убедиться, что в этом процессе нет спрятанных открытых петель), проверив следующие два случая:

(1) 362,262,112,262,163,323,111,123,123,123,123,666;

. 2;

. 362,123,123,666,112,123,123,666,323,111,123,123,123,123,666.

(2) 223,362,262,236,262,323,111,262,163;

. 1;

. 223,362,123,666,236,123,666,323,111,262,163.

Как обычно, один из примеров проходит проверку, а другой — нет. Назовем эти отношения между тремя номерами отношениями замены . Поскольку они примитивно рекурсивны, они могут быть представлены некоей формулой ТТЧ с тремя свободными переменными. Давайте запишем эту формулу сокращенно:

ZAM{a, a', a"}

Поскольку эта формула представляет отношения замены, нижеследующая формула ТТЧ должна являться теоремой:

ZAM{SSSSS..... SSSSS0/a, SS0/a', SSSSSS..... SSSS0/a"}

. |________| |________|

. 262,111,262-«S» 123,123,666,111,123,123,666 «S»

(Это основано на первом примере отношений замены, показанном ранее в виде параллельных колонок.) С другой стороны, поскольку формула ZAM представляет собой отношения замены, формула, данная ниже, не является теоремой ТТЧ:

ZAM{SSS0/a, SS0/a', S0/a"}

Пора соединить все эти части в одно гармоничное целое. Мы попробуем использовать технику ПАР-ДОКАЗАТЕЛЬСТВА-ТТЧ и формул ZAM для построения суждения ТТЧ, интерпретирующегося как «Эта строчка ТТЧ — не теорема ТТЧ». Как это возможно? Даже теперь, когда у нас есть все необходимые инструменты, ответ на этот вопрос найти нелегко.

Интересный и на вид довольно несерьезный прием состоит в подстановке в формулу ее собственного Гёделева номера. Это весьма похоже на другое, тоже легкомысленное на вид понятие «квайнирования», о котором вы прочли в «Арии в ключе G». Однако квайнирование оказалось важным, поскольку оно представляет из себя новый способ создания автореферентных суждений. Автореферентность подобного типа сначала кажется весьма странной, но, поняв ее принцип, вы найдете ее простой и изящной. Арифметическая версия квайнирования — назовем ее арифмоквайнированием — позволит нам получать суждения ТТЧ, «говорящие о себе самих».

Давайте рассмотрим пример арифмоквайнирования. Нам нужна формула, по меньшей мере, с одной переменной. Для этого годится следующая формула:

a=S0

Гёделев номер этой формулы — 262,111,123,666; теперь мы подставим этот номер в саму формулу — или, точнее, мы подставим в нее символ этого номера. У нас получится:

SSSSS.....SSSSSO=S0

|____________|

262,111,123,666 «S»

Эта новая формула очень глупа: она утверждает, что 262,111,123,666 равняется 1. Если бы мы начали со строчки ~a=S0, и затем арифмоквайнировали ее, у нас получилось бы верное высказывание, в чем вы сами можете убедиться.