Статья 496

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