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

ГЛАВА VIII: Типографская теория чисел

В «КРАБЬЕМ КАНОНЕ» есть три примера косвенной автореференции. Ахилл и Черепаха описывают известные им произведения искусства — и по случайному совпадению оказывается, что эти произведения построены по той же схеме, как и диалог, в котором они упоминаются. Вообразите мое удивление, когда я, автор, сам это заметил! Более того, краб описывает биологическую структуру, которая тоже имеет подобные свойства. Разумеется, можно прочитать и понять диалог, не заметив при этом, что он сделан в форме ракохода — но это было бы пониманием диалога только на одном уровне. Чтобы увидеть автореференцию, надо обратить внимание как на содержание, так и на форму диалога.

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

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

Вот некоторые типичные высказывания Ч — теории чисел:

(1) 5 — простое число.

(2) 2 не является квадратом другого числа.

(3) 1729 — сумма двух кубов.

(4) Сумма двух положительных кубов сама не является кубом.

(5) Существует бесконечное множество простых чисел.

(6) 6 — четное число.

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

(1) Не существует чисел а и b больших единицы, таких, что 5 равнялось бы а#215;b

(2) Не существует такого числа b, что b#215;b равнялось бы 2.

(3) Существуют такие числа b и с, что b#215;b#215;b + с#215;с#215;с равняется 1729.

(4) Для любых чисел b и с больше нуля не существует такого числа а, что а#215;а#215;а = b#215;b#215;b + с#215;с#215;с.

(5) Для каждого а существует b, большее, чем а, такое, что не существует чисел c и d, больших 1 и таких, что b равнялось бы c#215;d.

(6) Существует число e такое, что 2#215;e равняется 6.

Этот анализ продвинул нас на пути к основным элементам языка теории чисел. Очевидно, что некоторые фразы повторяются снова и снова:

для всех чисел b существует число b, такое, что больше чем равняется умноженное на О, 1, 2,…

Большинство таких фраз получат индивидуальные символы. Исключением является «больше чем», которое может быть упрощено еще. Действительно, высказывание «а больше b» становится:

существует число с отличное от 0, такое, что а = b + с.

Мы не будем вводить отдельного символа для каждого из натуральных чисел. Вместо этого у нас будет очень простой способ приписать каждому натуральному числу составной символ, так, как мы делали это в системе pr. Вот наше обозначение натуральных чисел.

нуль 0

один S0

два SS0

три SSS0

и т. д.

Символ S интерпретируется как «следующий за.» Таким образом, строчка SS0 интерпретируется буквально как «следующий за следующим за нулем.» Подобные строчки называются символами чисел.

Ясно, что нам нужен способ говорить о неопределенных, или переменных числах. Для этого мы будем использовать буквы а, b, с, d, e. Однако пяти букв будет недостаточно Так же, как для атомов в исчислении высказывании, нам требуется их неограниченное количество Мы используем похожий метод для получения большего количества переменных — добавление любого количества штрихов. Например:

e

d'

с"

b'''

a''''

все являются переменными.

В каком-то смысле, использовать целых пять букв алфавита — это слишком большая роскошь, так как мы могли бы легко обойтись просто буквой а и штрихами. Впоследствии я действительно опущу буквы b,c,d, и e — результатом будет более строгая версия ТТЧ, сложные формулы которой будет немного труднее расшифровать. Но пока давайте позволим себе некоторую роскошь! Как насчет сложения и умножения? Очень просто: мы будем использовать обычные символы «+» и «*». Однако мы также введем требование скобок (мы мало помалу углубляемся в правила, определяющие правильно построенные строчки ТТЧ). Например, чтобы записать «b плюс с» и «b, умноженное на с», мы будем использовать строчки:

(b + с)

(b*с)

В отношении скобок послабления быть не может; опустить их — значит произвести неправильно сформированную формулу. («Формула?» Я использую этот термин вместо слова «строчка» лишь для удобства. Формула — это просто строчка ТТЧ.)

Кстати, сложение и умножение всегда будут рассматриваться как бинарные операции, то есть операции, объединяющие не более, чем два числа. Таким образом, если вы хотите записать «1+2+3», вы должны решить, какое из двух выражений использовать:

(S0+(SS0+SSS0))

