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

Материал из свободной русской энциклопедии «Традиция»
Перейти к: навигация, поиск

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


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

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

Например:

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

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


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

Ссылки[править]

  1. П. И. Быстров. Математическая теория логического вывода. М., 1969.