10. Полнота резолютивного вывода (В.А. Захаров - Лекции)
Описание файла
Файл "10. Полнота резолютивного вывода" внутри архива находится в папке "В.А. Захаров - Лекции". PDF-файл из архива "В.А. Захаров - Лекции", который расположен в категории "". Всё это находится в предмете "математическая логика и логическое программирование" из 7 семестр, которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .
Просмотр PDF-файла онлайн
Текст из PDF
Îñíîâûìàòåìàòè÷åñêîéëîãèêèèëîãè÷åñêîãîïðîãðàììèðîâàíèÿËÅÊÒÎÐ: Â.À. ÇàõàðîâËåêöèÿ 10.Ïîëíîòà ðåçîëþòèâíîãî âûâîäà.Ïðèìåíåíèå ìåòîäà ðåçîëþöèé.ÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀÒåîðåìà î ïîëíîòå ðåçîëþòèâíîãî âûâîäàÅñëè S ïðîòèâîðå÷èâàÿ ñèñòåìà äèçúþíêòîâ, òî èç Sðåçîëþòèâíî âûâîäèì ïóñòîé äèçúþíêò .Äîêàçàòåëüñòâî.Åñëè S ïðîòèâîðå÷èâàÿ ñèñòåìà äèçúþíêòîâ, òî ñîãëàñíîòåîðåìå Ýðáðàíà ñóùåñòâóåò êîíå÷íàÿ ïðîòèâîðå÷èâàÿ ñèñòåìàS 0 îñíîâíûõ ïðèìåðîâ äèçúþíêòîâ èç S . Ïîýòîìó ìû1. Âíà÷àëå ïîêàæåì, ÷òî èç ïðîòèâîðå÷èâîé ñèñòåìû îñíîâíûõïðèìåðîâ äèçúþíêòîâ S 0 ìîæíî ðåçîëþòèâíî âûâåñòè ïóñòîéäèçúþíêò .2. À çàòåì íà îñíîâå ýòîãî âûâîäà ïîñòðîèì ðåçîëþòèâíûéâûâîä ïóñòîãî äèçúþíêòà èç ñàìîé ñèñòåìû S .ÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀËåììà îá îñíîâíûõ ïðèìåðàõ äèçúþíêòîâÅñëè S 0 êîíå÷íàÿ ïðîòèâîðå÷èâàÿ ñèñòåìà îñíîâíûõïðèìåðîâ äèçúþíêòîâ, òî èç S 0 ðåçîëþòèâíî âûâîäèì ïóñòîéäèçúþíêò .Äîêàçàòåëüñòâî ëåììû.Èíäóêöèåé ïî ÷èñëó N ðàçëè÷íûõ îñíîâíûõ àòîìîâ â ñèñòåìåäèçúþíêòîâ S 0.00Áàçèñ (N = 0).
Ñèñòåìà S ïðîòèâîðå÷èâà. Çíà÷èò, S 6= ∅.Íî â S 0 íåò íè îäíîãî àòîìà. Çíà÷èò, â S 0 ñîäåðæèòñÿ òîëüêîïóñòîé äèçúþíêò . È îí ðåçîëþòèâíî âûâîäèì èç S 0.ÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀÄîêàçàòåëüñòâî ëåììû.Èíäóêòèâíûé ïåðåõîä (N + 1 → N ). Ðàññìîòðèìïðîèçâîëüíûé îñíîâíîé àòîì A0, âõîäÿùèé â ñîñòàâäèçúþíêòîâ èç S 0, è ðàçîáüåì ñèñòåìó S 0 íà òðè ÷àñòè:1. S10 = {D : D ∈ S 0, D = Db1 ∨ A0};2. S20 = {D : D ∈ S 0, D = Db2 ∨ ¬A0}.3. S30 = {D : D ∈ S 0, A0 ∈/ D, ¬A0 ∈/ D};Ïîñòðîèì âñå ðåçîëüâåíòû ïî êîíòðàðíîé ïàðå A0, ¬A0b1 ∨ Db2 : D1 = Db1 ∨ A0 ∈ S 0 , D2 = Db2 ∨ ¬A0 ∈ S 0 }S00 = {D12è ïîêàæåì, ÷òî ìíîæåñòâî äèçúþíêòîâ S 00 = S00 ∪ S30ïðîòèâîðå÷èâî.ÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀÄîêàçàòåëüñòâî'ëåììû.'$'b1 ∨ A0D&&S01b2 ∨ ¬A0D%&$S02$'S0 $S03íåò ëèòåð A0, ¬A0%&%%ÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀÄîêàçàòåëüñòâî'ëåììû.'$'S01b1 ∨ A0D$S02b2 ∨ ¬A0DB$'S0 $S03íåò ëèòåð A0, ¬A0BB&%&%&%B&%BB'$00BS'$'$B0S03B S0BNb1 ∨ Db2Dðåçîëüâåíòû&&íåò ëèòåð A0, ¬A0%&%%ÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀÄîêàçàòåëüñòâî ëåììû.Ðàññìîòðèì ïðîèçâîëüíóþ èíòåðïðåòàöèþ I .Äëÿ îïðåäåëåííîñòè áóäåì ïîëàãàòü, ÷òî I |= A0(åñëè I |= ¬A0, òî ðàññóæäåíèÿ áóäóò àíàëîãè÷íû).Ïîêàæåì, ÷òî I 6|= S 00.Ò.
ê. S 0 ïðîòèâîðå÷èâàÿ ñèñòåìà, âåðíî I 6|= S10 ∪ S20 ∪ S30 .Ò. ê. I |= A0 è S10 = {D : D ∈ S 0, D = Db ∨ A0}, âåðíî I |= S10 .Çíà÷èò, I 6|= S20 ∪ S30 .Âîçìîæíû äâà âàðèàíòà.Âàðèàíò 1. I 6|= S30 .ÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀÄîêàçàòåëüñòâî ëåììû.Ðàññìîòðèì ïðîèçâîëüíóþ èíòåðïðåòàöèþ I .Äëÿ îïðåäåëåííîñòè áóäåì ïîëàãàòü, ÷òî I |= A0(åñëè I |= ¬A0, òî ðàññóæäåíèÿ áóäóò àíàëîãè÷íû).Ïîêàæåì, ÷òî I 6|= S 00.Ò.
ê. S 0 ïðîòèâîðå÷èâàÿ ñèñòåìà, âåðíî I 6|= S10 ∪ S20 ∪ S30 .Ò. ê. I |= A0 è S10 = {D : D ∈ S 0, D = Db ∨ A0}, âåðíî I |= S10 .Çíà÷èò, I 6|= S20 ∪ S30 .Âîçìîæíû äâà âàðèàíòà.Âàðèàíò 1. I 6|= S30 . Òîãäà I 6|= S 00, ÷òî è òðåáîâàëîñü.ÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀI |= A0''$'S01b1 ∨ A0D$S02$'íåò ëèòåð A0, ¬A0b2 ∨ ¬A0D&&%&%&b1 ∨ Db2D&&%%$''S0 $S03S00'$S00 $S03íåò ëèòåð A0, ¬A0&%%%ÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀI |= A0''$'S01trueb1 ∨ A0D$S02$'íåò ëèòåð A0, ¬A0b2 ∨ ¬A0D&&%&%&b1 ∨ Db2D&&%%$''S0 $S03S00'$S00 $S03íåò ëèòåð A0, ¬A0&%%%ÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀI |= A0''S01true$'b1 ∨ A0DÂàðèàíò 1.S02b2 ∨ ¬A0D$S0 $S03$'íåò ëèòåð A0, ¬A0I 6|= D&&%&%&$''b1 ∨ Db2D&&%%S00'$S00 $S03íåò ëèòåð A0, ¬A0&%%%ÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀI |= A0''S01true$'b1 ∨ A0DÂàðèàíò 1.S02$S0 $S03$'íåò ëèòåð A0, ¬A0b2 ∨ ¬A0DI 6|= D&&%&%&$''b1 ∨ Db2D&&%%S00$'S00 $S03íåò ëèòåð A0, ¬A0I 6|= D%&%%ÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀÄîêàçàòåëüñòâî ëåììû.Âàðèàíò 2.
I 6|= S20 .Çíà÷èò, ñóùåñòâóåò òàêîé äèçúþíêò Db2 ∨ ¬A0 ∈ S20 , ÷òîb2 ∨ ¬A0 . Ñëåäîâàòåëüíî, I 6|= Db2 (ïî÷åìó? ).I 6|= DÐàññìîòðèì òåïåðü èíòåðïðåòàöèþ I 0, êîòîðàÿ îòëè÷àåòñÿ îò Iòîëüêî òåì, ÷òî I 0 6|= A0.Ò. ê. I 0 6|= S10 ∪ S20 ∪ S30 (âåäü S 0 ïðîòèâîðå÷èâàÿ),b ∨ ¬A0 } è I 0 |= ¬A0 ),I 0 |= S20 (âåäü S20 = {D : D ∈ S 0 , D = D00I |= S3 (à èíà÷å ìû áû èìåëè âàðèàíò 1, âåäü A0 ∈/ S30 ),âåðíî I 0 6|= S10 .Çíà÷èò, ñóùåñòâóåò òàêîé äèçúþíêò Db1 ∨ A0 ∈ S10 , ÷òîb1 ∨ A0 . Ñëåäîâàòåëüíî, I 0 6|= Db1 . À ïîñêîëüêó A0 ∈b1 , à II 0 6|= D/D0îòëè÷àåòñÿ îò I òîëüêî îöåíêîé àòîìà A0, âåðíî I 6|= Db1 .ÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀI |= A0''S01true$'b1 ∨ A0D&&Âàðèàíò 2.S02b2 ∨ ¬A0D%&b1 ∨ Db2D&&true$S03%%$S00$'S00 $S03íåò ëèòåð A0, ¬A0%&$íåò ëèòåð A0, ¬A0%&''$'S0%%ÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀI |= A0''S01true$'b1 ∨ A0DÂàðèàíò 2.S02b2 ∨ ¬A0D'$true$S0$S03íåò ëèòåð A0, ¬A0b2I 6|= D&&%&%&$''b1 ∨ Db2D&&%%S00$'S00 $S03íåò ëèòåð A0, ¬A0%&%%ÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀI |= A0''S01true$'b1 ∨ A0DÂàðèàíò 2.S02b2 ∨ ¬A0D'$true$S0$S03íåò ëèòåð A0, ¬A0b2I 6|= D&&%&%&$''S00b1 ∨ Db2D&&%%b2I 6|= D$'S00 $S03íåò ëèòåð A0, ¬A0%&%%ÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀI0 6|= A0''S01$'b1 ∨ A0DÂàðèàíò 2.S02b2 ∨ ¬A0D'$true$S0$S03íåò ëèòåð A0, ¬A0b2I 6|= D&&%&%&$''S00b1 ∨ Db2D&&%%b2I 6|= D$'S00 $S03íåò ëèòåð A0, ¬A0%&%%ÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀI0 6|= A0''S01'$S02b1 ∨ A0Db2 ∨ ¬A0Db1I0 6|= Db2I 6|= D&&%&'$trueíåò ëèòåð A0, ¬A0%%$'S00b1 ∨ Db2Db2I 6|= D$'S00 $S03íåò ëèòåð A0, ¬A0%&$S0 $S03%&'&&Âàðèàíò 2.%%ÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀI0 6|= A0''S01'$S02b1 ∨ A0Db2 ∨ ¬A0Db1I0 6|= Db2I 6|= D&&%&trueíåò ëèòåð A0, ¬A0%%$'S00b1 ∨ Db2Db1I0 6|= D'$b2I 6|= D$'S00 $S03íåò ëèòåð A0, ¬A0%&$S0 $S03%&'&&Âàðèàíò 2.%%ÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀI0 6|= A0''S01'$S02b1 ∨ A0Db2 ∨ ¬A0Db1I0 6|= Db2I 6|= D&&%&trueíåò ëèòåð A0, ¬A0%%$S00b1 ∨ Db2Db1 ∨ Db2I 6|= D&&'$$'S00 $S03íåò ëèòåð A0, ¬A0%&$S0 $S03%&''Âàðèàíò 2.%%ÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀÄîêàçàòåëüñòâî ëåììû.Âàðèàíò 2.Ò.ê.
I 6|= Db1 è I 6|= Db2, âåðíî I 6|= Db1 ∨ Db2.Îñòàåòñÿ çàìåòèòü, ÷òî Db1 ∨ Db2 ýòî ðåçîëüâåíòà äèçúþíêòîâb2 ∨ ¬A0 ∈ S 0 è Db1 ∨ A0 ∈ S 0 , è ïîýòîìó Db1 ∨ Db2 ∈ S 0D210ÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀÄîêàçàòåëüñòâî ëåììû.Âàðèàíò 2.Ò.ê. I 6|= Db1 è I 6|= Db2, âåðíî I 6|= Db1 ∨ Db2.Îñòàåòñÿ çàìåòèòü, ÷òî Db1 ∨ Db2 ýòî ðåçîëüâåíòà äèçúþíêòîâb2 ∨ ¬A0 ∈ S 0 è Db1 ∨ A0 ∈ S 0 , è ïîýòîìó Db1 ∨ Db2 ∈ S 0D210000Ñëåäîâàòåëüíî, I 6|= S0. Òîãäà I 6|= S , ÷òî è òðåáîâàëîñü.ÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀÄîêàçàòåëüñòâî ëåììû.Âàðèàíò 2.Ò.ê.
I 6|= Db1 è I 6|= Db2, âåðíî I 6|= Db1 ∨ Db2.Îñòàåòñÿ çàìåòèòü, ÷òî Db1 ∨ Db2 ýòî ðåçîëüâåíòà äèçúþíêòîâb2 ∨ ¬A0 ∈ S 0 è Db1 ∨ A0 ∈ S 0 , è ïîýòîìó Db1 ∨ Db2 ∈ S 0D210000Ñëåäîâàòåëüíî, I 6|= S0. Òîãäà I 6|= S , ÷òî è òðåáîâàëîñü.Èòàê, â îáîèõ ñëó÷àÿõ I 6|= S 00. Ò. ê. I ïðîèçâîëüíàÿèíòåðïðåòàöèÿ, ïðèõîäèì ê çàêëþ÷åíèþ î òîì, ÷òî ñèñòåìàäèçúþíêòîâ S 00 = S00 ∪ S30I ïðîòèâîðå÷èâàÿ,I ïîëó÷åíà èç S 0 ïðè ïîìîùè ïðàâèëà ðåçîëþöèè,I íå ñîäåðæèò àòîìà A0 .Èíäóêòèâíûé ïåðåõîä çàâåðøåí, è ëåììà äîêàçàíà.ÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀËåììà î ïîäúåìåÏóñòü D1 è D1 äâà äèçúþíêòà, è ïðè ýòîì VarD ∩ VarD = ∅.Ïóñòü D10 = D1θ è D20 = D2θ äâà îñíîâíûõ ïðèìåðà ýòèõäèçúþíêòîâ D1 è D1.Ïóñòü D00 ðåçîëüâåíòà äèçúþíêòîâ D10 è D20 .Òîãäà èç äèçúþíêòîâ D1 è D2 ðåçîëþòèâíî âûâîäèì äèçúþíêòD0 , îñíîâíûì ïðèìåðîì êîòîðîé ÿâëÿåòñÿ äèçúþíêò D00 .12ÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀËåììà î ïîäúåìåD1D2?D10?D20= D1 θ@@@@R@D00= D2 θÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀËåììà î ïîäúåìåD1D2@@@@@RD0?D10?D20= D1 θ@@@@R@?D00= D2 θÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀËåììà î ïîäúåìåD1D2@@@@@RD0?D106?D20= D1 θ@@@@R@?D00= D2 θÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀÄîêàçàòåëüñòâî ëåììû î ïîäúåìåÏóñòü L00, ¬L00 ýòî êîíòðàðíàÿ ïàðà ëèòåð, ïî êîòîðîé áûëàïîñòðîåíà ðåçîëüâåíòà D00 äèçúþíêòîâ D10 è D20 .b 0 ∨ L0 ,D10 = D1000b ∨ ¬L0 ,D2 = D20b0 ∨ Db0 .D00 = D12Ïîñêîëüêó VarD ∩ VarD = ∅, ïîäñòàíîâêó θ ìîæíî ðàçäåëèòüíà äâå ïîëîâèíû θ1, θ2 òàê, ÷òî12θ = θ1 ∪ θ2 , Domθ1 ⊆ VarD1 , Domθ2 ⊆ VarD2 .ÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀÄîêàçàòåëüñòâî ëåììû î ïîäúåìåD1D2??b 0 ∨ L0 = D1 θ1D10b 0 ∨ ¬L0 = D2 θ2D20@@@@R@b0b0 ∨ DD12ÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀÄîêàçàòåëüñòâî ëåììû î ïîäúåìåÏîñêîëüêó D10 = D1θ1, ëèòåðà L00 ÿâëÿåòñÿ îñíîâíûì ïðèìåðîìíåêîòîðûõ ëèòåð L11, L12, .
. . , L1k , âõîäÿùèõ â ñîñòàâäèçúþíêòà D1, ò.å.L00 = L11 θ = L11 θ1 = · · · = L1k θ1 .Àíàëîãè÷íî, ëèòåðà ¬L00 ÿâëÿåòñÿ îñíîâíûì ïðèìåðîìíåêîòîðûõ ëèòåð ¬L21, ¬L22, . . . , ¬L2k , âõîäÿùèõ â ñîñòàâäèçúþíêòà D2, ò. å.¬L00 = ¬L21 θ2 = ¬L22 θ2 = · · · = ¬L2k θ2 .Çíà÷èò,1122b1 ∨ L11 ∨ L12 ∨ · · · ∨ L1kD1 = D1b2 ∨ ¬L21 ∨ ¬L22 ∨ · · · ∨ ¬L2kD2 = D2ÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀÄîêàçàòåëüñòâî ëåììû î ïîäúåìåb2 ∨ ¬L21 ∨ · · · ∨ ¬L2kD2b1 ∨ L11 ∨ · · · ∨ L1kD1θ1@θ2@@ @R@R@@@@@R@b 0 ∨ L0 = D1 θ1D10R@b 0 ∨ ¬L0 = D2 θ2D20@@@@@Rb0 ∨ Db0D12ÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀÄîêàçàòåëüñòâî ëåììû î ïîäúåìåÒàê êàê L00 = L11θ = L12θ1 = · · · = L1k θ1, ëèòåðûL11 , L12 , . . . , L1k óíèôèöèðóåìû. Çíà÷èò, îíè èìåþò ÍÎÓ η1 ,ò.
å.η1 ∈ ÍÎÓ(L11 , L12 , . . . , L1k ), θ1 = η1 ρ1 .Çíà÷èò D1η1 ñêëåéêà äèçúþíêòà D1 ïî ëèòåðàìL11 , L12 , . . . , L1k , è ïðè ýòîì D10 = D1 θ1 = (D1 η1 )ρ1 îñíîâíîéïðèìåð ñêëåéêè D1η2.Àíàëîãè÷íî, ëèòåðû ¬L21, ¬L22, . . . , ¬L2k èìåþò ÍÎÓ η2.Òîãäà D2η2 ñêëåéêà äèçúþíêòà D2 ïî ëèòåðàì¬L21 , ¬L22 , . . . , ¬L2k , è ïðè ýòîì D20 = D2 θ2 = (D1 η2 )ρ2 îñíîâíîé ïðèìåð ñêëåéêè D2η2.111122ÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀÄîêàçàòåëüñòâî ëåììû î ïîäúåìåb2 ∨ ¬L21 ∨ · · · ∨ ¬L2kD2@@η2b1 ∨ L11 ∨ · · · ∨ L1kD1@η1@@ @R@R@@b1 η1 ∨ L11 η1 = D1 η1Dρ1?@R@??b 0 ∨ L0 = D1 η1 ρ1D10R@b2 η2 ¬ ∨ L21 η2 = D2 η2Dρ2?b 0 ∨ ¬L0 = D2 η2 ρ2D20@@@@@Rb0b0 ∨ DD12ÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀÄîêàçàòåëüñòâî ëåììû î ïîäúåìåÑîãëàñíî íàøåé ïðèâû÷êå ïåðåèìåíîâûâàòü ïåðåìåííûå,äèçúþíêòû-ñêëåéêè D1η1 è D2η2 ñîäåðæàò ðàçíûå íàáîðûïåðåìåííûõ.
Ïîýòîìó Domρ ∩ Domρ = ∅, è ñóùåñòâóåòïîäñòàíîâêà ρ = ρ1 ∪ ρ2:1(L11 η1 )ρ = (L11 η1 )ρ1 ,2(L21 η2 )ρ = (L21 η2 )ρ2Òàê êàê L00 = L11η1ρ1 è ¬L00 = ¬L21η2ρ2, âåðíî(L11 η1 )ρ = (L21 η2 )ρ, ò. å. ëèòåðû L11 η1 è L21 η2 óíèôèöèðóåìû.Çíà÷èò, îíè èìåþò ÍÎÓ λ, ò. å.λ ∈ ÍÎÓ(L11 η1 , L21 η2 ), ρ = λµ.Ïîýòîìó äèçúþíêòû-ñêëåéêè D1η1 = Db1η1 ∨ L11η1 èb2 η2 ∨ ¬L21 η2 èìåþò ðåçîëüâåíòó D0 = (Db1 η1 ∨ Db2 η2 )λ,D2 η 2 = Dè ïðè ýòîìb0 ∨ Db0 = Db1 η1 ρ ∨ Db2 η2 ρ = (Db1 η1 ∨ Db2 η2 )λµ = D0 µ.D00 = D12ÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀÄîêàçàòåëüñòâî ëåììû î ïîäúåìåb2 ∨ ¬L21 ∨ · · · ∨ ¬L2kD2@@η2b1 ∨ L11 ∨ · · · ∨ L1kD1@η1@@ @R@R@@@R@R@b1 η1 ∨ L11 η1 = D1 η1b2 η2 ∨ ¬L21 η2 = D2 η2DDXXXXXλ ρρX9z Xb1 η1 ∨ Db2 η2 )λ(D??000bbD1 ∨ L0 = D1 η1 ρD2 ∨ ¬L00 = D2 η2 ρ@µ@@@@?Rb0 ∨ Db0D12ÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀÄîêàçàòåëüñòâî ëåììû î ïîäúåìåÒàêèì îáðàçîì, èç äèçúþíêòîâ D1 è D2 ðåçîëþòèâíî âûâîäèìäèçúþíêò D0, îñíîâíûì ïðèìåðîì êîòîðîãî ÿâëÿíòñÿ D00 .×òî è òðåáîâàëîñü äîêàçàòü â ëåììå î ïîäúåìå.Çàâåðøåíèå äîêàçàòåëüñòâà òåîðåìû ïîëíîòû.Ìû ïîêàçàëè, ÷òî1.
