Выводом формулы В из множества формул F1; F2; . . . Fn называется такая последовательность формул, что любая Fi есть либо аксиома, либо непосредственно выводима из подмножества предшествующих ей формул F1; F2;. . .Fn.
В этом случае формулу B называют заключением, а последовательность формул F1; F2;. . .Fn, сформированная отношением логического вывода, представляет схему дедуктивного вывода.
Схему дедуктивного вывода записывают так:
F1; F2; . . . Fn |¾ B,
где символ |¾ означает “верно, что B выводима из F1; F2;… Fn“.
Есть определенная связь между отношением логического вывода в схеме дедуктивного вывода и импликацией в схеме закона алгебры высказываний .
Этот факт записывают так:
|¾ F1&F2&. . . &Fn®B.
Известна другая форма записи дедуктивного вывода формулы В:
F1; F2; . . . Fn
B,
где над чертой записывают множество посылок и аксиом F1; F2;…Fn, а под чертой заключение В, принимающее значение “истины” при истинности всех посылок.