Статья 264

К непрямым правилам вывода относятся правила введения импликации, введения отрицания, удаления дизъюнкции и удаления квантора существования. Поскольку в формулировках непрямых правил используется понятие вывода, естественно включить эти формулировки непосредственно в определение вывода.
Вывод в системе есть субординантная последовательность формул каждый член которой является или формулой, или вспомогательным выводом, построенная в соответствии со следующими пунктами.
Формула есть вывод из множества посылок.
Если есть вывод из множества посылок - формула, то есть вывод из множества посылок.
Если есть вывод из множества посылок, формула входит и получена по одному из прямых однопосылочных правил вывода, тогда есть вывод из множества посылок.
Если а есть вывод из множества посылок, формулы входят в и формула получена из формул по одному из прямых двухпосылочных правил вывода, то есть вывод из множества посылок.