Общая характеристика исчисления секвенций
Секвенции – это формальная запись отношения логической выводимости, имеющая вид F → Θ, где F и Θ являются последовательностями (в частном случае, пустыми) из формул, разделенных запятыми.
В записи секвенции может использоваться не только символ «→» - допустим любой символ, обозначающий логическую выводимость. Части секвенции:
- антецедент – левая часть,
- сукцедент – правая часть.
В содержательном смысле (в соответствии с исходным генценовским вариантом) секвенция значит, что из конъюнкции формул, образующих антецедент, логически выводится дизъюнкция формул, образующих сукцедент. Если обе части секвенции пусты, можно интерпретировать ее как логическое противоречие.
Исчисление секвенций является одной из основных форм представления логических систем. В логике оно применяется наряду с системами гилбертовского типа (аксиоматическими) и системами естественного (натурального) вывода. Термин «секвенция» ввел П. Герц, а затем заимствовал Г. Генцен, впервые сформулировавший классическую и интуиционистскую логику предикатов первого порядка в форме исчисления секвенций.
В исчислении севенций выделяют два главных компонента:
- основная секвенция. В исходном генценовском варианте это секвенция, имеющая вид A → A (А – это формула). В современном варианте применяются и другие виды основной секвенции;
- правила заключения (также называемые «правила вывода»). Существует два типа правил вывода – логические и структурные. Логические правила служат для того, чтобы из более простых формул строить более сложные. Они бывают двух видов – первый вид нужен для того, чтобы вводить логический знак в антецедент, а второй – чтобы вводить логический знак в сукцедент. Логическое правило обеспечивает получение главной (более сложной) формулы из боковых формул (формул, входящих в посылки) путем введения логического знака. В исчислении секвенций число логических правил зависит от числа констант, используемых в этом исчислении. Второй тип правил – структурные – влияют на структуру секвенций, а не на структуру отдельных формул. К структурным правилам относят перестановку, сокращение и утончение. Результатом применения этих правил становится перестановка, сокращение или добавление формул в антецеденте или сукцеденте секвенции. Симметрия логических и структурных правил заключения в классической и интуиционистской логиках выражается в том, что каждому сукцедентному (антецедентному) правилу соответствует строго одно антецедентное (сукцедентное) правило.
Исчисление секвенций и поиск контрпримера
Исчисление секвенций играет важную роль в теории доказательств, поскольку оно удобно для проведения анализа синтаксической структуры вывода.
Рассмотрим задачу, состоящую в поиске контрпримере. Пусть имеется некоторая формула А и предполагается, что это не тавтология. Стоит задача найти такие значения переменных, которые обращают формулу в ложь. Естественный путь решения этой задачи – изучение структуры формулы А, например:
- если это импликация, нужно искать значения переменных, обращающие посылку в ложь, а следствие в истину;
- если это дизъюнкция, нужно искать значения переменных, обращающие оба дизъюнкта в ложь;
- если это конъюнкция, нужно искать значения переменных, обращающие в ложь любой из конъюнктов.
Таким образом, задача поиска для формулы А контрпримера сводится к подобным задачам поиска, в рамках которых необходимо обеспечить определенную истинностную характеристику (истина или ложь) других формул.
Каждая секвенция может быть связана с задачей поиска таких значений переменных, при которых все входящие в антецедент формулы истинны, а все входящие в сукцедент ложны. При этом конъюнкцию пустого множества считают тождественно истинной, а дизъюнкцию считают тождественно ложной.
В таком случае задача поиска контрпримера для формулы А может быть перформулирована как задача поиска контрпримера для секвенции, состоящей из пустого множества и А. Задача поиска контрпримера для секвенции решается по определенным правилам. На их основе постепенно выстраивается дерево поиска контрпримера.
Особая роль в исчислении секвенций отводится правилу, называемому сечением. Это правило является единственным, обеспечивающим исключение из вывода формулы сечения. Для всех остальных правил справедливо свойство подформульности вывода, заключающееся в следующем: все формулы, входящие в посылки конкретного правила, являются подформулами некоторых формул, входящих в заключение этого правила.
Секвенция является выводимой в том и только том случае, если для нее не существует контрпримера.
В исчислении секвенций вывод принимает форму дерева секвенций. Построение этого дерева начинается с основной секвенции и осуществляется по правилам заключения. Если удается построить вывод, в котором рассматриваемая секвенция является конечной (последней), то секвенция признается выводимой. Строго говоря, такие деревья – это не то, что обычно понимается под выводом, а метаконструкции, обеспечивающие выполнение логических переходов между записями о выводимости. При этом секвенции могут интерпретироваться по-разному, что открывает широкие возможности при исследовании общих свойств формальных логических доказательств.
В частности, если рассматриваемая изначально формула А – это тавтология, то секвенция из пустого множества и А в исчислении секвенций выводима.
Существует множество модификаций изначального генценовского варианта исчисления секвенций. Методологически эти модификации сводятся к изменению формы или числа основных секвенций либо правил заключения и введению ограничения на применение при построении дерева вывода конкретных правил заключения. Иногда изменяют само понятие секвенции и используют такие объекты, как «надсеквенции», «кортежи секвенций», «структуры» и другие. Достаточно прозрачен и эффективен подход к формулировке исчисления, при котором правилам заключения придается «глобальный» характер – их применение зависит не только от вида посылок, но и от состояния выводов этих посылок.
