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

(позднелатинское sequentia — последовательность, следствие)

секвенциальные исчисления, исчисления способов заключений, модификации понятия логического исчисления (См. Исчисление), в которых основными объектами преобразования являются не формулы, а т. н. секвенции, т. е. выражения вида A₁,..., A_l → B₁,..., Bm, где → аналогична знаку выводимости, A₁,..., A_lи B₁,..., Bm — произвольные формулы; первые — образующие антецедент секвенции, вторые — её сукцедент. При l, m ≥ 1 секвенция A₁,..., A_l → B₁,... B_mинтерпретируется как формула

A₁&... &A₁⊃B₁∨...∨ B_m.

(& — знак конъюнкции, ⊃ — импликации, ∨ — дизъюнкции, см. Логические операции), секвенция с пустым антецедентом интерпретируется как истина, а секвенция с пустым сукцедентом — как ложь (и, следовательно, секвенция →, состоящая из одной стрелки, — как противоречие). Аксиомами (исходными секвенциями) в С. и. являются все секвенции вида С →С (и только они). Правила вывода делятся на т. н. структурные и логические. Первые кодифицируют допустимые изменения «формульного состава» антецедента и сукцедента, вторые — введение в секвенции различных логических символов. Структурные правила — это «уточнение» (добавление произвольной формулы к антецеденту или сукцеденту), «сокращение» (вычёркивание повторяющихся формул), перестановка произвольных формул в антецеденте или сукцеденте, а также «сечение»

(латинскими буквами обозначаются произвольные формулы, греческими — строчки формул, разделённых запятыми, над чертой пишется посылка правила, под чертой — заключение). Логические правила вывода имеют для секвенциального классического исчисления высказываний (См. Исчисление высказываний) следующий вид:

;

Если и структурные, и логические правила вывода ограничить условием, согласно которому в сукцеденте каждой секвенции должно быть не более одной формулы, то получим секвенциальное интуиционистское исчисление высказываний: это условие оказывается достаточным для невыводимости в С. и. исключенного третьего принципа (См. Исключённого третьего принцип) (а также закона снятия двойного отрицания). Секвенциальное Исчисление предикатов получается присоединением к предыдущим правилам ещё двух пар правил введения Кванторов общности и существования.

Основной результат немецкого математика Г. Генцена состоит в установлении возможности приведения каждого вывода в С. и. к «нормальной форме», не содержащей применений правила сечения и тем самым представляющей в некотором смысле «прямой» вывод. Из многочисленных приложений этого результата особенно важны доказательства непротиворечивости (См. Непротиворечивость) арифметических формальных систем, использующие математическую технику, выходящую за рамки гильбертовского финитизма (см. Аксиоматический метод, Метаматематика), и тем самым обходящие в известном смысле трудности, обусловленные теоремой К. Гёделя (См. Гёдель)о неполноте формальной арифметики. Эта же основная теорема Генцена лежит в основе большинства алгоритмов выводимости для логических и логико-математических исчислений (см. Разрешения проблема), чем и обусловлена исключительная важность С. и. для интенсивно развивающихся исследований в области машинного поиска логического вывода, являющихся важным примером моделирования (См. Моделирование) интеллектуальной деятельности человека.

Лит.: Генцен Г., Исследования логических выводов, пер. с нем., в кн.: Математическая теория логического вывода, М, 1967, с. 9—74; его же. Непротиворечивость чистой теории чисел, там же, с. 77—153; его же, Новое изложение доказательства непротиворечивости для чистой теории чисел, там же, с. 154—90; Карри Х. Б Основания математической логики. пер. с англ., М., 1969, гл. 5С, 6B, 7B и 8B; Алгорифм машинного поиска естественного логического вывода в исчислении высказываний, М. — Л., 1965.

СЕКВЕНЦИЙ ИСЧИСЛЕНИЕ

(от лат. sequentia - последовательность) - введенная в рассмотрение нем. математиком Г. Генценом (1934-35) разновидность понятия формальной системы (исчисления). В отличие от наиболее распространенного типа "гильбертовских" формальных систем, в системах генценовского типа осн. объектами, к к-рым прилагаются правила преобразования (вывода), являются не формулы, а т.н. секвенции, т.е. пары конечных (в частном случае - пустых) последовательностей формул, соединенные знаком →, формальные свойства к-рого аналогичны свойствам знака выводимости|–, играющего осн. роль в натуральных исчислениях (также введенных Генценом в той же работе). Часть A1,..., Аl секвенции А 1,..., Аl → В1,..., Вm наз. ее антецедентом, В1,..., Вm - сукцедентом. При l, m ≥ 1 секвенция Α1,..., Аl → В1,..., Вm интерпретируется в С. и. так же, как формула А1&...&Аl ⊃ В1 v..., v Bm в системах гильбертовского типа, секвенция с пустым антецедентом интерпретируется как истина, а секвенция с пустым сукцедентом – как ложь (и, следовательно, секвенция → – как противоречие). С. и. дает возможность непосредств. построения разрешающих алгоритмов для тех (под) систем логич. и логико-математич. исчислений, для к-рых вообще такой алгоритм возможен (см. Разрешения проблемы) и служит основой для всех известных в наст. время алгоритмов выводимости. Этим объясняется чрезвычайно важное значение С. и. для интенсивно ведущихся сейчас работ по машинному поиску логич. вывода, являющихся наиболее существ. примером моделирования "творческой" деятельности человека (см. Эвристика). Из других приложений С. и. в первую очередь следует упомянуть о полученных самим Генценом и другими учеными (П. С. Новиков, К. Шютте, В. Аккерман и др.) доказательствах непротиворечивости различных арифметических формальных систем, обходящих в известном смысле трудности, обусловленные теоремой К. Гёделя о неполноте арифметики (см. Метатеория, Полнота).

Лит.: Клини С. К., Введение в метаматематику, пер. с англ., М., 1957, § 20, 23, 77–81; Gеntzеn G., Untersuchungen όber das logische Schliessen, "Math. Z.", 1934, Bd 39.

одна из формулировок предикатов исчисления. Благодаря удобной форме вывода С. и. находит широкое применение в доказательств теории, основаниях математики, при автоматич. поиске вывода. С. и. было предложено Г. Генценом в 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.

А. Г. Драгалин.