ГЕДЕЛЬ, ЭШЕР, БАХ: эта бесконечная гирлянда
Шрифт:
Первая строка пирамиды — также теорема; это прямо следует из аксиомы 2. Все, что теперь требуется, это правило, позволяющее нам заключить, что строчка, суммирующая всю пирамиду в целом, тоже является теоремой. Такое правило будет формализованным пятым постулатом Пеано.
Чтобы выразить это правило, нам необходимо ввести кое-какую нотацию.
Давайте запишем правильно сформированную формулу, в которой переменная а свободна:
X{a}
(Там могут встречаться и другие свободные переменные, но нам это неважно.) Тогда запись X{Sa/a} будет обозначать то же самое, с той разницей, что все а будут заменены
Приведем конкретный пример. Пусть 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.