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

2) А=>({А^А)=>А) является аксиомой, которая получается по схеме А 1, если положить В~А=>А; 3) (Az=>(Az=>A))=:f(A=>A) является непосредственным следствием из 1) и 2) по MF-, 4) Az=i>(A=i>A) является аксиомой, полученной по схеме А1 при В=А; 5) А=>А является непосредственным следствием из 3) и 4) по MP. Таким образом, получили последовательность формул 1)-5), каждая из которых - аксиома либо непосредственное следствие из некоторых предыдущих формул 1)-4) по правилу MP, причем последняя формула есть А=>А. Следовательно, формулы 1)-5) есть вывод формулы А=>А, которая и является теоремой в L. Теорема 4.1 (теорема дедукции). Если Г - множество формул, А,В - формулы и ГуА [- J 8, то Г [- А=>В. В частности, если А ]- В, |то \-А=>В. Доказательство. Пусть ВьВ2,...,В„ есть вывод формулы В из где В„=В. Индукцией по / (1 < i <п) докажем, что Г \-A^Bi. Пусть /=1. Покажем, что Г \- А^В\. Так как В\ является первой из формул в выводе Б изF u {^4}, то имеем следующие возможности: В\ &Г, В\ является аксиомой, вх=а. По схеме аксиом ^41 формула Bi=i>(A^ В\) есть аксиома. Поэто­ му в первых двух случаях (когда Bi аксиома или формула из Г) по MP получим Г В третьем случае, т.е. когда Bi совпадает с А {В\=А\ по лемме 4.1 имеем \-а=^вх, следовательно, Г \-А=>Вх. Тем самым случай г=1 исчерпан. 151