Теорема Гёделя — синтаксическая версия

Знаменитая Теорема Гёделя о неполноте имеет две версии — синтаксическую (объявленную и доказанную самим Гёделем) и семантическую (чаще всего фигурирующую в популярных рассуждениях о великой Теореме). Семантическая версия утверждает, что какую бы систему формальных доказательств ни придумать, в языке найдутся истинные утверждения, не доказуемые в рамках предложенной системы.
Таким образом, семантическая версия исходит из того, что некоторые выражения языка выражают осмысленные утверждения, являющиеся истинными или ложными. Синтаксическая версия не опирается на то, что какие бы то ни было выражения языка имеют какой-то смысл, она смотрит на выражения как на синтаксические конструкции, то есть как на цепочки символов, организованные по определённым правилам. Синтаксическая версия Теоремы Гёделя утверждает, что какую бы систему формальных доказательств ни придумать, в языке найдутся такие выражения, что ни их самих, ни их отрицания невозможно доказать в рамках предложенной системы.
Разумеется, обе версии предполагают выполнение некоторых естественных ограничений, налагаемых как на рассматриваемый язык, так и на систему формальных доказательств.
Среди таких ограничений центральное место занимает предположение о непротиворечивости языка. Для семантической версии нужна семантическая непротиворечивость, означающая, что никакое ложное утверждение не может быть доказуемым. Для синтаксической версии нужна синтаксическая непротиворечивость, означающая невозможность того, чтобы одновременно оказались бы доказуемыми и какое-то выражение и его отрицание.
Лекция будет посвящена синтаксической версии Теоремы Гёделя о неполноте (семантической версии были посвящены три лекции на Летней школе 2007 г.). Сам Гёдель доказал синтаксическую версию, используя более сильное, чем непротиворечивость, предположение, а именно так называемую омега-непротиворечивость. Через несколько лет после публикации Гёделя Россеру удалось заменить омега-непротиворечивость на простую непротиворечивость.
Когда Гёдель и Россер излагали свои теоремы, ещё не родилась теория алгоритмов. А она позволяет сделать более прозрачным изложение синтаксической версии — как в первоначальной гёделевской формулировке, то есть в предположении омега-непротиворечивости, так и в последующей россеровской формулировке, то есть в предположении простой непротиворечивости.