Секвенциальное исчисление и теорема Генцена

Мотивация: симметрия и нормализация доказательств

Натуральный вывод несимметричен: гипотезы слева, заключение справа, и введение/устранение связок асимметрично. Секвенциальное исчисление (Gentzen, 1935) — симметричная система, где доказательства имеют явную структуру, удобную для мета-теоремы. Главный результат — теорема об устранении сечений — говорит, что любое доказательство можно «нормализовать»: убрать «заимствование лемм».

Секвенции и исчисление LK

Секвенция: Γ ⊢ Δ (читается «из гипотез Γ следует хотя бы одна из Δ»). Γ и Δ — мультимножества формул.

Аксиома: φ ⊢ φ (тождественная секвенция).

Структурные правила:

Ослабление (Weakening): из Γ ⊢ Δ → Γ, φ ⊢ Δ (и аналогично справа).
Сжатие (Contraction): из Γ, φ, φ ⊢ Δ → Γ, φ ⊢ Δ.
Обмен (Exchange): перестановка формул в Γ или Δ.

Логические правила (пример для ∧ справа): из Γ ⊢ Δ, φ и Γ ⊢ Δ, ψ → Γ ⊢ Δ, φ∧ψ.

Правило сечения (Cut): из Γ ⊢ Δ, φ и φ, Π ⊢ Λ → Γ, Π ⊢ Δ, Λ. Это «использование леммы φ».

Теорема об устранении сечений (Cut Elimination / Hauptsatz)

Теорема (Gentzen, 1935): Любое доказательство в LK можно преобразовать в доказательство без правила Cut — в нормальной форме.

Следствие — свойство подформул (Subformula Property): В нормальном доказательстве все формулы — подформулы доказываемой секвенции. Нельзя «изобрести» вспомогательные формулы, которых нет в условии.

Доказательство: двойная индукция — по «рангу» сечения (сложности формулы φ в Cut) и числу сечений. Ключевые случаи: «ключевые сечения» — когда φ введена с одной стороны и устранена с другой — локально преобразуются в доказательство без Cut.

Приложения

Консистентность PA: Генцен (1936) с помощью трансфинитной индукции до ε₀ = ω^{ω^{ω^{...}}} доказал непротиворечивость арифметики Пеано PA. Это не противоречит теореме Гёделя: PA не доказывает Con(PA) внутри себя, но внешняя система (с ε₀-индукцией) может.

Автоматическое доказательство: Subformula Property → поиск доказательства — конечная задача (число кандидатов ограничено): основа алгоритма Prolog и таблиц Бет.

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

Задача: Вывести φ ∧ ψ ⊢ φ ∨ ψ в LK без правила Cut.

Шаг 1. Аксиома: φ ⊢ φ.

Шаг 2. ∨-введение справа: φ ⊢ φ ∨ ψ.

Шаг 3. Аксиома: ψ ⊢ ψ.

Шаг 4. ∨-введение справа: ψ ⊢ φ ∨ ψ.

Шаг 5. ∧-устранение слева (две посылки из шагов 2 и 4): φ ∧ ψ ⊢ φ ∨ ψ. ■

Запись дерева вывода (схематически): аксиомы φ ⊢ φ и ψ ⊢ ψ → правилом ∨R₁ получаем φ ⊢ φ∨ψ и ψ ⊢ φ∨ψ → применением ∧L объединяем посылки в φ∧ψ ⊢ φ∨ψ.

Проверка Subformula Property: все формулы в доказательстве (φ, ψ, φ∧ψ, φ∨ψ) — подформулы доказываемой φ∧ψ ⊢ φ∨ψ ✓.

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

Секвенциальное исчисление LK Генцена выражает доказательства через секвенты вида Γ ⊢ Δ (из посылок Γ выводимо хотя бы одно из Δ). Все правила симметричны: для каждого логического оператора есть правило введения слева и справа. Главный результат — теорема Hauptsatz (1934) о том, что правило сечения cut (соответствующее лемме «если из A выводимо B, а из B выводимо C, то из A выводимо C») избыточно: любое доказательство преобразуется в cut-free форму. Это даёт subformula property и доказывает консистентность теории. На практике cut-elimination лежит в основе автоматических доказателей: tableaux-методы, focused proofs, deep inference используют структурную нормальную форму для эффективного поиска.

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

Верификация программ с зависимыми типами (Lean, Isabelle): Cut Elimination означает, что доказательства могут быть «нормализованы» и их можно эффективно проверить. Без этой теоремы верификатор мог бы зависнуть при проверке корректности доказательства.

Исчисление LK Генцена строит доказательства как структурированные деревья секвенций, что позволяет провести строгое доказательство теоремы о нормализации без обращения к семантике. Эта теорема открыла дверь в современную автоматизированную математику: на её основе работают системы tableaux, focused proofs и focused linear logic, а также большинство интерактивных доказателей теорем.

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

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

В функциональном анализе и топологии секвенциальные системы лежат под «программой Гильберта–Бернайса–Гиреля»: доказательства теорем типа Хана–Банаха или Тихонова анализируются с точки зрения извлекаемости конструктивного содержимого через методы proof mining (Ульрих Кёлер, Ульрих Кохен, Ульрих Кёлер–Крейсл). Cut-elimination здесь играет роль механизма, отделяющего чисто логические шаги от употребления аксиомы выбора или полноты.

В теории вероятностей связь проявляется через логики вероятностного вывода, где секвенциальные системы для логик с мерами (работы Фагина и Халперна) используют модифицированные правила сечения, а их частичная элиминация даёт эффективные процедуры вывода ограничений на вероятности. В численных методах логические основы верификации алгоритмов (методы Флойда–Хоара, логика динамических систем Прана, система PVS) используют вариации секвенциальных исчислений: доказательство корректности схем интегрирования или методов конечных элементов формализуется в виде деревьев без сечений, а подформульное свойство гарантирует, что при проверке не появятся дополнительные «скрытые» условия.

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

Первые предвестники секвенциального подхода появляются у Школьма и Гильберта в 1920-е годы, но сам термин и строгая система LK были введены Герхардом Генценом в статьях 1934–1935 годов в «Mathematische Zeitschrift». Мотивация шла от программы Гильберта: требовалось дать финистический анализ классической математики и показать непротиворечивость арифметики. Генцен предложил два параллельных формализма — натуральный вывод и секвенциальное исчисление — однако именно второе позволило сформулировать Hauptsatz. Уже в 1936 году в той же серии работ он применил устранение сечений для доказательства непротиворечивости арифметики Пеано посредством трансфинитной индукции до ε₀. После Второй мировой войны идеи Генцена были переосмыслены в трудах Гентенка, Лоренцена, Шютте и Тайтса. Лоренцен развивал диалогические и операциональные интерпретации секвенций, Шютте в книге «Beweistheorie» (1960) подробно систематизировал технику cut-elimination для широких классов теорий. В 1960–1970-е годы работы Питера Шольце и Жан-Ива Жирара связали секвенциальные исчисления с линейной логикой и λ-исчислением, а Гирардино показал связь cut-elimination с нормализацией в типизированных λ-системах.