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

Подумайте, что это означает. А означает это, что великую теорему Ферма, гипотезу Пуанкаре или любую другую математическую загадку, которая только придет вам в голову, можно доказать, начав с аксиом теории множеств, а затем применяя эти простенькие правила раз за разом, снова и снова. Вероятно, делать это придется 300 миллионов раз, но все же…

Как же Гёдель доказывает свою теорему о полноте? Доказательство описывают как «вывод семантики из синтаксиса». Мы просто придумываем объекты на заказ по мере того, как их требуют аксиомы! И если мы когда-нибудь наткнемся на несогласованность, то случиться это может лишь по одной причине: что несогласованность присутствовала и в первоначальных аксиомах.

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

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

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

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

Но погодите! Разве теорема о неполноте не противоречит теореме о полноте, согласно которой, любое утверждение, которое следует из аксиом, может быть доказано исходя из этих аксиом? Придержите этот вопрос; мы проясним его чуть позже.

А сначала давайте посмотрим, как доказывается теорема о неполноте. Обычно говорят, что «доказательство теоремы о неполноте — это высший пилотаж математики, оно занимает 30 страниц и требует сложных построений с привлечением простых чисел», и т. п. Невероятно, но сегодня, через восемьдесят лет после Гёделя, это доказательство по-прежнему представлено в курсах математики именно так!

Ну хорошо, открыть вам секрет? Доказательство теоремы о неполноте занимает примерно две строчки. Оно почти тривиально. Но предупреждаю: чтобы доказать ее в две строчки, вам для начала потребуется представление о компьютере.

Где-то в средних классах школы у меня был приятель, который был очень силен в математике, но, возможно, не так уж силен в программировании. Он хотел написать программу с использованием массивов, но не знал, что такое массив. Что же он сделал? Каждому элементу массива он поставил в соответствие уникальное простое число, а затем их все перемножил; затем, когда ему требовалось считать из этого массива что-нибудь, он раскладывал это произведение на простые множители. (Если бы он программировал квантовый компьютер, не исключено, что такое решение было бы не самым неудачным!) Во всяком случае, мой приятель тогда делал, по существу, то же самое, что сделал Гёдель. Он придумал хитроумный ход, позволяющий программировать без программирования.