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

§ 10. прои з в одные (доказуемые) правила вывода в исчислении высказываний В исчислении высказываний (теории L) имеется только одно ис­ ходное правило вывода; modusp o n e n s ( M P ) . При этом доказана тео­ рема дедукции: если G, А \- В, тоG |- ^=>5. Последнее представляет тоже некоторое правило вывода, но уже производное (доказуемое) правило, получающееся, если принять правило M P . Кроме этого про­ изводного правила вывода, оказывается, есть и другие. Рассмотрим некоторые из них. Пусть G - произвольное множество формул из L; А,В,С - произ­ вольные формулы из L. Имеют место следующие п р о и з в о д н ы е прави­ лавывода. 1.Правило перевертывания (контрапозиции): если |- j 9, t o 0 ,1 В |-1 Y 4. Доказательство. 1) |- S - по условию; 2) G [- А=>В - по теореме дедукции; 3) (Л=^В)=?'(1 А )- теорема согласно п. д) леммы 4.2; 4 ) (А=^В) |- (1 А) - из 3) по МР\ 5) G\•'\B=>^ А - из 2) и 4) по третьему свойству выводимости (см. § 6); 6)g 1 в У \ в - по определению вывода; ~ из 5); 8) 1 B=i>'] А,']В |-1 - по MP; - 9)G^B\•^A - из 7) и 8) по третьему свойству выводимости. Что и требовалось доказать. 2. Правило удаления &: А&В |-/1. Доказательство. 1)^, В j- ^ - по определению вывода, 2 ) A ^ Л \ ^ B -из 1) по правилу перевертывания, 3)Ла \ а => Лв — по теореме дедукции, 156