Философская энциклопедия - исчисление секвенций

ИСЧИСЛЕНИЕ СЕКВЕНЦИЙ — одна из основных форм представления логических систем, применяемая в логике наряду с аксиоматическими системами (гильбертовского типа) и системами натурального (естественного) вывода. Термин “секвенция” происходит от слова sequent (последовательность). Он введен в логику П. Герцем (1929) и заимствован Г. Генценом, который впервые сформулировал в форме исчисления секвенций классическую и интуиционистскую логику предикатов первого порядка.

Секвенция — это формальная запись отношения логической выводимости вида Г-” Θ, где Г и θ — последовательности (возможно пустые) разделенных запятыми формул. Вместо стрелки может использоваться “ι—” или любой другой знак логической выводимости. Левую часть секвенции называют антецедентом, а правую — сукцедентом. Содержательно в исходном генценовском варианте секвенция означает, что из конъюнкции формул, входящих в ее антецедент, логически выводима дизъюнкция формул, входящих в ее сукцедент. Напр.:А|, ...,Ап-”В),..., Вп, означает А| &... &&А„ i—B|V...vByn;-”Bi,..., Вщ означает l— B|V ... νΒη,,Αι, ...,Αη-” означает ι— -ι(Αι& ...& &Αη); а секвенция, обе части которой пусты, может интерпретироваться как логическое противоречие.

Исчисление секвенций состоит из двух главных компонентов: основной секвенции и правил заключения (иногда их называют правилами вывода). Основная секвенция в первоначальном генценовском варианте — это секвенция вида А->А, где А — формула, но могут применяться основные секвенции и другого вида. Правила заключения делятся на два типа: логические и структурные. Логические правила заключения в свою очередь делятся на правила введения логического знака в антецедент и правила введения логического знака в сукцедент секвенции. По логическому правилу из формул, входящих в его посылки (боковых формул), в заключении с помощью введения логического знака получается более сложная формула (главная формула). Таким образом, логические правила позволяют строить сложные формулы из более простых. Число логических правил в исчислении секвенций определяется числом используемых в данном исчислении логических констант. Структурные правила (перестановка, сокращение и утончение) влияют не на структуру отдельных формул, а на структуру секвенций. В результате применения этих правил вхождения формул в антецедент или сукцедент секвенции переставляются, сокращаются или добавляются. Логические и структурные правила заключения для классической и интуиционистской логик симметричны в том смысле, что каждому антецедентному (сукцедентному) правилу соответствует в точности одно сукцеденгное (антецедентное) правило.

Особую роль в исчислении секвенций играет правило, называемое “сечением”: Γ-”Θ,Α Α,Δ->Ψ Γ,Δ