В серии работ, выполненных в период 1920-1930 гг., Гильберт и его ученики Вильгельм Аккерман (1896-1962), Пауль Бернайс (1888-1978) и Джон фон Нейман (1903-1957), постепенно создали метод, получивший название гильбертовской Beweistheorie [теории доказательства] или метаматематики, — метод доказательства непротиворечивости любой формальной системы (ср. [73], [74]). Суть основной идеи метаматематики можно пояснить с помощью следующей аналогии. Допустим, вы захотели бы изучить выразительные возможности японского языка и решили бы проводить этот анализ на японском языке — тогда ваши результаты оказались бы в значительной мере ограничены возможностями самого японского языка. Но если считать, что английский язык выразителен, то при изучении возможностей японского языка целесообразно было бы воспользоваться английским.
В метаматематике Гильберт предложил использовать особую логику, которая не вызывала бы никаких возражений. Истинность ее законов должна быть настолько очевидной, что всякий мог бы принять их без тени сомнения. По существу эти идеи Гильберта были весьма близки принципам интуиционизма. Все спорные моменты — доказательство существования от противного, трансфинитная индукция, актуально бесконечные множества, непредикативные определения — старательно изгонялись. Доказательства существования должны были быть конструктивными. Поскольку формальная система может продолжаться неограниченно, метаматематика не могла обойти вниманием понятия и проблемы, по крайней мере относящиеся к потенциально бесконечным системам. Но ссылки на бесконечное число структурных свойств формулы или использование бесконечного числа производимых над формулами операций объявлялись недопустимыми. Рассматривать формулы, в которые входят символы, означающие актуально бесконечные множества, не запрещалось, но сами множества могли входить лишь как символы в формулах. Математическая индукция по натуральным (положительным целым) числам считалась допустимой, поскольку она доказывает утверждение для любого конечного n; однако не следовало понимать этот метод так, будто он позволяет доказывать утверждение сразу для всего бесконечного множества натуральных чисел.
Понятия и методы метаматематического доказательства Гильберт назвал финитными. Строгого определения этого термина дано не было. В работе 1925 г. смысл финитности Гильберт пояснил на следующем примере. Высказывание «Если p — простое число, то существует простое число, которое больше p» не финитно, так как представляет собой утверждение о всех целых числах, которые больше p. Высказывание же «Если p — простое число, то существует простое число, которое больше p и меньше p! + 1 (p — факториал плюс единица)» финитно, так как при любом простом p нам необходимо лишь убедиться, существует ли простое число среди конечного{130} множества чисел, заключенных между p и p! + 1.
В книге, написанной вместе с Бернайсом и опубликованной в 1934 г., Гильберт описывает финитность следующим образом:
…Мы будем говорить о финитных понятиях и утверждениях, подчеркивая всюду словом «финитный», что рассматриваемое рассуждение, утверждение или определение придерживаются рамок принципиальной представимости объектов и принципиальной выполнимости операций, а тем самым происходят в рамках конкретного рассмотрения.
([75], т. I, с. 59.)
В тех случаях, когда это не могло привести к недоразумениям, формалисты использовали язык и некоторые обозначения интуитивной, или неформальной, математики.
Выступая с докладом о своей метаматематической программе на Международном математическом конгрессе 1928 г., Гильберт с уверенностью заявил: «Не сомневаюсь, что наш новый подход к основаниям математики, который можно было бы назвать теорией доказательства, позволит навсегда покончить со всеми проблемами обоснования математики». В частности, Гильберт выражал надежду на то, что ему удастся доказать непротиворечивость математики и решить проблему полноты. Иначе говоря, все высказывания, имеющие смысл, будут либо доказаны, либо опровергнуты. Не останется ни одного неразрешимого утверждения.
Как и следовало ожидать, формалистская программа вызвала критику со стороны представителей соперничающих направлений. Во втором издании «Принципов математики» (1937) Рассел заметил, что используемые формалистами аксиомы арифметики не задают однозначно значения символов 0, 1, 2, …, с тем же успехом счет можно было бы начать и с того, что мы интуитивно понимаем под числами 100, 101, 102, …. Поэтому утверждение «Апостолов было 12» с точки зрения формализма лишено смысла. «Формалисты напоминают часовщика, который настолько озабочен тем, как выглядят выпускаемые им часы, что забыл об их прямом назначении — измерять время — и не вставил в корпус механизм». Логицистское определение числа вкладывает смысл в связь этого понятия с реальным миром; формалистская теория лишает такую связь всякого смысла.
Рассел подверг критике и формалистское понятие существования. Гильберт считал приемлемыми бесконечные множества и другие идеальные элементы и утверждал, что если аксиомы какой-либо области математики, включающие закон исключенного третьего и закон противоречия, не приводят к противоречию, то тем самым гарантируется существование объектов; удовлетворяющих этим аксиомам. Такую трактовку существования Рассел назвал метафизической. Кроме того, он обратил внимание на то, что число непротиворечивых аксиоматических систем, которые можно придумать, неограниченно, но интерес представляют лишь такие системы, которые согласуются с эмпирическим материалом.
Критика Рассела напоминает поговорку «Не смейся, горох, ты не лучше бобов». Должно быть, к 1937 г. он успел основательно подзабыть то, что писал сам в 1901 г.: «Математику можно определить как предмет, в котором никогда не известно ни то, о чем мы говорим, ни истинно или ложно то, что мы говорим».
Формалистская программа была неприемлема и для интуиционистов. Помимо основных различий во взглядах на бесконечность и закон исключенного третьего интуиционисты неоднократно подчеркивали, что они полагаются на смысл математики и стремятся установить, насколько его можно считать здравым, в то время как формалисты (и логицисты) имеют дело с идеальными, или трансцендентальными, мирами, лишенными всякого смысла. Брауэр еще в 1908 г. показал, что в некоторых утверждениях классического математического анализа, в том числе в теореме Больцано — Вейершрасса (носящей сугубо специальный характер и утверждающей, что у любого ограниченного бесконечного множества существует по крайней мере одна предельная точка), логика и здравый смысл находятся в вопиющем противоречии. Мы должны выбирать, заявил Брауэр, между нашим априорным понятием положительного целого числа и неограниченным использованием закона исключенного третьего в тех случаях, когда последний применяется к любому утверждению, не поддающемуся проверке за конечное число шагов. Некритическое использование аристотелевой логики привело к появлению формально правильных, но бессмысленных утверждений. Порывая со смыслом во многих логических построениях, классическая математика тем самым порывала с реальностью.
Критика Брауэра заставила многих осознать неправильность казавшегося ранее бесспорным мнения о том, что великие математические теории правильно отражают некое заложенное в них реальное содержание. Разумеется, создатели математических теорий мыслили их как идеализации реальных вещей и явлений. Но впоследствии, особенно в XIX в., многие понятия математического анализа утратили какую бы то ни было интуитивную подоплеку, и в глазах интуиционистов они не выглядели логически удовлетворительными. Принять взгляды Бауэра означало отвергнуть значительную часть классической математики на том основании, что она лишена интуитивного смысла.
Современные интуиционисты заявляют, что формализованная математика бессодержательна, даже если бы Гильберту и удалось доказать ее непротиворечивость. Вейль сетовал на то, что Гильберт «спас» классическую математику «ценой коренного пересмотра ее содержания», формализовав и выхолостив ее и «тем самым в принципе превратив из системы с интуитивно воспринимаемыми результатами в игру с формулами по определенным, раз и навсегда установленным правилам… Вполне возможно, что математика Гильберта представляет собой великолепную игру с формулами, более увлекательную, чем шахматы. Но что, спрашивается, дает такая игра нашему разуму, если ее формулы умышленно лишены материального содержания, посредством которого они могли бы выражать интуитивные истины?» В защиту формалистской философии следует заметить, что Гильберт свел математику к бессодержательным формулам только во имя высокой цели: доказательства непротиворечивости, полноты и других не менее важных свойств. Что же касается математики в целом, то даже формалисты никогда не считали ее «просто игрой», а рассматривали как вполне содержательную научную дисциплину.
