Правило вывода
Правило вывода — эффективная процедура для проверки того, что одна заданная формула в рассматриваемой теории непосредственно за один шаг выводится из других заданных формул.
В непротиворечивой теории теоремы получаются путём цепочки применения правил вывода этой теории. При этом если формула выводится за некоторое количество шагов из формул , то для выражения этого факта применяется обозначение . Если в таком случае рассматриваемая теория непротиворечива, а каждое из утверждений является либо аксиомой, либо теоремой, то также является теоремой.
В исчислении предикатов в Шаблон:Iw правилами вывода являются модус поненс и правило обобщения. По теореме Гёделя о полноте формула является выводимой в исчислении предикатов первого порядка тогда и только тогда, когда она общезначима, то есть истинна в любой интерпретации этого исчисления предикатов.
В исчислениях генценовского типа (исчислениях секвенций, системах натурального вывода) правила вывода играют основную роль — в них используется небольшое количество аксиом и развитые системы правил вывода. В теории доказательств применяются именно такие исчисления, поскольку благодаря подбору симметричных систем правил вывода возможно получить конструктивные результаты о непротиворечивости систем.