((S0+SS0)+SSS0)

Теперь давайте символизируем понятие равенства. Для этого мы просто используем «=». Преимущество этого символа, принадлежащего Ч — неформальной теории чисел — очевидно: его весьма легко прочесть. Неудобство же при его использовании напоминает проблему, возникавшую при использовании слов «точка» и «линия» в формальном описании геометрии: если ослабить внимание, то легко спутать обыденное значение этих слов с поведением символов, подчиняющихся строгим правилам. Обсуждая проблемы геометрии, я различал между обыденными словами и терминами — последние печатались заглавными буквами. Так, в эллиптической геометрии ТОЧКОЙ было объединение двух точек. Здесь такого различия не будет, поэтому читатель должен постараться не спутать символ с многочисленными ассоциациями, которые он вызывает. Как я сказал ранее о системе pr, строчка --- не является числом 3; вместо этого она действует изоморфно с числом 3, по крайней мере, при сложении. То же самое можно сказать и о строчке SSS0.

Все символы исчисления высказываний, кроме букв, с помощью которых мы получали атомы (P, Q, R), будут использованы в ТТЧ; при этом они сохранят ту же интерпретацию. Роль атомов будут играть строчки, которые, будучи интерпретированы, дадут равенства, такие как S0=SS0 или (S0#215;S0) = S0. Теперь у нас есть достаточно данных, чтобы перевести несколько простых суждений в запись ТТЧ:

2+3 равняется 4: (SS0+SSS0)=SSSS0

2+2 не равняется 3: ~(SS0+SS0)=SSS0

Если 1 равняется 0, то 0 равняется 1: lt;S0=0э0=S0gt;

Первая из этих строчек — атом; остальные — составные формулы. (Внимание: «и» во фразе «1 и 1 будет 2» — всего лишь еще одно обозначение «плюса» и должно быть представлено «+» (и необходимыми скобками).

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

(b+S0)=SS0

Ее интерпретация — «b плюс 1 равняется 2». Поскольку b не определено, то невозможно сказать, истинно ли данное высказывание. Это напоминает высказывание с местоимением, взятое отдельно от контекста, такое, как «Она неуклюжа.» Это высказывание не истинно и не ложно — оно просто ждет, чтобы его поставили в контекст. Поскольку она не истинна и не ложна, подобная формула зовется открытой, а переменная b называется свободной переменной.

Одним из способов превратить открытую формулу в замкнутую формулу или высказывание является добавление квантора — фразы «существует число b такое, что…» или фразы «для всех b». В первом случае, у вас получается высказывание:

Существует число b такое, что b плюс 1 равняется 2.

Ясно, что это истинно. Во втором случае, вы получите:

Для всех чисел b, b плюс 1 равняется 2.

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

Eb:(b+S0)=SS0 ( E означает «существует»)

Ab:(b+S0)=SS0 ( A означает «все»)

Важно отметить, что речь идет уже не о неопределенных числах; первое высказывание — это утверждение существования, второе — утверждение общности. Их значение не изменится, даже если мы заменим b на c:

Ec:(c+S0)=SS0

Ac:(c+S0)=SS0

Переменная, управляемая квантором, называется квантифицированной переменной. Две следующие формулы иллюстрируют разницу между свободной и квантифицированной переменной.

(b*b)=SS0   (открытая)

~Eb:(b*b)=SS0   (замкнутая - высказывание ТТЧ)

Первая формула выражает свойство, которое может быть присуще какому-либо натуральному числу. Разумеется, такого числа не существует. Этот факт выражен второй формулой. Очень важно понять разницу между строчкой со свободной переменной и строчкой, в которой переменная квантифицирована. Последняя строчка — либо истинна, либо ложна. В переводе на русский язык, строчка, где есть по крайней мере одна свободная переменная, называется предикатом. Предикат — это высказывание без подлежащего (или с подлежащим, выраженным местоимением, лишенным контекста). Например, высказывания:

«является предложением без подлежащего»

«было бы аномалией»

«читается вперед и назад одновременно»

«сымпровизировал по требованию шестиголосную фугу»

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

(S0+S0)=b

означает «1 плюс 1 равняется чему-то». Это предикат с переменной b. Он выражает свойство, которым может обладать число b. Заменяя b на различные числа, мы получили бы последовательность формул, большинство которых выражало бы ошибочные суждения. Вот еще один пример разницы между открытыми формулами и высказываниями:

Ab:Ac:(b+c)=(c+b)

Эта формула, разумеется, выражает коммутативность сложения. С другой стороны:

Ac:(b+c)=(c+b)

— это открытая формула, поскольку b здесь свободно. Она выражает свойство, которым может обладать или не обладать число b, а именно — коммутативность по отношению ко всем числам с.

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

Начнем с последнего высказывания: «6 — четное число». Переведем его в

более примитивные понятия: «Существует число e, такое, что 2, умноженное на e, равняется 6.» Это легко перевести в нотацию ТТЧ:

Ee:(SS0*e)=SSSSSS0

Обратите внимание на необходимость квантора; недостаточно было бы написать просто:

(SS0*e)=SSSSSS0

Интерпретация последней строчки не была бы ни истинной, ни ложной; она выражает только свойство, которое может иметь число e.

Интересно, что, поскольку мы знаем, что умножение коммутативно, то вместо нашей строчки мы могли бы написать:

Ee:(e*SS0)=SSSSSS0

Таким же образом, зная, что равенство симметрично, мы могли бы поменять местами стороны этого равенства:

Ee:SSSSSS0=(SS0*e)

Эти три перевода высказывания «6 — четное число» дают три различные строчки; при этом совершенно не очевидно, что теоремность каждой из них связана с теоремностью остальных. (Совершенно так же тот факт, что строчка -p--r--- была теоремой, почти не соотносился с фактом, что ее «эквивалентная» строчка --p-r--- также была теоремой. Эквивалентность — у нас в голове, так как мы, люди, автоматически думаем об интерпретациях формул, а не об их структурных особенностях.)

С высказыванием 2: «2 не является квадратом» мы расправимся быстро:

~Eb:(b*b)=SS0

Однако здесь мы снова сталкиваемся с двусмысленностью. А что, если бы мы записали эту формулу по-другому?

Ab:~(b*b)=SS0

Интерпретация первой строчки — «Не существует такого числа b, квадрат которого равнялся бы 2»; вторая строчка читается как «Для всех чисел b неверно, что квадрат b равняется 2». Для нас эти строчки представляют одно и то же понятие — однако для ТТЧ это совершенно разные строчки.

Посмотрим теперь на высказывание 3: «1729 — сумма двух кубов». Тут нам понадобятся два квантора один за другим, вот так:

Eb:Ec:SSSSSS.....SSSSS0=(((b*b)*b)+((c*c)*c))

.          |--1729 раза--|

Есть несколько альтернатив этой записи: можно переменить порядок кванторов — сменить переменные на d и e; переменить порядок слагаемых; записать умножение по-иному и т. д., и т. п. Однако я предпочитаю следующие два варианта перевода:

Eb:Ec:(((SSSSSSSSSS0*SSSSSSSSSS0)*SSSSSSSSSS0)+((SSSSSSSSS0*SSSSSSSSS0)*SSSSSSSSS0))=(((b*b)*b)+((c*с)*с))

и

Eb:Ec:(((SSSSSSSSSSSS0*SSSSSSSSSSSS0)*SSSSSSSSSSSS0)+((S0*S0)*S0))=(((b*b)*b)+((c*c)*c))

 Понимаете, почему?

Давайте попробуем перевести теперь высказывание 4: «Сумма двух положительных кубов сама не является кубом». Предположим, что мы хотим сказать, что 7 не является суммой двух положительных кубов. Легче всего сделать это, отрицая формулу, утверждающую обратное. Эта формула будет почти как предыдущая, касавшаяся 1729, только теперь нам надо добавить, что кубы должны быть положительными. Мы можем сделать это при помощи следующего трюка: добавим к каждой переменной префикс S:

Eb:Ec:SSSSSSS0=(((Sb*Sb)*Sb)+((Sc*Sc)*Sc))

Как видите, мы возводим в куб не сами b и c, а следующие за ними числа, которые должны быть положительными, поскольку минимальная величина b и c — 0. Таким образом, правая сторона представляет сумму двух положительных кубов. Кстати, обратите внимание, что перевод высказывания «существуют числа b и c, такие, что…» не включает символа «#923;», заменяющего «и». Этот символ используется для соединения целых правильно сформированных строчек, а не для соединения двух кванторов.

Итак, мы перевели высказывание «7 — сумма двух положительных кубов»; теперь нам нужно записать его отрицание. Для этого мы должны только поставить тильду слева от него. (Заметьте, что не требуется отрицать каждый квантор в отдельности, хотя нам и надо получить высказывание «Не существует чисел b и c, таких, что…») Таким образом, мы получим:

~Eb:Ec:SSSSSSS0=(((Sb*Sb)*Sb)+((Sc*Sc)*Sc))

Однако нашей первоначальной целью было выразить свойства всех чисел, а не только 7. Для этого давайте заменим символ числа SSSSSSSO строчкой ((а*а)*а), являющейся переводом «а в кубе».

~Eb:Ec:((a*a)*a)=(((Sb*Sb)*Sb)+((Sc*Sc)*Sc))

Ha этом этапе у нас имеется открытая формула, так как а все еще свободно. Эта формула выражает свойство, которым может обладать или не обладать а — однако мы хотим сказать, что все числа обладают этим свойством. Это просто — надо только добавить к имеющейся у нас формуле квантор общности:

Aa:~Eb:Ec:((a*a)*a)=(((Sb*Sb)*Sb)+((Sc*Sc)*Sc))

Таким же правильным переводом было бы:

~Eа:Eb:Eс:((а*a)*a)=(((Sb*Sb)*Sb)+((Sc*Sc)*Sc))

В строгом ТТЧ мы могли бы использовать a' вместо b и a'' вместо c; таким образом, формула приобрела бы вид:

~Ea:Ea':Ea'':((a*a)*a)=(((Sa'*Sa')*Sa')+((Sa''*Sa'')*Sa''))

