Почему я вообще снова в это полезла
Есть темы, которые в университете просто проходишь, потому что надо. Запомнила, сдала, выдохнула, пошла дальше. А потом через какое-то время они неожиданно возвращаются, и ты смотришь на них уже совсем иначе.
С теоремой о неполноте Гёделя у меня вышло примерно так.
Формально это история из математической логики. Про аксиомы, доказуемость, формальные системы. Но программирование ведь тоже очень сильно связано с математикой. Поэтому в какой-то момент мне стало интересно: а почему бы не попробовать посмотреть на теорему о неполноте не только как на математический сюжет, но и как на вещь, которая довольно болезненно и честно касается программирования?
Вообще эта мысль пришла ко мне после небольшого фрагмента разговора Эдварда Френкеля и Лекса Фридмана. Эдвард Френкель, если вдруг не сталкивались, это математик из Калифорнийского университета в Беркли, который работает на стыке математики и квантовой физики, и автор книги «Любовь и математика: сердце скрытой реальности». И вот после этого куска интервью я снова мысленно вернулась к материалу, который нам когда-то давали на третьем курсе.
Сразу оговорюсь: я не научный работник и не человек, который сейчас будет читать строгую лекцию по матлогике. Этот текст скорее попытка еще раз пройтись по теме уже немного другой головой. Так что математиков очень прошу не судить строго.
Очень коротко: что вообще говорит Гёдель
Если совсем коротко, теорем о неполноте две.
Первая, если говорить по-человечески и сильно упрощать, утверждает примерно следующее: в любой достаточно сложной и непротиворечивой формальной системе, где можно выразить арифметику, найдутся утверждения, которые истинны, но не выводятся из аксиом этой системы.
Вторая добавляет еще одну неприятную, но важную вещь: такая система не может доказать собственную непротиворечивость изнутри самой себя.
И здесь есть важный момент, который мне хочется отдельно подчеркнуть: система вообще должна быть непротиворечивой. Потому что если внутри нее можно одновременно доказать и некоторое утверждение, и его отрицание, дальше становится совсем тревожно: из такой системы можно вывести практически что угодно. То есть проблема не только в том, что система может быть неполной. Она еще и не должна разваливаться от внутренних противоречий.
Если хочется более строгое и нормальное объяснение без моих вольностей, очень рекомендую вот этот разбор на Хабре. Он действительно хороший.
При чем здесь вообще Евклид
Почему тут вообще вспоминается Евклид? Потому что разговор о Гёделе довольно быстро упирается в разговор об аксиомах. Мы со школы привыкаем к евклидовой геометрии так, будто она единственно возможная. Есть точки, прямые, параллельные, и кажется, что мир просто обязан быть устроен именно так.
Но потом оказывается, что все интереснее. Стоит поменять одну из базовых аксиом, например знаменитый постулат о параллельных, и появляются другие геометрии: сферическая, гиперболическая. И это очень красиво отрезвляет. Не в том смысле, что Евклид был «неправ», а кто-то другой потом пришел и «исправил мир». А в том смысле, что от исходных допущений зависит, какую именно картину мы вообще строим.
Мне кажется, это важная мысль не только для математики. Мы очень любим думать, что наши системы описывают реальность как она есть. Но довольно часто они описывают реальность в рамках тех аксиом, правил и ограничений, которые мы сами же и приняли за основу.
И вот тут мне становится особенно интересно смотреть на программирование.
А теперь к программированию
Потому что программирование, если грубо, тоже живет внутри формальных рамок. У нас есть язык, синтаксис, правила, типы, спецификации, ограничения платформы, допущения автора кода. Мы все время строим маленькие формальные миры и надеемся, что они будут вести себя предсказуемо.
Отсюда, мне кажется, и рождается очень соблазнительный тезис: если мир можно формализовать, значит, в принципе, всё можно вычислить. Нужно просто больше данных, больше мощности, больше времени, лучше модели, больше кода. В такой логике жизнь почти незаметно начинает равняться вычислению.
Тут всплывают Гёдель с Тьюрингом, и как-то резко отрезвляет.
Тьюринг и проблема остановки
Вы, возможно, слышали про такую задачу: можно ли написать программу, которая для любого другого кода скажет, завершится он или будет выполняться бесконечно?
Это знаменитая проблема остановки, и Алан Тьюринг доказал, что в общем случае такой универсальной программы не существует. Нельзя построить алгоритм, который для любого возможного алгоритма безошибочно решит этот вопрос.
Для меня это один из самых интересных моментов. Здесь ограничения формальных систем перестают быть чем-то абстрактным из учебника по логике и напрямую проявляются в программировании - не на уровне философии, а вполне буквально.
У нас есть статический анализ, тесты, верификаторы, линтеры, системы типов - куча мощных инструментов. И они действительно работают и сильно помогают. Но идея о том, что однажды появится универсальный способ, который сможет про любой код сказать всё и при этом не ошибаться, уже не выглядит такой убедительной.
И в этом месте мне становится трудно безоговорочно соглашаться с лозунгом «всё в жизни вычислимо».
Я понимаю, почему он такой привлекательный. Особенно если ты связан с программированием, данными, ИИ, моделями. Нам нравится мысль, что любую сложность можно просто дожать. Что если пока что-то не вычисляется, то это лишь вопрос времени, мощности или качества метода. Но Гёдель и Тьюринг, как мне кажется, заставляют относиться к этой уверенности осторожнее.
Но ведь мы даже видим мир по-разному
Причем мне здесь важна не только математика, но и восприятие.
Помните то самое платье: сине-черное или бело-золотое? Я, кстати, из лагеря сине-черных. И ведь это хороший бытовой пример того, что один и тот же объект люди могут видеть по-разному. Одни и те же входные данные не гарантируют один и тот же «внутренний вывод».
Можно вспомнить и вазу Рубина, где кто-то сначала видит вазу, а кто-то два профиля. В каком-то смысле это все про одно и то же: восприятие не сводится к сухому считыванию сигнала. В нем всегда есть интерпретация.
Мне очень откликается и идея дополнительности Нильса Бора: одну и ту же вещь иногда приходится описывать разными способами, и эти способы не всегда легко свести друг к другу. Я сейчас не пытаюсь натянуть физику на всё подряд, но сама интонация мне близка. Одно и то же можно увидеть по-разному, и это не всегда означает, что кто-то один просто ошибся, а другой нет.
А что тогда с нейросетями
Если перенести это в разговор о нейросетях, становится еще интереснее. Мы часто говорим о моделях так, будто они работают с нейтральной реальностью. Но данные собирают люди. Данные размечают люди. Архитектуры проектируют люди. Метрики выбирают люди. А у каждого человека есть своя жизнь, свой опыт, свои предубеждения, свои слепые зоны.
Все создано людьми: нейросети, уравнения, языки, правила, системы. И след человека в них остается всегда. Это не обязательно плохо. Это просто, как мне кажется, честно признавать. Дальше уже начинается большая территория психологии, в которую я, если честно, даже боюсь глубоко заходить.
Что я в итоге из этого вынесла
Поэтому для меня теорема о неполноте Гёделя давно перестала быть только абзацем из курса математической логики. Я вижу в ней очень трезвое напоминание о границах любой системы, которая пытается описать мир изнутри самой себя.
Она не говорит, что математика бессильна.
Она не говорит, что программирование бессмысленно.
Она не говорит, что раз уж есть недоказуемые утверждения, то теперь можно махнуть рукой на точность и проверяемость.
Скорее наоборот. Она учит аккуратности. Учит не путать мощность системы с ее всемогуществом. Учит помнить, что даже самая красивая и строгая конструкция имеет пределы.
И, возможно, именно поэтому мне кажется важным смотреть на Гёделя не только как на математика, но и как на очень неприятного, но полезного собеседника для программиста. Особенно в эпоху, когда так легко поверить, что еще немного, и мы все наконец-то вычислим до конца.
P.S. Этот текст вообще не претендует на научный уровень, и я вполне могу быть неправа в каких-то интерпретациях. У меня нет цели выставить себя умной. Мне просто стало интересно еще раз разобрать тему, которую нам когда-то давали на третьем курсе университета, но уже немного с другой головой. Не только как учебный материал, а как повод подумать о программировании, мышлении и наших попытках всё формализовать. Ваше мнение с удовольствием почитаю в комментариях.