Для строгого формалиста вопрос о том, является ли то или иное утверждение о бесконечных множествах действительно истиннымв сколько угодно абсолютном смысле, не обязательно имеет смысл и, уж конечно же, не имеет никакого существенного отношения к процедурам формалистской математики. Таким образом, поиски абсолютной математической истины в отношении утверждений, связанных с упомянутыми бесконечными величинами, заменяются стремлением продемонстрировать непротиворечивость и полноту соответствующих формальных систем. Какие же математические правила допустимо использовать для такой демонстрации? Достойные доверия, прежде всего, причем формулировка этих правил ни в коем случае не должна основываться на сомнительных рассуждениях с привлечением слишком вольно определяемых бесконечных множеств (типа множества Рассела). Была надежда на то, что в рамках некоторых сравнительно простых и очевидно обоснованных формальных систем (например, такой достаточно элементарной системы, как  арифметика Пеано) отыщутся логические процедуры, которых будет достаточно для того, чтобы доказать непротиворечивость других, более сложных, формальных систем — скажем, системы F, — непротиворечивость которых уже не столь бесспорна и в рамках которых допускаются формальные рассуждения об очень «больших» бесконечных множествах. Если принять философию формалистов, то подобное доказательство непротиворечивости для F, как минимум, даст основание для использования методов рассуждения, допустимых в рамках системы F. Затем можно доказывать математические теоремы, применяя концепцию бесконечных множеств тем или иным непротиворечивым образом, а может, удастся и вовсе избавиться от необходимости отвечать на вопрос о реальном «смысле» таких множеств. Более того, если удастся показать, что система Fявляется еще и полной, то можно будет вполне резонно счесть, что эта система действительно содержит абсолютно вседопустимые математические процедуры, т.е. представляет собой, в некотором смысле, полноеописание математического аппарата рассматриваемой области.

Однако в 1930 году (публикация состоялась в 1931) Гёдель взорвал свою «бомбу», раз и навсегда показав, что идеал формалистов принципиально недостижим. Он продемонстрировал, что не может существовать формальной системы F, которая была бы одновременно и непротиворечивой (в некоем «сильном» смысле, который мы рассмотрим в следующем разделе), и полной, — при условии, что Fсчитается достаточно мощной, чтобы сочетать в себе формулировки утверждений обычной арифметики и стандартную логику. Таким образом, теорема Гёделя справедлива для таких систем F, в рамках которых арифметические утверждения типа теоремы Лагранжа и гипотезы Гольдбаха (см. §2.3) формулируются как утверждения математические.

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

2.8. Условие ω-непротиворечивости

Наиболее известная форма теоремы Гёделя гласит, что формальная система F (достаточно обширная) не может быть одновременно полной и непротиворечивой. Это не совсем та знаменитая «теорема о неполноте», которую Гёдель первоначально представил на конференции в Кенигсберге (см. §§2.1и 2.7), а ее несколько более сильный вариант, который был позднее получен американским логиком Дж. Баркли Россером (1936). По своей сути, первоначальный вариант теоремы Гёделя оказывается эквивалентен утверждению, что система Fне может быть одновременно полной и ω- непротиворечивой. Условие же ω-непротиворечивости несколько строже, нежели условие непротиворечивости обыкновенной. Для объяснения его смысла нам потребуется ввести некоторые новые обозначения. В систему обозначений формальной системы Fнеобходимо включить символы некоторых логических операций. Нам, в частности, потребуется символ, выражающий отрицание(«не»); можно выбрать для этого символ «~». Таким образом, если Qесть некое высказывание, формулируемое в рамках F, то последовательность символов ~ Qозначает «не Q». Нужен также символ, означающий «для всех [натуральных чисел]» и называемый квантор общности; он имеет вид «∀». Если P( n) есть некое высказывание, зависящее от натурального числа  n(т.е.  Pпредставляет собой так называемую пропозициональную функцию), то строка символов ∀ n[ P( n)] означает «для всех натуральных чисел n высказывание P( n) справедливо». Например, если высказывание P( n) имеет вид «число  nможно выразить в виде суммы квадратов трех чисел», то запись ∀ n[ P( n)] означает «любое натуральное число является суммой квадратов трех чисел», — что, вообще говоря, ложно (хотя, если мы заменим «трех» на «четырех», то это же утверждение станет истинным). Такие символы можно записывать в самых различных сочетаниях; в частности, строка символов

выражает отрицание того, что высказывание P( n) справедливо для всех натуральных чисел n.

Условие же ω-непротиворечивости гласит, что если высказывание ~ ∀ n[ P( n)] можно доказать с помощью методов формальной системы F, то это еще неозначает, что в рамках этой самой системы непременно доказуемы всеутверждения

Отсюда следует, что если формальная система Fне является ω-непротиворечивой, мы оказываемся в аномальной ситуации, когда для некоторого  Pоказывается доказуемой истинность всех высказываний P(0), P(1), P(2), P(3), P(4), …; и  одновременнос этим можно доказать и то, что невсе эти высказывания истинны! Безусловно, ни одна заслуживающая доверия формальная система подобного безобразия допустить не может. Поэтому если система Fявляется обоснованной, то она непременно будет и ω-непротиворечивой.

В дальнейшем утверждения «формальная система F является непротиворечивой» и «формальная система Fявляется ω-непротиворечивой» я буду обозначать, соответственно, символами « G( F)» и «Ω( F)». В сущности (если полагать систему F достаточно обширной), сами утверждения G( F) и Ω( F) формулируются как операции этой системы. Согласно знаменитой теореме Гёделя о неполноте, утверждение Ω( F) не является теоремойсистемы F(т.е. его нельзя доказать с помощью процедур, допустимых в рамках системы F); не является теоремой и утверждение Ω( F) — если, разумеется, система F действительно непротиворечива. Несколько более строгий вариант теоремы Гёделя, сформулированный позднее Россером, гласит, что если система Fнепротиворечива, то утверждение ~ G( F) также не является теоремой этой системы. В оставшейся части этой главы я буду формулировать свои доводы не столько исходя из утверждения Ω( F), сколько на основе более привычного нам G( F), хотя для большей части наших рассуждений в равной степени сгодится любое из них. (В некоторых наиболее явных аргументах главы 3я буду иногда обозначать через « G( F)» конкретное утверждение «вычисление C _k( k) не завершается» (см. §2.5); надеюсь, никто не сочтет это слишком большой вольностью с моей стороны.)