СЕКВЕНЦИЙ ИСЧИСЛЕНИЕ
(позднелат.
(латинскими буквами обозначаются
Если и структурные, и логич.
Лит.: Г е н ц е н
sequentia - последовательность, следствие), секвенциальные исчисления,
исчисления способов заключений, модификации понятия логич. исчисления,
в
к-рых основными объектами преобразования являются не формулы, а т. н. секвенции,
т. е. выражения вида A
B
..., Вт, где -> аналогична знаку выводимости,
А
..., A
формулы; первыеобразующие антецедент секвенции, вторые - её сукцедент.
При l, т >= 1 секвенция А
B
операции), секвенция
с пустым антецедентом интерпретируется как истина, а секвенция с пустым
сукцедентом -как ложь (и, следовательно, секвенция ->, состоящая из одной
стрелки,- как противоречие). Аксиомами (исходными секвенциями) в С. и.
являются все секвенции вида С -> С (и только они). Правила вывода делятся
на т. н. структурные и логические. Первые кодифицируют допустимые изменения
"формульного состава" антецедента и сукцедента, вторые-введение в секвенции
различных логич. символов. Структурные правила - это "уточнение" (добавление
произвольной формулы к антецеденту или сук-цеденту), "сокращение" (вычёркивание
повторяющихся формул), перестановка произвольных формул в антецеденте или
сукцеденте, а такж" "сечение"
произвольные формулы, греческими -строчки формул, разделённых запятыми,
над чертой пишется посылка правила, под чертой - заключение). Логич. правила
вывода имеют для секвенциального классич. исчисления высказываний следующий
вид:
правила вывода ограничить условием, согласно к-рому в сукцеденте каждой
секвенции должно быть не более одной формулы, то получим секвенциальное
интуиционистское исчисление высказываний: это условие оказывается достаточным
для невыводимости в С. и. исключённого третьего принципа (а также
закона снятия двойного отрицания). Секвенциальное исчисление предикатов
получается
присоединением к предыдущим правилам ещё двух пар правил введения кванторов
общности
и существования. Основной результат нем. математика Г. Генцена состоит
в установлении возможности приведения каждого вывода в С. и. к "нормальной
форме", не содержащей применений правила сечения и тем самым представляющей
в нек-ром смысле "прямой" вывод. Из многочисленных приложений этого результата
особенно важны доказательства
непротиворечивости арифметич. формальных
систем, использующие математич. технику, выходящую за рамки гильбертовского
финитизма (см. Аксиоматический метод, Метаматематика),
и тем самым
обходящие в известном смысле трудности, обусловленные теоремой К. Гёделя
о
неполноте формальной арифметики. Эта же основная теорема Генцена лежит
в основе большинства алгоритмов выводимости для логич. и логико-математич.
исчислений (см. Разрешения проблема),
чем и обусловлена исключит.
важность С. и. для интенсивно развивающихся исследований в области машинного
поиска логич. вывода, являющихся важным примером моделирования
интеллектуальной
деятельности человека.
Г., Исследования логических выводов, пер. с нем., в кн.: Математическая
теория логического вывода, М., 1967, с. 9 - 74; его же, Непротиворечивость
чистой теории чисел, там же, с. 77 -153; его же, Новое изложение доказательства
непротиворечивости для чистой теории чисел, там же, с. 154-90; Карри X.
Б., Основания математической логики, -пер. с англ., М., 1969, гл. 5С, 6В,
7В и 8В; Алгорифм машинного поиска естественного логического вывода в исчислении
высказываний, М.- Л., 1965.
А Б В Г Д Е Ё Ж З И Й К Л М Н О П Р С Т У Ф Х Ц Ч Ш Щ Ъ Ы Ь Э Ю Я