Формальные системы и аксиоматики

1900. Париж. Давид Гильберт публикует 23 задачи для математики XX века. Вторая: доказать непротиворечивость арифметики. 1931: Курт Гёдель доказывает, что это невозможно изнутри самой системы. Программа Гильберта рухнула. Но из её руин выросло кое-что неожиданное: CompCert - компилятор C, доказанно корректный, который используется в авиации и ядерной промышленности. Формальные системы оказались мощнее, чем думал сам Гильберт.

• **CompCert (Xavier Leroy, INRIA)**: формально верифицированный компилятор C - каждый шаг трансляции доказан в Coq. Используется в авиации и ядерной промышленности, где баг компилятора - катастрофа
• **TLA+ в Amazon**: формальная спецификация распределённых систем S3, DynamoDB, EBS. До внедрения - один найденный баг в distributed consensus стоил бы миллиарды. После: 17 критических багов обнаружены до деплоя
• **Z3 SMT solver (Microsoft Research)**: формальная верификация программ через автоматический поиск противоречий. Используется в слоях безопасности GitHub Copilot и AWS
• **seL4**: операционная система с доказанной безопасностью через Isabelle/HOL. Используется в военных беспилотниках - первый OS-kernel с machine-checked correctness proof

Аксиомы и аксиоматический метод

Формальная система состоит из трёх компонентов: алфавита (символов), грамматики (правил построения формул) и аксиом с правилами вывода. Доказательство - конечная последовательность формул, где каждая либо является аксиомой, либо получена из предыдущих по правилам вывода. Ключевое слово: конечная. Доказательство должно быть проверяемым механически - именно это делают Coq, Lean4, Isabelle.

Важно различать синтаксис (формальная выводимость |-) и семантику (логическая следуемость |=). Теорема о полноте Гёделя утверждает их совпадение для логики первого порядка: |- ф тогда и только тогда, когда |= ф. Это содержательный результат - синтаксис и семантика - разные миры, и их совпадение требует доказательства.

Геометрия Евклида: 5 аксиом порождают всю школьную геометрию. Три аксиомы Колмогорова определяют всю теорию вероятностей. Аксиоматический метод - это игра: выбираем правила, дальше всё следует из них. CompCert (Xavier Leroy, INRIA) - компилятор C, доказанно корректный в Coq. Используется в авиации и ядерной промышленности, где баг компилятора равен катастрофе.

**TLA+ в Amazon:** формальная спецификация распределённых систем S3, DynamoDB, EBS. До внедрения - один найденный баг в distributed consensus стоил бы миллиарды. После: 17 критических багов обнаружены до деплоя. Формальная логика - это не академия. Это страховой полис на сотни миллиардов долларов инфраструктуры.

Дедукция и теорема о дедукции

Дедукция - вывод следствий из посылок по правилам системы. Теорема о дедукции - мета-теорема, связывающая условный и безусловный вывод: гамма, ф |- пс тогда и только тогда, когда гамма |- ф -> пс. Это мощный инструмент: вместо доказательства «при гипотезе ф получаем пс» можно сразу доказывать импликацию «ф -> пс» как объект формальной системы.

Теорема о дедукции действует в большинстве пропозициональных и предикатных систем, но требует осторожности: в предикатной логике она не применяется к формулам, содержащим свободные переменные, связанные правилами обобщения. Это не баг - это фундаментальное ограничение, проявляющееся при работе с кванторами.

Теорема о дедукции - это мета-теорема: утверждение о формальной системе, а не внутри неё. Большинство таких мета-теорем доказывается индукцией по длине вывода - классическое применение математической индукции к синтаксическим объектам.

Непротиворечивость и полнота

Система называется непротиворечивой, если в ней нельзя вывести одновременно ф и не-ф. Полной - если любая истинная формула доказуема. Эти два свойства были целью программы Гильберта. Гёдель в 1931 году показал: система, достаточно богатая чтобы выражать арифметику, либо противоречива, либо неполна. Выбора нет. Это не баг формальных систем - это фундаментальный предел.

Система Гильберта и соответствие Карри-Говарда

Система Гильберта - это стиль формальных систем с минимальным набором правил вывода (обычно только modus ponens) и богатым набором аксиомных схем. Альтернативы: натуральный вывод Генцена (удобнее для рассуждений) и секвентное исчисление (мощнее для метатеории и автоматического доказательства). Именно секвентное исчисление лежит в основе Z3 SMT solver - того самого, что верифицирует программы в GitHub Copilot safety layer.

Соответствие Карри-Говарда - одно из глубочайших открытий XX века. Логика и теория типов - это одно и то же, описанное разными языками. Agda, Coq и Lean4 используют это для машинной верификации математических теорем. Когда Lean4 компилирует корректный тип - он верифицирует доказательство. seL4 - операционная система с доказанной безопасностью через Isabelle/HOL. Используется в военных беспилотниках - первый OS-kernel с machine-checked correctness proof.

Программа Гильберта потерпела поражение в 1931 году. Но провал породил неожиданный плод: осознание того, что формальные системы - не только математика. Это вычисления. Curry-Howard сделал это точным: доказательство есть программа, тип есть формула. Lean4 содержит более 100 000 машинно-верифицированных теорем. За каждой - вариант той же структуры, которую изучает этот урок.

Ключевые идеи

• Формальная система = алфавит + грамматика + аксиомы + правила вывода. Доказательство - конечная последовательность формул, механически проверяемая
• Непротиворечивость: нельзя вывести ф и не-ф одновременно. Иначе - explosion, и всё выводимо
• Теорема о дедукции: Гамма, ф |- пс тогда и только тогда, когда Гамма |- ф -> пс
• Первая теорема Гёделя: богатые непротиворечивые теории неполны - в них есть истинные, но недоказуемые утверждения
• Соответствие Карри-Говарда: доказательство = программа, тип = формула. CompCert, seL4, Lean4 - это оно в действии

К теоремам Гёделя

Программа Гильберта потерпела поражение в 1931 году, когда Гёдель доказал два фундаментальных ограничения. Следующий урок посвящён теореме о полноте - положительному результату, который предшествовал крушению.

• Теоремы Гёделя о неполноте — Прямое следствие анализа формальных систем - невозможность полноты для богатых теорий
• Неразрешимость и полнота — Алгоритмические следствия теорем Гёделя - связь с проблемой остановки

Вопросы для размышления

• Почему математики до XX века обходились без формальных систем? Что изменилось с открытием парадоксов теории множеств?
• Если доказательство - это программа, то что такое «баг» с логической точки зрения?
• Amazon использует TLA+ и находит баги в DynamoDB до деплоя. Это формальная верификация или просто тестирование? В чём разница?

Связанные уроки

• ml-03 — Предикатная логика - язык, на котором строятся формальные системы
• ml-05 — Теорема о полноте Гёделя - следующий результат после формальных систем
• dm-04 — Методы доказательств - практика того, что формальные системы описывают в теории
• dm-03 — Предикатная логика как живой пример аксиоматической системы
• fl-18-turing-machine