Гильберт уловил самую суть проблемы, положив в основу своих попыток построения «абсолютных» доказательств непротиворечивости различие между формальным исчислением и его описанием. Он поставил задачу развития специального метода, с помощью которого можно было бы проводить доказательства непротиворечивости той же степени убедительности, что и доказательства, использующие конечные модели, на которых реализуются определенные системы постулатов. Искомый метод должен был бы состоять в исчерпывающем анализе конечного числа структурных свойств выражений в полностью формализованных исчислениях. Анализ должен исходить из точной фиксации различных видов, входящих в рассматриваемое исчисление символов, указания на способы соединения этих символов в формулы, описания способа вывода одних формул из других и давать способ решения вопроса, выводимы ли формулы какого-либо определенного вида из некоторых определенных формул посредством явно сформулированных правил оперирования с формулами. Гильберт был убежден в том, что каждое математическое исчисление можно представить «на геометрический манер», т. е. в виде такой совокупности формул, каждая из которых связана с любой другой формулой того же исчисления лишь структурными соотношениями из некоторого конечного перечня соотношений.
На этом убеждении и основывался его расчет, что он сумеет посредством систематического и исчерпывающего обозрения этих структурных свойств выражений данной системы показать, что из аксиом данного исчисления нельзя получить формально противоречащие друг другу формулы. Существеннейшим условием гильбертовской программы в первоначальной ее формулировке было разрешение употреблять в доказательствах непротиворечивости лишь такие приемы рассуждений, которые ни в какой форме не используют ни бесконечного множества структурных свойств формул, ни бесконечного множества операций над формулами.
Такие методы рассуждений он назвал «финитными», а доказательства непротиворечивости, проведенные финитными средствами, — «абсолютными». «Абсолютное» доказательство достигает своей цели с помощью некоторого минимального арсенала принципов вывода и не исходит из непротиворечивости никакой другой системы аксиом. Таким образом, если бы, например, удалось получить абсолютное доказательство непротиворечивости арифметики, оно должно было бы посредством некоторой финитной метаматематической процедуры установить невозможность одновременного вывода из аксиом (т. е. из исходных формул) арифметики с помощью фиксированных правил вывода никакой пары взаимно противоречивых формул, скажем «0 = 0» и ее отрицания «~ (0 = 0)» (здесь знак «~» означает «не»).
Вполне точных указаний на то, какие именно математические методы следует считать «финитными», Гильберт не дал. В первоначальной формулировке его программы требования, которым должны были удовлетворять абсолютные доказательства непротиворечивости, были значительно более сильными, чем в последующих разъяснениях гильбертовской программы, данных представителям школы Гильберта.
Будет, пожалуй, небесполезно сравнить метаматематику, понимаемую как теорию доказательства, с теорией шахматной игры. В шахматы играют с помощью 32 фигур определенного вида, передвигающихся по квадратной доске, разделенной на 64 клетки, причем передвижения эти («ходы») совершаются по некоторым строго определенным правилам. Разумеется, для игры не требуется никакой «интерпретации» фигур и их различных положений на доске, хотя такую интерпретацию при желании можно было бы и придумать. Например, можно было бы считать, что пешки — это армейские полки, а клетки доски — определенные географические районы и т. п. Но такого рода соглашения (интерпретации) не употребительны — на самом деле ни фигуры, ни клетки доски, ни положения фигур не означают ровно ничего вне игры как таковой. Иначе говоря, можно было бы сказать, что фигуры и их положения на доске «бессмысленны». Таким образом, игра в шахматы является далеко идущим аналогом формализованного математического исчисления. Фигуры и клетки доски соответствуют элементарным символам исчисления; допустимые правилами игры позиции соответствуют формулам исчисления; начальная позиция партии (или любой шахматной задачи) соответствует набору аксиом исчисления; последующие позиции — формулам, выводимым из аксиом (т. е. теоремам); наконец, правила игры соответствуют правилам вывода (правилам преобразования) исчисления. Аналогия простирается и дальше. Хотя сами по себе позиции (расположения фигур на доске), подобно формулам исчисления, «бессмысленны», высказывания об этих позициях, подобно метаматематическим высказываниям о формулах, вполне осмысленны.
«Меташахматное» утверждение может, например, гласить, что в данной позиции у белых возможны двадцать различных ходов, или, скажем, что в данной позиции белые, начиная, могут заматовать черных за три хода. Более того, можно говорить и об общих «меташахматных» теоремах, в доказательствах которых используется наличие лишь конечного числа возможных позиций. Можно, например, получить теорему относительно числа возможных ходов для белых в начальной (или любой другой) позиции; или, скажем, доказать теорему, согласно которой два белых коня с королем не могут форсировать мат одинокому черному королю. Эти и другие «меташахматные» теоремы удается, таким образом, доказывать, пользуясь финитными методами рассуждений, т. е. исследуя лишь конечное число возможных позиций, удовлетворяющих четко сформулированным условиям. Совершенно аналогично цель гильбертовской теории доказательства состоит в доказательстве такого же рода финитными методами невозможности вывода противоречащих друг другу формул в данном математическом исчислении.
4
Систематическое построение формальной логики
Прежде чем перейти к самой теореме Гёделя, нам придется преодолеть еще два препятствия. Прежде всего нам надо разобраться, зачем, собственно, ему понадобилась Principia Mathematica Уайтхеда и Рассела и в чем суть этой системы; далее, нам понадобится рассмотреть в качестве примера формализации дедуктивной системы один небольшой фрагмент системы Principia,и показать, как можно получить абсолютное доказательство непротиворечивости этого фрагмента.
Обычно, даже если математические доказательства проводятся с соблюдением общепринятых норм профессиональной строгости, эта строгость существенно умаляется в результате некоторого упрощения весьма принципиального характера. Дело в том, что принципы (правила) вывода, употребляемые в доказательствах, в явной форме не формулируются, так что математики применяют их не вполне осознанно. Возьмем, например, евклидовское доказательство того факта, что не существует наибольшего простого числа (целое число, как известно, называется простым, если оно не делится без остатка ни на одно число, кроме единицы и самого себя). Доказательство, проводимое методом reductio ad absurdum (от противного), выглядит следующим образом.
Пусть, в противоречии с доказываемым утверждением, имеется наибольшее простое число. Обозначим его через «x». Тогда:
1. x есть наибольшее простое число.
2. Образуем произведение всех простых чисел, меньших или равных x, и прибавим к этому произведению число 1. В результате получим некоторое число y:
y = (2 × З × 5 × 7 × … × x) + 1.
3. Если у само есть простое число, то x не есть наибольшее простое число, так как у, очевидно, больше x.