Вывода правило, добавление к-рого в исчисление не меняет объема выводимых в этом исчислении слов. Введение в исчисление Д. п. является мощным и часто применяемым средством сокращения выводов, во многих случаях полезно для совершенствования алгоритмов установления выводимости. Одним из важнейших результатов математич. логики является теорема о допустимости правила сечения (см. Генцена формальная система). См. Выводимое правило, Производное правило. С. Ю. Маслов.