Концепция абсолютного доказательства и метод формализованной аксиоматики. Чтобы доказать непротиворечивость, Гильберт использует метод так называемого абсолютного доказательства, который находит реализацию в идее формализованной аксиоматики. Вообще, аксиоматика уже вошла в арсенал математических средств.
Благодаря этому геометрия древних была расшифрована как наука получения следствий из принятых предложений, то есть выявлен механизм выведения знаний, имеющих принудительный характер. Однако с усилением абстрактности математики в частности, благодаря открытию неэвклидовых геометрий, с утратой наглядности аксиом, возникло сомнение в непротиворечивости последних. Обычно непротиворечивость доказывалась построением моделей интерпретаций. Необходимо, чтобы каждый постулат оказался истинным утверждением об объектах модели.
Если это выполняется, значит постулаты системы совместимы. Так, неэвклидовы геометрии интерпретируются на эвклидовой, непротиворечивость которой служит аргументом непротиворечивости первых. Для интерпретации же самой эвклидовой системы прибегали к арифметической модели предложенной также Гильбертом. Но здесь и обнаружилось несовершенство описанных методов доказательств.
Они не абсолютны, поскольку предполагали ссылки на другие системы, в конечном счете - на арифметику. Последняя же включает бесконечное число объектов натуральный ряд и не обозрима в конечное число шагов. Поэтому постулаты не могли быть интерпретированы. Так, для аксиомы о параллельных требовалась модель бесконечно продолженных параллельных. Невозможность получения такой модели означала отсутствие гарантий, что на каком-то этапе ее построения не встретимся с противоречием.
Предложенное Гильбертом доказательство не связано с интерпретацией допущением непротиворечивости другой системы и опирается лишь на наличное, заданное построение. Потому оно названо абсолютным прямым, непосредственным. В чем же его суть? Новый метод предполагал построение формализованной аксиоматики. До этого была известна модель содержательной аксиоматики, осуществленной Гильбертом же на основе построения геометрии Эвклидом.
При этом Гильберт внес существенные коррективы в систему Эвклида, для которой характерно следующее. 1. Отсутствие списка исходных объектов. 2. Наличие ссылок на интуицию и опыт, например, в понятиях лежать между, находиться внутри и т.п. 3. Отсутствие четко фиксированных правил вывода. Последние принимались сами собой разумеющимися, предшествующими математике и взятыми из логики аналогично тому, как используются логические правила в обыденных рассуждениях мы соблюдаем их, специально не договариваясь об этом. Приводя содержательную аксиоматику эвклидовой геометрии, Гильберт соответственно уточняет. 1. Приводит полный список исходных объектов и аксиом. 2. Объекты вводятся им без каких-либо ссылок на опыт. Он избегает попытки дать определения путем указания свойств.
Вернее, избегает давать обычные определения через родовидовые или генетические признаки и использует так называемы имплицитные скрытые, неявные определения - через аксиомы.
Это содержательная аксиоматика. Но теперь Гильберт идет дальше к аксиоматике формализованной, в которой в качестве исходных образований фигурируют абстрактные символы, а вместо содержательных предложений аксиом, теорем и т.п сочетания символов. В результате остаются лишь формулы. Формализация предполагает следующие шаги. 1 Задают полный перечень символов, которые используются в системе алфавит системы. Так водятся исходные объекты. Гильберт в связи с этим говорил следующее.
Будем мыслить три системы вещей. Вещи 1-ой называем точками и обозначаем A, B, C вещи 2-ой системы - прямыми a, b, c вещи 3-ей - плоскостями a, b , c. Далее, 2 вводятся правила образования из букв алфавита его формул предложения системы. Это формальная грамматика исчисления, то есть допустимые в системе знаковые сочетания предложения, формулы. Но их много. Потому из числа формул отбираем исходные 3 . Они образуют базис системы. Наконец, 4 устанавливаем правила преобразования формул правила вывода, чтобы из исходных получать все остальные.
Тогда исходные формулы суть аксиомы, а получаемые путем применения к ним правил - теоремы. Последние образуют тело системы. Таким образом, все составляющие математику предложения оказываются формулами. Налицо исчисление в совокупность исходных символов входят те и только те, на которые мы указали, аксиомы же и теоремы - просто строчки, последовательности лишенных значения знаков. А теперь перейдем к решающему пункту программы Д. Гильберта.
Имея такую формализованную систему, можем провести прямое не выходящее за рамки системы доказательство ее непротиворечивости. Это и есть абсолютное, без каких-либо ссылок на эмпирию, на интерпретационные модели, доказательство. Оно имеет алгоритм и цель. Алгоритм заключает три шага 1 предъявляется формула 2 что из предъявленной формулы следует другая правила заданы. И эта другая - следствие либо из аксиом, либо из ранее доказанных теорем 3 предъявляется другая формула. Это средства, а цель? Именно непротиворечивость.
Доказательство реализуется так манипулируя с принятыми символами по правилам системы, никогда не получим два логически противоречивых высказывания F и не-F .Например, утверждение 0 0 и его отрицание. Иными словами, неравенство 0 0 в системе не должно быть доказуемо. Свои методы Гильберт назвал финитными они не используют ни бесконечных множеств структурных свойств формул, ни бесконечных множеств операций над формулами. Так было получено понятие доказательства абсолютной непротиворечивости формальных систем, а вместе с ним, как полагал Гильберт и доказательство непротиворечивости математики.
Иначе говоря, казалось, что получено обоснование последней С помощью теории доказательства ?я хотел бы, v писал Гильберт, v окончательно разделаться с вопросами обоснования математики как таковыми- Гильберт Д. Основания геометрии. М Л. ОГИЗ, 1948. С. 365 Вывод, к которому приходит формалистское направление, состоит в том, что обоснование математики в ней самой.
Вскоре однако произошло событие, имевшее столь же радикальные последствия, как в свое время обнаружение парадоксов Рассела. 6.2