Приведем конкретный пример. Пусть X{a} обозначает строчку (0+а)=а. Тогда X{Sa/a} представляет строчку (0+Sa)=Sa, a X{0/a} — строчку (0+0)=0.
(Внимание: эта нотация не является частью ТТЧ; она служит нам лишь для того, чтобы говорить о ТТЧ.)
С помощью этой новой нотации мы можем выразить последнее правило ТТЧ весьма точно:
ПРАВИЛО ИНДУКЦИИ. Предположим, что u — переменная и X{u} — правильно сформированная формула, в которой и свободно. Если и Au<X{u}эX{Su/u} и X{0/u} — теоремы, то Au:X{u} также является теоремой.
Мы подошли так близко, как возможно, к введению пятого постулата Пеано в ТТЧ. Давайте теперь используем его, чтобы показать, что 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) <Ad:(d+Sc)=(Sd+c)эAd:(d+SSc)=(Sd+Sc)> правило фантазии
(18) Ac:<Ad:(d+Sc)=(Sd+c)эAd:(d+SSc)=(Sd+Sc)> обобщение
*****
(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) <Ac:(c+d)=(d+c)эAc:(c+Sd)=(Sd+c)> правило фантазии
(49) Ad:<Ac:(c+d)=(d+c)эAc:(c+Sd)=(Sd+c)> обобщение
[Если 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 — истинно. (Следите ли вы за ходом рассуждения? Очень важно держать в голове разницу между формальной системой ТТЧ и ее неформальным соответствием — теорией чисел; читатель должен постараться хорошо понять эту разницу.) Так что в принципе, если бы ТТЧ была полной, специалисты по теории чисел остались бы без работы: со временем любую проблему можно было бы решить чисто механическим путем. Оказывается, однако, что это невозможно; по этому поводу можно радоваться или огорчаться, в зависимости от вашей точки зрения.
