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

рая при этом преследуется, состоит в том, чтобы построить язык, свободный от недостатков обычного языка. Благодаря точности и од­ нозначности формализованные языки находят применение там, где предъявляются повышенные требования к строгости. Д. Гильберт писал: "Подзнакомаксиоматического методама­ тематика проявляет свою руководящую рольвнауке вообще". § 17. Теория естественного вывода Естественный вывод является интересным подходом к заданию дедуктивной теории. Здесь, как и в любой дедуктивной теории, зада­ ются алфавит, формулы (правильно построенные выражения), но нет аксиом, есть только правила вывода. Оказывается, что задание только правил выводов позволяет выделить из множества всех формул неко­ торое подмножество формул, элементы которого и называются теоре­ мами. Следовательно, не имея ни одной аксиомы (!) можно получить теоремы. Рассмотрим задание исчисления высказываний в виде теории естественного вывода. Пусть символами являются 1, &, v, =>, (,), а\,а2, ..., а формула­ ми - пропозициональные формы, образованные из А\, с помощью V, =>. Пусть А , В, С — произвольные формулы. Правила вывода зада­ ются следующим образом. В каждом правиле вывода справа стоит символ в качестве имени этого правила. Например, одно из правил записывается в виде: sc. А & В Это правило называется правилом введения конъюнкции и оз­ начает, что из А и В можно вывести А&В. Правило введения дизъюнк­ ции А V Aw В 179