Вывод заключения из множества посылок записывается так же, как в исчислении высказываний
F1;F2;¼Fn|¾ B, где слева от знака “|¾” записывают множество формул посылок и необходимые аксиомы F1;F2;¼Fn, а справа – формулу заключения B. Тогда знак “|¾” означает “верно, что B выводима из F1;F2;¼Fn.
Отношение логического вывода эквивалентно теореме
|¾F1;F2;¼Fn®B.
Другая форма записи : F1; F2;¼Fn
B,
где над чертой записывают множество посылок и аксиом F1;F2;¼Fn, а под чертой заключение B.
Для организации вывода заключения из множества посылок используют правила подстановки и правила заключения.