Как насчет высказывания 1: «5 — простое число»? Мы перефразировали его следующим образом: «Не существует чисел a и b больших 1, таких, что 5 равнялось бы a умноженному на b.» Теперь мы можем это немного изменить: «Не существует чисел а и b таких, что 5 равнялось бы а плюс 2 умноженному на b плюс 2.» Это еще один трюк- поскольку а и b здесь — натуральные числа, эта формулировка кажется более адекватной. Далее, «b+2» может быть переведено как (b+SS0), но есть и более короткий способ записать то же самое: SSb. Точно так же, «c плюс 2» может быть записано как SSc. Теперь наш перевод становится совсем коротким:

~Eb:Ec:SSSSS0=(SSb*SSc)

Без тильды в начале это было бы утверждением того, что существуют два натуральных числа, которые, если их увеличить на два, дают при умножении 5. Тильда в начале это отрицает; таким образом, мы получаем утверждение того, что 5 — простое число.

Если бы вместо 5 мы хотели бы сказать то же самое про d плюс e плюс 1, самым экономным способом было бы заменить символ числа 5 на строчку (d+Se):

~Eb:Ec:(d+Se)=(SSb*SSc)

Мы снова получили открытую формулу; ее интерпретация — не истина и не ложь, а лишь некое утверждение о каких-то двух числах d и e. Обратите внимание, что число, выраженное строчкой (d+Se), больше d, так как мы добавили к d хотя и неопределенную, но положительную величину. Таким образом, если мы добавим к переменной e квантор существования, мы получим формулу, утверждающую, что

