Секвенция (логика)

Термин «секвенция» происходит от слова sequent (последовательность). Он введён в логику П.Герцем (1929) и заимствован Г.Генценом, который впервые сформулировал в форме исчисления секвенций классическую и интуиционистскую логику предикатов первого порядка.

Секвенция — это формальная запись отношения логической выводимости вида F→Θ, где Г и Θ — последовательности (возможно пустые) разделенных запятыми формул. Вместо стрелки может использоваться «⊢» или любой другой знак логической выводимости. Левую часть секвенции называют антецедентом, а правую — сукцедентом.

Содержательно в исходном генценовском варианте секвенция означает, что из конъюнкции формул, входящих в её антецедент, логически выводима дизъюнкция формул, входящих в её сукцедент.

Например:

А1, …, Аn, → В1, …, Вm означает А1& … & & Аn ⊢В1∨… ∨Bm;

→ В1, …, Bm означает ⊢ В1,∨… ∨Bm;

A1, …, Аn, → означает ⊢ (Α1& …& &An),

a секвенция, обе части которой пусты, может интерпретироваться как логическое противоречие.

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