Исчисление секвенций

Исчисление секвенций (англ. Sequent calculus) — система формального вывода формул логики первого порядка (и как частного случая логики высказываний) предложенная немецким логиком Герхардом Генценом. Генценом были разработаны несколько эквивалентных вариантов исчисления секвенций.

Концептуальный принцип

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

Это формальная система, в которой в алфавит языка логики (включающий операции ∨, &, ¬ и кванторы ∀ и ∃) добавлен символ следования, обозначаемый ├, который читается «выводимо» или «доказуемо». Правила вывода a├ b (b выводима из a) применяются непосредственно к формулам, а не к таблицам истинности, позволяя из истинности одних формул делать вывод об истинности других формул. Символы a, b в правиле вывода обозначают одну или несколько формул; a называется условием (антецедентом), а b — следствием (сукцедентом, консеквентом). Если в условии или следствии формул несколько, то они записываются через запятую. Представляют интерес только такие правила вывода, с помощью которых на основании истинности всех формул, входящих в условие правила вывода, можно при любой интерпретации сделать заключение об истинности всех формул, входящих в следствие правила вывода. Обычно такие правила называют состоятельными.

Если U₁,U₂, …, U_k, C — формулы, то выражения вида U₁,U₂, …, U_k├ C называются секвенциями.

Вывод в исчислении секвенций — это конечная последовательность секвенций ∑₁, ∑₂, …, ∑_k такая, что для каждого i , 1 ≥ i ≤ k, секвенция ∑_i есть либо аксиома, либо непосредственное следствие из предыдущих секвенций по правилам вывода.

Исчисление секвенций является корректным и полным. То есть все формулы, которые можно вывести с его помощью является логически значимые и все логически значимые формулы можно вывести с помощью исчисления секвенций.

Правила вывода

Правила вывода для исчисления секвенций делятся на две категории: логические и структурные. В правилах вывода посылки, то есть секвенции, написанные над чертой, называются верхними секвенциями, а заключение, то есть секвенция, написанная ниже черты, — нижней секвенцией. В каждом двухпосылочном правиле имеются две верхние секвенции — левая (L) и правая (R).

Ниже представлены правила вывода для LK-исчисления (нем. «Klassische Prädikatenlogik» — логики предикатов), предложенного Генценом в 1934 году.

Аксиома:	Сечение:
$\cfrac{\qquad }{ A \vdash A} \quad (I)$	$\cfrac{\Gamma \vdash \Delta, A \qquad A, \Sigma \vdash \Pi} {\Gamma, \Sigma \vdash \Delta, \Pi} \quad (\mathit{Cut})$
Left логические правила:	Right логические правила:
$\cfrac{\Gamma, A \vdash \Delta} {\Gamma, A \and B \vdash \Delta} \quad ({\and}L_1)$	$\cfrac{\Gamma \vdash A, \Delta}{\Gamma \vdash A \or B, \Delta} \quad ({\or}R_1)$
$\cfrac{\Gamma, B \vdash \Delta}{\Gamma, A \and B \vdash \Delta} \quad ({\and}L_2)$	$\cfrac{\Gamma \vdash B, \Delta}{\Gamma \vdash A \or B, \Delta} \quad ({\or}R_2)$
$\cfrac{\Gamma, A \vdash \Delta \qquad \Sigma, B \vdash \Pi}{\Gamma, \Sigma, A \or B \vdash \Delta, \Pi} \quad ({\or}L)$	$\cfrac{\Gamma \vdash A, \Delta \qquad \Sigma \vdash B, \Pi}{\Gamma, \Sigma \vdash A \and B, \Delta, \Pi} \quad ({\and}R)$
$\cfrac{\Gamma \vdash A, \Delta \qquad \Sigma, B \vdash \Pi}{\Gamma, \Sigma, A\rightarrow B \vdash \Delta, \Pi} \quad ({\rightarrow }L)$	$\cfrac{\Gamma, A \vdash B, \Delta}{\Gamma \vdash A \rightarrow B, \Delta} \quad ({\rightarrow}R)$
$\cfrac{\Gamma \vdash A, \Delta}{\Gamma, \lnot A \vdash \Delta} \quad ({\lnot}L)$	$\cfrac{\Gamma, A \vdash \Delta}{\Gamma \vdash \lnot A, \Delta} \quad ({\lnot}R)$
$\cfrac{\Gamma, A[t/x] \vdash \Delta}{\Gamma, \forall x A \vdash \Delta} \quad ({\forall}L)$	$\cfrac{\Gamma \vdash A[y/x], \Delta}{\Gamma \vdash \forall x A, \Delta} \quad ({\forall}R)$
$\cfrac{\Gamma, A[y/x] \vdash \Delta}{\Gamma, \exists x A \vdash \Delta} \quad ({\exists}L)$	$\cfrac{\Gamma \vdash A[t/x], \Delta}{\Gamma \vdash \exists x A, \Delta} \quad ({\exists}R)$
Left структурные правила:	Right структурные правила:
$\cfrac{\Gamma \vdash \Delta}{\Gamma, A \vdash \Delta} \quad (\mathit{WL})$	$\cfrac{\Gamma \vdash \Delta}{\Gamma \vdash A, \Delta} \quad (\mathit{WR})$
$\cfrac{\Gamma, A, A \vdash \Delta}{\Gamma, A \vdash \Delta} \quad (\mathit{CL})$	$\cfrac{\Gamma \vdash A, A, \Delta}{\Gamma \vdash A, \Delta} \quad (\mathit{CR})$
$\cfrac{\Gamma_1, A, B, \Gamma_2 \vdash \Delta}{\Gamma_1, B, A, \Gamma_2 \vdash \Delta} \quad (\mathit{PL})$	$\cfrac{\Gamma \vdash \Delta_1, A, B, \Delta_2}{\Gamma \vdash \Delta_1, B, A, \Delta_2} \quad (\mathit{PR})$

