Теория доказательств — раздел математической логики, изучающий формальные системы вывода и структуру доказательств. Основана Давидом Гильбертом в начале XX века как часть программы формализации математики. Герхард Генцен в 1934-1935 годах создал естественный вывод и секвенциальное исчисление — две ключевые системы, на которых строится современная теория.
Представьте доказательство как дерево: аксиомы — корни, правила вывода — ветви, теорема — вершина. Теория доказательств изучает структуру этого дерева: можно ли сократить ветви (нормализация)? Какие правила необходимы (полнота системы)? Можно ли автоматизировать построение доказательств?
Системы вывода
Аксиоматическая система (Гильберт, 1920-е) — набор аксиом и правил вывода. Пример: логика высказываний с аксиомами A → (B → A), (A → (B → C)) → ((A → B) → (A → C)) и правилом modus ponens (из A и A → B следует B). Доказательство — последовательность формул, каждая из которых либо аксиома, либо получена правилами.
Естественный вывод (Генцен, 1934) — система без аксиом, только правила введения и удаления логических связок. Для импликации:
- →-введение: Если из допущения A выводится B, то выводится A → B (правило закрытия допущения).
- →-удаление: Из A и A → B следует B (modus ponens).
Естественный вывод ближе к математической практике: доказательства структурированы, используют локальные допущения ("предположим A, тогда...B, следовательно A → B").
Секвенциальное исчисление (Генцен, 1934) — система с секвенциями Γ ⊢ Δ, где Γ — множество посылок, Δ — множество заключений. Секвенция истинна, если из конъюнкции Γ следует дизъюнкция Δ. Правила разбивают сложные формулы на части, строя дерево вывода снизу вверх.
Теорема об устранении сечения
Генцен в 1935 году доказал для секвенциального исчисления: любое доказательство можно преобразовать в доказательство без правила сечения (cut). Правило сечения: из Γ ⊢ A, Δ и A, Π ⊢ Σ следует Γ, Π ⊢ Δ, Σ ("лемма" A используется, но исчезает).
Устранение сечения — аналог нормализации в естественном выводе: доказательство становится "прямым", без обходных лемм. Следствия:
- Консистентность: если ⊢ A и ⊢ ¬A, после устранения сечения получаем противоречие с пустым заключением — невозможно.
- Разрешимость для некоторых логик: можно систематически искать доказательство (обратный поиск сверху вниз).
Изоморфизм Карри-Ховарда
Хаскелл Карри (1934) и Уильям Ховард (1969) обнаружили: доказательства соответствуют программам, формулы — типам. Импликация A → B — тип функции, принимающей A и возвращающей B. Доказательство A → B — программа этого типа.
Примеры соответствия:
- A → A (тождественная функция id(x) = x).
- A → (B → A) (константная функция const(x)(y) = x).
- (A → B → C) → (A → B) → A → C (аппликативная комбинаторная логика S-комбинатор).
Изоморфизм лежит в основе языков с зависимыми типами (Coq, Agda, Lean): доказательство теоремы = программа нужного типа. Проверка доказательства = проверка типов компилятором.
Нормализация доказательств
В естественном выводе доказательство нормализуемо, если можно устранить "обходные пути" (редексы — пары введение/удаление). Нормальное доказательство — без редексов, "кратчайший путь" от аксиом к заключению.
Теорема о нормализации (Генцен, 1935; Правиц, 1965): В интуиционистской и классической логике каждое доказательство нормализуемо. Процесс нормализации конечен (сильная нормализация).
Нормализация важна для вычислений: по изоморфизму Карри-Ховарда это соответствует выполнению программы. Ненормализуемость означала бы зацикливание.
Программа Гильберта
Давид Гильберт в 1920-х годах предложил программу: доказать непротиворечивость математики финитными (конечными, конструктивными) методами. Теория доказательств должна была показать: из аксиом арифметики нельзя вывести противоречие.
Теорема Гёделя о неполноте (1931) разрушила программу: в достаточно мощных теориях (арифметика Пеано) непротиворечивость недоказуема внутри системы. Но теория доказательств выжила, переключившись на изучение структуры доказательств, а не абсолютной обоснованности.
Ординальный анализ
Генцен в 1936 году доказал непротиворечивость арифметики Пеано, используя трансфинитную индукцию до ординала ε₀ (первый ординал, для которого ω^α = α). Это обошло теорему Гёделя, так как метод не формализуем в PA.
Ординальный анализ измеряет "силу" теории числом, показывающим сложность доказательств. Чем больше ординал, тем мощнее теория. Например:
- Примитивная рекурсивная арифметика: ω^ω.
- Арифметика Пеано: ε₀.
- Теория множеств ZFC: не имеет известного ординала (слишком сложна).
Линейная логика
Жан-Ив Жирар в 1987 году создал линейную логику — систему, где ресурсы (посылки) используются ровно один раз. В классической логике из A следует A ∧ A (дубликация), A ∨ A можно упростить до A (сжатие). В линейной логике это запрещено.
Применение: Моделирование ресурсов в программировании (память, файловые дескрипторы). Rust использует идеи линейной логики для управления владением (ownership): значение можно переместить, но не дублировать произвольно.
Автоматическое доказательство
Теория доказательств — основа автоматических доказывателей теорем (ATP). Методы:
Резолюция (Робинсон, 1965) — правило вывода для КНФ: из C ∨ A и ¬A ∨ D следует C ∨ D. Полный метод для логики первого порядка: если формула выводима, резолюция найдёт доказательство (но может не остановиться, если формула невыводима).
Tableau-методы — систематический поиск противоречий. Строят дерево возможных моделей, отсекая ветви с противоречиями. Если все ветви закрыты — формула общезначима.
SMT-решатели (Satisfiability Modulo Theories) — расширение SAT теориями (арифметика, массивы, битовые векторы). Используются в верификации программ (например, Z3 от Microsoft Research).
Proof assistants
Системы интерактивного доказательства (Coq, Isabelle, Lean, Agda) позволяют формализовать математику. Примеры формализованных теорем:
- Теорема о четырёх красках (Жорж Гонтье, Coq, 2005) — первое компьютерное доказательство сложной теоремы.
- Формализация Великой теоремы Ферма (Lean, Kevin Buzzard et al., в процессе).
- CompCert (верифицированный компилятор C, Coq) — корректность доказана формально.
Конструктивная математика
Интуиционистская логика (Брауэр, 1920-е) отвергает закон исключённого третьего A ∨ ¬A и двойное отрицание ¬¬A → A. Доказательство ∃x P(x) требует конструктивного предъявления x, а не доказательства от противного.
Теория доказательств интуиционистской логики — основа конструктивной математики. Изоморфизм Карри-Ховарда даёт программы-свидетели: доказательство существования = алгоритм построения объекта.