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

Таким образом, А^(В^>С),В,А \- С, тогда по теореме дедукции А^(В^>С),В \-А^>С. Что и требовалось доказать. Лемма 4.2. Для любых формул А,В следующие формулы являются теоремами в L: а) —1—В^В; 6) В^ —1—В; а) —i—iB^B; 6) В^ —i—B; в) —А^(А^В); г) ( —iB^—A)^(A^B); д) (А^В)^( —В^—А); о) А^(—\В^—\(А^В)); ж) (А^В)^(( —А^В)^В). Доказательство. а) I— t —iB^B: 1) (—iB^ —i—B)^(( —В^ —\В)^В) - является аксиомой, полученной по схеме A3 при А= 1В, 2) -пВ^ -пВ - является теоремой в силу леммы 4.1, т.е. эта формула выводима и при желании можно выписать весь вывод этой формулы, 3) (—В^ —1—В)^В - по следствию 4.2 из 1) и 2), 4) -n-nB^( —iB^ - п—В) - является аксиомой, полученной по схеме А1, когда вместо АжВ взяты формулы —i — L 8 И —iS соответственно, 5) —1—В^В - по следствию 4.1 из 3) и 4). Утверждение а) доказано; б) \-В^^^: 1) ( —i—i—B^ - пВ)^(( -п-п—В^В)^ —1— L 8 - является аксиомой, полученной по A3, когда вместо Аж В взяты формулы В и —i —iS соответственно, 2) —i—1 —В^ —В - теорема согласно п. а), 3) (—1—1—В^В)^—1—В - по MP из 1) и 2), 4) В^(—г-^—В^В) - аксиома, полученная по схеме А1, когда вместо А ж В взяты формулы В и —1—1— L 8 соответственно, 5) В^ —1— L 8 - согласно следствию 4.1 из 4) и 3). Утверждение б) доказано; в) I— А =^(А^В)\ 1) -А - гипотеза, 2)А- гипотеза, 3)A^f —B^AJ - схема аксиом^7, 4) -nA^ f —iB^^ J - схема аксиом^7, 5) -^В^А - по MP из 2) и 3), 6) —17^^ -А - по MP из 1) и 2), 7) —,В^А)^В) - схема аксиом^5, 8) ( —iB^A)^B - поMP из 6) и 7), 9) 5 - по MP из 5) и 8). Итак, в силу I) - 9) —А, А \- В. Тогда по теореме дедукции —А [• А^В и, снова по той же теореме, получим, что |—A^fA^BJ . 112