Статья 269

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

построение

построение


Понятие вывода в аксиоматических системах не позволяет применять такое упрощение, что вынуждает решать задачу построения вывода напрямую, ограничиваясь применением лишь двух прямых правил вывода.