Существует некое простое число, большее d.

Ee:~Eb:Ec:(d+Se)=(SSb*SSc)

Осталось только добавить, что это свойство верно всегда, вне зависимости от d. Для этого мы должны добавить квантор общности для d:

Ad:Ee:~Eb:Ec:(d+Se)=(SSb*SSc)

Перед нами — перевод высказывания 5!

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

~Ac:Eb:(SS0*b)=c

Ac:~Eb:(SS0*b)=c

Ac:Eb:~(SS0*b)=c

~Eb:Ac:(SS0*b)=c

Eb:~Ac:(SS0*b)=c

Eb:Ac:~(SS0*b)=c

(Еще одна подсказка, либо четыре из них истинны и два ложны, либо, наоборот, два истинны и четыре ложны.)

Теперь давайте на минуту остановимся и переведем дыхание — а заодно подумаем, что означало бы иметь такую формальную систему, которая могла бы отличить все истинные высказывания от ложных. Для такой системы все эти строчки были бы просто некими формальными конструкциями, лишенными содержания (в то время как мы видим в них высказывания). Эта система была бы словно решето, сквозь которое проходили бы только конструкции определенного стиля — «стиля истины». Если вы сами имели дело с шестью формулами выше и отделили истинные от ложных, размышляя об их значении, вы сможете оценить, насколько тонкой должна быть система, которая сможет проделать то же самое, но чисто типографским путем! Граница, отделяющая истинные высказывания от ложных (записанных нотацией ТТЧ) вовсе не пряма — это граница со множеством предательских извилин (вспомните рис. 18). Математики смогли установить некоторые отрезки этой границы, работая над этим сотни лет. Представьте себе, как было бы здорово иметь типографский метод, который с гарантией мог бы поставить любую формулу по правильную сторону границы!

