6. ВОКРУГ ТЕОРЕМЫ ГЕДЕЛЯ

6.1. Методологическое значение теорем о неполноте

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

Возьмем любую формальную теорию T, которая содержит полноценное понятие натурального числа (т.е. фундаментальную теорию, по нашей терминологии). Формула Геделя G_T, построенная для теории T, утверждает: "Я недоказуема в T". И К.Гедель показал, что она действительно недоказуема в T. Таким образом, К.Гедель умел доказывать истинность формулы G_T (которая - как формула из языка EA - является также утверждением о свойствах натуральных чисел). Это значит, что какую бы формальную теорию T мы ни взяли, К.Гедель с помощью своего "творческого мышления" докажет нам истинность некоторого утверждения G_T о свойствах натуральных чисел, которое нельзя доказать в теории T. Таким образом, никакая формальная теория не в состоянии отразить в себе "живое, человеческое" понятие о ряде натуральных чисел (не говоря уже об остальных "богатствах содержательной математики"). Как только формальная теория T зафиксирована, "творческий разум" безошибочно находит истину G_T, выводящую за пределы этой теории.

То, что мы узнали о теореме Геделя в предыдущих разделах, должно заставить нас кое-что в этом рассуждении пересмотреть. К.Гедель смог доказать, что формула G_T недоказуема в теории T, только предположив, что эта теория непротиворечива. Т.е. он выводил истинность G из предположения непротиворечивости T. Иначе и быть не могло: если доказана истинность G_T, то тем самым доказана непротиворечивость теории T (истинность G_T означает, что эта формула недоказуема в T, недоказуемость же в T хотя бы одной формулы означает непротиворечивость T). Таким образом, не зная ничего о противоречивости или непротиворечивости теории T, мы не можем ничего сказать и об истинности или ложности формулы G . Как же могут относиться к вопросу о непротиворечивости те, кто считает G_T безошибочно найденной истиной, недоказуемой в T?

Во-первых, они не могут полагать, что всякая формальная теория непротиворечива. Искусственный пример противоречивой теории получить легко: добавим к теории EA аксиому 0=1. Так как в EA доказуема формула ~(0=1), то полученная теория противоречива. Однако с такого рода искусственными примерами мало кто станет считаться. Более серъезно необходимо относиться к следующему факту: не существует алгоритма, который по системе аксиом и правил вывода определял бы, противоречива ли соответствующая формальная теория.

Упражнение 6.1. Предполагая, что теория EA непротиворечива, покажите (ср. раздел 6.3), что невозможен алгоритм, определяющий по замкнутой формуле F, противоречива теория EA+F или нет. (Теория EA+F получена присоединением к EA формулы F в качестве аксиомы.)

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

Наконец, следует упомянуть о теориях, которые в свое время их создатели считали непротиворечивыми, но которые позднее оказались все же противоречивыми. Такая судьба постигла первую в истории формальную систему математики, разработанную еще в прошлом веке Г.Фреге. В 1902 г., когда второй, завершающий том книги с изложением системы Г.Фреге находился уже в печати, Б.Рассел обнаружил, что эта система содержит противоречие. Г.Фреге прожил до 1925 г., но серьезных работ больше не опубликовал - такой страшный удар нанес парадокс Рассела по абсолютной уверенности автора в безупречности исходных посылок его системы. (Следует, однако, заметить, что Г.Фреге зря принял этот удар как лично его касающийся. Знакомство с принципами его системы производит на всякого непредубежденного человека, не знающего о парадоксе Рассела, такое же впечатление абсолютной надежности, как на самого Г.Фреге. В этом смысле Г.Фреге принял на себя удар, "причитающийся" всему предшествующему математическому образу мышления.)

Несколькими годами раньше такая же судьба постигла другое великолепное творение математики XIX в. - теорию множеств Г.Кантора. Так же как система Г.Фреге, теория Г.Кантора производит при знакомстве с ее основами впечатление абсолютной надежности и фундаментальности. Кажется, тут не может быть места сомнениям. Принципы математического мышления доведены у Г.Кантора до логического конца - понятия произвольного бесконечного множества. И тем не менее в 1895 г. Г.Кантор сам обнаруживает, что из его принципов можно вывести противоречие...

Со времен Г.Фреге и Г.Кантора формальные теории математики значительно усовершенствованы. Противоречия в них пока не найдены. Тем не менее горький опыт этих великих мыслителей должен был научить нас по крайней мере одному: никакая наша "внутренняя уверенность" в надежности исходных посылок теории (сколько бы людей ни разделяли эту уверенность) не может быть абсолютной гарантией от противоречий.

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

