Эрнст Нагель - Teopeма Гёделя

Точно так же неверно было бы написать:

« x = 5 есть уравнение».

Правильная запись такова:

«„ x = 5" есть уравнение».

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

Точно таково же соотношение между математикой и метаматематикой: предмет первой составляют сами формальные системы, которые придумывают математики, предмет второй — описание таких формальных систем, выяснение и обсуждение их свойств.

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

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

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

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