В таких условиях Гёдель вышел из ситуации, составив формулу 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 году, во втором томе «Оснований математики» Бернайса и Гильберта.
Мало того, к синтаксическим ограничениям, которые открыл Гёдель, присоединилось другое ограничение — семантическое, формальных систем первого порядка: теорема, сформулированная Леопольдом Лёвенгеймом (1878-1957) и Туральфом Скулемом (1887-1963) около 1920 года (Скулем вернулся к ней в 1933 году). В 1930 году в рамках своего доказательства полноты логики первого порядка Гёдель мимоходом доказал, что любая непротиворечивая теория первого порядка имеет модель, в которой аксиомы проверяются, хотя и ничего не добавил о том, какие характеристики имеет эта модель и как ее построить. Лёвенгейм и Скулем до этого заметили, что любая непротиворечивая формальная система первого порядка имеет, по сути, счетную модель. Это порождает парадокс Скулема: если ZF непротиворечиво, то оно обладает счетной моделью. То есть несчетный континуум, которым мы намереваемся оперировать в ZF, может относиться к счетному множеству вне ZF. Теория действительных чисел, от которой мы ждем знакомой несчетной модели («настоящие» действительные числа), также имеет счетную модель.