Пожалуй, наиболее ярко нелепость критикуемой точки зрения проявляется в следующем "силлогизме":

а) Чтобы "превзойти через Геделя" формальную теорию T, нужно доказать истинность формулы G_T.

б) Чтобы доказать истинность G_T, нужно доказать непротиворечивость теории T.

в) Чтобы доказать непротиворечивость T, нужно применить средства, выходящие за пределы этой теории (вторая теорема Геделя).

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

Будучи не в состоянии доказать непротиворечивость какой- либо теории, но будучи уверенными, что "на самом деле" так оно и есть, мы можем попытаться принять утверждение о непротиворечивости в качестве новой аксиомы. И изучить следствия, вытекающие отсюда. Такой подход не является чем-то необычным для математики (в теории чисел изучаются следствия гипотезы Римана, в теории множеств - следствия континуум-гипотезы Кантора и т.п.). Заметим, однако, что здесь все время говорится о гипотезах. Такой же гипотезой следует считать и утверждение о непротиворечивости теории, в надежности которой мы уверены. Нужно всегда помнить об этом: принятие гипотезы в качестве аксиомы - это постулирование, т.е. принятие без достаточных на то оснований. В ходе изучения следствий из гипотезы могут быть обнаружены противоречия, и тогда гипотезу придется отвергнуть.

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

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

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

Всякая формальная теория с методологической точки зрения является моделью некоторой застывшей системы мышления. С учетом этого основной вывод из теорем о неполноте можно переформулировать так: всякая достаточно всеобъемлющая (фундаментальная?), но застывшая система мышления неизбежно оказывается несовершенной - в ней содержатся либо противоречия, либо проблемы, для решения которых данной (застывшей!) системы недостаточно. Именно в строгом доказательстве принципиального несовершенства всякой застывшей системы мышления состоит подлинный диалектический смысл достижений Геделя. (Однако отсюда не следует, что незастывшая система мышления может существовать в качестве математической теории.)

Замечание. Иногда теории определяются как произвольные множества формул, называемых теоремами. Такая точка зрения очень абстрактна. Сущность теории не исчерпывается множеством ее теорем. Теория - это достаточно определенная система мышления (а формальная теория - модель абсолютно определенной, т.е. застывшей, системы мышления), а не только совокупность результатов (теорем), которые можно получить с помощью средств данной системы, она включает и сами эти средства. Волновая механика Э.Шредингера и матричная механика В.Гейзенберга - различные теории, хотя доказано, что по своим результатам они совпадают. С упомянутой абстрактной точки зрения (сводящей теорию к множеству ее теорем), противоречивая теория кажется "пустой" (в ней доказуемы все формулы без разбора, т.е. такая теория как будто не делает различия между истиной и ложью). Однако, если, совершенствуя аксиомы теории, противоречия (обнаруженного типа) удается исключить, то неужели при этом совершенствуется "пустота"? Если смотреть на теорию конкретно - как на систему мышления, противоречия представляются уже не как "пустота", а как несовершенство аксиом теории. Несовершенные аксиомы должны совершенствоваться.

6.2. Теорема о двойной неполноте

Неразрешимость формулы Б.Россера R_T, построенной для теории T, можно было доказать, предположив только непротиворечивость T. В остальном рассуждения Б.Россера проходят в рамках теории EA. Это значит, что доказательство неразрешимости формулы R_T можно формализовать в теории EA+Con(T) (т.е. в теории, полученной присоединением к EA гипотезы о непротиворечивости T). Теорию, с помощью которой изучаются свойства другой теории, принято называть метатеорией. Итак, неразрешимость R_T можно доказать в метатеории EA+Con(T). Вероятно, в этой метатеории можно доказать неразрешимость (средствами теории T) и многих других формул. Не может ли оказаться, однако, что неразрешимость некоторых формул недоказуема в EA+Con(T) (т.е. для установления их неразрешимости недостаточно предположить только непротиворечивость теории T)?

Ответ на этот вопрос можно получить путем моделирования парадокса Усиленный Лжец (см. раздел 5.1):

q: q ложно или q неразрешимо.

