Важность столь настоятельно подчеркиваемого нами различения математики и метаматематики трудно переоценить. Игнорирование или недооценка этого различения приводят к недоразумениям, а то и к прямым противоречиям. Осознание его важности позволило глубже уяснить логическую структуру математических методов рассуждения и четко регламентировать употребление различных формальных символов, превращая математику в чисто формальное исчисление, свободное от всяческих неявно подразумеваемых допущений и побочных смысловых ассоциаций. Только на базе таких новых представлений стало возможным дать точные определения математических операций и логических правил, которыми математики пользовались до тех пор без ясного понимания того, что же, собственно, они делают.
Гильберт уловил самую суть проблемы, положив в основу своих попыток построения «абсолютных» доказательств непротиворечивости различие между формальным исчислением и его описанием. Он поставил задачу развития специального метода, с помощью которого можно было бы проводить доказательства непротиворечивости той же степени убедительности, что и доказательства, использующие конечные модели, на которых реализуются определенные системы постулатов. Искомый метод должен был бы состоять в исчерпывающем анализе конечного числа структурных свойств выражений в полностью формализованных исчислениях. Анализ должен исходить из точной фиксации различных видов, входящих в рассматриваемое исчисление символов, указания на способы соединения этих символов в формулы, описания способа вывода одних формул из других и давать способ решения вопроса, выводимы ли формулы какого-либо определенного вида из некоторых определенных формул посредством явно сформулированных правил оперирования с формулами. Гильберт был убежден в том, что каждое математическое исчисление можно представить «на геометрический манер», т. е. в виде такой совокупности формул, каждая из которых связана с любой другой формулой того же исчисления лишь структурными соотношениями из некоторого конечного перечня соотношений.
На этом убеждении и основывался его расчет, что он сумеет посредством систематического и исчерпывающего обозрения этих структурных свойств выражений данной системы показать, что из аксиом данного исчисления нельзя получить формально противоречащие друг другу формулы. Существеннейшим условием гильбертовской программы в первоначальной ее формулировке было разрешение употреблять в доказательствах непротиворечивости лишь такие приемы рассуждений, которые ни в какой форме не используют ни бесконечного множества структурных свойств формул, ни бесконечного множества операций над формулами.
Такие методы рассуждений он назвал «финитными», а доказательства непротиворечивости, проведенные финитными средствами, — «абсолютными». «Абсолютное» доказательство достигает своей цели с помощью некоторого минимального арсенала принципов вывода и не исходит из непротиворечивости никакой другой системы аксиом. Таким образом, если бы, например, удалось получить абсолютное доказательство непротиворечивости арифметики, оно должно было бы посредством некоторой финитной метаматематической процедуры установить невозможность одновременного вывода из аксиом (т. е. из исходных формул) арифметики с помощью фиксированных правил вывода никакой пары взаимно противоречивых формул, скажем «0 = 0» и ее отрицания «~ (0 = 0)» (здесь знак «~» означает «не»).
>Вполне точных указаний на то, какие именно математические методы следует считать «финитными», Гильберт не дал. В первоначальной формулировке его программы требования, которым должны были удовлетворять абсолютные доказательства непротиворечивости, были значительно более сильными, чем в последующих разъяснениях гильбертовской программы, данных представителям школы Гильберта.
Будет, пожалуй, небесполезно сравнить метаматематику, понимаемую как теорию доказательства, с теорией шахматной игры. В шахматы играют с помощью 32 фигур определенного вида, передвигающихся по квадратной доске, разделенной на 64 клетки, причем передвижения эти («ходы») совершаются по некоторым строго определенным правилам. Разумеется, для игры не требуется никакой «интерпретации» фигур и их различных положений на доске, хотя такую интерпретацию при желании можно было бы и придумать. Например, можно было бы считать, что пешки — это армейские полки, а клетки доски — определенные географические районы и т. п. Но такого рода соглашения (интерпретации) не употребительны — на самом деле ни фигуры, ни клетки доски, ни положения фигур не означают ровно ничего
