§ 5. Исследования, направленные на непосредственное финитное построение анализа; возврат к прежней постановке проблемы; теория доказательств

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

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

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

В течение длительного времени план действий, намеченный Кронекером, отвергался полностью, и лишь в последнее время Брауэр принялся за задачу независимого от закона исключенного третьего построения анализа и развил в рамках этой программы значительные разделы анализа и теории множеств. Разумеется, при этом подходе пришлось поступиться существенными результатами и получить в придачу значительные осложнения в способах образования понятий.

Методическая установка «интуиционизма», которую берет за основу Брауэр, в известном смысле представляет собой расширение финитной установки, поскольку Брауэр допускает, чтобы справедливость какого-либо вывода или доказательства принималась без учета его наглядности. Так, например, с точки зрения Брауэра допустимыми являются теоремы вида «если в предположении имеет место то имеет место также и а также вида «предположение, что опровержимо, ведет к противоречию» пли, по выражению Брауэра, «абсурдность абсурдна».

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

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

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

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

Однако эта проблема представляет собой не что иное, как проблему установления непротиворечивости нашего традиционного анализа.

В гл. I для обсуждения этой проблемы мы предполагали привлечь уже разработанный в символической логике метод формализации логического вывода Этот метод во всяком случае

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

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

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