Квантовые вычисления со времен Демокрита - Скотт Ааронсон

(то есть путем перебора всех возможных доказательств и опровержений высказывания о том, что Q остановится, в некоей формальной системе F). Тогда, как в доказательстве Тьюринга, предположим, что мы модифицируем P и получим новую программу P′, такую, что она

1. Работает вечно, если доказано, что Q при получении на вход собственного кода останавливается, или

2. Останавливается, если доказано, что Q при получении на вход собственного кода работает вечно.

Далее предположим, что мы подаем на вход P′ ее собственный код. В этом случае мы знаем, что P′ будет работать вечно и никогда не обнаружит доказательства или опровержения высказывания о том, что она остановится. Ибо если P′ найдет доказательство того, что остановится, то она будет работать вечно, а если она найдет доказательство того, что будет работать вечно, то остановится, а это противоречие.

Но здесь присутствует очевидный парадокс: почему приведенный аргумент не является сам по себе доказательством того, что P′, получив на вход собственный код, будет работать вечно? И почему P′ не может найти доказательство того, что она будет работать вечно, — и, следовательно, остановится, и, следовательно, работать вечно, и, следовательно, остановится и т. п.?

Ответ в следующем: при «доказательстве» того, что P′ будет работать вечно, мы сделали скрытое предположение, а именно что система доказательства F непротиворечива. Если бы условия непротиворечивости не было, то вполне могло бы существовать доказательство того, что P′ остановится, хотя в реальности P′ работала бы вечно.

Но это означает, что если F могла бы доказать, что F непротиворечива, то F могла бы также доказать, что P′ будет работать вечно, — и таким образом вновь вытащила бы на свет божий приведенное выше противоречие. Из всего этого можно сделать единственный вывод: если система F непротиворечива, то F не может доказать собственную непротиворечивость. Этот результат иногда называют второй теоремой Гёделя о неполноте.

Вторая теорема о неполноте устанавливает то, что нам, вероятно, следовало ожидать с самого начала: что математические теории, достаточно напыщенные, чтобы доказывать собственную непротиворечивость, не могут на самом деле похвастать этой самой непротиворечивостью! Если мы хотим доказать, что теория F непротиворечива, то сделать это мы можем только в рамках другой, более мощной теории; в качестве тривиального примера можно привести F + Con(F) (теория F плюс аксиома о непротиворечивости F). Но как мы можем знать, что F + Con(F) само по себе непротиворечиво? Ну, мы можем доказать это только в рамках еще более сильной теории: F + Con(F) + Con(F + Con(F)) (это F + Con(F) плюс аксиома о том, что F + Con(F) непротиворечива). И так до бесконечности. (И даже дальше, чем до бесконечности, в область счетных ординальных чисел.)

Возьмем конкретный пример: вторая теорема о неполноте говорит нам, что самая популярная система аксиом для целых чисел, арифметика Пеано, не может доказать собственной непротиворечивости. Или, в символьной форме, PA не может доказать Con (PA). Если мы хотим доказать Con (PA), нам необходимо перейти к более сильной системе аксиом, такой как ZF (аксиомы теории множеств Цермело — Френкеля). В системе ZF мы можем доказать Con (PA) без особого труда, использовав аксиому бесконечности для конструирования бесконечного множества, которое затем служит моделью PA.

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

Быстрый вопрос на понимание: хотя мы не можем доказать Con(PA) в рамках PA, можем мы хотя бы доказать в рамках PA, что из Con(PA) следует Con(ZF)?

Нет, не можем. Потому что тогда мы могли бы также доказать в рамках ZF, что из Con(PA) следует Con(ZF). Но поскольку в ZF можно доказать Con(PA), это означало бы, что в ZF можно доказать Con(ZF), что противоречит второй теореме о неполноте.

Я обещал объяснить, почему теорема о неполноте не противоречит теореме о полноте. Проще всего, вероятно, сделать это через пример. Рассмотрим «самоненавистническую теорию» PA + не (Con(PA)), то есть арифметику Пеано плюс утверждение о ее противоречивости. Нам известно, что если PA непротиворечива, то эта странная теория тоже должна быть непротиворечива, поскольку в противном случае PA доказала бы свою непротиворечивость, чего теорема о неполноте не позволяет. Из этого следует, согласно теореме о полноте, что PA + не (Con(PA)) должна иметь модель. Но как такая модель могла бы выглядеть? В частности, что произошло бы, если бы вы в рамках этой модели просто захотели бы увидеть доказательство противоречивости PA?

Я скажу вам, что произошло бы: аксиомы сказали бы вам, что доказательство противоречивости PA зашифровано некоторым положительным целым числом X. После чего вы сказали бы: «Но что такое X?» И аксиомы сказали бы: «X». А вы сказали бы: «Но что есть X как обычное положительное целое число?»

— Что вы имеете в виду под обычным положительным целым числом?

— Я имею в виду — не какая-то абстрактная сущность, обозначенная каким-то символом, к примеру X, но 1, или 2, или 3, или какое-то другое конкретное целое число, которое получается, если начать с 0 и прибавить 1 конечное число раз.

— Что вы имеете в виду, говоря «конечное число раз»?

— Я имею в виду, ну, один раз, или два, или три раза…

— Но тогда ваше определение образует замкнутый круг!

— Послушайте, вы прекрасно знаете, что я имею в виду, говоря «конечный»!

— Нет-нет-нет! Говорите на языке аксиом.

— Ну хорошо, это ваше X больше или меньше 10500 000?

— Больше. (Аксиомы не глупы и понимают, что если они скажут «меньше», вы сможете просто проверить все меньшие числа и убедиться, что ни в одном из них не зашифровано доказательство противоречивости PA.)

— Так, ладно, что есть X + 1?

— Y.

И так далее. Аксиомы будут и дальше выдавать на ваши запросы всевозможные выдуманные числа, и, считая, что PA