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

СЕКВЕНЦИЙ ИСЧИСЛЕНИЕ (позднелат. sequentia - последовательность, следствие), секвенциальные исчисления, исчисления способов заключений, модификации понятия логич. исчисления, в к-рых основными объектами преобразования являются не формулы, а т. н. секвенции, т. е. выражения вида A1, ..., Al-> B1, ..., Вт, где -> аналогична знаку выводимости, А1, ..., Al и В1, ..., Вт - произвольные формулы; первыеобразующие антецедент секвенции, вторые - её сукцедент. При l, т >= 1 секвенция А1, ..., Al-> B1, ..., Вт интерпретируется как формула

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

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

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

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




Смотреть больше слов в «Большой советской энциклопедии»

СЕКВЕСТР →← СЕКВЕНС

Смотреть что такое СЕКВЕНЦИЙ ИСЧИСЛЕНИЕ в других словарях:

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

(позднелатинское sequentia — последовательность, следствие)        секвенциальные исчисления, исчисления способов заключений, модификации понятия логич... смотреть

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

одна из формулировок предикатов исчисления. Благодаря удобной форме вывода С. и. находит широкое применение в доказательств теории, основаниях м... смотреть

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

СЕКВЕНЦИЙ ИСЧИСЛЕНИЕ (от лат. sequentia - последовательность) - введенная в рассмотрение нем. математиком Г. Генценом (1934-35) разновидность поняти... смотреть

T: 232