Полезно иметь таблицу Правил Образования для правильно сформированных формул Такая таблица приведена ниже. На подготовительных этапах определяются символы чисел, переменные и термы. Эти три класса строчек являются ингредиентами правильно сформированных формул, но сами они не являются правильно сформированными. Минимальные правильно сформированные формулы — это атомы; существуют способы для соединения атомов. Многие из этих правил — рекурсивные и удлиняющие: в качестве вводных данных они берут элемент определенного класса и производят более длинный элемент того же класса. В этой таблице я использую «x» и «у» как символы для правильно сформированных формул и «s», «t» и «u» — как символы для всех остальных строчек ТТЧ. Нет нужды говорить, что никакой из этих пяти символов сам по себе не является символом ТТЧ.

СИМВОЛЫ ЧИСЕЛ

0 — это символ числа.

Символ числа, слева от которого стоит S — также символ числа.

Примеры: 0 S0 SS0 SSS0 SSSS0 SSSSS0

ПЕРЕМЕННЫЕ

a — это переменная Если забыть об аскетизме, то b, c, d, и e — тоже переменные. Переменная со штрихом справа — также переменная.

Примеры: а b' c" d''' e''''

ТЕРМЫ

Термами являются символы чисел и переменные. Терм, слева от которого стоит S — это также терм.

Если s и t — термы, то (s+t) и (s*t) — также термы.

Примеры: 0  b  SSa'  (S0*(SS0)+c))  S(Sa*(SbSc))

ТЕРМЫ могут быть подразделены на две категории:

(1) ОПРЕДЕЛЕННЫЕ термы. В них нет переменных.

Примеры: 0  (S0+S0)  SS((S0*SS0)+(S0*S0))

(2) НЕОПРЕДЕЛЕННЫЕ термы. В них есть переменные.

Примеры: b  Sa(b+S0)  (((S0+S0)+S0)+e)

Приведенные выше правила объясняют нам, как получить части правильно сформированных формул; остальные правила говорят нам, как получить полные правильно сформированные формулы.

АТОМЫ

Если s и t — термы, то s+t — атом.

Примеры: S0=0  (SS0+SS0)=SSSS0  S(b+c)=((c*d)*e)

Если атом содержит переменную u, то u в нем свободна.

Таким образом, в последнем примере есть четыре свободных переменных.

ОТРИЦАНИЯ.

Правильно сформированная формула перед которой стоит тильда также правильно сформирована.

Примеры: ~S0=0   ~Eb:(b+b)=S0   ~lt;0=0эS0=0gt;   ~b=S0

Кванторный статус переменной (говорящий нам, свободна или квантифицирована эта переменная) не меняется при отрицании.

СОСТАВНЫЕ.

Если x и у — правильно сформированные формулы и при этом ни одна переменная, свободная в одной из них, не квантифицирована в другой, тогда все следующие формулы правильно сформированы: lt;x #923; ygt;, lt;x V ygt;,lt;x э ygt;

Примеры: lt;0=0э~0=0gt;    lt;b=bV~Ec:c=bgt;    lt;S0=0эAc:~Еb:(b+b)=cgt;

Кванторный статус переменной здесь не меняется.

КВАНТИФИКАЦИЯ.

Если u — переменная и x — правильно сформированная формула, в которой и свободна, то следующие строчки — также правильно сформированные формулы:Eu:x и Au:x

Примеры: Ab:lt;b=bV~Ec:c=bgt;    Ac:~Eb:(b+b)=c    ~Еc:Sc=d

ОТКРЫТЫЕ ФОРМУЛЫ содержат по крайней мере одну свободную переменную.

Примеры: ~c=c  b=b  lt;Ab:b=b#923;~c=cgt;

ЗАМКНУТАЯ ФОРМУЛА (суждение) не содержит свободных переменных.

Примеры: S0=0  ~Ad:d=0  Ec:lt;Ab:b=b#923;~c=cgt;

Это дает нам полную таблицу Правил Образования для правильно сформированных формул ТТЧ.

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

Все натуральные числа равны 4.

Ни одно натуральное число не равно собственному квадрату.

Различные натуральные числа имеют различные последующие элементы.

Если 1 равняется 0, то любое число нечетно.

b — это степень 2.

Последнее может показаться вам трудным. Однако это еще цветочки по сравнению со следующим:

b — это степень 10.

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

Мы изложили нотацию ТТЧ; остается только превратить ТТЧ в ту амбициозную систему, которую мы только что описали. Если нам это удастся, это будет значить, что интерпретация, которую мы дали символам, была правильна. До тех пор, однако, наши интерпретации не более оправданы, чем интерпретация «лошадь — яблоко — счастливая» для символов системы pr.

Можно было бы предложить следующий способ для построения ТТЧ: (1) Не использовать никаких правил вывода — они не нужны, так как (2) мы будем считать за аксиомы все истинные суждения теории чисел (записанные нотацией ТТЧ). Какой простой рецепт! К несчастью, он начисто лишен смысла, как нам и подсказывает наша первая реакция. Часть (2), разумеется, не является типографским описанием строчек, в то время как целью ТТЧ является именно типографское описание истинных высказываний.

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

lt;S0 = 0 V ~ S0 = 0gt;

Она может быть выведена так же, как lt;P V ~ P gt;. Прежде чем приводить правила, давайте запишем пять аксиом. ТТЧ:

АКСИОМА 1: Aa:~Sa=0

АКСИОМА 2: Aa:(a+0)=a

АКСИОМА 3: Aa:Ab:(a+Sb)=S(a+b)

АКСИОМА 4: Aa:(a*0)=0

АКСИОМА 5: Aa:Ab:(a*Sb)=((a*b)+a)

(В строгой версии вместо b используйте a'.) Все они очень просты. Аксиома 1 сообщает что-то о числе 0; аксиомы 2 и 3 говорят о свойствах сложения; аксиомы 4 и 5 говорят о свойствах умножения и о его отношении к сложению.

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

(1) Джинн — это Гений.

(2) Каждый Гений имеет мету (которая тоже является Гением).

(3) Джинн не является метой никакого Гения.

(4) Различные Гении имеют различные меты.

(5) Если джинн имеет X и каждый Гений передает X своей мете, тогда все Гении получают X.

В свете ламп «Маленького гармонического лабиринта» мы должны наименовать множество всех Гениев «БОГом». Это напоминает нам о знаменитом высказывании немецкого математика и логика Леопольда Кроникера, архиврага Георга Кантора: «Бог сотворил натуральные числа; все остальное — работа человека.»

Вы можете узнать в пятом постулате Пеано принцип математической индукции — другой термин для «наследственного» доказательства. Пеано надеялся, что его ограничения понятий «джинна», «Гения» и «меты» были так сильны, что эти понятия были бы идентичны для всех людей и формировали бы у них в сознании совершенно изоморфные структуры. Например, для любого человека существовало бы бесконечное число различных Гениев. И, предположительно, каждый согласился бы с тем, что ни один Гений не совпадает со своей метой или мета-метой… и т. д.

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

Мы подошли к новым правилам ТТЧ. Многие из них позволят нам забраться внутрь этой системы и поменять внутреннюю структуру ее атомов. В этом смысле эти правила имеют дело с «микроскопическими» особенностями строчек в большей степени, чем правила исчисления высказываний, обращающиеся с атомами как с неделимыми. Например, было бы хорошо, если бы мы могли выделить строчку ~S0=0 из первой аксиомы. Для этого нам понадобилось бы правило, позволяющее опустить общий квантор и при необходимости одновременно поменять внутреннюю структуру остающейся строчки. Вот это правило:

ПРАВИЛО СПЕЦИФИКАЦИИ. Предположим, что u — переменная, встречающаяся внутри строчки x. Если строчка Au:x  — теорема, то x — тоже теорема, как и все строчки, получающиеся из x путем замены и на любой (один и тот же) терм.

(Ограничение: Терм, заменяющий и, не должен содержать никакой переменной, квалифицированной в x.)

Правило спецификации позволяет нам выделить нужную строчку из Аксиомы

1. Это одноступенчатая деривация:

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

~S0=0  спецификация

Обратите внимание, что правило спецификации позволяет некоторым формулам, содержащим свободные переменные (то есть, открытым формулам), стать теоремами. Например, следующие строчки также могут быть выведены из аксиомы 1 при помощи спецификации:

~Sa=0

~S(c+SS0)=0

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

Ac:~S(c+SS0)=0

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

ПРАВИЛО ОБОБЩЕНИЯ: Предположим, что x — теорема, в которой встречается свободная переменная u. Тогда Au:x — тоже теорема.

(Ограничение: к переменным, которые встречаются в свободном виде в посылках фантазий, обобщение неприложимо.)

Вскоре я ясно покажу, почему эти два правила нуждаются в ограничениях. Кстати, это обобщение — то же самое, о котором я упомянул в главе II в Эвклидовом доказательстве бесконечного количества простых чисел. Уже отсюда видно, как правила, манипулирующие символами, начинают приближаться к типу рассуждений, используемых математиками.

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

ПРАВИЛО ОБМЕНА: Представьте, что 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)  lt;a=0эSa=0gt;      правило фантазии

(7)  Aa:lt;a=0эSa=0 обобщение

(8)  lt;0=0эS0=0gt;      спецификация

(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. Если приведенная выше строчка — не теорема, то у нас есть основания подозревать, что в ТТЧ есть какой-то дефект. На самом деле, существует даже название для систем с подобным дефектом — они называются #969;-неполными. (Символ #969; — «омега» — выбран потому, что иногда все множество натуральных чисел обозначается этой буквой.) Далее следует точное определение:

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

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

~Aa:(0+a)=a

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

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

~Ea:(0+a)=a

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

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

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

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

В конкретной пирамиде, которую мы рассматривали, такая схема существует; она представлена строчками 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} — правильно сформированная формула, в которой и свободно. Если и Ault;X{u}эX{Su/u} и X{0/u} — теоремы, то Au:X{u} также является теоремой.

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

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

(11) Ab:lt;(0+b)=bэ(0+Sb)=Sbgt;   обобщение

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

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) lt;Ad:(d+Sc)=(Sd+c)эAd:(d+SSc)=(Sd+Sc)gt; правило фантазии

(18) Ac:lt;Ad:(d+Sc)=(Sd+c)эAd:(d+SSc)=(Sd+Sc)gt; обобщение

*****

(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) lt;Ac:(c+d)=(d+c)эAc:(c+Sd)=(Sd+c)gt; правило фантазии

(49) Ad:lt;Ac:(c+d)=(d+c)эAc:(c+Sd)=(Sd+c)gt; обобщение

[Если 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#215;1000 — это нарисовать решетку размером 1000x1000 и подсчитать в ней клеточки. На самом деле, после полной формализации остается единственный путь — дать формальной системе послабление. Иначе она становится такой громоздкой, что теряет всякую практическую пользу. Таким образом, необходимо внести ТТЧ в более широкий контекст, такой, который позволит нам получить правила вывода, ускоряющие деривацию. Для этого нам понадобится формализовать язык, на котором выражены эти правила вывода — то есть метаязык. Можно пойти еще намного дальше; однако никакие из этих трюков не сделают ТТЧ более мощной — они лишь сделают ее более удобной для пользования. Дело в том, что мы выразили в ТТЧ все типы рассуждений, на которые опираются математики, занимающиеся теорией чисел. Введение ее в более широкий контекст не увеличит количества теорем; оно лишь сделает работу в ТТЧ — или в любой «улучшенной» ее версии — более похожей на работу в традиционной теории чисел.

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

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

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

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

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