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

Отметим, что по доказанному следствию имеем: ~\л=>в,в=^с |-"U=>C. Исключив импликацию, получим: AvB, TB V C [AVC, т.е. бинарная резольвента дизъюнктов AvBи ISvC выводима изэтих дизъюнктовтеории L. Следствие 4.2.А::^{В=>С},В |-^=>С. Доказательство. 1) y 4=>(S=>C) - гипотеза, 2 ) А - гипотеза, 3) В=>С - по MP из 1) и 2), 4 ) В - гипотеза, 5) С ~ по MP из 3) и 4). Таким образом, у 4=>(В=>С), Д ^ [- С, тогда по теореме дедукции А=>{В=>С),В [-А=>С. Что и требовалось доказать. Л е м м а 4 .2. Для любых формул А,В следующие формулы являются теоремами в L: a ) 11S^S ; б)b=>^^b; в) 1 A=i'(A=>B); г) (1 В=>] А)=>(А=>В); д) (y4=>S)=>(15=>1 А); е) ^=>(1( y 4=>S)); ж) (А^В)=>((1А:^В)=>В). Доказательство. а) f\\B=>B-. 1) (1 В=^Т\ В)=>((\ i?=^1 В)=>В) -является аксиомой, полученн по схеме АЪ при А=\ В, 2) 1 S=>1 В является теоремой в силу леммы 4.1, т.е. эта формула выводима и при желании можно выписать весь вывод этой формулы, 3)(1В=>11 в)=:>в - по следствию 4.2 из 1) и 2), 153