Вначале была аксиома. Гильберт. Основания математики

Парадокс лжеца был для Гёделя одним из двигателей доказательства теорем о неполноте. Поскольку доказательство было на грани перехода в цикличность, некоторые математики — в частности, 60-летний Цермело — не осознали его ценности. Гёдель придумал ловкий перевод на метаязык внутри языка: арифметизацию метаматематики. С помощью смелой цифровой кодификации, основанной на простых числах (которую с тех пор называют гёделизацией), он назначил номера знакам так, чтобы с каждой формулой (и также с каждым доказательством) можно было связать число, кодировавшее бы всю структуру. Пропозиции, в которых говорилось о свойствах формальной системы, выражались в рамках системы посредством арифметических формул. Доказуемость, например, была представлена в виде числового отношения.

В таких условиях Гёдель вышел из ситуации, составив формулу G, которая говорит сама о себе: «я недоказуемо». Эта формула стала примером неразрешимого утверждения внутри формальной системы: ни она, ни ее отрицание не являются теоремами, то есть чем-то доказуемым. Действительно, Іеделю удалось доказать, что G доказуемо тогда и только тогда, когда ¬G доказуемо. Следовательно, если мы хотим, чтобы формальная система была непротиворечивой, ни G, ни ¬G не могут быть таковыми. Если бы G было доказуемо, так как ¬G утверждает в метаматематических терминах, что G доказуемо (отрицает то, что оно недоказуемо, как сказано в нем самом), то было бы возможно доказать также ¬G и вывести противоречие (G^¬G). И наоборот, если бы ¬G было доказуемым, мы могли бы по той же причине доказать G и прийти к тому же противоречию. В итоге доказательство любой из этих двух формул автоматически предполагало бы противоречивость системы. Более того, если допустить, что формальная система непротиворечива, то G недоказуемо, но истинно. Если бы G было ложно, так как в G говорится: «я недоказуемо», то G было бы доказуемо, что невозможно. Следовательно, у нас есть высказывание G, которое, хотя и недоказуемо, является истинным.

Существование неразрешимого утверждения предполагает, что аксиомы теории не содержат ответа на все вопросы, формулируемые формальным языком, потому что ни утверждение, ни его отрицание не являются теоремами. И так как либо оно, либо его отрицание должно быть истинным, у нас есть истинная недоказуемая формула. Хуже всего, что если добавить неразрешимое утверждение в качестве аксиомы, появляются другие, новые. Математика вдруг очнулась от гильбертова сна — от мечты о полноте, в которой аксиоматические системы не содержат неразрешимых формул, а истинное всегда совпадает с доказуемым. Проще говоря, «непротиворечивый» предполагает «неполный», и наоборот, «полный» предполагает «противоречивый». Ни одна формальная система, содержащая привычную арифметику, не может быть одновременно и той и другой. Если мы предположим, что она непротиворечива, она всегда будет неполной, то есть будет содержать недоказуемые истины. Будут существовать некоторые истинные свойства формально неразрешимых чисел, то есть свойства, которые мы не можем ни доказать, ни отвергнуть на основе аксиом.

Но за первой теоремой о неполноте следует вторая: так как непротиворечивость равносильна утверждению, что формула 0/=0 недоказуема, Гёдель трансформировал это последнее математическое свойство в арифметическую формулу (назовем ее С) и заметил, что в первой теореме установлено, по сути, что «C->G». Непротиворечивость предполагает, что существует неразрешимое утверждение и, следовательно, неполнота. Так что доказательство С позволило бы нам исключить G из импликации «C->G» посредством modus ponens и, следовательно, доказать G, что невозможно, поскольку G недоказуемо. Это удивительное следствие сводится к тому, что непротиворечивость формальной системы, которая включает в себя арифметику, недоказуема в рамках формальной системы. Гёдель не доказал должным образом эту вторую теорему, он только высказался о ее приемлемости, но так никогда и не записал обещанного доказательства. Первое полное доказательство, очень тщательное, появилось, что любопытно, в 1939 году, во втором томе «Оснований математики» Бернайса и Гильберта.