Цель Гильберта понятна из его переписки, в которой он, например, объясняет, что геометрия не изменится, если вместо терминов «точка», «прямая» и «плоскость» мы напишем «любовь», «закон» и «трубочист». Как следствие, для формалиста выражения «глава третья» и «глава 3» — это два разных высказывания, единственная связь между которыми заключается в особенностях синтаксиса: оба выражения начинаются с одного и того же слова.
Основу гильбертовой формальной системы составляло множество базовых символов L, основанных на алфавите нашего языка. На их основе можно создать формулы, которые будут представлять собой не что иное, как конечные последовательности символов, составленные согласно ряду грамматических правил. Если, например, язык содержит открывающую и закрывающую скобки, то одно из его правил может звучать так: справа от каждой открывающей скобки обязательно должна быть записана закрывающая скобка.
Чтобы определить формальную систему, помимо алфавита, необходимы аксиомы и правила вывода. Аксиомы отличаются от всех остальных формул только тем, что занимают привилегированное положение. Как мы указывали в главе 1, выбор аксиом — одна из сложнейших задач при определении формальной системы: если мы выберем слишком много аксиом, то они могут смешаться с остальными формулами, а если мы выберем слишком мало аксиом, то некоторые формулы нельзя будет ни доказать, ни опровергнуть. Правила вывода, в свою очередь, это процедуры, позволяющие получить новые формулы на основе уже известных. Аксиомы и правила вывода объединяются в формальные доказательства — последовательности формул, каждая из которых является либо аксиомой, либо получена из предыдущих формул с помощью правил вывода. Традиционно последняя формула доказательства называется теоремой.
Следовательно, первое требование программы Гильберта заключалось в том, чтобы описать алфавит, определить аксиомы и формальные правила вывода для арифметики. Этой задаче Бертран Рассел и Альфред Норт Уайтхед посвятили три объемных тома «Начал математики», опубликованных в 1910–1913 годах. В действительности теория, предложенная Расселом и Уайтхедом и названная вскоре логицизмом, выходила далеко за рамки формалистской программы: оба ее автора не ограничивались формализацией арифметики и хотели свести ее к логике, то есть определить все понятия теории натуральных чисел исходя из чисто логических обозначений, а также вывести из этих понятий все теоремы арифметики. Одним из величайших успехов математики XIX века было построение любого класса чисел на основе натуральных, таким образом, если бы Рассел и Уайтхед достигли своей цели, математика и логика пошли бы рука об руку по дороге, свободной от противоречий (по крайней мере, основоположники логицизма на это надеялись).
* * *
НЕПРИБЫЛЬНАЯ МАТЕМАТИКА
Ключевой труд Рассела и Уайтхеда был опубликован издательством Cambridge University Press. Издательство смогло выделить на публикацию всего 300 фунтов, что составляло половину необходимой суммы. Недостающие 300 фунтов обязалось внести Лондонское королевское общество, членом которого был Рассел, однако в итоге было внесено лишь 200, а остаток Расселу и Уайтхеду пришлось заплатить из своего кармана. «Неплохой баланс, — шутил Рассел впоследствии, — за десять лет работы мы заработали минус пятьдесят фунтов на каждого».
* * *
В упрощенной версии формальная система арифметики, предложенная Расселом и Уайтхедом в «Началах математики», состояла из следующих основных символов: 0 (число ноль), s (функция следования), ¬ (отрицание), V (дизъюнкция «или»), 
(существование), = (равенство) и открывающая и закрывающая скобки. Позднее к этим символам были добавлены переменные х, у, z типа 0, которые обозначали натуральные числа, а также переменные А, В, С типа 1, то есть множества натуральных чисел, и т. д. по мере того, как требовались элементы все новых и новых типов. Возможно, внимательный читатель заметил отсутствие других символов, которые должны быть частью языка: например, наряду с квантором существования, благодаря которому можно формализовать высказывания вида «существует натуральное число, обладающее свойством Р», можно было бы добавить еще один символ, который означал бы «для всех», как в высказывании «для всех натуральных чисел выполняется утверждение Р». По сути, этот универсальный квантор очень широко используется в математике: «для всех» обозначается символом