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

от лат. 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.