Наименование: | Исчисление секвенций (образовано от латинского слова: sequentia — последовательность). | ||||
Определение: | Исчисление секвенций — это одна из основных форм представления логических систем, применяемая в логике наряду с аксиоматическими системами и системами натурального (естественного) вывода. | ||||
Раздел: | Концепты философского дискурса Концепты научного дискурса | ||||
Дискурс: | Философия Наука | ||||
Субдискурс: | Логика | ||||
Текст статьи: © П. И. Быстров. Подготовка электронной публикации и общая редакция: © Центр гуманитарных технологий. Ответственный редактор: А. В. Агеев. Информация на этой странице периодически обновляется. Последняя редакция: 29.07.2025. | |||||
Исчисление секвенций — это одна из основных форм представления логических систем, применяемая в логике наряду с аксиоматическими системами (гилбертовского типа) и системами натурального (естественного) вывода. Термин «секвенция» введён в логику П. Герцем (1929) и заимствован Г. Генценом (1934), который впервые сформулировал в форме исчисления секвенций классическую и интуиционистскую логику предикатов первого порядка. Секвенция — это формальная запись отношения логической выводимости вида F → Θ, где F и Θ — последовательности (возможно пустые) разделённых запятыми формул. Вместо стрелки может использоваться «⊢» или любой другой знак логической выводимости. Левую часть секвенции называют антецедентом, а правую — сукцедентом. Содержательно в исходном генценовском варианте секвенция означает, что из конъюнкции формул, входящих в её антецедент, логически выводима дизъюнкция формул, входящих в её сукцедент. Например: A₁, … An, → B₁, … Bm означает A₁ & … & & An ⊢ B₁ ∨ … ∨ Bm; → B₁, … Bm означает ⊢ B₁, ∨ … ∨ Bm; A₁, … An, → означает ⊢ ¬ (Α₁ & … & & An); a секвенция, обе части которой пусты, может интерпретироваться как логическое противоречие. Исчисление секвенций состоит из двух главных компонентов: основной секвенции и правил заключения (иногда их называют правилами вывода). Основная секвенция в первоначальном генценовском варианте — это секвенция вида Особую роль в исчислении секвенций играет правило, называемое «сечением»:
Это единственное правило, в результате применения которого формула сечения (в данном случае A) вычёркивается из вывода. Все остальные правила сохраняют так называемое свойство подформульности вывода: все формулы, входящие в посылки конкретного правила, являются подформулами некоторых формул, входящих в заключение этого правила. Вывод в исчислении секвенций имеет форму дерева секвенций, построение которого начинается с основной секвенции (основных секвенций) и продолжается по правилам заключения. Секвенция считается выводимой в исчислении секвенций, если можно построить вывод, в котором она является последней (конечной) секвенцией. Строго говоря, деревья в исчислении секвенций являются не выводами в стандартном смысле термина «логический вывод», а метаконструкциями, при построении которых выполняются логические переходы от одних записей о выводимости к другим. Интерпретация секвенций при этом может быть различной, что открывает широкие возможности для исследования общих свойств формальных логических доказательств. С исчислением секвенций связан полученный Генценом фундаментальный результат современной логики — теорема об устранении сечения, или элиминационная теорема. В доказательстве этой теоремы Генцен заменяет сечение правилом смешения:
Где Δ* и Θ* не содержат формулы A, и показывает, что из любого вывода в исчислении секвенций классической и интуиционистской первопорядковой логики можно устранить все применения этого правила. Существует множество модификаций первоначального генценовского варианта исчисления секвенций для классической (см. Логика) и неклассических (см. Логики неклассические) логик. Методологически эти модификации сводятся к тому, что изменяется форма или/и число основных секвенций, форма или/и число правил заключения или/и вводятся ограничения на применения конкретных правил заключения при построении дерева вывода. Иногда изменяется само понятие секвенции и используются такие объекты, как «надсеквенции», «кортежи секвенций», «структуры» и другие. Достаточно прозрачен и эффективен подход к формулировке исчисления, при котором правилам заключения придаётся «глобальный» характер — их применение зависит не только от вида посылок, но Исчисления секвенций тесно связаны с табличными представлениями логических систем и обеспечивают естественный переход между синтаксическим и семантическим уровнями анализа неклассических логик. Они являются удобным аппаратом исследования количественных и качественных характеристик логических выводов и процедур поиска логических доказательств. | |||||
Библиография | |||||
---|---|---|---|---|---|
| |||||