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

одна из формулировок предикатов исчисления. Благодаря удобной форме вывода С. И. Находит широкое применение в доказательств теории, основаниях математики, при автоматич. Поиске вывода. С. И. Было предложено Г. Генценом в 1934 (см. [1]). Ниже приводится один из вариантов классич. Исчисления предикатов в форме С. И. Н а б о р о м ф о р м у л наз. Конечное множество формул нек-рого логико-математического языка W, причем в этом множестве допускаются повторения формул. Порядок формул в наборе Г несуществен, но для каждой формулы указано, в скольких экземплярах она присутствует в Г. Набор формул может быть и пустым. Набор jГ получается из Г присоединением одного экземпляра формулы j. С е к в е н ц и е й наз. Фигура вида , где Г и D - наборы формул, Г наз.

А н т е ц е д е н т о м секвенции, а D-ее с у к ц е д е н т о м. Аксиомы С. И. Имеют вид , где Г, D - произвольные наборы формул, а j - произвольная атомарная (элементарная) формула. Правила вывода исчисления устроены очень симметрично и вводят логич. Связки в антецедент или сукцедент секвенции. Здесь в правилах предполагается, что переменная уне есть параметр Г и D, а x не есть параметр j. С. И. Эквивалентно обычной форме исчисления предикатов в том смысле, что формула j выводима в исчислении предикатов тогда и только тогда, когда секвенция выводима в С. И. Для доказательства этого утверждения существенна основная теорема Генцена (или теорема о нормализации), к-рая для С. И. Может быть сформулирована следующим образом.

Если в С. И. Выводимы секвенции и , то выводима и секвенция Правило вывода наз. Правилом сечения, и теорема о нормализации утверждает, таким образом, что правило сечения допустимо в С. И. Или что добавление правила сечения не изменяет объема выводимых секвенций. Ввиду этого теорему Генцена наз. Также теоремой об устранении сечения. Симметричное устройство С. И. В значительной мере облегчает изучение его свойств, поэтому в теории доказательств важное место занимает поиск секвенциальных вариантов прикладных исчислений. Арифметики, анализа, теории типов и доказательство для таких исчислений теоремы об устранении сечения в той или иной форме (см. [2], [3]). Найдены секвенциальные варианты и для многих исчислений, основанных на неклассич.

Логиках - интуиционистской, модальных и релевантных логиках и др. (см. [3], [4]). Лит.:[1] Математическая теория логического вывода. Сб. Переводов, М., 1967. [2] Т а к е у т и Г., Теория доказательств, пер. С англ., М., 1978. [3] Д р а г а л и н А. Г., Математический интуиционизм. Введение в теорию доказательств, М., 1979. [4] Ф е й с Р., Модальная логика, пер. [с англ.], М., 1974. А. Г. Драгалин.