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

Допустим теперь, что лемма верна при любом j<n. Случай 1. А имеет вид отрицания: — L8. ЧИСЛО вхождений примитивных связок в В, очевидно, меньше п. Случай 1а. Пусть при выбранном распределении истинностных значений букв Bi,B2,...,Bk форма В принимает значение И. Тогда^ принимает значение Л и ^ - —Л, а В -В. По индуктивному предположению, имеем В-,.В-2 В), |-В. (4.9) Согласно пункта б) леммы 4.2 имеем: (4.10) Из (4.9) и (4.10) по MP получим: В'ьВ'г В \ (4.11) В рассматриваемом случае—1Д А' = —i—B, тогда из (4.11) следует требуемое: В'J,В'2,...,В'k \-А'. Случай 16. Пусть В принимает значение Л, тогда В' есть —В, а А' совпадает с А. По индуктивному предположению В'i,B'2,...,B\ \ В, что и требовалось получить, ибо —В есть А '. Случай 2. А имеет вид В^С. Тогда число вхождений примитивных связок в В иС меньше, чем в А. Поэтому, в силу индуктивного предположения -В', (4.12) -С. (4.13) Случай 2а. В принимает значение Л, тогда вне зависимости от значения формулы С формула принимает значение И. Так как значение В есть Л, то В' = —15 , а из истинности А следует, что А' = А. Из соотношения (4.12) получаем B'bB'i В), | - - , а (4.14) Согласно лемме 4.2(e) имеем: \-^^(В^). (4.15) Из (4.14) и (4.15) по MP следует: в 'i.B -2в \ \ в^с. Последнее и есть требуемое, так как В^С есть А Случай 26. С принимает значение И. Следовательно, А принимает значение И п С есть С, а А' есть А. Тогда из (4.13) получим: В'ьВ'з В}, 1-е. (4.16) Согласно схеме аксиом^7 имеем l -C^ f B^ J . (4.17) Из (4.16) и (4.17) по MP следует В-,,В'2 В \ [ в ^ (4.18) И так как В^С совпадает с ^ то (4.18) является требуемым. B'J,B'2,...,B'K B'J,B'2,...,B'K 117