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

Наиболее известная форма теоремы Гёделя гласит, что формальная система 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 ); надеюсь, никто не сочтет это слишком большой вольностью с моей стороны.)

В большей части предлагаемых рассуждений я не стану проводить четкую границу между непротиворечивостью и -непротиворечивостью, однако тот вариант теоремы Гёделя, что представлен в §2.5 , по сути, гласит, что если формальная система Fнепротиворечива, то она не может быть полной, так как не может включать в себя в качестве теоремы утверждение G( F). Здесь я всего этого демонстрировать не буду (интересующиеся же могут обратиться к [ 223 ]). Вообще говоря, для того чтобы эту форму гёделевского доказательства можно было свести к доказательству в моей формулировке, система Fдолжна содержать в себе нечто большее, нежели просто «арифметику и обыкновенную логику». Необходимо, чтобы система Fбыла обширной настолько, чтобы включать в себя действия любой машины Тьюринга. Иначе говоря, среди утверждений, корректно формулируемых с помощью символов системы F, должны присутствовать утверждения типа: «Такая-то машина Тьюринга, оперируя над натуральным числом n, дает на выходе натуральное число p». Более того, имеется теорема (см. [ 223 ], главы 11 и 13), согласно которой так оно само собой и получается, если, помимо обычных арифметических операций, система Fсодержит следующую операцию (так называемую -операцию, или операцию минимизации): «найти наименьшее натуральное число, обладающее таким-то арифметическим свойством». Вспомним, что в нашем первом вычислительном примере, (A), предложенная процедура действительно позволяла отыскать наименьшеечисло, не являющееся суммой трех квадратов. То есть, вообще говоря, право на подобные вещи за вычислительными процедурами следует сохранить. С другой стороны, именно благодаря этойих особенности мы и сталкиваемся с вычислениями, которые принципиально не завершаются, — например, вычисление (В), где мы пытаемся отыскать наименьшее число, не являющееся суммой четырехквадратов, а такого числа в природе не существует.

В предложенной мною формулировке доказательства Гёделя—Тьюринга (см. §2.5 ) говорится только о «вычислениях» и ни словом не упоминается о «формальных системах». Тем не менее, между этими двумя концепциями существует очень тесная связь. Одним из существенных свойств формальной системы является непременная необходимость существования алгоритмической (т.е. «вычислительной») процедуры F, предназначенной для проверкиправильности применения правил этой системы. Если, в соответствии с правилами системы F, некое высказывание является ИСТИННЫМ, то вычисление Fэтот факт установит. (Для достижения этого результата вычисление F, возможно, «просмотрит» все возможные последовательности строк символов, принадлежащих «алфавиту» системы F, и успешно завершится, обнаружив заключительной строкой искомое высказывание P; при этом любые сочетания строк символов являются, согласно правилам системы F, допустимыми.)

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