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

Благодарю вас, г-жа Ч, за ваше объяснение по поводу того хулиганского звонка.

Черепаха: А я вас — за прелестную прогулку. Надеюсь, мы скоро увидимся опять.

ГЛАВА XIV: О формально неразрешимых суждениях ТТЧ и родственных систем [41]

Две идеи «устрицы»

НАЗВАНИЕ ЭТОЙ ГЛАВЫ — адаптация заглавия знаменитой статьи Гёделя, опубликованной в 1931 году; я заменил «Principia mathematica» на ТТЧ. Гёдель написал эту статью строго техническим языком, стараясь дать безупречное доказательство своей теоремы; в этой главе я постараюсь изложить его идеи более интуитивно. Сосредоточусь на двух идеях, лежащих в основе Гёделева доказательства. Первая идея — это открытие того факта, что некоторые строчки ТТЧ могут быть интерпретированы как суждения о других строчках ТТЧ; иными словами, ТТЧ оказалась языком, способным к самоанализу. Этот факт вытекает из Гёделевой нумерации. Вторая идея — это то, что данное свойство может быть сконцентрировано полностью в одной строке: в фокусе такой строки — она сама. Этот прием восходит, в принципе, к диагональному методу Кантора.

41

Заглавие статьи Гёделя включало в конце римское I; это означало, что он собирался написать продолжение этой статьи с тем, чтобы подробно остановиться на особенно трудных моментах доказательства. Однако первая статья получила настолько широкое признание, что нужда в продолжении отпала, и вторая статья так и не была написана.

По моему мнению, всякий, кто желает достичь глубокого понимания Гёделева доказательства, должен признать, что в его основе лежит слияние этих двух идей. Каждая из них по отдельности уже является шедевром, но чтобы соединить их, потребовался гений. Однако если бы мне предложили выбрать, какая из двух идей важнее, я, безусловно, указал бы на первую — Гёделеву нумерацию, поскольку эта идея приложима к понятию значения и упоминания во всех системах, имеющих дело с символами. Эта идея выходит далеко за пределы математической логики, в то время как Канторов прием, как бы значим он ни был для математиков, почти не связан с реальной жизнью.

Первая идея: пары доказательства

Не откладывая дела в долгий ящик, приступим к рассмотрению самого доказательства. В IX главе мы уже объяснили довольно подробно идею Гёделева изоморфизма. Здесь мы постараемся описать математическое понятие, позволяющее нам перевести предложение типа «Строчка 0=0 — теорема ТТЧ» в высказывание теории чисел. Для этого мы воспользуемся парами доказательства. Пара доказательства — это пара натуральных чисел, соотносящихся между собой таким образом:

Два натуральных числа m и n (в данном порядке) являются парой доказательства в ТТЧ тогда и только тогда, если m — Гёделев номер такой деривации ТТЧ, последняя строчка которой имеет Гёделев номер n.

Аналогичное понятие существует и для системы MIU; пожалуй, интуитивно легче понять именно этот случай. Так что давайте на минуту оставим пары доказательства ТТЧ и обратимся к парам доказательства в системе MIU. Их определение почти такое же:

Два натуральных числа m и n (в данном порядке) являются парой доказательства в MIU тогда и только тогда, если m — Гёделев номер такой деривации MIU, последняя строчка которой имеет Гёделев номер n.

Давайте рассмотрим несколько примеров пар доказательства в системе MIU. Пусть m — 3131131111301, n = 301. Эти значения тип составляют пару доказательства, поскольку m — Гёделев номер следующей деривации MIU:

MI

MII

MIIII

MUI

где последняя строчка — MUI — имеет Гёделев номер 301, то есть n.

С другой стороны, при m = 31311311130, и n = 30 пары доказательства не получается. Чтобы понять, почему, рассмотрим деривацию, кодом которой должно было бы являться m:

MI

MII

MIII

MU

В этой предположительной деривации есть неверный шаг. Это — переход от второй к третьей строке: от MII к MIII. В системе MIU нет правила, которое позволяло бы подобный типографский шаг. Соответственно — и это очень важно — нет такого арифметического шага, который позволил бы вам перейти от 311 к 3111. Возможно, что, после того как вы прочли главу IX, это покажется вам тривиальным, но именно подобные наблюдения лежат в основе Гёделева изоморфизма. Все, что мы делаем в формальных системах, имеет свою параллель в арифметических действиях.

Так или иначе, величины m = 31311311130, и n = 30, безусловно, не являются парой доказательства MIU. Само по себе, это еще не означает, что 30 — не номер MIU. Могло бы найтись другое число, составляющее пару доказательства с 30. (На самом деле, мы уже выяснили ранее, что 30 — не теорема MIU. Следовательно, ни одно число не может составлять пару доказательства с 30.)

А как насчет пар доказательства в ТТЧ? Я приведу вам два параллельных примера, лишь один из которых является действительной парой доказательства. Можете ли вы определить, какой именно? (Кстати, именно здесь появляется кодон «611», функция которого — отделять Гёделевы номера последующих строк в деривации ТТЧ. В этом смысле, «611» служит в качестве знака препинания. В системе MIU эту роль выполняет начальное «3» каждой строки; там не нужна никакая дополнительная пунктуация.)

1) m = 626,262,636,223,123.262,111,666,611,223,123,666,111,666

n = 123,666,111,666

(2) m = 626,262,636,223,123,262,111.666,611,223.333,262,636123,262,111,666

n = 223,333,262,636,123.262,111,666

Легко обнаружить, какая из этих дериваций настоящая, переведя их в традиционную нотацию и произведя стандартный анализ. При этом выясняется:

(1) является ли предполагаемая деривация, кодом которой является m, «законной»;

(2) если это так, то совпадает ли последняя строка деривации со строчкой, кодом которой является n.

Шаг (2) тривиален; шаг (1) тоже довольно прямолинеен, поскольку для него не нужен бесконечный поиск и в нем не спрятаны никакие петли. Вспомните примеры из системы MIU и просто мысленно замените правила MIU и ее аксиому на правила и аксиомы ТГЧ. В обоих случаях алгоритм один и тот же:

Следить за деривацией, переходя от строчки к строчке.

Отмечать строчки, являющиеся аксиомами.

Для каждой строчки, НЕ являющейся аксиомой, проверять, следует ли она из предыдущих строчек предполагаемой деривации.

Если все не-аксиомы следуют по правилам вывода из предыдущих строчек, значит, перед вами — законная деривация; в противном случае, перед вами — фальшивка.

На каждой ступени здесь совершается ограниченное число вполне определенных действий.

Свойство «пара-доказательности» примитивно рекурсивно …

Я делаю такой упор на ограниченность петель потому, что, как вы могли догадаться, я собираюсь доказать