Парадокс лжеца и теоремы Гёделя глазами программиста

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

В любой непротиворечивой системе, достаточно сильной для арифметики, найдётся истинное утверждение, которое внутри неё невозможно доказать. Полнота и непротиворечивость несовместимы.

Фраза, которая сама себя кусает

Рассмотрим предложение: «Это утверждение ложно». Попробуем определить, истинно оно или нет.

Если оно истинно, то, как оно само и заявляет, оно ложно.
Если оно ложно, то его заявление о собственной ложности неверно — значит, оно истинно.

Замкнутый круг. Это парадокс лжеца, известный ещё античности. Долго он считался лингвистическим курьёзом — пока в 1931 году Курт Гёдель не превратил его в математическое оружие.

Трюк Гёделя: заставить математику говорить о себе

Гёдель придумал способ кодировать утверждения о числах самими числами (гёделева нумерация) — примерно как любой текст в компьютере становится числом в памяти. Это позволило строить высказывания, которые ссылаются сами на себя.

И он сконструировал особое утверждение $G$, смысл которого: «Это утверждение недоказуемо в данной системе». Узнаёте лжеца? Только вместо скользкого «ложно» — строгое «недоказуемо». Дальше происходит магия:

Если $G$ доказуемо, то оно ложно (ведь оно утверждает обратное) — а доказывать ложь в честной системе нельзя. Противоречие.
Значит, $G$ недоказуемо. Но тогда оно говорит правду! Получаем истинное утверждение, которое система доказать не в силах.

Две теоремы о неполноте

Первая теорема: любая непротиворечивая формальная система, способная описывать арифметику, неполна — в ней есть истинные, но недоказуемые утверждения. Залатать дыру нельзя: добавите $G$ как аксиому — появится новое $G'$.

Вторая теорема: такая система не может доказать собственную непротиворечивость. Если математика докажет, что она сама себе не противоречит, — это как раз и будет признаком, что она противоречит.

При чём здесь программирование

Для программиста Гёдель — близкий родственник проблемы остановки. И там, и там фокус один: самоссылка плюс отрицание ломают систему. Программа, которая делает обратное тому, что про неё предсказали; утверждение, которое объявляет себя недоказуемым. Тьюринг и Гёдель, по сути, описали одно и то же явление с разных сторон.

Практические следствия вполне осязаемы:

Верификация кода	Не существует программы, доказывающей корректность любой программы — иначе она решала бы и проблему остановки.
Автоматические доказательства	Доказатели теорем неизбежно либо чего-то не докажут, либо зависнут — полной автоматизации математики не будет.
Системы типов	Чем выразительнее система типов, тем больше в ней принципиально непроверяемых вещей.

Что это значит для нас

Теоремы Гёделя — не повод для уныния и не «крах математики», как иногда пишут. Математика отлично работает. Гёдель лишь показал её честные границы: ни одна формальная система не охватит всю истину о числах и не подтвердит собственную безупречность изнутри. Для инженера это здоровая прививка от перфекционизма: некоторые вопросы о коде нельзя решить автоматически не потому, что мы не доросли, а потому, что так устроена логика. Парадокс лжеца оказался не глупой игрой слов, а трещиной в фундаменте, сквозь которую видно очень далеко.