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

Автор книги: Даглас Хофштадтер

сообщить о нарушении

Текущая страница: 21 (всего у книги 64 страниц)

Квантор существования

Два предыдущих правила объяснили нам, как можно убрать квантор общности и вернуть его на место; следующие два правила покажут, как обращаться с кванторами существования.

ПРАВИЛО ОБМЕНА: Представьте, что u – переменная. Тогда строчки Au:~ и ~Eu: взаимозаменимы везде внутри системы.

Давайте, например, применим это правило к аксиоме 1:

Aa:~Sa=0  аксиома 1

~Ea:Sa=0  обмен

Кстати, вы можете заметить, что обе эти строчки – естественный перифраз в ТТЧ высказывания «Нуль не следует ни за одним из натуральных чисел.» Следовательно, хорошо, что они могут быть с легкостью превращены одна в другую.

Следующее правило еще более интуитивно. Оно соответствует весьма простому типу рассуждений, который мы употребляем, переходя от утверждения «2 – простое число» к утверждению «существует простое число.» Название этого правила говорит само за себя:

ПРАВИЛО СУЩЕСТВОВАНИЯ: Предположим, что некий терм (могущий содержать свободные переменные), появляется один или много раз в теореме. Тогда каждый (или несколько, или все) из этих термов может быть заменен на переменную, которая больше нигде в теореме не встречается, и предварен соответствующим квантором существования.

Давайте применим, как обычно, это правило к аксиоме 1:

Aa:~Sa=0  аксиома 1

Eb:Aa:~Sa=b  существование

Вы можете поиграть с символами и при помощи данных правил получить теорему: ~Ab:Ea:Sa=b

Правила равенства и следствия

Мы привели правила, объясняющие, как обращаться с кванторами – но пока ни одно из них не сказало нам, как обращаться с символами «=» и «S». Сейчас мы это сделаем; в следующих правилах r, s и t – произвольные термы.

ПРАВИЛА РАВЕНСТВА:

СИММЕТРИЯ: Если r = s – теорема, то s = r также является теоремой.

ТРАНЗИТИВНОСТЬ: Если r = s и s = t – теоремы, то r = t также является теоремой.

ПРАВИЛА СЛЕДОВАНИЯ:

ДОБАВЛЕНИЕ S: Если r = t – теорема, то Sr = St также является теоремой.

ВЫЧИТАНИЕ S: Если Sr = St – теорема, то r = t также является теоремой.

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

(1) Aa:Ab:(a+Sb)=S(a+b)     аксиома 3

(2) Ab:(S0+Sb)=S(S0+b)      спецификация (S0 для а)

(3) (S0+S0)=S(S0+0) спецификация (0 для b)

(4) Aa:(a+0)=a     аксиома 2

(5) (S0+0)=S0     спецификация (S0 для а)

(6) S(S0+0)=SS0    добавление S

(7) (S0+S0)=SS0    транзитивность (строчки 3,6)

*****

(1) Aa:Ab:(a*Sb)=((a*b)+a)    аксиома 5

(2) Ab:(S0*Sb)=((S0*b)+S0)    спецификация (S0 для а)

(3) (S0*S0)=((S0*0)+S0)      спецификация (0 для b)

(4) Aa:Ab:(a+Sb)=S(a+b)    аксиома 3

