4. Подстановки. Табличный вывод. Корректность табличного вывода (1158019)

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла

Îñíîâûìàòåìàòè÷åñêîéëîãèêèèëîãè÷åñêîãîïðîãðàììèðîâàíèÿËÅÊÒÎÐ: Â.À. Çàõàðîâ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, .

Характеристики

Тип файла PDF

PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.

Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.

Список файлов лекций