Математическая логика и теория алгоритмов

Описанную процедуру можно свести в схему, представленную на рис. 4.1. |- {Av ( S&Q) => (AvB)&(AvQ J к Введение => (Av (S&Q) |- (AvB)&(AvB}&(AvC) X. Удаление v A \-{A-vB)&.iAvC) BScC \-{AvB)&{A^/Q Введение iS —^Введение & A 1-^vS A \-AvC B&C j-.4vS B&C \-AvC t t ^ L Ji. Введение v Введение v Введение v Введение v B&C [-fi B&C |- с Удаление ^ Удаление & t Рис. 4.1 Теперь доказательство формулы (4.27) восстанавливается, если проделать все рассуждения по приведенной схеме, начиная снизу. Отметим, что доказательство предложения (4.27) в формальной аксиоматической теории при обычных аксиомах будет значительно более длинным и громоздким. Для того, чтобы задать исчисление предикатов в виде естест­ венного вывода, на заданные правила вывода накладывают некоторые ограничения и добавляют еще примерно столько же новых правил вывода. 182