Статья 263

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