Warning: date(): Invalid date.timezone value 'Europe/Kyiv', we selected the timezone 'UTC' for now. in /var/www/h77455/data/www/psyoffice.ru/engine/init.php on line 69 Warning: date(): Invalid date.timezone value 'Europe/Kyiv', we selected the timezone 'UTC' for now. in /var/www/h77455/data/www/psyoffice.ru/engine/init.php on line 69 Warning: strtotime(): Invalid date.timezone value 'Europe/Kyiv', we selected the timezone 'UTC' for now. in /var/www/h77455/data/www/psyoffice.ru/engine/modules/news/academicru/academicru_news.php on line 46 Warning: date(): Invalid date.timezone value 'Europe/Kyiv', we selected the timezone 'UTC' for now. in /var/www/h77455/data/www/psyoffice.ru/engine/modules/news/academicru/academicru_news.php on line 47 Warning: strtotime(): Invalid date.timezone value 'Europe/Kyiv', we selected the timezone 'UTC' for now. in /var/www/h77455/data/www/psyoffice.ru/engine/modules/news/academicru/academicru_news.php on line 49 Warning: date(): Invalid date.timezone value 'Europe/Kyiv', we selected the timezone 'UTC' for now. in /var/www/h77455/data/www/psyoffice.ru/engine/modules/news/academicru/academicru_news.php on line 50
|
СЕКВЕНЦИЙ ИСЧИСЛЕНИЕСЕКВЕНЦИЙ ИСЧИСЛЕНИЕ (от лат. 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. Философская Энциклопедия. В 5-х т. — М.: Советская энциклопедия. Под редакцией Ф. В. Константинова. 1960—1970. Категория: Словари и энциклопедии » Философия » Философская энциклопедия Другие новости по теме: --- Код для вставки на сайт или в блог: Код для вставки в форум (BBCode): Прямая ссылка на эту публикацию:
|
|