2. Концепция абсолютного доказательства и метод формализованной аксиоматики

Чтобы доказать непротиворечивость, Гильберт использует метод так называемого абсолютного доказательства, который находит реализацию в идее формализованной аксиоматики.

Вообще, аксиоматика уже вошла в арсенал математических средств. Благодаря этому геометрия древних была "расшифрована" как наука получения следствий из принятых предложений, то есть выявлен механизм выведения знаний, имеющих принудительный характер.

Однако с усилением абстрактности математики (в частности, благодаря открытию неэвклидовых геометрий), с утратой наглядности аксиом, возникло сомнение в непротиворечивости последних. Обычно непротиворечивость доказывалась построением моделей (интерпретаций). Необходимо, чтобы каждый постулат оказался истинным утверждением об объектах модели. Если это выполняется, значит постулаты системы совместимы.

Так, неэвклидовы геометрии интерпретируются на эвклидовой, непротиворечивость которой служит аргументом непротиворечивости первых. Для интерпретации же самой эвклидовой системы прибегали к арифметической модели (предложенной также Гильбертом). Но здесь и обнаружилось несовершенство описанных методов доказательств. Они не абсолютны, поскольку предполагали ссылки на другие системы, в конечном счете - на арифметику. Последняя же включает бесконечное число объектов (натуральный ряд) и не обозрима в конечное число шагов. Поэтому постулаты не могли быть интерпретированы. Так, для аксиомы о параллельных требовалась модель бесконечно продолженных параллельных. Невозможность получения такой модели означала отсутствие гарантий, что на каком-то этапе ее построения не встретимся с противоречием.

Предложенное Гильбертом доказательство не связано с интерпретацией (допущением непротиворечивости другой системы) и опирается лишь на наличное, заданное построение. Потому оно названо абсолютным (прямым, непосредственным). В чем же его суть?

Новый метод предполагал построение формализованной аксиоматики. До этого была известна модель содержательной аксиоматики, осуществленной Гильбертом же на основе построения геометрии Эвклидом. При этом Гильберт внес существенные коррективы в систему Эвклида, для которой характерно следующее. 1. Отсутствие списка исходных объектов. 2. Наличие ссылок на интуицию и опыт, например, в понятиях "лежать между", "находиться внутри" и т.п. Попытки же дать определения термина уводили в бесконечность (regressus in infinitum). Скажем, "прямая есть кратчайшее расстояние между двумя точками". Немедленно встает вопрос, а что такое "расстояние"? Что такое точка? Положим, "точка есть то, что не имеет измерения". Но что такое "измерение"? И т.д. Или определение Эвклида: "линия есть длина без ширины". 3. Отсутствие четко фиксированных правил вывода. Последние принимались сами собой разумеющимися, предшествующими математике и взятыми из логики (аналогично тому, как используются логические правила в обыденных рассуждениях: мы соблюдаем их, специально не договариваясь об этом).

Приводя содержательную аксиоматику эвклидовой геометрии, Гильберт соответственно уточняет. 1. Приводит полный список исходных объектов и аксиом. 2. Объекты вводятся им без каких-либо ссылок на опыт. Он избегает попытки дать определения путем указания свойств. Вернее, избегает давать обычные определения через родовидовые или генетические признаки и использует так называемы имплицитные (скрытые, неявные определения - через аксиомы. Так, перечисляя исходные объекты - точки, прямые, плоскости - и указывая, что мы о них ничего не знаем и не должны знать (ибо это означало бы уход в бесконечность), Гильберт подчеркивает: "Все, что мы имеем право об этом знать, это то, чему научают нас об этом аксиомы"¹¹².

Это содержательная аксиоматика. Но теперь Гильберт идет дальше к аксиоматике формализованной, в которой в качестве исходных образований фигурируют абстрактные символы, а вместо содержательных предложений (аксиом, теорем и т.п.) - сочетания символов. В результате остаются лишь формулы. "Основная мысль моей теории доказательства, - писал Д. Гильберт, - такова: все высказывания, которые составляют вместе математику, превращаются в формулы, так что сама математика превращается в совокупность формул"¹¹³/

Формализация предполагает следующие шаги. (1) Задают полный перечень символов, которые используются в системе ("алфавит системы"). Так водятся исходные объекты. Гильберт в связи с этим говорил следующее. Будем мыслить три системы вещей. Вещи 1-ой называем точками и обозначаем A, B, C,...; вещи 2-ой системы - прямыми (a, b, c,...); вещи 3-ей - плоскостями (a , b , g ,...). Далее, (2) вводятся правила образования из "букв" алфавита его формул (предложения системы). Это формальная грамматика исчисления, то есть допустимые в системе знаковые сочетания (предложения, формулы). Но их много. Потому из числа формул отбираем исходные (3). Они образуют базис системы. Наконец, (4) устанавливаем правила преобразования формул (правила вывода), чтобы из исходных получать все остальные. Тогда исходные формулы суть аксиомы, а получаемые путем применения к ним правил - теоремы. Последние образуют "тело" системы.

Таким образом, все составляющие математику предложения оказываются формулами. Налицо исчисление: в совокупность исходных символов входят те и только те, на которые мы указали, аксиомы же и теоремы - просто "строчки", последовательности лишенных значения знаков.

А теперь перейдем к решающему пункту программы Д. Гильберта. Имея такую формализованную систему, можем провести прямое (не выходящее за рамки системы) доказательство ее непротиворечивости. Это и есть абсолютное, без каких-либо ссылок на эмпирию, на интерпретационные модели, доказательство. Оно имеет алгоритм и цель. Алгоритм заключает три шага: 1) предъявляется формула; 2) что из предъявленной формулы следует другая (правила заданы). И эта другая - следствие либо из аксиом, либо из ранее доказанных теорем; 3) предъявляется другая формула. Это средства, а цель? Именно непротиворечивость. Доказательство реализуется так: манипулируя с принятыми символами по правилам системы, никогда не получим два логически противоречивых высказывания F и не-F .Например, утверждение "0=0" и его отрицание. Иными словами, неравенство "0 0" в системе не должно быть доказуемо. Свои методы Гильберт назвал финитными: они не используют ни бесконечных множеств структурных свойств формул, ни бесконечных множеств операций над формулами.

В качестве иллюстрации метода Гильберт ссылается на шахматную игру. Фигуры и клетки шахматной доски - исходные символы (буквы алфавита); позиции фигур, допустимые правила игры, - формулы исчисления; начальные позиции партии (или шахматной задачи) - набор аксиом исчисления; последующие позиции - формулы, выводимые из аксиом, то есть теоремы; правила игры суть правила вывода (преобразования).

Как в исчислении нельзя получить , так и в правильно разыгранной шахматной партии не может встретиться положения, когда бы на доске было одновременно 10 ферзей одного цвета. Ибо, согласно правилам, ходы не могут увеличивать общей суммы числа пешек (8) и ферзей (1), имеющихся в начале игры. Значит, и далее их общее число не превзойдет 9. Соблюдая правила, никогда не окажемся в ситуации, позволяющей утверждать: "На доске может быть не более 9 ферзей одного цвета" и "На доске может быть более 9 ферзей одного цвета".

Так было получено понятие доказательства абсолютной непротиворечивости формальных систем, а вместе с ним, как полагал Гильберт, - и доказательство непротиворечивости математики. Иначе говоря, казалось, что получено обоснование последней¹¹⁴. Вывод, к которому приходит формалистское направление, состоит в том, что обоснование математики в ней самой.

Вскоре однако произошло событие, имевшее столь же радикальные последствия, как в свое время обнаружение парадоксов Рассела.