Математическая логика и теория алгоритмов. Для изучающих компьютерные науки

Рассмотрим задание исчисления высказываний в виде теории естественного вывода. Пусть символами являются —i, &, v, =^, (, ), Aj, А2,..., а формулами - пропозициональные формы, образованные mAi,A2,... с помощью —i, &, v, Пусть А, В, С - произвольные формулы. Правила вывода задаются следующим образом. В каждом правиле вывода справа стоит символ в качестве имени этого правила. Например, одно из правил записывается в виде: ^ <1. А&В Это правило называется правилом введения конъюнкции и означает, что из А я В можно вывести А&В. Точно так же в каждом правиле вывода в "числителе" записываются гипотезы (посылки), а в "знаменателе" то, что выводится из этих гипотез. Отметим, что здесь, как и в формальной аксиоматической теории правила читаются сверху вниз, в то время, как в исчислении секвенций снизу вверх. Все правила вывода подразделяются на правила введения и правила исключения. Правилами введения являются: А,В ^ А,В ^ А А &; &; v ; v ; а&в в&а AvB BvA а[в а[в,^в. а^в —а Правилами исключения (удаления) являются: а &В ^ а &В ^ а,а ^В &: &: ^ а В В а\-с ,В \-c ,AvB -п^а 1; с А Так как в естественном выводе нет аксиом, то доказательство должно основываться на правиле введения импликации, которое говорит, что если В может быть выведено из а по правилам вывода, то а^в доказано. В формальной аксиоматической теории всякая формула вывода является либо аксиомой, либо непосредственным следствием по правилам вывода из предыдущих формул этого вывода. В доказательстве естественного вывода начинаем с гипотез (т.е. с недоказанных предложений), исследуем следствия, получающиеся по правилам вывода, и затем используем информацию вида а j- В для того, чтобы заключить о доказуемости предложения ^4^5. Например, докажем, что для любой формулы а формула ^-па^а является теоремой. Это моментально следует, если применить правило исключения отрицания 138