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

одна из формулировок предикатов исчисления. Благодаря удобной форме вывода С. и. находит широкое применение в доказательств теории, основаниях математики, при автоматич. поиске вывода. С. и. было предложено Г. Генценом в 1934 (см. [1]). Ниже приводится один из вариантов классич. исчисления предикатов в форме С. и. Н а б о р о м ф о р м у л наз. конечное множество формул нек-рого логико-математического языка W, причем в этом множестве допускаются повторения формул. Порядок формул в наборе Г несуществен, но для каждой формулы указано, в скольких экземплярах она присутствует в Г. Набор формул может быть и пустым. Набор jГ получается из Г присоединением одного экземпляра формулы j. С е к в е н ц и е й наз. фигура вида [img: http://localhost:8080/file/041904-62.jpg], где Г и D - наборы формул, Г наз. а н т е ц е д е н т о м секвенции, а D-ее с у к ц е д е н т о м. Аксиомы С. и. имеют вид [img: http://localhost:8080/file/041904-63.jpg], где Г, D - произвольные наборы формул, а j - произвольная атомарная (элементарная) формула. Правила вывода исчисления устроены очень симметрично и вводят логич. связки в антецедент или сукцедент секвенции: [img: http://localhost:8080/file/041904-64.jpg] Здесь в правилах [img: http://localhost:8080/file/041904-65.jpg] предполагается, что переменная уне есть параметр Г и D, а x не есть параметр j. С. и. эквивалентно обычной форме исчисления предикатов в том смысле, что формула j выводима в исчислении предикатов тогда и только тогда, когда секвенция [img: http://localhost:8080/file/041904-66.jpg] выводима в С. и. Для доказательства этого утверждения существенна основная теорема Генцена (или теорема о нормализации), к-рая для С. и. может быть сформулирована следующим образом: если в С. и. выводимы секвенции [img: http://localhost:8080/file/041904-67.jpg] и [img: http://localhost:8080/file/041904-68.jpg], то выводима и секвенция [img: http://localhost:8080/file/041904-69.jpg] Правило вывода [img: http://localhost:8080/file/041904-70.jpg] наз. правилом сечения, и теорема о нормализации утверждает, таким образом, что правило сечения допустимо в С. и. или что добавление правила сечения не изменяет объема выводимых секвенций. Ввиду этого теорему Генцена наз. также теоремой об устранении сечения. Симметричное устройство С. и. в значительной мере облегчает изучение его свойств, поэтому в теории доказательств важное место занимает поиск секвенциальных вариантов прикладных исчислений: арифметики, анализа, теории типов и доказательство для таких исчислений теоремы об устранении сечения в той или иной форме (см. [2], [3]). Найдены секвенциальные варианты и для многих исчислений, основанных на неклассич. логиках - интуиционистской, модальных и релевантных логиках и др. (см. [3], [4]).