Секвенциальное исчисление

Секвенциальное исчисление — это формальная система логического вывода, в которой доказательства строятся в виде деревьев или последовательностей секвенций. Секвенция, в свою очередь, представляет собой выражение вида Γ ⊢ Δ, где Γ и Δ — конечные множества (или последовательности) формул. Левая часть секвенции (Γ) называется антецедентом, а правая (Δ) — сукцедентом. Интуитивно, секвенция Γ ⊢ Δ означает, что из конъюнкции формул антецедента следует дизъюнкция формул сукцедента. Секвенциальное исчисление было разработано немецким логиком Герхардом Генценом в 1934 году как альтернатива гильбертовским исчислениям и как инструмент для доказательства непротиворечивости арифметики.

История

Предпосылки создания

К началу XX века в математической логике доминировали аксиоматические системы, восходящие к работам Джузеппе Пеано и Бертрана Рассела. В таких системах (например, в «Principia Mathematica») доказательство строилось из небольшого набора аксиом с помощью правил вывода, главным из которых было modus ponens. Однако такой подход имел существенные недостатки: доказательства были громоздкими, а связь между посылками и заключением часто оставалась неявной. Кроме того, аксиоматические системы плохо подходили для автоматического поиска доказательств и для метатеоретических исследований, таких как доказательство непротиворечивости.

Работы Герхарда Генцена

В 1934 году Герхард Генцен опубликовал статью «Untersuchungen über das logische Schließen» («Исследования о логическом выводе»), в которой предложил два новых типа исчислений: натуральный вывод и секвенциальное исчисление (LK для классической логики и LJ для интуиционистской). Основной целью Генцена было создание системы, в которой каждое правило вывода было бы «обратимым» в некотором смысле, что позволило бы доказывать теорему об устранении сечения (Hauptsatz). Эта теорема стала центральным результатом его работы: любое доказательство в секвенциальном исчислении может быть преобразовано в доказательство, не использующее правило сечения, что делает его аналитическим, то есть разбивающим сложные формулы на более простые. Генцен использовал это свойство для доказательства непротиворечивости арифметики Пеано (в 1936 году), что стало важным шагом в программе Гильберта.

Развитие после Генцена

После работ Генцена секвенциальные исчисления были адаптированы для многих неклассических логик: модальных, временных, субструктурных, линейных и других. В 1950-х годах Дана Скотт и другие логики разработали секвенциальные исчисления для модальных логик, введя понятие помеченных секвенций. В 1970-х годах Жан-Ив Жирар создал линейную логику, в основе которой лежит секвенциальное исчисление с особым вниманием к управлению ресурсами (количество использований каждой формулы). В 1980-х и 1990-х годах секвенциальные исчисления стали основой для многих систем автоматического доказательства теорем, таких как tableau-методы и системы, основанные на методе резолюций.

Основные понятия

Секвенция

Секвенция — это пара конечных последовательностей (или мультимножеств) формул, записываемая в виде Γ ⊢ Δ. Если Γ пусто, секвенция записывается как ⊢ Δ и означает, что дизъюнкция формул Δ является общезначимой. Если Δ пусто, секвенция Γ ⊢ означает, что конъюнкция формул Γ противоречива. В интуиционистской логике (LJ) сукцедент может содержать не более одной формулы, что отражает конструктивный характер доказательства.

Правила вывода

Правила вывода в секвенциальном исчислении делятся на три категории:

1. Аксиомы (начальные секвенции): обычно имеют вид A ⊢ A, где A — атомарная формула.
2. Логические правила: вводят логические связки (конъюнкцию, дизъюнкцию, импликацию, отрицание, кванторы) в антецедент или сукцедент. Например, правило введения конъюнкции в сукцедент (∧R) имеет вид: если Γ ⊢ Δ, A и Γ ⊢ Δ, B, то Γ ⊢ Δ, A ∧ B.
3. Структурные правила: управляют перестановкой, сокращением и ослаблением формул. Ключевым структурным правилом является сечение (cut): если Γ ⊢ Δ, A и A, Γ' ⊢ Δ', то Γ, Γ' ⊢ Δ, Δ'. Теорема об устранении сечения утверждает, что это правило можно исключить из любого доказательства без потери выводимости.

Дерево доказательства

Доказательство в секвенциальном исчислении обычно представляется в виде дерева, в корне которого находится доказываемая секвенция, а в листьях — аксиомы. Каждый внутренний узел соответствует применению одного из правил вывода.

Классификация секвенциальных исчислений

По типу логики

