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

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

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

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

См. также

• Формальная система
• Автоматическое доказательство
• Классическое генценовское исчисление секвенций

Литература

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