ИСЧИСЛЕНИЕ СЕКВЕНЦИЙ
СЕКВЕНЦИЙ ИСЧИСЛЕНИЕ
от лат. 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-х т.
ИСЧИСЛЕНИЕ СЕКВЕНЦИЙ
одна из основных форм представления логических систем, применяемая в логике наряду с аксиоматическими системами (гильбертовского типа) и системами натурального (естественного) вывода. Термин «секвенция» происходит от слова sequent (последовательность). Он введен в логику П. Герцем (1929) и заимствован Г. Генценом, который впервые сформулировал в форме исчисления секвенций классическую и интуиционистскую логику предикатов первого порядка.
Исчисление секвенций состоит из двух главных компонентов: основной секвенции и правил заключения (иногда их называют правилами вывода). Основная секвенция в первоначальном генценовском варианте — это секвенция вида А->А, где А — формула, но могут применяться основные секвенции и другого вида. Правила заключения делятся на два типа: логические и структурные. Логические правила заключения в свою очередь делятся на правила введения логического знака в антецедент и правила введения логического знака в сукцедент секвенции. По логическому правилу из формул, входящих в его посылки (боковых формул), в заключении с помощью введения логического знака получается более сложная формула (главная формула). Таким образом, логические правила позволяют строить сложные формулы из более простых. Число логических правил в исчислении секвенций определяется числом используемых в данном исчислении логических констант. Структурные правила (перестановка, сокращение и утончение) влияют не на структуру отдельных формул, а на структуру секвенций. В результате применения этих правил вхождения формул в антецедент или сукцедент секвенции переставляются, сокращаются или добавляются. Логические и структурные правила заключения для классической и интуиционистской логик симметричны в том смысле, что каждому антецедентному (сукцедентному) правилу соответствует в точности одно сукцеденгное (антецедентное) правило.
Это единственное правило, в результате применения которого формула сечения (в данном случае А) вычеркивается из вывода. Все остальные правила сохраняют так называемое свойство подформульности вывода: все формулы, входящие в посылки конкретного правила, являются подформулами некоторых формул, входящих в заключение этого правила.
Вывод в исчислении секвенций имеет форму дерева секвенций, построение которого начинается с основной секвенции (основных секвенций) и продолжается по правилам заключения. Секвенция считается выводимой в исчислении секвенций, если можно построить вывод, в котором она является последней (конечной) секвенцией. Строго говоря, деревья в исчислении секвенций являются не выводами в стандартном смысле термина «логический вывод», а метаконструкциями, при построении которых выполняются логические переходы от одних записей о выводимости к другим. Интерпретация секвенций при этом может быть различной, что открывает широкие возможности для исследования общих свойств формальных логических доказательств.
С исчислением секвенций связан полученный Г. Генценом фундаментальный результат современной логики — теорема об устранении сечения, или элиминационная теорема. В доказательстве этой теоремы Г. Генцен заменяет сечение правилом смешения: » » Г*-» где * и * не содержат формулы А, и показывает, что из любого вывода в исчислении секвенций классической и интуиционистской первопорядковой логики можно устранить все применения этого правила.
Существует множество модификаций первоначального генценовского варианта исчисления секвенций для классической и неклассических логик. Методологически эти модификации сводятся к тому, что изменяется форма или/и число основных секвенций, форма или/и число правил заключения или/и вводятся ограничения на применения конкретных правил заключения при построении дерева вывода. Иногда изменяется само понятие секвенции и используются такие объекты, как «надсеквенции», «кортежи секвенций», «структуры» и т. д. Достаточно прозрачен и эффективен подход к формулировке исчисления, при котором правилам заключения придается «глобальный» характер — их применение зависит не только от вида посылок, но и от состояния выводов этих посылок. Такие правила, в частности, расширяют возможности доказательства теоремы об устранении сечения для неклассических логик.
Исчисления секвенций тесно связаны с табличными представлениями логических систем и обеспечивают естественный переход между синтаксическим и семантическим уровнями анализа неклассических логик. Они являются удобным аппаратом исследования количественных и качественных характеристик логических выводов и процедур поиска логических доказательств. Лит.: Математическая теория логического вывода. М., 1969.
П. И. Быстрое
Исчисление секвенций состоит из двух главных компонентов: основной секвенции и правил заключения (иногда их называют правилами вывода). Основная секвенция в первоначальном генценовском варианте — это секвенция вида А->А, где А — формула, но могут применяться основные секвенции и другого вида. Правила заключения делятся на два типа: логические и структурные. Логические правила заключения в свою очередь делятся на правила введения логического знака в антецедент и правила введения логического знака в сукцедент секвенции. По логическому правилу из формул, входящих в его посылки (боковых формул), в заключении с помощью введения логического знака получается более сложная формула (главная формула). Таким образом, логические правила позволяют строить сложные формулы из более простых. Число логических правил в исчислении секвенций определяется числом используемых в данном исчислении логических констант. Структурные правила (перестановка, сокращение и утончение) влияют не на структуру отдельных формул, а на структуру секвенций. В результате применения этих правил вхождения формул в антецедент или сукцедент секвенции переставляются, сокращаются или добавляются. Логические и структурные правила заключения для классической и интуиционистской логик симметричны в том смысле, что каждому антецедентному (сукцедентному) правилу соответствует в точности одно сукцеденгное (антецедентное) правило.
Это единственное правило, в результате применения которого формула сечения (в данном случае А) вычеркивается из вывода. Все остальные правила сохраняют так называемое свойство подформульности вывода: все формулы, входящие в посылки конкретного правила, являются подформулами некоторых формул, входящих в заключение этого правила.
Вывод в исчислении секвенций имеет форму дерева секвенций, построение которого начинается с основной секвенции (основных секвенций) и продолжается по правилам заключения. Секвенция считается выводимой в исчислении секвенций, если можно построить вывод, в котором она является последней (конечной) секвенцией. Строго говоря, деревья в исчислении секвенций являются не выводами в стандартном смысле термина «логический вывод», а метаконструкциями, при построении которых выполняются логические переходы от одних записей о выводимости к другим. Интерпретация секвенций при этом может быть различной, что открывает широкие возможности для исследования общих свойств формальных логических доказательств.
С исчислением секвенций связан полученный Г. Генценом фундаментальный результат современной логики — теорема об устранении сечения, или элиминационная теорема. В доказательстве этой теоремы Г. Генцен заменяет сечение правилом смешения: » » Г*-» где * и * не содержат формулы А, и показывает, что из любого вывода в исчислении секвенций классической и интуиционистской первопорядковой логики можно устранить все применения этого правила.
Существует множество модификаций первоначального генценовского варианта исчисления секвенций для классической и неклассических логик. Методологически эти модификации сводятся к тому, что изменяется форма или/и число основных секвенций, форма или/и число правил заключения или/и вводятся ограничения на применения конкретных правил заключения при построении дерева вывода. Иногда изменяется само понятие секвенции и используются такие объекты, как «надсеквенции», «кортежи секвенций», «структуры» и т. д. Достаточно прозрачен и эффективен подход к формулировке исчисления, при котором правилам заключения придается «глобальный» характер — их применение зависит не только от вида посылок, но и от состояния выводов этих посылок. Такие правила, в частности, расширяют возможности доказательства теоремы об устранении сечения для неклассических логик.
Исчисления секвенций тесно связаны с табличными представлениями логических систем и обеспечивают естественный переход между синтаксическим и семантическим уровнями анализа неклассических логик. Они являются удобным аппаратом исследования количественных и качественных характеристик логических выводов и процедур поиска логических доказательств. Лит.: Математическая теория логического вывода. М., 1969.
П. И. Быстрое
Источник: Новая философская энциклопедия