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

Из (4.14) и (4.15) по MP следует; В\,В\,...,В\ \В^С. Последнее и есть требуемое, так как В=>С есть Л Случай 26. С принимает значение И. Следовательно, А прини­ мает значениеЯ и С* есть С, йА' есть^. Тогда из (4.13) получим; B'bB\,...,B'k 1-е. (4.16) Согласно схеме аксиом^ 1 имеем \ -C^ (B^Q. (4-17) Из (4.16) и (4.17) по MP следует В'иВ'ь-.В', \-В=>С (4.18) и так как 5=>С совпадает с А', то (4.18) является требуемым. С л у ч а й 2в. В принимает значение И, С принимает значение Л. Тогда А принимает значение Л, следовательно, А' =~] А, В' есть В, а С есть 1с. Таким образом, из (4.12) и (4.13) получим соответственно В\,В\,...,В\ [- В, (4.19) В'ьВ'г,...,В\ ПС. (4.20) По п. е) леммы 4.2 имеем \- В=>(\ (5=>С)). (4.21) Из (4.19) и (4.21) по MP следует В'иВ'2,...,В^ [ ^C=>]{B=>C), (4.22) а из (4.20) и (4.22) по MP следует в'„в\...,в\ Последнее является требуемым, ибо l(B=:i'C) естьЛ'. Лемма до1сазана. Теорема 4.5 (о полноте). Если формула теории L является тавтологией, то она является теоремой теории L. 162