|
|
Большая Советская Энциклопедия (цитаты)
|
|
|
|
|
Секвенций исчисление | Секвенций исчисление (далее С) (позднелатинское sequentia - последовательность, следствие), секвенциальные исчисления, исчисления способов заключений, модификации понятия логического исчисления, в которых основными объектами преобразования являются не формулы, а т. н. секвенции, т. е. выражения вида A1,..., Al ® 1,..., Bm, где ® аналогична знаку выводимости, A1,..., Al и 1,..., Bm - произвольные формулы; первые - образующие антецедент секвенции, вторые - ее сукцедент. При l, m ³ 1 секвенция A1,..., Al ® 1,... m интерпретируется как формула
A1&... &A1 É1 Ú...Ú m.
(& - знак конъюнкции, É - импликации, Ú - дизъюнкции, см. Логические операции), секвенция с пустым антецедентом интерпретируется как истина, а секвенция с пустым сукцедентом - как ложь (и, следовательно, секвенция ®, состоящая из одной стрелки, - как противоречие). Аксиомами (исходными секвенциями) в С являются все секвенции вида С ® С (и только они). Правила вывода делятся на т. н. структурные и логические. Первые кодифицируют допустимые изменения "формульного состава" антецедента и сукцедента, вторые - введение в секвенции различных логических символов. Структурные правила - это "уточнение" (добавление произвольной формулы к антецеденту или сукцеденту), "сокращение" (вычеркивание повторяющихся формул), перестановка произвольных формул в антецеденте или сукцеденте, а также "сечение"
(латинскими буквами обозначаются произвольные формулы, греческими - строчки формул, разделенных запятыми, над чертой пишется посылка правила, под чертой - заключение). Логические правила вывода имеют для секвенциального классического исчисления высказываний следующий вид:
 ;  ;
 
 
  .
Если и структурные, и логические правила вывода ограничить условием, согласно которому в сукцеденте каждой секвенции должно быть не более одной формулы, то получим секвенциальное интуиционистское исчисление высказываний: это условие оказывается достаточным для невыводимости в С исключенного третьего принципа (а также закона снятия двойного отрицания). Секвенциальное исчисление предикатов получается присоединением к предыдущим правилам еще двух пар правил введения кванторов общности и существования.
Основной результат немецкого математика Г. Генцена состоит в установлении возможности приведения каждого вывода в С к "нормальной форме", не содержащей применений правила сечения и тем самым представляющей в некотором смысле "прямой" вывод. Из многочисленных приложений этого результата особенно важны доказательства непротиворечивости арифметических формальных систем, использующие математическую технику, выходящую за рамки гильбертовского финитизма (см. Аксиоматический метод, Метаматематика), и тем самым обходящие в известном смысле трудности, обусловленные теоремой К. Геделя о неполноте формальной арифметики. Эта же основная теорема Генцена лежит в основе большинства алгоритмов выводимости для логических и логико-математических исчислений (см. Разрешения проблема), чем и обусловлена исключительная важность С для интенсивно развивающихся исследований в области машинного поиска логического вывода, являющихся важным примером моделирования интеллектуальной деятельности человека.
Лит.: Генцен Г., Исследования логических выводов, пер. с нем., в кн.: Математическая теория логического вывода, М, 1967, с. 9-74; его же. Непротиворечивость чистой теории чисел, там же, с. 77-153; его же, Новое изложение доказательства непротиворечивости для чистой теории чисел, там же, с. 154-90; Карри Х. Б Основания математической логики. пер. с англ., М., 1969, гл. 5С, 6, 7 и 8; Алгорифм машинного поиска естественного логического вывода в исчислении высказываний, М. - Л., 1965.
|
Для поиска, наберите искомое слово (или его часть) в поле поиска
|
|
 |
 |
 |
|
|
|
Новости 21.11.2024 11:41:55
|
|
|
|
|
|
|
|
|
|
|
