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

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

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

В исчислении предикатов

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