Натуральный вывод и системы Генцена

Мотивация: как формализовать реальные математические рассуждения?

Система аксиом Гильберта (A1, A2, A3 + MP) технически адекватна, но неудобна для работы: реальные математики не рассуждают «выведи p→p за пять шагов». Натуральный вывод (Gentzen, 1935) — система, имитирующая привычную математическую практику: вводим гипотезы, разбираем случаи, применяем правила введения и устранения связок. Это основа современных систем верификации доказательств (Coq, Lean, Agda).

Правила натурального вывода

Вывод — дерево, в корне — доказываемая формула, в листьях — гипотезы (могут быть «разряжены»).

Конъюнкция (∧):

∧-введение (∧I): из φ и ψ ⊢ φ ∧ ψ.
∧-устранение (∧E₁): из φ ∧ ψ ⊢ φ. (∧E₂): ⊢ ψ.

Импликация (→):

→-введение (→I): если из [φ] доказано ψ (гипотеза φ разряжается) → ⊢ φ → ψ.
→-устранение (modus ponens): из φ→ψ и φ ⊢ ψ.

Дизъюнкция (∨):

∨-введение: из φ ⊢ φ ∨ ψ (и из ψ ⊢ φ ∨ ψ).
∨-устранение: из φ∨ψ, [φ]⊢χ, [ψ]⊢χ ⊢ χ (разбор случаев).

Отрицание: ¬φ := φ→⊥. Из φ и ¬φ ⊢ ⊥. Из [¬φ]⊢⊥ ⊢ φ (reductio ad absurdum — в классике).

Кванторы (ЛПП):

∀-введение: из φ(y) (y не свободна в гипотезах) ⊢ ∀x φ(x).
∀-устранение: из ∀x φ(x) ⊢ φ(t) для любого терма t.
∃-введение: из φ(t) ⊢ ∃x φ(x).
∃-устранение: из ∃xφ(x) и [φ(y)⊢χ] (y не свободна в χ) ⊢ χ.

Соответствие Карри–Говарда

Изоморфизм типов и доказательств:

Логика	Теория типов (λ-исчисление)
Формула φ	Тип A
Доказательство φ	Терм t: A
φ → ψ	Функциональный тип A → B
φ ∧ ψ	Произведение A × B (пара)
φ ∨ ψ	Сумма A + B (объединение)
⊥	Пустой тип

Следствие: конструктивное доказательство φ → ψ — это программа, преобразующая доказательство φ в доказательство ψ. Coq и Agda: писать программы = строить математические доказательства.

Численный пример

Задача: Доказать в натуральном выводе: (p ∧ q) → (q ∧ p) (коммутативность конъюнкции).

Шаг 1. Вводим гипотезу [h: p ∧ q].

Шаг 2. Применяем ∧E₂ к h: получаем q.

Шаг 3. Применяем ∧E₁ к h: получаем p.

Шаг 4. Применяем ∧I к q и p: получаем q ∧ p.

Шаг 5. Применяем →I, разряжая гипотезу h: получаем (p ∧ q) → (q ∧ p). ■

Дерево вывода (схематически):

[p ∧ q]ʰ → ∧E₂ → q; [p ∧ q]ʰ → ∧E₁ → p; затем ∧I даёт q ∧ p; правило →I разряжает гипотезу h, получая (p ∧ q) → (q ∧ p).

Соответствующий λ-терм: λh: A×B. ⟨π₂(h), π₁(h)⟩ — функция, берущая пару (h.first, h.second) и возвращающая (h.second, h.first). Это в точности swap: A×B → B×A.

Дополнительные аспекты

Теория доказательств (proof theory) — раздел логики, изучающий доказательства как формальные объекты. Гильбертовские системы дают аксиоматический подход; натуральный вывод Генцена ближе к интуитивным рассуждениям; секвенциальное исчисление LK/LJ позволяет доказать теорему о нормализации (cut-elimination). Из cut-elimination следуют непротиворечивость арифметики (Генцен 1936, через ε₀-индукцию), интерполяционная теорема Крейга и теорема Эрбрана. Современные приложения: системы Coq, Lean, Agda — интерактивные пруверы на базе теории типов и принципа Карри–Говарда (программы = доказательства, типы = формулы). На Lean уже формализованы теоремы Ферма, классификация конечных простых групп (фрагменты), большие куски analysis textbook, что открывает эпоху верифицированной математики.

Реальное приложение

Coq — язык доказательств и программирования, основанный на натуральном выводе с зависимыми типами. Доказательство теоремы Фейта–Томпсона в Coq (Gonthier et al., 2012): 150 000 строк, 6 лет работы. Используется в верификации ядра ОС (CompCert — верифицированный компилятор C).

Связь с другими разделами математики

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

В алгебре натуральный вывод тесно связан с теорией категорий. Результаты Ламбека показывают, что доказательства в интуиционистской логике соответствуют морфизмам в картецианско-замкнутых категориях, а правила натурального вывода переводятся в композицию и экспоненциальные объекты. Обобщение на линейную логику Жирара приводит к моноидально-замкнутым категориям и, далее, к моделям теории операторов и квантовой логики.

В топологии логика высших порядков и зависимые типы (как обобщение натурального вывода) реализуются в унивалентной основе Воэводского: типы рассматриваются как пространства, термы — как точки, а равенства — как пути. Здесь правила введения и устранения кванторов и конструкторов типов описывают топологические операции, а соответствие Карри–Говарда–Ламбека превращается в мост между гомотопической алгеброй и формальной логикой.

В теории вероятностей логика с натуральным выводом применяется через стохастический λ-исчислительный аппарат: работы Джонса и Моргана связывают доказательства с вероятностными программами, а нормализация выводов интерпретируется как процесс выборки распределений. В численных методах анализ доказательств теорем о сходимости и устойчивости позволяет, через программы-экстракторы (Kreisel, Kohlenbach), получать явные оценочные алгоритмы и мажоранты скоростей сходимости итерационных схем.

Историческая справка и развитие идеи

Предпосылки натурального вывода прослеживаются в работах Фреге (Begriffsschrift, 1879) и последующей аксиоматике Гильберта (Grundlagen der Geometrie, 1899), где уже присутствует идея управляемого вывода из явно выписанных предпосылок. Однако именно Герхард Генцен в статье «Untersuchungen über das logische Schließen» (Mathematische Zeitschrift, 1934–1935) формализовал натуральный вывод и секвенциальное исчисление как два взаимосвязанных формата доказательства. Мотивацией Генцена были программы Гильберта по обоснованию арифметики и потребность в синтаксическом анализе доказательств. Его теорема об устранении правила сечения (1935) и последующая работа 1936 года о непротиворечивости арифметики Пеано через трансфинитную индукцию до ординала ε0 стали центральными результатами ранней теории доказательств. В середине XX века идеи Генцена развивали Пауэль Лоренцен, Стивен Клини, Курт Шютте, систематизировав различные варианты натурального вывода и секвенциальных систем для интуиционистской и классической логики.