Все три возможные альтернативы (q истинно, q ложно, q неразрешимо) приводят к противоречию. Если теория T обсуждается в метатеории M, мы можем попытаться получить формулу H, которая утверждала бы: "H опровержима в T или в M доказуема T-неразрешимость H". Это действительно можно сделать, в результате получается первый ("геделевский") вариант теоремы о двойной неполноте: если теории T, M w-непротиворечивы, то формула H неразрешима в теории T, однако этот факт нельзя доказать в метатеории M (см. К.М.Подниекс [1975]). Отсюда и название - "теорема о двойной неполноте".

Ниже мы докажем сразу усиленный ("россеровский") вариант этой теоремы (К.М.Подниекс [1976]). Сначала уточним смысл отношения "M - метатеория для T". Пусть T, M - фундаментальные теории. Через (N_T , pi_T ), (N_M , pi_M ) будем обозначать относительные интерпретации теории EA в теориях T, M соответственно. Будем говорить, что M - метатеория для T, если зафиксированы формулы PR_T(x), RF_T(x) из языка EA такие, что для любой формулы F (из языка EA):

а) если T|- pi_T(F), то M|- pi_M(PR_T(F)),

б) если T|- pi_T(~F), то M|- pi_M(RF_T(F)).

Таким образом, теория M "знает кое-что" об арифметических утверждениях, которые доказуемы или опровержимы в теории T. Чтобы не загромождать запись символами pi_T, pi_M, мы будем далее писать просто T|-F, T|- ~F, M|- PR_T(F), M|- RF_T(F) вместо T|- pi_T(F), M|- pi_M(PR_T(F)) и т.п. Такая вольность записи допустима, если мы интересуемся только арифметическими утверждениями, которые доказуемы в теориях T, M.

ТЕОРЕМА О ДВОЙНОЙ НЕПОЛНОТЕ. Пусть T, M - фундаментальные теории, причем M - метатеория для T. Тогда найдется замкнутая формула H из языка EA, такая, что если теории T, M непротиворечивы, то H неразрешима в T, однако в M нельзя доказать ни ~PR_T(H), ни ~RF_T(H) (т.е. в метатеории M нельзя доказать ни T-недоказуемость, ни T-неопровержимость формулы H).

Д о к а з а т е л ь с т в о. Возьмем машину, которая перечисляет все арифметические теоремы теорий T, M:

(A₀, T) (A₁, M) (A₂, M) (A₃, T)...

Появление пары (A_i, T) означает T|- A_i , а появление пары (A_i , M) - M|- A_i . Такая перечисляющая машина существует, поскольку множество всех теорем всякой формальной теории эффективно перечислимо. Наша цель - получить формулу H такую, что ни одна из следующих четырех выводимостей невозможна:

T|-H, T|- ~H, M|- ~PR_T(H), M|- ~RF_T(H). (1)

Поэтому будем называть формулу Q из языка EA позитивной, если в указанном перечислении раньше появляется пара (Q, T) или (~RF_T(Q), M), и негативной - если раньше появляется (~Q, T) или (~PR_T(Q), M). (Формула H, которую мы ищем, не должна быть ни позитивной, ни негативной.) Номер (в перечислении) первой появившейся пары будем называть (позитивным или негативным) номером формулы Q. Очевидно, следующие предикаты разрешимы:

a(x,y) = "y есть позитивный номер формулы с номером x",

b(x,y) = "y есть негативный номер формулы с номером x".

Пусть формулы A(x, y), B(x, y) выражают эти предикаты в теории EA.

Следуя методу Россера, возьмем теперь формулу

(Ay)(A(x,y) -> (Ez<y)B(x,z))

и применим лемму об автоссылках. В результате получится замкнутая формула H, обладающая свойствами

EA|- H <-> (Ay)(A(H,y) -> (Ez<y)B(H,z)).

("Если я позитивна, то я негативна, причем с меньшим номером".)

Упражнение 6.2. Следуя доказательству теоремы Россера (см. раздел 5.3), покажите, что выводимости (1) несовместимы с непротиворечивостью теорий T, M.

Теорема о двойной неполноте доказана.

Если взять M=EA+Con(T), т.е. если обсуждать теорию T средствами EA, предполагая непротиворечивость T, то оказывается, что существуют формулы, неразрешимость которых нельзя доказать исходя только из этого предположения. Для доказательства неразрешимости таких формул (если они получены из теоремы о двойной неполноте) нужно предположить Con(EA+Con(T)), т.е. непротиворечивость самой метатеории. Это ответ на вопрос, сформулированный в начале раздела.

