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

Вг^Г, Д- =А, Bi - следствие по MP из некоторых Bj и В„, где j<i, т<4 и В„ имеет вид Bj^Bi. В первых трех случаях то, что Г \-A^Bi, доказывается так же, как для i=l. В последнем случае применим индуктивное предположение, согласно которому \)Г [A^B j, 2) г \-A^{Bj^Bi). По схеме аксиом^2: 3) h (A^(Bj^Bi))^((A^Bj)^(A^Bi)); далее, применяя правило MP, из 3) и 2) получим: 4) Г [ (А^В^^(А^В^1 снова по MP из 4) и 1) имеем: г [ а ^ в . Таким образом, доказательство по индукции завершено и для i=n получим требуемое утверждение. Теорема доказана. Следствие 4.1. А^В, В^С \-А^>С. Доказательство. \)А ^ В - гипотеза, 2) В^>С - гипотеза, 3)А- гипотеза, 4) В - поMP из 1) и 3), 5) С- по MP из 2) и 4). Таким образом, А^В, В^, А \- С. Отсюда по теореме дедукции А^В,В^>С \- А^>С. Что и требовалось доказать. Отметим, что по доказанному следствию имеем: —А^В,В^>С I— А^>С. Исключив импликацию, получим: AvB, -^vC \-AvC, т.е. бинарная резольвента дизьюнктов Av В и —В v С выводима из этих дизьюнктов в теории L. Следствие 4.2. А=^(В ),В \-А=^. Доказательство. 1)A^fB^>CJ - гипотеза, 2)А- гипотеза, 3) В^С-по MP из 1)и2), 4) В - гипотеза, 5) С - по MP из 3) и 4). 111