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

означает, что из А можно вывести AvB, где В - произвольная форму­ ла. Точно так же в каждом правиле вывода в "числителе" записывают­ ся гипотезы (посылки), а в "знаменателе" то, что выводится из этих гипотез. Все правила вывода подразделяются на правила введения и пра­ вила исключения. Правилами введения являются; А,В . А,В А , А & , & ; - - — - V , - — - V , А&В В&А A v B B v A i М л }-5J5 1 , А ^ В ЛА а правилами исключения (удаления): А&В А&В j L r ' n L r ' A D &J &,• f-C.B \- С. AvBV; A В С I L l l ; A A,A=i' В =>. В Так как в естественном выводе нет аксиом, то доказательство должно основываться на правиле введения импликации, которое гово­ рит, что если В может быть выведено из А по правилам вывода, то доказано, В формальной аксиоматической теории всякая формула вывода является либо аксиомой, либо непосредственным следствием по правилам вывода из предыдущих формул этого вывода. В доказательстве естественного вывода начинаем с гипотез (т.е. с недоказанных предложений), исследуем следствия, получаю­ щиеся по правилам вывода, и затем используем информацию вида А\-В для того, чтобы заключить о доказуемости предложения А=>В. Например, докажем, что для любой формулы А формула Ц А:=>А является теоремой. Это моментально следует, если применить прави­ ло исключения отрицания ] 1 1 . г А 180