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

§ 8. Некоторые теоремы исчисления высказываний Проведем доказательство некоторых теорем исчисления высказываний (теории L). Лемма 4.1. |- А^А для любой формулы А теории L, т. е. формула А^А является теоремой теории L для любой формулы А из L. Доказательство. 1) (А^((А^А) ^А)) ^((А^(А^А)) ^(А^А)) - является аксиомой, так как получается по схеме ^2, если положить В=А^А и С=А; 2) A^ffA^AJ^AJ является аксиомой, которая получается по схеме AJ, если положить В=А^А; 3) (A^(A^AJJ^(A^AJ является непосредственным следствием из 1) и 2) шМР; 4) А^(А^А) является аксиомой, полученной по схеме А1 при В=А; 5) А^А является непосредственным следствием из 3) и 4) по MP. Таким образом, получили последовательность формул 1)-5), каждая из которых аксиома или непосредственное следствие из некоторых предыдущих формул 1)-4) по правилу MP, причем последняя формула есть А^А. Следовательно, формулы 1)- 5) есть вывод формулы А^А, которая и является теоремой в L.. Теорема 4.1 (теорема дедукции). Если Г - множество формул. А,В - формулы и Г,А \-В, то Г \-А^В. В частности, если^ |- В, то \-А^В. Доказательство. Пусть5 7 , ^ 2 , е с т ь вывод формулы В и з г д е Вп=В. Индукцией по i (1 < i <п) докажем, что Г \-A^Bi. Пусть i=l. Покажем, что Г \- А^Bi. Так как Bi является первой из формул в выводе ВшГ и {А}, то имеем следующие возможности: BIEP, Bi является аксиомой, Bi=A. По схеме аксиом^7 формула есть аксиома. Поэтому в первых двух случаях (когда Bj аксиома или формула из Г) по MP получим Г [A^Bi. В третьем случае, т.е. когда 5^ совпадает о, А {Bi=A), по лемме 4.1 имеем \-A^Bi, следовательно, Г \-A^Bi. Тем самым случай i=l исчерпан. Допустим теперь, что Г \- A^Bk для любого к<4. Для Bi имеем четыре возможности: Bi есть аксиома. 110