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

ТТЧ доказала коммутативность сложения. Даже если вы не следили за всеми деталями этой деривации, важно понять, что, так же как и музыкальная пьеса, она имеет свой собственный естественный "ритм". Это вовсе не случайная про­гулка, во время которой мы вдруг наткнулись на нужную строчку. Я ввел "паузы для дыхания", чтобы показать "артикуляцию" этой деривации. В частно­сти, строчка 28 является переломным моментом в деривации - что-то вроде середины в пьесе типа ААББ, где происходит временное разрешение, хотя и не в ключевую тональность. Подобные "важные промежуточные моменты часто называют "леммами".
Легко вообразить себе читателя, который начинает со строки 1 этой дери­вации, не зная, где он закончит, и постепенно, с каждой новой строкой, понима­ющего, куда он направляется. Это порождает внутреннее напряжение, очень похожее на то, которое порождает в музыке прогрессия аккордов, указывающая на тонику, но не разрешающаяся в нее. Прибытие к строке 28 подтверждает интуицию читателя и дает ему некое чувство удовлетворения; в то же время, это усиливает его желание дойти до предполагаемой конечной цели.
Строчка 49 - критически важный увеличитель напряжения, поскольку она вызывает ощущение "почти у цели". Прервать деривацию в этот момент было бы очень неприятно. С этого момента мы уже почти можем предсказать развитие событий. Однако вам не хотелось бы прервать музыкальную пьесу в том момент, когда вам уже очевидно, как она разрешится. Вам не хотелось бы воображать финал - вам хотелось бы его услышать. Так же и здесь, мы должны закончить деривацию. Строка 55 Неизбежна и производит максималь­ное финальное напряжение, которое затем разрешается в строке 56.
Это типично не только для структуры формальных дериваций, но и для неформальных доказательств. Чувство напряжения, возникающее у математи­ков, тесно связано с восприятием красоты; это делает математику интересным и стоящим занятием. Обратите внимание, однако, что в самой ТТЧ это напряже­ние, по-видимому, не отражается. Иными словами, понятия напряжения и раз­решения, цели и временной цели, "естественности" и "неизбежности" не форма­лизованы в ТТЧ подобно тому, как музыкальная пьеса не является книгой о гармонии и ритме. Возможно ли создать более сложную формальную систему, которая осознавала бы напряжение и цель внутри дериваций?


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

Я предпочел бы показать вам, как выводится теорема Эвклида (бесконечность простых чисел), но это, возможно, сделало бы книгу вдвое длиннее. Теперь, после доказательства теоремы, естественным продолжением было бы доказать ассоциативность сложения, коммутативность и ассоциативность умножения и дистрибутивность умножения со сложением. Это создало бы прочную базу для дальнейшей работы.
В нашей теперешней формулировке ТТЧ достигла "критической массы". Ее мощь сравнялась с мощью "Principia mathematica" - в ней стало возможным доказать любую теорему, которую можно найти в стандартном труде по теории чисел. Конечно, никто не стал бы утверждать, что вывод теорем в ТТЧ - это наилучший способ заниматься теорией чисел. Человек, так считающий, принад­лежал бы к классу людей, которые думают, что лучший способ узнать, сколько будет 1000х1000 - это нарисовать решетку размером 1000х1000 и подсчитать в ней клеточки. На самом деле, после полной формализации остается един­ственный путь - дать формальной системе послабление. Иначе она становится такой громоздкой, что теряет всякую практическую пользу. Таким образом, не­обходимо внести ТТЧ в более широкий контекст, такой, который позволит нам получить правила вывода, ускоряющие деривацию. Для этого нам понадобится формализовать язык, на котором выражены эти правила вывода - то есть метаязык. Можно пойти еще намного дальше; однако никакие из этих трюков не сделают ТТЧ более мощной - они лишь сделают ее более удобной для пользования. Дело в том, что мы выразили в ТТЧ все типы рассуждений, на которые опираются математики, занимающиеся теорией чисел. Введение ее в более широкий контекст не увеличит количества теорем; оно лишь сделает работу в ТТЧ - или в любой "улучшенной" ее версии - более похожей на работу в традиционной теории чисел.


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

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


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

