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

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

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