4. Подстановки. Табличный вывод. Корректность табличного вывода (В.А. Захаров - Лекции)
Описание файла
Файл "4. Подстановки. Табличный вывод. Корректность табличного вывода" внутри архива находится в папке "В.А. Захаров - Лекции". PDF-файл из архива "В.А. Захаров - Лекции", который расположен в категории "". Всё это находится в предмете "математическая логика и логическое программирование" из 7 семестр, которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .
Просмотр PDF-файла онлайн
Текст из PDF
Îñíîâûìàòåìàòè÷åñêîéëîãèêèèëîãè÷åñêîãîïðîãðàììèðîâàíèÿËÅÊÒÎÐ: Â.À. Çàõàðîâzakh@cs.msu.suËåêöèÿ 4.Ïîäñòàíîâêè.Òàáëè÷íûé âûâîä.Êîððåêòíîñòü òàáëè÷íîãî âûâîäà.ÏÎÄÑÒÀÍÎÂÊÈÏîäñòàíîâêà ýòî âñÿêîå îòîáðàæåíèå θ : Var → Term,ñîïîñòàâëÿþùåå êàæäîé ïåðåìåííîé íåêîòîðûé òåðì.Ïîäñòàíîâêè íóæíû äëÿ òîãî, ÷òîáû èìåòü âîçìîæíîñòüïåðåõîäèòü îò îáùèõ óòâåðæäåíèé ∀x∀yP(x, y ) ê èõ ÷àñòíûìâàðèàíòàì P(f (z), c).Ìíîæåñòâî Domθ = {x : θ(x) 6= x} íàçûâàåòñÿ îáëàñòüþïîäñòàíîâêè . Åñëè îáëàñòü ïîäñòàíîâêè ýòî êîíå÷íîåìíîæåñòâî ïåðåìåííûõ, òî òàêàÿ ïîäñòàíîâêà íàçûâàåòñÿêîíå÷íîé. Ìíîæåñòâî êîíå÷íûõ ïîäñòàíîâîê îáîçíà÷èì Subst .Åñëè θ ∈ Subst è Domθ = {x1, x2, .
. . , xn }, òî ïîäñòàíîâêà θîäíîçíà÷íî îïðåäåëÿåòñÿ ìíîæåñòâîì ïàð{x1 /θ(x1 ), x2 /θ(x2 ), . . . , xn /θ(xn )}.Êàæäàÿ ïàðà xi /θ(xi ) íàçûâàåòñÿ ñâÿçêîé .ÏÎÄÑÒÀÍÎÂÊÈÄëÿ çàäàííîãî ëîãè÷åñêîãî âûðàæåíèÿ E è ïîäñòàíîâêè θçàïèñü E θ îáîçíà÷àåò ðåçóëüòàò ïðèìåíåíèÿ ïîäñòàíîâêè θ ê E ,êîòîðûé îïðåäåëåòñÿ òàê:Åñëè E = x, x ∈ Var , òî E θ = θ(x);Åñëè E = c, c ∈ Const , òî E θ = c ;Åñëè E = f (t1, t2, . . .
, tk ), òî E θ = f (t1θ, t2θ, . . . , tn θ);Åñëè E = P(t1, t2, . . . , tk ), òî E θ = P(t1θ, t2θ, . . . , tn θ);Åñëè E = ϕ&ψ, òî E θ = ϕθ & ψθ(àíàëîãè÷íî äëÿ ôîðìóë ϕ ∨ ψ, ϕ → ψ, ¬ϕ);Åñëè E = ∀x0 ϕ, òî E θ = ∀x0 (ϕθ0), ãäå η íîâàÿïîäñòàíîâêà, óäîâëåòâîðÿþùàÿ óñëîâèþθ0 (x) =x0 , åñëè x = x0 ,θ(x), åñëè x 6= x0 ,∃x0 ϕ(àíàëîãè÷íî äëÿ ôîðìóë).ÏÎÄÑÒÀÍÎÂÊÈÏðèìåðϕ : ∀x(P(x) → ¬R(y )) → R(f (x)) ∨ ∃yP(y )θ = { x/g (x, c), y /x, z/f (z) }Âûäåëÿþòñÿ âñå ñâîáîäíûå âõîæäåíèÿ ïåðåìåííûõ â ϕϕ : ∀x(P(x) → ¬R(y )) → R(f (x)) ∨ ∃yP(y )Ê ñâîáîäíûì âõîæäåíèÿì ïåðåìåííûõ ïðèìåíÿåòñÿ θϕθ : ∀x(P(x) → ¬R(x)) → R(f (g (x, c))) ∨ ∃yP(y )ÏÎÄÑÒÀÍÎÂÊÈ ðåçóëüòàòå ïðèìåíåíèÿ íåêîòîðûõ ïîäñòàíîâîê ñìûñëóòâåðæäåíèé (ôîðìóë) ìîæåò çíà÷èòåëüíî èñêàçèòüñÿ.¾Åñëè ó êàæäîãî åñòü äåä, òî ó ñóáúåêòà x òîæå åñòü äåä¿ϕ(x) : ∀x∃yP(x, y ) → ∃yP(x, y )Î÷åâèäíî, |= ϕ(x)Ïðèìåíèì ê ϕ(x) ïîäñòàíîâêó θ = { x/y }ϕ(x)θ : ∀x∃yP(x, y ) → ∃yP(y , y )¾Åñëè ó êàæäîãî åñòü äåä, òî åñòü è òàêèå, êîòîðûå ïðèõîäÿòñÿäåäîì ñàìèì ñåáå¿Î÷åâèäíî, 6|= ϕ(x)θÊàê ñòðàííî: îáùåå óòâåðæäåíèå ϕ(x) âåðíî, à åãî ÷àñòíûéñëó÷àé ϕ(x)θ íåò.ÏÎÄÑÒÀÍÎÂÊÈÏåðåìåííàÿ x íàçûâàåòñÿ ñâîáîäíîé äëÿ òåðìà t â ôîðìóëåϕ(x), åñëè ëþáîå ñâîáîäíîå âõîæäåíèå ïåðåìåííîé x âôîðìóëå ϕ(x) íå ëåæèò â îáëàñòè äåéñòâèÿ íè îäíîãîêâàíòîðà, ñâÿçûâàþùåãî ïåðåìåííóþ èç ìíîæåñòâà Vart .Ïîäñòàíîâêà θ = { x1/t1, .
. . , xn /tn } íàçûâàåòñÿ ïðàâèëüíîé äëÿôîðìóëû ϕ, åñëè äëÿ ëþáîé ñâÿçêè xi /ti ïåðåìåííàÿ xiñâîáîäíà äëÿ òåðìà ti â ôîðìóëå ϕ.ÏðèìåðÏåðåìåííàÿ y íå ÿâëÿåòñÿ ñâîáîäíîé äëÿ òåðìà f (x, z) âôîðìóëå ϕϕ : ∀x(P(x) → ¬R(y )) → R(f (x)) ∨ ∃yP(y )À âîò äëÿ òåðìà f (y , z) ïåðåìåííàÿ y â ôîðìóëå ϕ ñâîáîäíà.ÒÀÁËÈ×ÍÛÉ ÂÛÂÎÄÏðàâèëà òàáëè÷íîãî âûâîäà èìåþò âèäT0 ,T0èëèT1T1, T2ãäå T0, T1, T2 ñåìàíòè÷åñêèå òàáëèöû.
Ïðî÷òåíèå ïðàâèëàòàêîâî:Òàáëèöà T0 âûïîëíèìà òîãäà è òîëüêî òîãäà, êîãäàâûïîëíèìà òàáëèöà T1 (èëè T2 ). òåõ ñëó÷àÿõ, êîãäà òàáëèöà T0 ðåäóöèðóåòñÿ â ïàðó òàáëèöT1 , T2 , áóäåì ãîâîðèòü, ÷òî ïðàâèëî èìååò àëüòåðíàòèâû.ÒÀÁËÈ×ÍÛÉ ÂÛÂÎÄÏðàâèëà òàáëè÷íîãî âûâîäàL&hΓ, ϕ&ψ|∆ihΓ, ϕ, ψ|∆iL∨hΓ, ϕ ∨ ψ|∆iR∨hΓ, ϕ|∆i, hΓ, ψ|∆iL→hΓ, ϕ → ψ|∆ihΓ|∆, ϕ → ψiR→hΓ, ψ|∆i, hΓ|ϕ, ∆ihΓ, ϕ|∆, ψiL¬hΓ, ¬ϕ|∆ihΓ|∆, ϕiR&R¬hΓ|∆, ϕ&ψihΓ|∆, ϕi, hΓ | ∆, ψihΓ|∆, ϕ ∨ ψihΓ|∆, ϕ, ψihΓ|∆, ¬ϕihΓ, ϕ|∆iÒÀÁËÈ×ÍÛÉ ÂÛÂÎÄÏðàâèëà òàáëè÷íîãî âûâîäàL∀hΓ, ∀xϕ(x)|∆ihΓ, ∀xϕ(x), ϕ(x){x/t}|∆ix ñâîáîäíàϕ(x)ïåðåìåííàÿâ ôîðìóëåR∀äëÿ òåðìàthΓ|∆, ∀xϕ(x)ihΓ|∆, ϕ(x){x/c}iêîíñòàíòàèçΓ, ∆cíå ñîäåðæèòñÿ â ôîðìóëàõè â ôîðìóëåϕ(x)ÒÀÁËÈ×ÍÛÉ ÂÛÂÎÄÏðàâèëà òàáëè÷íîãî âûâîäàL∃hΓ, ∃xϕ(x)|∆ihΓ, ϕ(x){x/c}|∆iêîíñòàíòàèçR∃Γ, ∆cíå ñîäåðæèòñÿ â ôîðìóëàõè â ôîðìóëåϕ(x)hΓ|∆, ∃xϕ(x)ihΓ|∆, ∃xϕ(x), ϕ(x){x/t}ix ñâîáîäíàϕ(x)ïåðåìåííàÿâ ôîðìóëåäëÿ òåðìàtÒÀÁËÈ×ÍÛÉ ÂÛÂÎÄÇà÷åì íóæíû îãðàíè÷åíèÿ íà ïîäñòàâëÿåìûå òåðìûâ ïðàâèëàõ L∀, R∀, L∃, R∃?Åñëè â ïðàâèëå òàáëè÷íîãî âûâîäà L∀ íå ïðèäåðæèâàòüñÿïðàâèëüíûõ ïîäñòàíîâîê, òî âûïîëíèìàÿ òàáëèöà− L∀ :h ∀x∃yR(x, y ) | ∃yR(y , y ) ih ∀x∃yR(x, y ), ∃yR(y , y ) | ∃yR(y , y ) iïðåîáðàçóåòñÿ â çàêðûòóþ, ò.å.
íåâûïîëíèìóþ òàáëèöó .Ïðè÷èíà â òîì, ÷òî ïåðåìåííàÿ x íåñâîáîäíà äëÿ òåðìà y âôîðìóëå ∃yR(x, y ).ÒÀÁËÈ×ÍÛÉ ÂÛÂÎÄÇà÷åì íóæíû îãðàíè÷åíèÿ íà ïîäñòàâëÿåìûå òåðìûâ ïðàâèëàõ L∀, R∀, L∃, R∃?Åñëè â ïðàâèëå òàáëè÷íîãî âûâîäà L∃ ïîäñòàâèòü ¾íåñâåæóþ¿êîíñòàíòó, òî âûïîëíèìàÿ òàáëèöà− L∃ :h ∃x P(x) | P(c) ih P(c) | P(c) iïðåîáðàçóåòñÿ â çàêðûòóþ, ò.å. íåâûïîëíèìóþ òàáëèöó .Ïðè÷èíà â òîì, ÷òî êîíñòàíòà, ïîäñòàâëÿåìàÿ âìåñòîïåðåìåííîé x, äîëæíà áûòü îòëè÷íà îò âñåõ ðàíååèñïîëüçîâàííûõ êîíñòàíò.ÒÀÁËÈ×ÍÛÉ ÂÛÂÎÄÎïðåäåëåíèå òàáëè÷íîãî âûâîäàÒàáëè÷íûé âûâîä äëÿ òàáëèöû T0 ýòî êîðíåâîå äåðåâî,âåðøèíàìè êîòîðîãî ñëóæàò ñåìàíòè÷åñêèå òàáëèöû è ïðè ýòîì1) êîðíåì äåðåâà ÿâëÿåòñÿ òàáëèöà T0;yT0@Tyj?yT3@@TR yT@y1i@@@@@@R yT@R yT@2k?yT4ÒÀÁËÈ×ÍÛÉ ÂÛÂÎÄÎïðåäåëåíèå òàáëè÷íîãî âûâîäà2)èç âåðøèíû Ti èñõîäÿò äóãè â âåðøèíû Tj (Tk )⇐⇒TiTj , (Tk ) ïðàâèëî òàáëè÷íîãî âûâîäà;TyjL∃yT0@L→ @@TR yT@y1i@@R& @L∀ @@@R yT@R yT@2kR¬?yT3?Ty4ÒÀÁËÈ×ÍÛÉ ÂÛÂÎÄÎïðåäåëåíèå òàáëè÷íîãî âûâîäà3) ëèñòüÿìè äåðåâà ìîãóò áûòü òîëüêî çàêðûòûå èàòîìàðíûå òàáëèöû.TyjyT0@L→ @@TR yT@y1i@@R& @L∀ @@@R yT@R yT@2kL∃àòîì.
òàáë.R¬?yT3çàêð. òàáë.?Ty4çàêð. òàáë.ÒÀÁËÈ×ÍÛÉ ÂÛÂÎÄÎïðåäåëåíèå òàáëè÷íîãî âûâîäàÒàáëè÷íûé âûâîä áóäåì íàçûâàòü óñïåøíûì (èëè òàáëè÷íûìîïðîâåðæåíèåì ), åñëè äåðåâî âûâîäà êîíå÷íîå, è âñå ëèñòüÿäåðåâà çàêðûòûå òàáëèöû.Ñóùåñòâîâàíèå óñïåøíîãî âûâîäà îçíà÷àåò, ÷òî êîðíåâàÿñåìàíòè÷åñêàÿ òàáëèöà T0 íåâûïîëíèìà.Åñëè T0 = h ∅ | ϕ i, òî ýòî îçíà÷àåò, ÷òî |= ϕ.T0 = h ∅ | ∀x(P(x) → B(x)) → (∀xP(x) → ∀xB(x)) iT0 = h ∅ | ∀x(P(x) → B(x)) → (∀xP(x) → ∀xB(x)) iR→(?)T1 = h ∀x(P(x) → B(x)) | ∀xP(x) → ∀xB(x) iT0 = h ∅ | ∀x(P(x) → B(x)) → (∀xP(x) → ∀xB(x)) iR→()?T1 = h ∀x(P(x) → B(x)) | ∀xP(x) → ∀xB(x) iR→(?)T2 = h ∀x(P(x) → B(x)), ∀xP(x) | ∀xB(x) iT0 = h ∅ | ∀x(P(x) → B(x)) → (∀xP(x) → ∀xB(x)) iR→()?T1 = h ∀x(P(x) → B(x)) | ∀xP(x) → ∀xB(x) iR→()?T2 = h ∀x(P(x) → B(x)), ∀xP(x) | ∀xB(x) iR∀( )?T3 = h ∀x(P(x) → B(x)), ∀xP(x) | B(c) iT0 = h ∅ | ∀x(P(x) → B(x)) → (∀xP(x) → ∀xB(x)) iR→()?T1 = h ∀x(P(x) → B(x)) | ∀xP(x) → ∀xB(x) iR→()?T2 = h ∀x(P(x) → B(x)), ∀xP(x) | ∀xB(x) iR∀( )?T3 = h ∀x(P(x) → B(x)), ∀xP(x) | B(c) iL∀( )?T4 = h ∀x(P(x) → B(x)), ∀xP(x), P(c) | B(c) iT0 = h ∅ | ∀x(P(x) → B(x)) → (∀xP(x) → ∀xB(x)) iR→()?T1 = h ∀x(P(x) → B(x)) | ∀xP(x) → ∀xB(x) iR→()?T2 = h ∀x(P(x) → B(x)), ∀xP(x) | ∀xB(x) iR∀( )?T3 = h ∀x(P(x) → B(x)), ∀xP(x) | B(c) iL∀( )?T4 = h ∀x(P(x) → B(x)), ∀xP(x), P(c) | B(c) iL∀( )?T5 = h ∀x(P(x) → B(x)), P(c) → B(c), ∀xP(x), P(c) | B(c) iT0 = h ∅ | ∀x(P(x) → B(x)) → (∀xP(x) → ∀xB(x)) iR→()?T1 = h ∀x(P(x) → B(x)) | ∀xP(x) → ∀xB(x) iR→()?T2 = h ∀x(P(x) → B(x)), ∀xP(x) | ∀xB(x) iR∀( )?T3 = h ∀x(P(x) → B(x)), ∀xP(x) | B(c) iL∀( )?T4 = h ∀x(P(x) → B(x)), ∀xP(x), P(c) | B(c) iL∀( )?T5 = h ∀x(P(x) → B(x)), P(c) → B(c), ∀xP(x), P(c) | B(c) iPPL→PP)()qPT6 = h∀x(P(x) → B(x)), |B(c)i T7 = h∀x(P(x) → B(x)), |B(c), P(c)i∀xP(x), B(c), P(c)∀xP(x), P(c)T0 = h ∅ | ∀x(P(x) → B(x)) → (∀xP(x) → ∀xB(x)) iR→()?T1 = h ∀x(P(x) → B(x)) | ∀xP(x) → ∀xB(x) iR→()?T2 = h ∀x(P(x) → B(x)), ∀xP(x) | ∀xB(x) iR∀( )?T3 = h ∀x(P(x) → B(x)), ∀xP(x) | B(c) iL∀( )?T4 = h ∀x(P(x) → B(x)), ∀xP(x), P(c) | B(c) iL∀( )?T5 = h ∀x(P(x) → B(x)), P(c) → B(c), ∀xP(x), P(c) | B(c) iPPL→PP)()qPT6 = h∀x(P(x) → B(x)), |B(c)i T7 = h∀x(P(x) → B(x)), |B(c), P(c)i∀xP(x), B(c), P(c)∀xP(x), P(c)T0 = h ∅ | ∀x(P(x) → B(x)) → (∀xP(x) → ∀xB(x)) iR→()?T1 = h ∀x(P(x) → B(x)) | ∀xP(x) → ∀xB(x) iR→()?T2 = h ∀x(P(x) → B(x)), ∀xP(x) | ∀xB(x) iR∀( )?T3 = h ∀x(P(x) → B(x)), ∀xP(x) | B(c) iL∀( )?T4 = h ∀x(P(x) → B(x)), ∀xP(x), P(c) | B(c) iL∀( )?T5 = h ∀x(P(x) → B(x)), P(c) → B(c), ∀xP(x), P(c) | B(c) iPPL→PP)()qPT6 = h∀x(P(x) → B(x)), |B(c)i T7 = h∀x(P(x) → B(x)), |B(c), P(c)i∀xP(x), B(c), P(c)∀xP(x), P(c)çàêðûòàÿ òàáëèöàçàêðûòàÿ òàáëèöàT0 = h ∅ | ∃x(P(x) → ∀xP(x) iT0 = h ∅ | ∃x(P(x) → ∀xP(x) iR→(?)T1 = h ∃xP(x) | ∀xP(x) iT0 = h ∅ | ∃x(P(x) → ∀xP(x) iR→()?T1 = h ∃xP(x) | ∀xP(x) iL∃( )?T2 = h P(c1 ) | ∀xP(x) iT0 = h ∅ | ∃x(P(x) → ∀xP(x) iR→()?T1 = h ∃xP(x) | ∀xP(x) iL∃( )?T2 = h P(c1 ) | ∀xP(x) iR∀( )?T3 = h P(c1 ) | P(c2 ) iT0 = h ∅ | ∃x(P(x) → ∀xP(x) iR→()?T1 = h ∃xP(x) | ∀xP(x) iL∃( )?T2 = h P(c1 ) | ∀xP(x) iR∀( )?T3 = h P(c1 ) | P(c2 ) iàòîìàðíàÿ òàáëèöàT0 = h ∅ | ∀y ∃xP(x, y ) → ∃x∀yP(x, y ) iT0 = h ∅ | ∀y ∃xP(x, y ) → ∃x∀yP(x, y ) iR→(?)T1 = h ∀y ∃xP(x, y ) | ∃x∀yP(x, y ) iT0 = h ∅ | ∀y ∃xP(x, y ) → ∃x∀yP(x, y ) iR→()?T1 = h ∀y ∃xP(x, y ) | ∃x∀yP(x, y ) iL∀( )?T2 = h ∀y ∃xP(x, y ), ∃xP(x, c1 ) | ∃x∀yP(x, y ) iT0 = h ∅ | ∀y ∃xP(x, y ) → ∃x∀yP(x, y ) iR→()?T1 = h ∀y ∃xP(x, y ) | ∃x∀yP(x, y ) iL∀( )?T2 = h ∀y ∃xP(x, y ), ∃xP(x, c1 ) | ∃x∀yP(x, y ) iR∃( )?T3 = h ∀y ∃xP(x, y ), ∃xP(x, c1 ) | ∀yP(c2 , y ), ∃x∀yP(x, y ) iT0 = h ∅ | ∀y ∃xP(x, y ) → ∃x∀yP(x, y ) iR→()?T1 = h ∀y ∃xP(x, y ) | ∃x∀yP(x, y ) iL∀( )?T2 = h ∀y ∃xP(x, y ), ∃xP(x, c1 ) | ∃x∀yP(x, y ) iR∃( )?T3 = h ∀y ∃xP(x, y ), ∃xP(x, c1 ) | ∀yP(c2 , y ), ∃x∀yP(x, y ) iL∃( )?T4 = h ∀y ∃xP(x, y ), P(c3 , c1 ) | ∀y P(c2 , y ), ∃x∀yP(x, y ) iT0 = h ∅ | ∀y ∃xP(x, y ) → ∃x∀yP(x, y ) iR→()?T1 = h ∀y ∃xP(x, y ) | ∃x∀yP(x, y ) iL∀( )?T2 = h ∀y ∃xP(x, y ), ∃xP(x, c1 ) | ∃x∀yP(x, y ) iR∃( )?T3 = h ∀y ∃xP(x, y ), ∃xP(x, c1 ) | ∀yP(c2 , y ), ∃x∀yP(x, y ) iL∃( )?T4 = h ∀y ∃xP(x, y ), P(c3 , c1 ) | ∀y P(c2 , y ), ∃x∀yP(x, y ) iR∀( )?T5 = h ∀y ∃xP(x, y ), P(c3 , c1 ) | P(c2 , c4 ), ∃x∀yP(x, y ) iT0 = h ∅ | ∀y ∃xP(x, y ) → ∃x∀yP(x, y ) iR→()?T1 = h ∀y ∃xP(x, y ) | ∃x∀yP(x, y ) iL∀( )?T2 = h ∀y ∃xP(x, y ), ∃xP(x, c1 ) | ∃x∀yP(x, y ) iR∃( )?T3 = h ∀y ∃xP(x, y ), ∃xP(x, c1 ) | ∀yP(c2 , y ), ∃x∀yP(x, y ) iL∃( )?T4 = h ∀y ∃xP(x, y ), P(c3 , c1 ) | ∀y P(c2 , y ), ∃x∀yP(x, y ) iR∀( )?T5 = h ∀y ∃xP(x, y ), P(c3 , c1 ) | P(c2 , c4 ), ∃x∀yP(x, y ) i?∞ÊÎÐÐÅÊÒÍÎÑÒÜ ÒÀÁËÈ×ÍÎÃÎ ÂÛÂÎÄÀËåììà î êîððåêòíîñòè ïðàâèë âûâîäàÊàêîâî áû íè áûëî ïðàâèëî òàáëè÷íîãî âûâîäàL&, R&, L∨, R∨, L →, R →, L¬, R¬, L∀, R∀, L∃, R∃T0 ,T1 , (T2 )òàáëèöà T0 âûïîëíèìà òîãäà è òîëüêî òîãäà, êîãäàâûïîëíèìà òàáëèöà T1 (èëè âûïîëíèìà òàáëèöà T2 ).ÊÎÐÐÅÊÒÍÎÑÒÜ ÒÀÁËÈ×ÍÎÃÎ ÂÛÂÎÄÀÄîêàçàòåëüñòâî ëåììûϕ → ψ|∆iÐàññìîòðèì ïðàâèëî L →: hΓ,hΓ,ψ|∆i,.hΓ|ϕ, ∆iÒàáëèöà hΓ, ϕ → ψ|∆i âûïîëíèìà ⇐⇒ñóùåñòâóåò èíòåðïðåòàöèÿ I è íàáîð d̄ = hd1, .
. . , dn i çíà÷åíèéñâîáîäíûõ ïåðåìåííûõ, äëÿ êîòîðûõ I |= Γ[d̄],I 6|= ∆[d̄],I |= (ϕ → ψ)[d̄]⇐⇒ I |= Γ[d̄],I 6|= ∆[d̄],I |= ψ[d̄]⇐⇒èëè I |= Γ[d̄],I 6|= ∆[d̄],I |= ψ[d̄] èëè I 6|= ϕ[d̄] I |= Γ[d̄],I 6|= ∆[d̄],I 6|= ϕ[d̄]⇐⇒⇐⇒îäíà èç òàáëèö T1 = hΓ, ψ|∆i èëè T2 = hΓ|ϕ, ∆i âûïîëíèìà.ÊÎÐÐÅÊÒÍÎÑÒÜ ÒÀÁËÈ×ÍÎÃÎ ÂÛÂÎÄÀÄîêàçàòåëüñòâî ëåììûÀíàëîãè÷íî äîêàçûâàåòñÿ êîððåêòíîñòü îñòàëüíûõ 7 ïðàâèëäëÿ ëîãè÷åñêèõ ñâÿçîêÊÎÐÐÅÊÒÍÎÑÒÜ ÒÀÁËÈ×ÍÎÃÎ ÂÛÂÎÄÀÄîêàçàòåëüñòâî ëåììû∀x0 ϕ(x0 )|∆i.Ðàññìîòðèì ïðàâèëî L∀: hΓ, ∀x0hΓ,ϕ(x0 ), ϕ(x0 ){x0 /t}|∆iÒàáëèöà hΓ, ∀x0ϕ(x0)|∆i âûïîëíèìà ⇐⇒ ñóùåñòâóåòèíòåðïðåòàöèÿ I è íàáîð d1, .
