Teopeмa Гёделя

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

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

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

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

Приведем несколько примеров, иллюстрирующих различие между математикой и метаматематикой. Скажем, выражение «2+3=5» принадлежит математике (арифметике) и строится исходя лишь из элементарных арифметических символов, в то время как высказывание «„2+3=5“ есть арифметическая формула» утверждает нечто об этом выражении. Оно само по себе не выражает никакого арифметического факта и не принадлежит формальному языку арифметики, а относится к метаматематике, характеризуя некоторую строчку, составленную из арифметических символов, как формулу.

Формулы

x = x,

0 = 0,

0 /= 0