Читать «Teopeмa Гёделя» онлайн - страница 14

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

Гильберт уловил самую суть проблемы, положив в основу своих попыток построения «абсолютных» доказательств непротиворечивости различие между формальным исчислением и его описанием. Он поставил задачу развития специального метода, с помощью которого можно было бы проводить доказательства непротиворечивости той же степени убедительности, что и доказательства, использующие конечные модели, на которых реализуются определенные системы постулатов. Искомый метод должен был бы состоять в исчерпывающем анализе конечного числа структурных свойств выражений в полностью формализованных исчислениях. Анализ должен исходить из точной фиксации различных видов, входящих в рассматриваемое исчисление символов, указания на способы соединения этих символов в формулы, описания способа вывода одних формул из других и давать способ решения вопроса, выводимы ли формулы какого-либо определенного вида из некоторых определенных формул посредством явно сформулированных правил оперирования с формулами. Гильберт был убежден в том, что каждое математическое исчисление можно представить «на геометрический манер», т. е. в виде такой совокупности формул, каждая из которых связана с любой другой формулой того же исчисления лишь структурными соотношениями из некоторого конечного перечня соотношений.

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

Такие методы рассуждений он назвал «финитными», а доказательства непротиворечивости, проведенные финитными средствами, — «абсолютными». «Абсолютное» доказательство достигает своей цели с помощью некоторого минимального арсенала принципов вывода и не исходит из непротиворечивости никакой другой системы аксиом. Таким образом, если бы, например, удалось получить абсолютное доказательство непротиворечивости арифметики, оно должно было бы посредством некоторой финитной метаматематической процедуры установить невозможность одновременного вывода из аксиом (т. е. из исходных формул) арифметики с помощью фиксированных правил вывода никакой пары взаимно противоречивых формул, скажем «0 = 0» и ее отрицания «~ (0 = 0)» (здесь знак «~» означает «не»).