Открытие явления неполноты привело к новому методу развития математических теорий. Если в теории T не удается утверждение F ни доказать, ни опровергнуть, мы можем попытаться принять F (или ~F) в качестве новой аксиомы. Однако такой прием связан с определенной опасностью: не исключено, что в будущем утверждение F будет доказано (тогда теория T+~F окажется противоречивой) или опровергнуто (тогда противоречивой окажется теория T+F). Но до того как это произошло, трудно сделать выбор с гарантией. Хотелось бы, принимая F в качестве новой аксиомы, "обезопасить" себя от возможных противоречий. Как это сделать? Нужно доказать непротиворечивость новой теории T+F. Однако из второй теоремы Геделя мы знаем, что абсолютное доказательство непротиворечивости фундаментальной теории невозможно (для такого доказательства нужны средства, выходящие за рамки самой теории, т.е. средства, менее надежные, чем сама теория). Таким образом, абсолютные гарантии от противоречий невозможны. Но мы можем попытаться получить гарантию относительную - доказать, что принятие новой аксиомы не порождает новых противоречий (кроме тех, которые, возможно, уже содержатся в "старой" теории T). Чтобы такому доказательству можно было доверять, его следует проводить в рамках теории T, предполагая только ее непротиворечивость. Т.е. речь идет о доказательстве непротиворечивости теории T+F средствами метатеории T+Con(T). Если оно удается, то, обнаружив противоречие, вытекающее из принятой новой аксиомы F, мы сумеем преобразовать вывод этого противоречия в вывод противоречия, не зависящий от F, в вывод противоречия средствами теории T (которой сейчас неограниченно доверяем). Таким образом, если непротиворечивость теории T+F доказана в метатеории T+Con(T), то тем самым доказано, что принятие F в качестве аксиомы столь же "безопасно", как принятие аксиом теории T.

Это новый подход к развитию математических теорий, возможность которого была осознана в начале XIX в. - с изобретением неевклидовых геометрий. Будучи не в состоянии решить вопрос об истинности утверждения F на основе общепризнанных аксиом, мы пытаемся доказать, что принятие F (или ~F) столь же "безопасно", как принятие общепризнанных аксиом. И затем присоединяем F (или ~F) к этим аксиомам. (Заметим, что здесь появляется возможность ветвления в развитии теории - можно изучать как теорию T+F, так и T+~F, ср. раздел 2.4.)

Раньше казалось, что единственный способ развития математической теории - вывод все новых следствий при неизменном списке аксиом. Теоремы о неполноте показали принципиальную недостаточность этого подхода - некоторые проблемы неизбежно не смогут быть решены, оставаясь в рамках существующих аксиом. При упомянутом новом подходе мы уже не считаем список аксиом неприкосновенным - к нему разрешается добавлять новые аксиомы, даже противоречащие друг другу (разумеется, не вместе, а порознь - получая из одной теории несколько различных). Неизменной здесь должна оставаться только "безопасность" от противоречий - аксиому F разрешается принять, если средствами метатеории T+Con(T) доказана непротиворечивость теории T+F. Таким образом, отвергая принцип "неизменных аксиом", новый подход сохраняет принцип "неизменной безопасности".

Теорема о двойной неполноте показывает недостаточность и этого принципа (он совершеннее принципа неизменных аксиом, но все же не является абсолютно совершенным). В самом деле, положив M=T+Con(T), мы получаем формулу H, которая неразрешима в теории T, однако средствами теории M нельзя доказать ни ~PR_T(H) (непротиворечивость теории T+~H), ни ~RF_T(H) (непротиворечивость теории T+H). Аксиома детерминированности (AD, см. раздел 2.4) является, возможно, примером аксиомы, "безопасность" принятия которой, т.е.

Con(ZF) -> Con(ZF+AD),

доказать никогда не удастся.

Интересно отметить, что явление "двойной неполноты" предвидел еще в 1926 г. П.Леви (см. П.Леви [1926]).

6.3. Проблема творчества в математике

Все математические теоремы выводятся из фиксированного набора аксиом. Иногда говорят по этому поводу, что в математике не может появиться ничего такого, чего уже ранее не было в аксиомах. Итак, в процессе развития математики не может появиться "ничего нового"?

Как относиться к такого рода рассуждениям? Если новым считать новое положение, которое привносится в исходные принципы теории (и не вытекает из этих принципов), то действительно - отличительной чертой математических теорий является именно застывшая система исходных принципов. Новое исходное положение приводит к новой теории. Однако если новое понимать так узко, то "откровение" предыдущего абзаца становится тавтологией.