• Классическое секвенциальное исчисление (LK): допускает произвольное количество формул в сукцеденте. Подчиняется законам классической логики, включая закон исключённого третьего.
• Интуиционистское секвенциальное исчисление (LJ): сукцедент содержит не более одной формулы. Отражает конструктивную природу интуиционистской логики.
• Модальные секвенциальные исчисления: расширяют LK или LJ правилами для модальных операторов (□, ◇). Например, в модальной логике K правило введения □ в сукцедент требует, чтобы все формулы антецедента были модализированы.
• Субструктурные логики: ослабляют или модифицируют структурные правила. Например, в линейной логике запрещены правила ослабления и сокращения, что позволяет моделировать «потребление» ресурсов.
• Многозначные логики: секвенции могут содержать более двух частей, например, Γ ⊢ Δ | Θ, где вертикальная черта обозначает различные значения истинности.

По структуре секвенции

• Стандартные секвенции: Γ и Δ — множества или мультимножества формул.
• Помеченные секвенции: каждая формула снабжена меткой (например, миром в модальной логике или временной меткой).
• Вложенные секвенции: допускают вложение секвенций друг в друга, что используется для неклассических логик (например, для логик доказуемости).

Свойства и теоремы

Теорема об устранении сечения (Hauptsatz)

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

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

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

Разрешимость

Для пропозициональных логик (как классической, так и интуиционистской) секвенциальное исчисление даёт разрешимую процедуру: существует алгоритм, который за конечное число шагов определяет, выводима ли секвенция. Для логики первого порядка процедура полуразрешима: если секвенция выводима, алгоритм найдёт доказательство, но если нет, он может работать бесконечно.

Применение

Доказательство непротиворечивости

Генцен использовал секвенциальное исчисление для доказательства непротиворечивости арифметики Пеано (в 1936 году). Он показал, что любое доказательство в арифметике может быть преобразовано в нормальную форму, не содержащую сечения, и что такая нормальная форма не может привести к противоречию. Это доказательство было ограниченным (использовалась трансфинитная индукция до ε₀), но оно стало важным шагом в метаматематике.

Автоматическое доказательство теорем

Секвенциальные исчисления лежат в основе многих систем автоматического доказательства, таких как:

• Tableau-методы: по сути, являются обратным применением правил секвенциального исчисления (поиск доказательства от корня к листьям).
• Системы, основанные на методе резолюций: хотя резолюция формально не является секвенциальным исчислением, она может быть получена из него путём устранения структурных правил.
• Интерактивные доказатели: такие как Coq, Isabelle, Lean, используют секвенциальные исчисления (или их варианты) для представления доказательств.

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

Секвенциальное исчисление лежит в основе изоморфизма Карри — Ховарда — Ламбека, который устанавливает соответствие между логическими выводами и программами. В частности, интуиционистское секвенциальное исчисление (LJ) соответствует типизированному λ-исчислению, а правило сечения — подстановке терма. Это используется в языках программирования с зависимыми типами (Agda, Idris) и в системах типов для функциональных языков.

Семантика и метатеория

Секвенциальные исчисления используются для изучения свойств логик: разрешимости, интерполяции, свойства Бета, свойства дизъюнктивности. Например, свойство дизъюнктивности для интуиционистской логики (если ⊢ A ∨ B выводимо, то выводимо ⊢ A или ⊢ B) легко доказывается с помощью устранения сечения.

Критика и ограничения

Сложность доказательств

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

Ограничения для неклассических логик

Для некоторых неклассических логик (например, некоторых модальных логик с аксиомами, не являющимися правилами) построение адекватного секвенциального исчисления может быть затруднено. В таких случаях используются более сложные структуры, такие как вложенные секвенции или гибридные системы.

Неполнота для арифметики

Как показала вторая теорема Гёделя о неполноте, никакое секвенциальное исчисление, достаточно мощное для выражения арифметики Пеано, не может доказать собственную непротиворечивость (если она непротиворечива). Доказательство Генцена обходило это ограничение, используя внешние средства (трансфинитную индукцию).

См. также

• Натуральный вывод
• Теорема об устранении сечения
• Линейная логика
• Изоморфизм Карри — Ховарда
• Логическое программирование

Источники

1. Gentzen, G. (1934). «Untersuchungen über das logische Schließen». Mathematische Zeitschrift, 39(1), 176–210.
2. Gentzen, G. (1936). «Die Widerspruchsfreiheit der reinen Zahlentheorie». Mathematische Annalen, 112(1), 493–565.
3. Takeuti, G. (1987). «Proof Theory». 2nd ed. North-Holland.
4. Troelstra, A. S., & Schwichtenberg, H. (2000). «Basic Proof Theory». 2nd ed. Cambridge University Press.
5. Girard, J.-Y. (1987). «Linear Logic». Theoretical Computer Science, 50(1), 1–102.
6. Новиков, П. С. (1973). «Элементы математической логики». Наука.