Основания математики в XX веке: от Гильберта и Гёделя до теории типов

XX век был веком потрясений для оснований математики — но к чему это привело?

Всё началось с желания построить строгий фундамент для самой строгой из всех наук.
К XIX веку стало окончательно ясно: для физики, химии, биологии эксперимент — это основной способ проверки.
Но математика — другая. Никакой опыт не докажет, что простых чисел бесконечно много, а доказательство теоремы Ферма перебором принципиально невозможно.

Математика работает на строгих правилах — аксиомах.
Но главный вопрос: каких именно аксиом? И кто вообще решил, что именно они допустимы?

Аксиомы и парадоксы: трещины в основаниях математики

Попытки избавиться от аксиомы о параллельных прямых Евклида привели к появлению новых, внутренне непротиворечивых геометрий — геометрии Лобачевского, геометрии Римана и других. Это уже было тревожным сигналом: строгая математика может существовать в нескольких версиях.
Но вскоре выяснилось, что похожие проблемы есть и у самого фундамента математики — арифметики и логики. Появились парадоксы, вроде парадокса брадобрея, которые, казалось, ломали саму идею строгого рассуждения.

Подумайте сами:
«Это утверждение ложно».
Оно истинно или ложно?

Четыре школы в поисках строгих оснований математики

Математике нужно было строгое решение. Так оформились четыре больших направления:

📖 Формалисты во главе с Давид Гильберт считали, что любое математическое утверждение в принципе можно доказать, если правильно выбрать аксиомы и правила вывода.

📖 Логицизм с Бертран Расселом и Уайтхедом пытался свести всю математику к логике, решая парадоксы ценой искусственных ограничений и сложных конструкций.

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

📖 Теоретико-множественный подход, начатый Кантором и развитый Цермело и Френкелем (ZFC), сделал акцент на иерархии множеств, аксиоме выбора и гипотезе континуума.

Гёдель и множественность математических систем

Но уже к 1930-м годам Курт Гёдель нанёс решающий удар. Любая достаточно мощная система аксиом неполна: всегда существуют утверждения, которые нельзя ни доказать, ни опровергнуть внутри этой системы.
Лёвенгейм и Сколем показали, что у одной и той же системы аксиом могут быть принципиально разные интерпретации.
А Пол Коэн, доказав независимость аксиомы выбора и гипотезы континуума от остальных аксиом Цермело–Френкеля, фактически показал: существует не одна математика, а много.

Оказалось, что математика стоит на не менее шатком фундаменте, чем физика или химия. Там, где ожидали абсолютную строгость, обнаружился хаос из множества разрозненных аксиоматических систем — каждая полезная, каждая ограниченная и каждая с собственными недоказуемыми утверждениями.

Теория типов и новые основания математики

Что же появилось за последние 100 лет?

Сегодня официальным стандартом остаётся ZFC — просто потому, что он удобен и привычен. Но вокруг него выросли конкуренты. Одна из главных надежд — теория типов. Вместо множеств она работает с типами, где утверждения и конструкции неразделимы. Доказательство здесь одновременно является объектом, а логика тесно связана с вычислениями. В гомотопической теории типов равенство понимается как структура, а не как формальное совпадение, что делает её особенно удобной для компьютерных доказательств.

Сегодня мы всё больше имеем дело с искусственным интеллектом и формальными системами, что естественным образом сближает математику с конструктивным и интуиционистским подходом. Некогда долго спорить о философских основаниях, когда нужно проверять результат LLM здесь и сейчас. Но именно поэтому будущее (и настоящее!) выглядит особенно интересно.

И всё же хочется придерживаться мнения Гильберта:
в математике не существует иных пределов познания, кроме пределов таланта исследователя.