Структурные правила

Ослабления (W) позволяет добавлять произвольные элементы в последовательности. Ослабление антецедента (WL) интуитивно понятно, потому что мы всегда можем ограничить сферу нашего доказательства (если все автомобили имеют колеса, то можно с уверенностью сказать, что все чёрные автомобили имеют колеса); в случае с сукцедентом (WR), ослабление допустимо, когда мы можем предположить альтернативные выводы (если все автомобили имеют колёса, то можно с уверенностью сказать, что все автомобили имеют либо колеса либо крылья).

Сокращение (.С) и перестановка (Р) допустимы, когда ни кратность вхождения (.С), ни порядок (Р) элементов не относятся к вопросам исследования последовательностей.

Свойства исчисления

Логические и структурные правила исчисления секвенций обладают рядом интересных свойств. Во первых, легко установить, что все правила являются обратимыми, то есть правила вывода, полученные из исходных заменой верхней секвенции (верхних секвенций) на нижнюю, а нижней на верхнюю, являются производными правилами. Во-вторых, все правила вывода, исключая сечение, обладают свойством подформуленности, то есть в верхние секвенции входят только формулы, графически совпадающие с формулами нижней секвенции, или являющиеся подформулами формул, входящих в нижнюю секвенцию.

Сечение

Единственным правилом, играющим в исчислении особую роль, является сечение. Оно нарушает указанные выше свойства. Однако Генценом было доказано, что и в классической и в интуиционистской логике первого порядка сечение является допустимым правилом: если можно построить вывод некоторой секвенции с помощью сечения, то можно построить вывод той же секвенции, не содержащей применений сечения. Теорема Генцена об устранимости сечения является фундаментальным результатом в логике и имеет исключительно важное значение в первую очередь для обоснования логики. В частности, из этой теоремы непосредственно следует теорема о непротиворечивости исчисления, опровергающая Теоремы Гёделя о неполноте.

Субструктурные логики

В качестве вариантов исчисления, можно ограничить или запретить использование некоторых из структурных правил. Это дает множество субструктурных логических систем (англ. Substructural logic). Они, как правило, слабее, чем LK-исчисление (то есть имеют меньше теорем), и, таким образом, не пересекаются с классической семантикой логики первого порядка. Тем не менее, у них имеются другие интересные свойства, которые используются в качестве приложений в теоретической информатике и искусственном интеллекте.

Ссылки

• Генцен Г. Математическая теория логического вывода. М., 1967.