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

Допустим теперь, что Г [- A=>Bii для любого k<i. Для В, имеем четыре возможности: В/ есть аксиома, В, еЛ в,=^а, Bj - следствие по MP из некоторых Bj и Вт, где j < i ,m<i и В„ имеет вид Bj=>Bi. В первых трех случаях то, что Г A-=>Bi доказывается такясе, как для i ~ \ . В последнем случае применим индуктивное предполонсе- ние, согласно которому 1) \-A:^Bj, 2) Г" |- A-=>{Bj^Bi}. По схеме аксиом А 2 : 3) |- (^=>(Syrs »5,))=>((.4=>Sy)=>(^=?S,)); далее, применяя правило MP, из 3) и 2) получим: 4) Г {A=>Bj):^{A=^Bi); снова по MP из 4) и 1) имеем: Г |- A^Bj. Таким образом, доказательство по индукции завершено и для i=n получим требуемое утверлсдение. Теорема доказана. Следствие4.1.А=>В, В=>С [•А=^. Доказательство. 1) ^ =>5 - гипотеза, 2) S=>C - гипотеза, 3 ) А - гипотеза, 4) В - по MP из 1) и 3), 5) С- по MP из 2) и 4). Таким образом, А=>В,В::^С,А [-С. Отсюда по теореме дедук­ ции А=^В,В::^С А-=>С. Что и требовалось доказать. 152