Но, может быть, здесь хотят утверждать, что в математике не может быть ничего нового, поскольку математика - "механическая" наука, в которой аксиомы и правила вывода, а не "живой человек" определяют, что и как делать?

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

F₀ , F₁ , F₂ , F₃ ,...

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

Но если решение задачи нам неизвестно, мы высказали некоторое предположение F и хотим узнать, истинно ли оно (рассуждая в рамках теории T)? Т.е. нас интересует, будет ли T|-F или T|- ~F. Здесь указанное перечисляющее устройство мало чем может помочь: из теорем о неполноте мы знаем, что возможна ситуация, когда ни T|-F, ни T|- ~F (формула F неразрешима в теории T). В этом случае мы можем просидеть у ленты сколько угодно долго, но ни формула F, ни ~F напечатаны не будут - решения задачи от машины мы не получим.

Вообще говоря, творчество можно было бы считать устраненным из теории T, если бы удалось "механизировать" различение формул трех родов:

а) доказуемые в T,

б) опровержимые в T,

в) неразрешимые в T.

Разумеется, если теория T противоречива, то в ней доказуема любая формула, и классы а), б) в этом случае совпадают, а класс в) оказывается пустым. Если противоречие в T действительно найдено (найдена формула A такая, что T|-A и T|- ~A одновременно), то по аксиоме исчисления высказываний ~A->(A->B) можно уже без всяких усилий доказать произвольную формулу B. Таким образом, после того как противоречие в теории T найдено, в рассуждениях этой теории пропадает всякий творческий момент, все удается без труда "механизировать". (Правда, само нахождение противоречия в серьезной теории обычно бывает настоящим творческим актом - см., например, раздел 2.2.)

Отсюда следует, что проблему "механизации" различения классов а)-в) можно обсуждать только в такой метатеории, которая способна доказать непротиворечивость теории T (или эту непротиворечивость постулирует). Так мы и будем поступать.

Итак, пусть T - фундаментальная формальная теория. Предполагая непротиворечивость T, покажем, что класс а) эффективно-неотделим (см. дальше) от класса б). Отсюда будет следовать, что "механизация" различения классов а)-в) невозможна (и, в частности, что классы а),б), являясь эффективно перечислимыми, не являются, тем не менее, разрешимыми, а класс в) не является даже эффективно перечислимым).

Допустим от противного, что классы а),б) эффективно отделимы. Тогда существует разрешимый предикат s(x) (x пробегает натуральные числа), такой, что для любого n, являющегося номером формулы в языке EA,

1) если s(n), то перевод формулы с номером n нельзя опровергнуть в теории T (т.е. этот перевод не принадлежит классу б)).

2) если не s(n), то перевод формулы с номером n нельзя доказать в T (т.е. этот перевод не принадлежит классу а)).

Таким образом, предикат s(x) отделяет множество pi^-1(а) от pi^-1(б). Пусть истинность предиката s(x) распознается машиной Тьюринга M. Через C(x, t), D(x, t) обозначим формулы, выражающие в теории EA рекурсивные предикаты:

"машина M, работая с аргументом x, останавливается ровно за t шагов и выдает результат "истинно",

"машина M, работая с аргументом x, останавливается ровно за t шагов и выдает результат "ложно".

Используя идею конструкции Россера, по лемме об автоссылках можно получить формулу E такую, что

EA|- E <-> (At)(C(E, t) -> (Ez<t)D(E, z)).

Упражнение 6.3. Следуя доказательству теоремы Россера (см. раздел 5.3), покажите, что если s(E) истинно, то EA|- ~E, а если -s(E) ложно, то EA|-E.

Таким образом, значение s(E) не может быть ни истинным, ни ложным (оба предположения приводят к противоречию). Отсюда вытекает, что предикаты, отделяющие T-доказуемые формулы от T-опровержимых формул, не могут быть разрешимыми. В частности, не может быть речи о "механизации" различения классов а)-в).

Если, работая в фундаментальной теории T, мы задались гипотезой F и хотим решить, будет ли T|-F или T|- ~F (или, быть может, F неразрешима средствами T), то мы должны искать те конкретные особенности своей гипотезы, которые делают ее доказуемой, опровержимой или неразрешимой в теории T. Общего метода, пригодного для решения всевозможных таких вопросов, как мы только что показали, не существует. Ну а конкретный подход к проблеме (при условии невозможности общего метода) требует самого настоящего творчества. Подметив особенности гипотезы H₁, которые делают ее доказуемой в теории T, мы не можем с уверенностью рассчитывать, что этих наших идей будет достаточно для решения вопроса об истинности другой гипотезы H₂ и т.д.

