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