(5) Ab:((S0*0)+Sb)=S((S0*0)+b спецификация ((S0*0) для а)

(6) ((S0*0)+S0)=S((S0*0)+0)    спецификация (0 для b)

(7) Aa:(a+0)=a         аксиома 2

(8) ((S0*0)+0)=(S0*0)       спецификация ((S0*0) для а)

(9) Aa:(a*0)=0         аксиома 4

(10) (S0*0)=0         спецификация (S0 для а)

(11) ((S0*0)+0)=0                   транзитивность (строчки 8,10)

(12)  S((S0*0)+0)=S0      добавление S

(13)  ((S0*0)+S0)=S0      транзитивность (строчки 6,12)

(14)  (S0*S0)=S0                      транзитивность (строчки 3,13)

Нелегальные упрощения

Возникает интересный вопрос: «Каким образом мы можем вывести строчку 0=0?» Кажется, что очевидным способом было бы сначала вывести строчку Aa:a=a и затем использовать спецификацию. Как вы думаете, где ошибка в нижеследующем «выводе» Aa:a=a... Можете ли вы ее исправить?

(1) Aa:(a+0)=a   аксиома 2

(2) Aa:a=(a+0)   симметрия

(3) Aa:a=a транзитивность (строчки 2,1)

Я привел это маленькое упражнение, чтобы указать на следующий простой факт: при манипуляции хорошо знакомыми символами, такими, как «=», мы не должны торопиться. Мы должны следовать правилам, а не нашему знанию пассивных значений символов. (Тем не менее, это знание весьма ценно, чтобы помочь нам направить вывод по верному пути.)

Почему спецификация и общность ограничены

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

(1)  [                    проталкивание

(2)     a=0             посылка

(3)     Aa:a=0        обобщение (ложно!)

(4)     Sa=0           спецификация

(5)  ]                   выталкивание

(6)        правило фантазии

(7)  Aa:

(8)  <0=0эS0=0>      спецификация

(9)  0=0               предыдущая теорема

(10) S0=0             отделение (строчки 9,8)

Это первое из печальных последствий. Другое получается из неверной спецификации.

(1) Aa:a=a предыдущая теорема

(2) Sa=Sa спецификация

(3) Eb:b=Sa существование

(4) Aa:Eb:b=Sa обобщение

(5) Eb:b=Sb спецификация (ложно!)

Теперь вы убедились, почему необходимы ограничения. Вот простая задачка: переведите (если вы этого уже не сделали раньше) четвертый постулат Пеано в нотацию ТТЧ, и затем выведите эту строчку как теорему.

Чего-то не хватает

Если вы поэкспериментируете с теми правилами и аксиомами ТТЧ, которые я привел до сих пор, вы обнаружите, что возможно вывести следующую пирамидальную семью теорем (множество строчек, отлитых из одной формы и отличающихся только тем, что символы чисел 0, S0, SS0, и так далее, идут по нарастающей):

(0+0)=0

(0+S0)=S0

(0+SS0)=SS0

(0+SSS0)=SSS0

(0+SSSS0)=SSSS0

и так далее.

Каждая из теорем этой семьи может быть выведена из предыдущей теоремы с помощью коротенькой, всего лишь в пару строчек, деривации. Результатом является нечто вроде каскада теорем, каждая из которых вызывает к жизни следующую. (Эти теоремы напоминают теоремы pr, где средняя и правая группы тире возрастали одновременно.)

Существует одна строчка, которую легко записать и которая суммирует пассивное значение всех этих строчек, вместе взятых. Вот эта универсально квантифицированная суммирующая строчка:

Aa:(0+a)=a

Однако при помощи правил, данных до сих пор, эту строчку вывести нельзя. Попробуйте сами, и вы в этом убедитесь!

Вы можете подумать, что ситуацию легко исправить, используя следующее:

(ПРЕДЛАГАЕМОЕ) ВСЕОБЩЕЕ ПРАВИЛО: Если все строчки в пирамидальной семье – теоремы, то универсально квалифицированная строчка, их суммирующая, также является теоремой.

Недостаток этого правила в том, что оно не может быть использовано при работе по способу M. Только люди, думающие о системе, могут знать, что каждая из бесконечного множества строчек – теорема. Следовательно, это правило не может являться частью формальной системы.

ω-неполные системы и неразрешимые строчки

Мы очутились в странной ситуации, в которой возможно типографским путем производить теоремы о сложении любых конкретных чисел, но даже такая простая строчка, как приведенная выше, выражающая свойство сложения в общем, не является теоремой. Вы, возможно, найдете это не таким уж странным, поскольку мы уже были в похожей ситуации с системой pr. Однако система pr не имела претензий по поводу своих возможностей; на самом деле, там было невозможно даже выразить общие свойства, а тем более, доказать их. В той системе просто не было соответствующего «оборудования» – при этом нам и в голову не приходило, что система была дефектна. Однако у ТТЧ возможностей гораздо больше; соответственно, мы ожидаем от нее большего, чем от системы pr. Если приведенная выше строчка – не теорема, то у нас есть основания подозревать, что в ТТЧ есть какой-то дефект. На самом деле, существует даже название для систем с подобным дефектом – они называются ω-неполными. (Символ ω – «омега» – выбран потому, что иногда все множество натуральных чисел обозначается этой буквой.) Далее следует точное определение:

Система является ω-неполной, если все строчки в пирамидальной семье – теоремы, но универсально квантифицированная строчка, их суммирующая, – не теорема.

Кстати, отрицание приведенной суммирующей строчки —

~Aa:(0+a)=a

– тоже не-теорема ТТЧ. Это означает, что первоначальная строчка неразрешима внутри системы. Если бы та или другая были теоремами, мы сказали бы, что они разрешимы. Хотя это и звучит как мистический термин, в неразрешимости внутри данной системы нет ничего таинственного. Это означает, что система может быть дополнена. Например, внутри абсолютной геометрии пятый постулат Эвклида неразрешим. Чтобы получить геометрию Эвклида, его необходимо добавить; а отрицание пятого постулата, наоборот, производит не-эвклидову геометрию. Поскольку мы обратились к геометрии, давайте вспомним, почему это происходит. Дело в том, что четыре постулата не определяют термины «точка» и «линия» с достаточной точностью, так что остается возможность для различных интерпретаций этих понятий. Точки и линии Эвклидовой геометрии представляют собой лишь одну из возможных интерпретаций понятий «точка» и «линия» – ТОЧКИ и ЛИНИИ неэвклидовой геометрии – другая интерпретация. Однако то, что люди в течение тысячелетий пользовались такими хорошо известными словами как «точка» и «линия», заставило их думать, что эти слова могут иметь лишь одно-единственное значение.

Неэвклидова ТТЧ

С подобной же ситуацией мы сталкиваемся в ТТЧ Мы приняли нотацию, которая способствует созданию у нас некоторых предрассудков Например, использование символа «+» создает у нас впечатление, что любая теорема, использующая этот знак, сообщает нам что-то значимое о хорошо нам знакомой операции, под названием «сложение» Поэтому нам кажется, что предложить «шестую аксиому»

~Ea:(0+a)=a

было бы неверным. Она не совпадает с нашими знаниями о сложении Однако это одна из возможностей расширить ту ТТЧ, что мы сформулировали до сих пор Система, использующая данную строчку в качестве шестой аксиомы, последовательна в том смысле, что в ней нет двух теорем типа x и ~x. Однако если вы наложите эту «шестую аксиому» на пирамидальную семью теорем, вы, возможно, будете поражены кажущимся несоответствием теорем этой семьи с новой аксиомой Этот тип непоследовательности, однако, не так вреден, как другой (где и x и ~x – теоремы). На самом деле это даже нельзя назвать непоследовательностью, так как существует такая интерпретация символов ТТЧ, в которой все получается хорошо.

ω-противоречивость не то же самое, что просто противоречивость

Этот тип противоречивости, созданный наложением (1) пирамидальной семьи теорем, которые, вместе взятые, утверждают, что все натуральные числа имеют определенное свойство, и (2) одной теоремы, утверждающей, что не все числа обладают этим свойством, называется ω-противоречивостью. ω-противоречивая система похожа на сначала-раздражающую-но-в-конце-концов-приемлемую неэвклидову геометрию. Чтобы построить мысленную модель того, что происходит, вообразите себе, что имеются некоторые дополнительные числа – давайте будем называть их не натуральными, а экстранатуральными – у которых нет численных символов Поэтому их свойства не могут быть представлены в пирамидальной семье (Это немного напоминает представление Ахилла о БОГе – что-то вроде «супергения», существа, находящегося выше всех гениев. Хотя это представление и было опровергнуто Гением, тем не менее это хороший образ, и может помочь вам вообразить экстранатуральные числа ).

Все это говорит нам о том, что аксиомы и правила ТТЧ, как мы до сих пор ее представляли, не описывают с достаточной полнотой интерпретации символов этой системы В нашей воображаемой модели понятий, которые эти символы представляют, еще остается место для вариантов Каждый из возможных вариантов системы опишет эти понятия немного полнее, но сделает это по-своему. Какие из символов приобретут «раздражающие» пассивные значения, если мы добавим приведенную выше «шестую аксиому»? Все ли символы окажутся «испорченными», или некоторые из них сохранят то значение, которые мы имели в виду? Предлагаю вам над этим поразмыслить. В главе XIV мы снова встретимся с подобным вопросом; там мы обсудим его подробнее. В любом случае, не будем здесь останавливаться на этом дополнении системы; вместо этого мы попытаемся исправить ω-неполноту ТТЧ.

Последнее правило

Недостаток обобщающего правила был в том, что оно требовало знания того факта, что все строчки бесконечной пирамидальной семьи – теоремы; это слишком много для конечного существа. Однако представьте себе, что каждая строчка пирамиды может быть выведена из своей предшественницы регулярным путем. Тогда у нас оказалась бы конечное основание на то, чтобы считать все строчки пирамиды теоремами. Таким образом, трюк состоит в том, чтобы найти ту схему, которая порождает пирамиду, и показать, что сама эта схема является теоремой. Это подобно доказательству того, что каждый гений передает послание своему Мета-гению, как в детской игре в телефончик. Остается только доказать, что эта цепочка посланий начинается с гения – то есть установить, что первая строчка пирамиды – теорема. Тогда мы можем быть уверены, что послание дойдет до БОГа!

В конкретной пирамиде, которую мы рассматривали, такая схема существует; она представлена строчками 4-9 данной ниже деривации.

(1) Aa:Ab:(a+Sb)=S(a+b)  аксиома 3

(2) Ab:(0+Sb)=S(0+b)       спецификация

(3) (0+Sb)=S(0+b) спецификация

(4) [        проталкивание

(5) (0+b)=b    посылка

(6) S(0+b)=Sb   добавление S

(7) (0+Sb)=S(0+b) перенос строки 3

(8) (0+Sb)=Sb   транзитивность

(9) ]        выталкивание

Посылка здесь – (0+b)=b; результат – (0+Sb)=Sb.

Первая строка пирамиды – также теорема; это прямо следует из аксиомы 2. Все, что теперь требуется, это правило, позволяющее нам заключить, что строчка, суммирующая всю пирамиду в целом, тоже является теоремой. Такое правило будет формализованным пятым постулатом Пеано.

Чтобы выразить это правило, нам необходимо ввести кое-какую нотацию.

Давайте запишем правильно сформированную формулу, в которой переменная а свободна:

X{a}

(Там могут встречаться и другие свободные переменные, но нам это неважно.) Тогда запись X{Sa/a} будет обозначать то же самое, с той разницей, что все а будут заменены на Sa. Таким же образом, X{0/а} будет обозначать ту же строку, в которой все а заменены на 0.

Приведем конкретный пример. Пусть X{a} обозначает строчку (0+а)=а. Тогда X{Sa/a} представляет строчку (0+Sa)=Sa, a X{0/a} – строчку (0+0)=0.

(Внимание: эта нотация не является частью ТТЧ; она служит нам лишь для того, чтобы говорить о ТТЧ.)

С помощью этой новой нотации мы можем выразить последнее правило ТТЧ весьма точно:

ПРАВИЛО ИНДУКЦИИ. Предположим, что u – переменная и X{u} – правильно сформированная формула, в которой и свободно. Если и Au

Мы подошли так близко, как возможно, к введению пятого постулата Пеано в ТТЧ. Давайте теперь используем его, чтобы показать, что Aa:(0+a)=a действительно является теоремой ТТЧ Выходя из области фантазии в приведенной выше деривации, мы можем использовать правило фантазии, чтобы получить

(10) <(0+b)=bэ(0+Sb)=Sb> правило фантазии

(11) Ab:<(0+b)=bэ(0+Sb)=Sb>   обобщение

Это – первая из двух вводных теорем, требующихся для правила индукции другая – первая строка пирамиды – у нас уже имелась Следовательно мы можем применить правило индукции и получить то, что нам требуется

Ab:(0+b)=b

Спецификация и обобщение позволят нам изменить переменную с b на a, таким образом, Aa:(0+a)=a перестает быть неразрешимой строчкой ТТЧ.

Длинная деривация

Я хочу представить здесь более длинную деривацию ТТЧ с тем, чтобы читатель посмотрел, как она выглядит; эта деривация доказывает простой, но важный факт теории чисел.

(1) Aa:Ab:(a+Sb)=S(a+b) аксиома 3

(2) Ab:(d+Sb)=S(d+b) спецификация

(3) (d+SSc)=S(d+Sc) спецификация

(4) Ab:(Sd+Sb)=S(Sd+b) спецификация (строка 4)

(5) (Sd+Sc)=S(Sd+c) спецификация

(6) S(Sd+c)=(Sd+Sc) симметрия

(7) [ проталкивание

(8) Ad:(d+Sc)=(Sd+c) посылка

(9) (d+Sc)=(Sd+c) спецификация

(10) S(d+Sc)=S(Sd+c) добавление S

(11) (d+SSc)=S(d+Sc) перенос 3

(12) (d+SSc)=S(Sd+c) транзитивность

(13) S(Sd+c)=(Sd+Sc) перенос 6

(14) (d+SSc)=(Sd+Sc) транзитивность

(15) Ad:(d+SSc)=(Sd+Sc) обобщение

(16) ] выталкивание

(17) правило фантазии

(18) Ac: обобщение

*****

(19) (d+S0)=S(d+0) спецификация (строчка 2)

(20) Aa:(a+0)=a аксиома 1

(21) (d+0)=d спецификация

(22) S(d+0)=Sd добавление S

(23) (d+S0)=Sd транзитивность (строки 19,22)

(24) (Sd+0)=Sd спецификация (строка 20)

(25) Sd=(Sd+0) симметрия

(26) (d+S0)=(Sd+0) транзитивность (строчки 23, 25)

(27) Ad:(d+S0)=(Sd+0) обобщение

*****

(28) Ac:Ad:(d+Sc)=(Sd+c) индукция (строчки 18,27)

[В сложении S может быть передвинуто вперед или назад.]

(29) Ab:(c+Sb)=S(c+b) спецификация (строчка 1)

(30) (c+Sd)=S(c+d) спецификация

(31) Ab:(d+Sb)=S(d+b) спецификация (строчка 1)

(32) (d+Sc)=S(d+c) спецификация

(33) S(d+c)=(d+Sc) симметрия

(34) Ad:(d+Sc)=(Sd+c) спецификация (строчка 28)

(35) (d+Sc)=(Sd+c) спецификация

(36) [ проталкивание

(37) Ac:(c+d)=(d+c) посылка

(38) (c+d)=(d+c) спецификация

(39) S(c+d)=S(d+c) добавление S

(40) (c+Sd)=S(c+d) перенос 30

(41) (c+Sd)=S(d+c) транзитивность

(42) S(d+c)=(d+Sc) перенос

(43) (c+Sd)=(d+Sc) транзитивность

(44) (d+Sc)=(Sd+c) перенос 35

(45) (c+Sd)=(Sd+c) транзитивность

(46) Ac:(c+Sd)=(Sd+c) обобщение

(47) ] выталкивание

(48) правило фантазии

(49) Ad: обобщение

[Если d коммутирует с любым с, то Sd обладает таким же свойством.]

*****

(50) (с+0)=с спецификация (строка 20)

(51) Aa:(0+a)=a предыдущая теорема

(52) (0+с)=с спецификация

(53) с=(0+с) симметрия

(54) (с+0)=(0+с) транзитивность (строчки 50, 53)

(55) Ac:(c+0)=(0+c) обобщение

[О коммутирует с любым с]

*****

(56) Ad:Ac:(c+d)=(d+c) индукция (строчки 49,55)

[Таким образом, любое d коммутирует с любым с]

Напряжение и разрешение в ТТЧ

ТТЧ доказала коммутативность сложения. Даже если вы не следили за всеми деталями этой деривации, важно понять, что, так же как и музыкальная пьеса, она имеет свой собственный естественный «ритм». Это вовсе не случайная про гулка, во время которой мы вдруг наткнулись на нужную строчку. Я ввел «паузы для дыхания», чтобы показать «артикуляцию» этой деривации. В частности, строчка 28 является переломным моментом в деривации – что-то вроде середины в пьесе типа ААББ, где происходит временное разрешение, хотя и не в ключевую тональность. Подобные важные промежуточные моменты часто называют «леммами».

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

Строчка 49 – критически важный увеличитель напряжения, поскольку она вызывает ощущение «почти у цели». Прервать деривацию в этот момент было бы очень неприятно. С этого момента мы уже почти можем предсказать развитие событий. Однако вам не хотелось бы прервать музыкальную пьесу в том момент, когда вам уже очевидно, как она разрешится. Вам не хотелось бы воображать финал – вам хотелось бы его услышать. Так же и здесь, мы должны закончить деривацию. Строка 55 Неизбежна и производит максимальное финальное напряжение, которое затем разрешается в строке 56.

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

Формальные и неформальные рассуждения

Я предпочел бы показать вам, как выводится теорема Эвклида (бесконечность простых чисел), но это, возможно, сделало бы книгу вдвое длиннее. Теперь, после доказательства теоремы, естественным продолжением было бы доказать ассоциативность сложения, коммутативность и ассоциативность умножения и дистрибутивность умножения со сложением. Это создало бы прочную базу для дальнейшей работы.

В нашей теперешней формулировке ТТЧ достигла «критической массы». Ее мощь сравнялась с мощью «Principia mathematica» – в ней стало возможным доказать любую теорему, которую можно найти в стандартном труде по теории чисел. Конечно, никто не стал бы утверждать, что вывод теорем в ТТЧ – это наилучший способ заниматься теорией чисел. Человек, так считающий, принадлежал бы к классу людей, которые думают, что лучший способ узнать, сколько будет 1000×1000 – это нарисовать решетку размером 1000x1000 и подсчитать в ней клеточки. На самом деле, после полной формализации остается единственный путь – дать формальной системе послабление. Иначе она становится такой громоздкой, что теряет всякую практическую пользу. Таким образом, необходимо внести ТТЧ в более широкий контекст, такой, который позволит нам получить правила вывода, ускоряющие деривацию. Для этого нам понадобится формализовать язык, на котором выражены эти правила вывода – то есть метаязык. Можно пойти еще намного дальше; однако никакие из этих трюков не сделают ТТЧ более мощной — они лишь сделают ее более удобной для пользования. Дело в том, что мы выразили в ТТЧ все типы рассуждений, на которые опираются математики, занимающиеся теорией чисел. Введение ее в более широкий контекст не увеличит количества теорем; оно лишь сделает работу в ТТЧ – или в любой «улучшенной» ее версии – более похожей на работу в традиционной теории чисел.

Специалисты по теории чисел закрывают лавочки

Представьте себе, что вы не знали заранее, что ТТЧ окажется неполной – напротив, вы ожидали, что она полна, то есть, что любое истинное высказывание, которое можно выразить в нотации ТТЧ, является теоремой. В таком случае вы могли бы иметь разрешающую процедуру для всей теории чисел. Ваш метод был бы прост; если вы хотите знать, истинно ли высказывание X теории чисел, вы должны закодировать его в строчку x ТТЧ. Теперь, если X – истинно, то полнота говорит нам, что x – теорема. С другой стороны, если не-X – истинно, тогда ~x – теорема. Таким образом, либо x, либо ~x должны оказаться теоремами, поскольку либо X, либо не-X истинны. Теперь вы должны систематически пронумеровать все теоремы ТТЧ, так же как мы сделали это для систем MIU и pr. Какое-то время спустя, вы наткнетесь либо на x, либо на ~x, и, таким образом, узнаете, какое из двух высказываний – X или не-X – истинно. (Следите ли вы за ходом рассуждения? Очень важно держать в голове разницу между формальной системой ТТЧ и ее неформальным соответствием – теорией чисел; читатель должен постараться хорошо понять эту разницу.) Так что в принципе, если бы ТТЧ была полной, специалисты по теории чисел остались бы без работы: со временем любую проблему можно было бы решить чисто механическим путем. Оказывается, однако, что это невозможно; по этому поводу можно радоваться или огорчаться, в зависимости от вашей точки зрения.

Программа Гильберта

Последний вопрос, который мы рассмотрим в этой главе, таков: должны ли мы так же верить в непротиворечивость ТТЧ, как мы верили в непротиворечивость исчисления высказываний? И если нет, то возможно ли укрепить нашу веру в ТТЧ, доказав, что она непротиворечива? Для начала можно утверждать, подобно тому, как Неосторожность утверждала об исчислении высказываний, что непротиворечивость ТТЧ «очевидна» – а именно, что каждое правило воплощает принцип логических рассуждений, в который мы верим безоговорочно; следовательно, ставить под вопрос непротиворечивость ТТЧ, это все равно, что сомневаться в собственном здравом уме. Этот аргумент все еще имеет некоторый вес, но уже не такой, как раньше. Дело в том, что теперь у нас слишком много правил вывода, и в какие-то из них могла вкрасться ошибка. Более того, откуда мы знаем, что наша мысленная модель неких абстрактных единиц под названием «натуральные числа» последовательна? Может быть, наши собственные мыслительные процессы, те неформальные процессы, которые мы пытались выразить в правилах формальной системы, сами по себе непоследовательны! Конечно, мы не ожидаем подобного подвоха. Тем не менее, можно представить, что чем сложнее объект нашей мысли, тем легче в нем запутаться; а натуральные числа – объект совсем не тривиальный. Так что в этом случае мы должны серьезнее воспринимать аргументы Осторожности, когда она требует доказательства непротиворечивости. Не то, чтобы мы действительно сомневались в непротиворечивости ТТЧ – но у нас все же есть малюсенькое сомнение, тень сомнения, и доказательство помогло бы эту тень рассеять.

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

С первого взгляда может показаться, что у нас есть такая веревка. Наша цель – доказать, что в ТТЧ есть некоторое типографское свойство (непротиворечивость): в ней не встречаются одновременно теоремы формы x и ~x. Это похоже на доказательство того, что MU не является теоремой системы MIU. В обоих случаях мы имеем дело с утверждениями о типографских свойствах си стем, манипулирующих символами. Наше сравнение с веревкой основано на предположении о том, что факты теории чисел не нужны для доказательства некоего типографского свойства. Иными словами, если не использовать свойства целых чисел вообще – или использовать только несколько простейших свойств – мы можем доказать непротиворечивость ТТЧ, используя способы, более простые, чем наша внутренняя система рассуждений.

Именно на это надеялась школа математиков и логиков начала века; главой этой влиятельной школы был Давид Гильберт. Их целью было доказать непротиворечивость формализации теории чисел, подобных ТТЧ, используя весьма ограниченный набор логических принципов рассуждения, называемых финитными. Эти принципы были бы их «веревкой». Среди финитных методов – все методы исчисления высказываний, и некоторые методы численных рассуждений. Однако труды Гёделя показали, что любые усилия протащить через про пасть канат непротиворечивости ТТЧ, пользуясь веревкой финитных методов, обречены на провал. Гёдель показал, что для того, чтобы перетащить этот канат, невозможно пользоваться более легкой веревкой – просто нет настолько крепкой веревки, чтобы она выдержала такую нагрузку. Выражаясь менее метафорично, можно сказать: любая система, достаточно мощная, чтобы доказать непротиворечивость ТТЧ, по крайней мере так же мощна, как сама ТТЧ. Поэтому порочного круга здесь не избежать.