(Эта часть нашей новой "философии творчества" действительна лишь в предположении непротиворечивости теории T. Но если T "на самом деле" противоречива - и мы об этом не знаем, нам предстоит совершить также творческий акт - найти это противоречие. Ведь из упражнения 6.1 мы знаем, что не существует общего метода, который определял бы по описанию любой теории, противоречива она или нет. Итак, без творчества не обойтись и в этом случае.)

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

6.4. Теорема о сокращении доказательств

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

Если мы присоединяем к теории T в качестве новой аксиомы гипотезу H, которая неразрешима в T, то получаем новую теорию T+H, которая "сильнее" T. И нет ничего удивительного в том, что в T+H не только можно доказывать новые теоремы (недоказуемые ранее в T), но к тому же еще многое, что в T делалось с трудом, в T+H становится проще.

То, что сказано в двух предыдущих абзацах, нельзя все же считать строгим обоснованием возможности этого явления. Если теорема как-то доказана в теории T и (более просто) - в теории T+H, то еще нельзя считать доказанным, что эту теорему нельзя доказать проще и в самой теории T. Недостающее строгое обоснование было дано К.Геделем в 1936 г.

ТЕОРЕМА О СОКРАЩЕНИИ ДОКАЗАТЕЛЬСТВ. Пусть T - фундаментальная теория, в которой недоказуема замкнутая формула L. Тогда для любой вычислимой функции f(x), которая монотонно стремится к бесконечности, найдется теорема K теории T такая, что l_T+L(K) < f(l_T(K)).

Формулировка нуждается, видимо, в комментариях. Во-первых, символы l_T+L(K), l_T(K) обозначают "длину" кратчайшего доказательства теоремы K соответственно в теориях T+L и T (более подробно о понятии длины доказательства см. дальше). Во-вторых, о роли функции f(x). Если взять конкретно f(x)=[x/100], то по теореме о сокращении доказательств найдется теорема K теории T такая, что l_T+L(K ) < l_T(K )/100 (при условии, что дополнительная аксиома L недоказуема в T). Т.е. кратчайшее доказательство K в теории T+L более чем в сто раз короче кратчайшего доказательства этой теоремы в теории T. Можно взять в качестве f(x) еще более медленно растущие функции, например [x/1000]], [sqrt(x], [log₁₀ x] и т.д.

Теперь более подробно о понятии длины доказательства, которое используется в теореме. Дело в том, что эта теорема остается справедливой при любом естественном способе измерения длины доказательств. Самый простой способ измерения - по количеству символов. Доказательство - это некоторая последовательность формул F₀, F₁ ,..., F_n , оканчивающаяся интересующей нас теоремой. Если через |F| обозначить число символов, образующих формулу F , длину нашего доказательства мы могли бы определить iкак сумму |F₀|+|F₁|+ ... +|F_n|.

Достаточными условиями для способа измерения длины доказательств, при которых оказывается справедливой теорема о сокращении, являются следующие:

а) длину доказательства можно вычислить, зная само доказательство (т.е. существует алгоритм, который по каждому T-доказательству вычисляет его длину),

б) для любого числа t существует только конечное число доказательств длины <=t, и все эти доказательства можно выписать, зная t (т.е. существует алгоритм, который по числу t перечисляет все T-доказательства длины <=t и, сделав это, "ставит точку", показывая, что больше доказательств не будет).

Упражнение 6.4. Учитывая конечность алфавита формальной теории, убедитесь, что способ измерения длины доказательств "по числу символов" удовлетворяет условиям а),б).

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

Д о к а з а т е л ь с т в о т е о р е м ы. Будем рассуждать от противного. Пусть f(x) - вычислимая функция (монотонно стремящаяся к бесконечности), такая, что для всех формул K, доказуемых в теории T,

f(l_T(K)) <= l_T+L(K). (1)

Выведем отсюда, что в таком случае множество всех теорем теории T+~L разрешимо. Это даст нужное нам противоречие, так как T+~L - фундаментальная теория (вместе с T), условие недоказуемости L средствами T предполагает непротиворечивость T+~L, а из раздела 6.3 мы знаем, что тогда множество всех теорем T+~L должно быть неразрешимым.

Если некоторая формула K доказуема в теории T+~L, то по теореме дедукции T |- ~L->K. Применяя (1), получаем T