Последний вопрос, который мы рассмотрим в этой главе, таков: должны ли мы так же верить в непротиворечивость ТТЧ, как мы верили в непротиворечивость исчисления высказываний? И если нет, то возможно ли укрепить нашу веру в ТТЧ, доказав, что она непротиворечива? Для начала можно утверждать, по­добно тому, как Неосторожность утверждала об исчислении высказываний, что непротиворечивость ТТЧ "очевидна" - а именно, что каждое правило вопло­щает принцип логических рассуждений, в который мы верим безоговорочно;
следовательно, ставить под вопрос непротиворечивость ТТЧ, это все равно, что сомневаться в собственном здравом уме. Этот аргумент все еще имеет некото­рый вес, но уже не такой, как раньше. Дело в том, что теперь у нас слишком много правил вывода, и в какие-то из них могла вкрасться ошибка. Более того, откуда мы знаем, что наша мысленная модель неких абстрактных единиц под названием "натуральные числа" последовательна? Может быть, наши собственные мыслительные процессы, те неформальные процессы, которые мы пытались выразить в правилах формальной системы, сами по себе непоследовательны! Конечно, мы не ожидаем подобного подвоха. Тем не менее, можно представить, что чем сложнее объект нашей мысли, тем легче в нем запутаться; а натураль­ные числа - объект совсем не тривиальный. Так что в этом случае мы должны серьезнее воспринимать аргументы Осторожности, когда она требует доказа­тельства непротиворечивости. Не то, чтобы мы действительно сомневались в непротиворечивости ТТЧ - но у нас все же есть малюсенькое сомнение, тень сомнения, и доказательство помогло бы эту тень рассеять.
Какой же метод доказательства нам бы хотелось использовать? Здесь мы снова сталкиваемся с проблемой порочного круга. Если мы будем использовать в доказательстве факта о системе те же инструменты, какие используются внутри самой системы, то чего мы таким образом добьемся? Если бы нам удалось убедиться в непротиворечивости ТТЧ, используя более слабую систему рассуж­дений, чем сама ТТЧ, мы избежали бы этого порочного круга! Подумайте о том, как протягивают тяжелый канат между двумя кораблями (по крайней мере, я читал об этом, когда был мальчишкой): сначала с одного из кораблей пускается стрела, которая перетаскивает через промежуток между кораблями веревку, затем при помощи этой веревки перетягивается канат. Если бы нам удалось использовать "легкую" систему, Чтобы показать непротиворечивость "тяжелой" системы, тогда мы могли бы считать, что действительно чего-то добились.
С первого взгляда может показаться, что у нас есть такая веревка. Наша цель - доказать, что в ТТЧ есть некоторое типографское свойство (непротиво­речивость): в ней не встречаются одновременно теоремы формы х и ~х. Это похоже на доказательство того, что MU не является теоремой системы MIU. В обоих случаях мы имеем дело с утверждениями о типографских свойствах си­стем, манипулирующих символами. Наше сравнение с верейкой основано на предположении о том, что факты теории чисел не нужны для доказательства некоего типографского свойства. Иными словами, если не использовать свой­ства целых чисел вообще - или использовать только несколько простейших свойств - мы можем доказать непротиворечивость ТТЧ, используя способы, более простые, чем наша внутренняя система рассуждений.
Именно на это надеялась школа математиков и логиков начала века; гла­вой этой влиятельной школы был Давид Гильберт. Их целью было доказать непротиворечивость формализации теории чисел, подобных ТТЧ, используя весьма ограниченный набор логических принципов рассуждения, называемых финит­ными. Эти принципы были бы их "веревкой". Среди финитных методов - все методы исчисления высказываний, и некоторые методы численных рассужде­ний. Однако труды Гёделя показали, что любые усилия протащить через про­пасть канат непротиворечивости ТТЧ, пользуясь веревкой финитных методов, обречены на провал. Гёдель показал, что для того, чтобы перетащить этот канат, невозможно пользоваться более легкой веревкой - просто нет настолько креп­кой веревки, чтобы она выдержала такую нагрузку. Выражаясь менее метафо­рично, можно сказать: любая система, достаточно мощная, чтобы дока­зать непротиворечивость ТТЧ, по крайней мере так же мощна, как сама ТТЧ. Поэтому порочного круга здесь не избежать.

Вопросы? Предложения? Претензии?
Обсудить материал в моем ЖЖ