Правило вывода

Эта статья находится на начальном уровне проработки, в одной из её версий выборочно используется текст из источника, распространяемого под свободной лицензией
Материал из энциклопедии Руниверсалис

Правило вывода — эффективная процедура для проверки того, что одна заданная формула в рассматриваемой теории непосредственно за один шаг выводится из других заданных формул.

В непротиворечивой теории теоремы получаются путём цепочки применения правил вывода этой теории. При этом если формула [math]\displaystyle{ {\cal B} }[/math] выводится за некоторое количество шагов из формул [math]\displaystyle{ {\cal A_1}, }[/math] [math]\displaystyle{ \dots, }[/math] [math]\displaystyle{ {\cal A_n} }[/math], то для выражения этого факта применяется обозначение [math]\displaystyle{ {\cal A_1},\dots,{\cal A_n}\vdash{\cal B} }[/math]. Если в таком случае рассматриваемая теория непротиворечива, а каждое из утверждений [math]\displaystyle{ {\cal A_1}, }[/math] [math]\displaystyle{ \dots, }[/math] [math]\displaystyle{ {\cal A_n} }[/math] является либо аксиомой, либо теоремой, то [math]\displaystyle{ {\cal B} }[/math] также является теоремой.

В исчислении предикатов в гильбертовском варианте[англ.] правилами вывода являются модус поненс и правило обобщения. По теореме Гёделя о полноте формула является выводимой в исчислении предикатов первого порядка тогда и только тогда, когда она общезначима, то есть истинна в любой интерпретации этого исчисления предикатов.

В исчислениях генценовского типа (исчислениях секвенций, системах натурального вывода) правила вывода играют основную роль — в них используется небольшое количество аксиом и развитые системы правил вывода. В теории доказательств применяются именно такие исчисления, поскольку благодаря подбору симметричных систем правил вывода возможно получить конструктивные результаты о непротиворечивости систем.

См. также

Литература

  • Драгалин А. Г. Математический интуиционизм. Введение в теорию доказательств. — М.: Наука, 1979. — 256 с. — (Математическая логика и основания математики).