f(l_T(~L->K)) <= l_T+L(~L->K).

Заметим теперь, что формула ~L->K доказывается в теории T+L очень легко. В самом деле, будем исходить из того, что в исчислении высказываний доказуема формула L->(~L->K) ("из противоречия следует все, что угодно"):

...

...

L->(~L->K) в исчислении высказываний

L аксиома теории T+L

~L->K по правилу MODUS PONENS

Очевидно, длина этого вывода является вычислимой функцией g(K,L) от формул K, L (свойство а), см. выше), тогда

l_T+L(~L->K) <= g(K, L).

Отсюда

f(l_T(~L->K)) <= g(K,L). (2)

Таким образом, если формула K доказуема в теории T+~L, то T |- ~L->K и имеет место (2). Но, используя методы вычисления функций f, g и зная, что f монотонно стремится к бесконечности, мы можем получить отсюда вычислимую функцию h(K, L), такую, что если K доказуема в T+~L, то

l_T(~L->K) <= h(K,L). (3)

Упражнение 6.5. Покажите, что это действительно так. Как вычисляется функция h?

Имея функцию h, можно предложить следующий метод для решения вопроса о том, доказуема ли формула K в теории T+~L, Если T+~L|-K, то T|- ~L->K, причем длина кратчайшего доказательства удовлетворяет (3). Вычисляем h(K, L) и выписываем (по свойству б)) все T-доказательства длины <=h(K, L). Если среди них имеется доказательство формулы ~L->K, то T+~L|-K, если нет - K недоказуема в T+~L.

Теорема о сокращении доказательств доказана.

6.5. Теорема Геделя в диофантовой форме

Как бы мы доказывали теорему Геделя о неполноте, используя то, что всякое эффективно перечислимое множество имеет диофантово представление (см. раздел 4.1)?

Пусть T - фундаментальная теория, рассмотрим для нее предикат:

"x есть номер формулы EA, перевод которой доказуем в T". (1)

Это эффективно перечислимый предикат, пусть

(Ez₁... Ez_n )P_T(x,z₁,..., z_n)=0

1 n T 1 n- его диофантово представление (P_T - полином с целыми коэффициентами, число n может зависеть от теории T). По лемме об автоссылках найдется замкнутая формула D_T , такая, что

EA|- D_T <-> ~(Ez₁... Ez_n)P_T (D_T, z₁,..., z_n)=0.

Ясно, что D_T - диофантова версия формулы Геделя G_T. Как же она поведет себя?

Если T|- D_T, то номер D_T удовлетворяет предикату (1) и уравнение

P_T(D_T, z₁,..., z_n )=0 (2)

должно иметь решения в натуральных числах. Обозначим одно из этих решений через (b₁,...,b_n), тогда

EA|- P_T(D_T, b₁,..., b_n)=0

(поскольку речь идет о числовом равенстве, не содержащем переменных, см. упражнение 3.5). Отсюда вытекает, что

EA|- (Ez₁... Ez_n)P_T(D_T, z₁,..., z_n)=0

и T|- ~D . Таким образом, если T|-D , то теория T оказывается противоречивой.

Если же теория T непротиворечива, то формула D_T недоказуема в ней и поэтому номер D_T уже не удовлетворяет предикату (1). Как следствие, уравнение (2) не имеет решений в натуральных числах. Однако формула

~(Ez₁... Ez_n)P_T(D_T, z₁,..., z_n)=0,

утверждающая этот факт, будучи равносильной D_T, недоказуема в теории T.

Таким образом, нами доказана

ТЕОРЕМА О НЕПОЛНОТЕ В ДИОФАНТОВОЙ ФОРМЕ. Пусть T - фунда- ментальная теория. Тогда существует диофантово уравнение Q_T(z₁,..., z_n )=0 такое, что либо теория T противоречива (тогда данное уравнение имеет решение в натуральных числах), либо уравнение не имеет решений в натуральных числах, однако формула

~(Ez₁... Ez_n)Q_T(z₁,..., z_n)=0, утверждающая этот факт, недоказуема в T.

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

Но неразрешимость уравнения Q_EA=0 удается доказать в теории множеств Цермело-Френкеля. Однако, если взять уравнение Q_ZFC=0, ситуация повторится: найдя решение этого уравнения, мы придем к противоречию в теории Цермело-Френкеля: если же решений не существует, этот факт нельзя будет доказать средствами данной теории (а так как теория ZFC формализует все средства рассуждения, признаваемые в математике, можно сказать даже, что неразрешимость уравнения Q_ZFC=0 нельзя доказать средствами, общепризнанными сегодня в математике).

