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

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

одна из формулировок предикатов исчисления. Благодаря удобной форме вывода С. и. находит широкое применение в доказательств теории, основаниях математики, при автоматич. поиске вывода. С. и. было предложено Г. Генценом в 1934 (см. [1]). Ниже приводится один из вариантов классич. исчисления предикатов в форме С. и.

Н а б о р о м ф о р м у л наз. конечное множество формул нек-рого логико-математического языка W, причем в этом множестве допускаются повторения формул. Порядок формул в наборе Г несуществен, но для каждой формулы указано, в скольких экземплярах она присутствует в Г. Набор формул может быть и пустым. Набор jГ получается из Г присоединением одного экземпляра формулы j. С е к в е н ц и е й наз. фигура вида , где Г и D - наборы формул, Г наз. а н т е ц е д е н т о м секвенции, а D-ее с у к ц е д е н т о м.

Аксиомы С. и. имеют вид , где Г, D - произвольные наборы формул, а j - произвольная атомарная (элементарная) формула. Правила вывода исчисления устроены очень симметрично и вводят логич. связки в антецедент или сукцедент секвенции:


Здесь в правилах предполагается, что переменная уне есть параметр Г и D, а x не есть параметр j.

С. и. эквивалентно обычной форме исчисления предикатов в том смысле, что формула j выводима в исчислении предикатов тогда и только тогда, когда секвенция выводима в С. и. Для доказательства этого утверждения существенна основная теорема Генцена (или теорема о нормализации), к-рая для С. и. может быть сформулирована следующим образом: если в С. и. выводимы секвенции и , то выводима и секвенция

Правило вывода наз. правилом сечения, и теорема о нормализации утверждает, таким образом, что правило сечения допустимо в С. и. или что добавление правила сечения не изменяет объема выводимых секвенций. Ввиду этого теорему Генцена наз. также теоремой об устранении сечения.

Симметричное устройство С. и. в значительной мере облегчает изучение его свойств, поэтому в теории доказательств важное место занимает поиск секвенциальных вариантов прикладных исчислений: арифметики, анализа, теории типов и доказательство для таких исчислений теоремы об устранении сечения в той или иной форме (см. [2], [3]). Найдены секвенциальные варианты и для многих исчислений, основанных на неклассич. логиках - интуиционистской, модальных и релевантных логиках и др. (см. [3], [4]).

Лит.:[1] Математическая теория логического вывода. Сб. переводов, М., 1967; [2] Т а к е у т и Г., Теория доказательств, пер. с англ., М., 1978; [3] Д р а г а л и н А. Г., Математический интуиционизм. Введение в теорию доказательств, М., 1979; [4] Ф е й с Р., Модальная логика, пер. [с англ.], М., 1974.

А. Г. Драгалин.


Математическая энциклопедия. — М.: Советская энциклопедия. . 1977—1985.

Игры ⚽ Нужно решить контрольную?

Полезное


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

  • СЕКВЕНЦИЙ ИСЧИСЛЕНИЕ — (от лат. sequentia последовательность) введенная в рассмотрение нем. математиком Г. Генценом (1934 35) разновидность понятия формальной системы (исчисления). В отличие от наиболее распространенного типа гильбертовских формальных систем, в… …   Философская энциклопедия

  • Секвенций исчисление — (позднелатинское sequentia последовательность, следствие)         секвенциальные исчисления, исчисления способов заключений, модификации понятия логического исчисления (См. Исчисление), в которых основными объектами преобразования являются не… …   Большая советская энциклопедия

  • ИСЧИСЛЕНИЕ СЕКВЕНЦИЙ —     ИСЧИСЛЕНИЕ СЕКВЕНЦИЙ одна из основных форм представления логических систем, применяемая в логике наряду с аксиоматическими системами (гильбертовского типа) и системами натурального (естественного) вывода. Термин “секвенция” происходит от… …   Философская энциклопедия

  • ИСЧИСЛЕНИЕ — (формальная система) система символов, основными компонентами которой являются: 1) алфавит (совокупность элементарных символов букв. цифр, скобок и т.п.), 2) правила построения формул из символов алфавита, 3) аксиомы (исходные доказуемые формулы) …   Философская энциклопедия

  • Логическое исчисление —         Исчисление (формальная система), интерпретируемое в терминах какого либо фрагмента дедуктивной логики (См. Логика). Различные Л. и. служат базой для построения более богатых «нелогических» (например, математических) теорий. Примерами Л. и …   Большая советская энциклопедия

  • ПРЕДИКАТОВ ИСЧИСЛЕНИЕ — формальная аксиоматич. теория; исчисление, предназначенное для описания логических законов, справедливых для любой непустой области объектов с произвольными заданными на этих объектах предикатами (т. в. свойствами и отношениями). Для формулировки …   Математическая энциклопедия

  • ЛОГИЧЕСКОЕ ИСЧИСЛЕНИЕ — см. Логистика. Философский энциклопедический словарь. 2010. ЛОГИЧЕСКОЕ ИСЧИСЛЕНИЕ исчисление ( …   Философская энциклопедия

  • ПРЕДИКАТОВ ИСЧИСЛЕНИЕ — общее название исчислений математической логики, являющихся формализацией тех разделов совр. логики, к рые изучают субъектно предикатную структуру предложений (высказываний), понимаемую в более широком, чем в традиц. логике, смысле: помимо теории …   Философская энциклопедия

  • НАТУРАЛЬНОЕ ИСЧИСЛЕНИЕ — (исчисление естественного в ы в о д а) – общее название логич. исчислений [введенных и впервые описанных нем. логиком и математиком Г. Генценом (1934) и польским логиком С. Яськовским (1934) с целью формализации процесса логич. вывода ], более… …   Философская энциклопедия

  • ЛОГИКА ВЫСКАЗЫВАНИЙ — раздел логики, в котором изучаются истинностные взаимосвязи между высказываниями. В рамках данного раздела высказывания (пропозиции, предложения) рассматриваются только с т.зр. их истинности или ложности, безотносительно к их внутренней субъектно …   Философская энциклопедия


Поделиться ссылкой на выделенное

Прямая ссылка:
Нажмите правой клавишей мыши и выберите «Копировать ссылку»