Такое положение вещей противоречит распространенному мнению, что понятие натурального ряда в математике является первичным, не зависящим от более сложных понятий действительного числа и произвольного множества (эффектная формулировка этого мнения принадлежит Л.Кронекеру: "Бог создал целые числа, все остальное - дело рук человеческих"). Даже такие "коренные" вопросы, касающиеся натуральных чисел, как решение диофантовых уравнений, в некоторых случаях оказываются разрешимыми только с привлечением более сложных понятий. Приходится заключить, что понятие натурального ряда в истории математики развивалось - введение действительных чисел прибавило новые черты и натуральному ряду. Введение Г.Кантором понятия произвольного множества также прибавило новые черты понятию натурального ряда (в частности, стало возможным доказательство неразрешимости уравнения Q_EA=0). Еще более впечатляющий пример см. в приложении 2.

6.6. Теорема Леба

Формула G_T, с помощью которой К.Гедель доказывал свою теорему о неполноте, обладала свойством -

EA|- G_T <-> ~PR_T(G_T).

Она утверждала: "Я недоказуема в теории T", и оказалось, что если теория T непротиворечива, то G_T действительно недоказуема в T.

По аналогии с этой ситуацией в 1952 г. Л.Хенкин поставил следующий вопрос. Будем рассматривать формулу, которая (в противоположность формуле Геделя) утверждает: "Я доказуема в теории T", т.е. обладает свойством

EA|- A <-> PR_T(A).

Вопрос: формула A действительно доказуема в T?

Положительный ответ на этот вопрос был получен в 1955 г. М.Лебом.

ТЕОРЕМА ЛЕБА. Пусть T - фундаментальная теория, а PR_T(x) - формула из языка EA, удовлетворяющая условиям Гильберта. Тогда для любой формулы A, T|-PR_T(A)->A влечет T|-A.

Д о к а з а т е л ь с т в о. Имеем:

T|- ~A -> ~PR_T(A).

Таким образом -

T+~A|- ~PR_T(A),

т.е. в теории T+~A можно доказать, что формула A недоказуема в теории T. Но если A недоказуема в T, то теория T+~A непротиворечива (если она противоречива, то в T предположение ~A влечет противоречие, что является с точки зрения доказательством A). Таким образом, теория T+~A доказывает свою собственную непротиворечивость. По второй теореме Геделя, это означает, что T+~A - противоречивая теория, т.е. что формула A доказуема в теории T.

Теорема Леба доказана.

Упражнение 6.6. Изложенное доказательство содержит множество пробелов. Сначала попытайтесь самостоятельно определить их (и только потом читайте дальше). Во-первых, если к теории T+~A применяется вторая теорема Геделя, то должна быть определена формула Con(T+~A), выражающая непротиворечивость теории. К сожалению, стандартный способ построения формул Con в нашем случае непригоден - у нас имеется формула PR_T, но нет формулы PR_T+~A. Мы можем попытаться определить Con(T+~A) как ~PR_T(~A->0=1)..., но тогда придется передоказывать вторую теорему Геделя (применительно к теории T+~A). Сделайте это: предположите, что существует формула L такая, что EA|-L<->~PR_T(~A->L), и покажите, что тогда T|- Con(T+~A)->L. Отсюда будет следовать, что если T+~A|- Con(T+~A), то T+~A|-L. Покажите, что последнее означает противоречие в теории T+~A (повторив первую часть доказательства теоремы Геделя о неполноте). В конечном счете должно получиться: если T+~A|- Con(T+~A), то теория T+~A противоречива. Но как доказать существование формулы L? Если формула F(x, y) представляет в EA следующую функцию f: f(B)=~A->B, то по лемме об автоссылках найдется формула L такая, что

EA|- L <-> (Ey)(~PR_T(y)&F(L,y)).

Поскольку единственное значение y, удовлетворяющее формуле F(L, y) - это ~A->L, то получаем также

T|- L <-> ~PR_T(~A->L).

Этим завершается доказательство второй теоремы Геделя в нужной нам форме. Другой пробел в нашем доказательстве теоремы Леба - переход от T+~A|- ~PR_T(A) к T+~A|- Con(T+~А) был у нас неформальным. Для устранения этого пробела достаточно показать, что

T|- PR_T(~A->0=1)->PR_T(A).

Сделайте это. Какой еще (последний) пробел остается?