Лекции В.А. Захарова, страница 5

Òîãäà ñóùåñòâóåòèíòåðïðåòàöèÿ I (êîíòðìîäåëü), êîòîðàÿ îïðîâåðãàåò ϕ.ϕ = ∃x P(x) → ∀x P(x)I |= ∃x P(x)I |= P(x)[d1 ]I |6 = ∃x P(x) → ∀x P(x)I |6 = ∀x P(x)ÏÐÎÁËÅÌÀ ÎÁÙÅÇÍÀ×ÈÌÎÑÒÈ ÔÎÐÌÓËÏðèìåð.Ïðîâåðèòü îáùåçíà÷èìîñòü ôîðìóëû.Ïðåäïîëîæèì, ÷òî ϕ íåîáùåçíà÷èìà. Òîãäà ñóùåñòâóåòèíòåðïðåòàöèÿ I (êîíòðìîäåëü), êîòîðàÿ îïðîâåðãàåò ϕ.ϕ = ∃x P(x) → ∀x P(x)I |= ∃x P(x)I |= P(x)[d1 ]I |6 = ∃x P(x) → ∀x P(x)I |6 = ∀x P(x)I 6|= P(x)[d2 ]ÏÐÎÁËÅÌÀ ÎÁÙÅÇÍÀ×ÈÌÎÑÒÈ ÔÎÐÌÓËÏðèìåð.Ïðîâåðèòü îáùåçíà÷èìîñòü ôîðìóëû.Ïðåäïîëîæèì, ÷òî ϕ íåîáùåçíà÷èìà. Òîãäà ñóùåñòâóåòèíòåðïðåòàöèÿ I (êîíòðìîäåëü), êîòîðàÿ îïðîâåðãàåò ϕ.ϕ = ∃x P(x) → ∀x P(x)I |= ∃x P(x)I |= P(x)[d1 ]I |6 = ∃x P(x) → ∀x P(x)I |6 = ∀x P(x)I 6|= P(x)[d2 ]Ïðîòèâîðå÷èÿ íåò.I = hDI , Predi: DI = {d1 , d2 }, P(d1 ) =, P(d2) =I 6|= ϕ.Ñëåäîâàòåëüíî, 6|= ϕ.true,falseÑÅÌÀÍÒÈ×ÅÑÊÈÅ ÒÀÁËÈÖÛÏîïðîáóåì ñèñòåìàòèçèðîâàòü ýòîò ñïîñîá ïðîâåðêèîáùåçíà÷èìîñòè ôîðìóë.I Îáùåçíà÷èìîñòü ôîðìóëû äîêàçûâàåì ¾îò ïðîòèâíîãî¿,ïûòàÿñü ïîñòðîèòü êîíòðìîäåëü.I Êîíòðìîäåëü ñòðîèì, óêàçûâàÿ, êàêèå ôîðìóëû äîëæíû âíåé âûïîëíÿòüñÿ, à êàêèå íåò.

Òðåáîâàíèÿ(íå)âûïîëíèìîñòè ôîðìóë, ïðåäúÿâëÿåìûå ê êîíòðìîäåëè,ñâîäèì â òàáëèöó è ïîñëåäîâàòåëüíî èõ óòî÷íÿåì.I Åñëè òðåáîâàíèÿ, êîòîðûå ïðåäúÿâëÿþòñÿ ê êîíòðìîäåëè,îêàçûâàþòñÿ íåñîâìåñòíûìè, çíà÷èò, ïðîâåðÿåìàÿôîðìóëà íåîïðîâåðæèìà, ò. å. îáùåçíà÷èìà.ÑÅÌÀÍÒÈ×ÅÑÊÈÅ ÒÀÁËÈÖÛÑåìàíòè÷åñêàÿ òàáëèöà ýòî óïîðÿäî÷åííàÿ ïàðà ìíîæåñòâôîðìóë h Γ ; ∆ i , Γ, ∆ ⊆ Form.Γ ýòî ìíîæåñòâî ôîðìóë, êîòîðûå ìû õîòèì ñ÷èòàòüèñòèííûìè,∆ ýòî ìíîæåñòâî ôîðìóë, êîòîðûå ìû õîòèì ñ÷èòàòüëîæíûìè.Ïóñòü {x1, x2, . . . , xn } ìíîæåñòâî ñâîáîäíûõ ïåðåìåííûõ âôîðìóëàõ ìíîæåñòâ Γ, ∆.Ñåìàíòè÷åñêàÿ òàáëèöà h Γ ; ∆ i íàçûâàåòñÿ âûïîëíèìîé ,åñëè ñóùåñòâóåò òàêàÿ èíòåðïðåòàöèÿ I è òàêîé íàáîð çíà÷åíèéd1 , d2 , .

. . , dn ∈ DI ñâîáîäíûõ ïåðåìåííûõ, äëÿ êîòîðûõI I |= ϕ(x1 , x2 , . . . , xn )[d1 , d2 , . . . , dn ] äëÿ ëþáîé ôîðìóëû ϕ,ϕ ∈ Γ,I I 6|= ψ(x1 , x2 , . . . , xn )[d1 , d2 , . . . , dn ] äëÿ ëþáîé ôîðìóëû ψ ,ψ ∈ ∆.ÑÅÌÀÍÒÈ×ÅÑÊÈÅ ÒÀÁËÈÖÛÏðèìåðûÑåìàíòè÷åñêàÿ òàáëèöàT = h {∃x P(x), ¬P(y )} ; {∀xP(x), P(x) & ¬P(x)} iâûïîëíèìà. Åå âûïîëíèìîñòü ïîäòâåðæäàåò èíòåðïðåòàöèÿ, P(d2) = , èI = hDI , Predi: DI = {d1 , d2 }, P(d1 ) =íàáîð d1, d2 çíà÷åíèé ñâîáîäíûõ ïåðåìåííûõ x, y.Ñåìàíòè÷åñêàÿ òàáëèöàtruefalseT = h ∅ ; {∃y ∀xR(x, y ) → ∀x∃yR(x, y )} iíåâûïîëíèìà. Ïî÷åìó?ÑÅÌÀÍÒÈ×ÅÑÊÈÅ ÒÀÁËÈÖÛÒåîðåìà (î òàáëè÷íîé ïðîâåðêå îáùåçíà÷èìîñòè)|= ϕ ⇐⇒òàáëèöàTϕ = h ∅ ; {ϕ} iíåâûïîëíèìà.Äîêàçàòåëüñòâî. |= ϕ ⇐⇒ äëÿ ëþáîé èíòåðïðåòàöèè I è äëÿëþáîãî íàáîðà d1, . .

. , dn ∈ DI çíà÷åíèé ñâîáîäíûõ ïåðåìåííûõx1 , . . . , xn èìååò ìåñòî I |= ϕ(x1 , . . . , xn )[d1 , . . . , dn ] ⇐⇒òàáëèöà Tϕ = h ∅ ; {ϕ} i íåâûïîëíèìà íè â îäíîéèíòåðïðåòàöèè.ÑÅÌÀÍÒÈ×ÅÑÊÈÅ ÒÀÁËÈÖÛÑåìàíòè÷åñêàÿ òàáëèöà h Γ ;íàçûâàåòñÿ çàêðûòîé .∆i, ó êîòîðîé Γ ∩ ∆ 6= ∅,ÓòâåðæäåíèåÇàêðûòàÿ òàáëèöà íåâûïîëíèìà.Äîêàçàòåëüñòâî. Ñàìîñòîÿòåëüíî.Ñåìàíòè÷åñêàÿ òàáëèöà h Γ ; ∆ i, ó êîòîðîé ìíîæåñòâà Γ, ∆ñîñòîÿò òîëüêî èçôîðìóë, íàçûâàåòñÿ àòîìàðíîé .àòîìàðíûõÓòâåðæäåíèåÍåçàêðûòàÿ àòîìàðíàÿ òàáëèöà âûïîëíèìà.Äîêàçàòåëüñòâî. Ñàìîñòîÿòåëüíî.ÑÅÌÀÍÒÈ×ÅÑÊÈÅ ÒÀÁËÈÖÛÒàêèì îáðàçîì, äëÿ äîêàçàòåëüñòâà îáùåçíà÷èìîñòè |= ϕäîñòàòî÷íî ðàçðàáîòàòü ñèñòåìó ïðàâèë, ïîçâîëÿþùèõïðåîáðàçîâûâàòü ñåìàíòè÷åñêóþ òàáëèöó Tϕ = h ∅ ; {ϕ} i êçàêðûòûì òàáëèöàì.Äîêàçàòåëüñòâà òàêîãî âèäà íàçûâàþòñÿ ëîãè÷åñêèì âûâîäîì .Åñëè â âûâîäå ó÷àñòâóþò ñåìàíòè÷åñêèå òàáëèöû, òîëîãè÷åñêèé âûâîä íàçûâàåòñÿ òàáëè÷íûì .×òîáû òàáëè÷íûé âûâîä áûë êîððåêòíûì, ïðàâèëàïðåîáðàçîâàíèÿ òàáëèö (ïðàâèëà òàáëè÷íîãî âûâîäà ) äîëæíûñîõðàíÿòü âûïîëíèìîñòü ñåìàíòè÷åñêèõ òàáëèö.Ïîýòîìó íà÷íåì ñ ðàçðàáîòêè ïðàâèë òàáëè÷íîãî âûâîäà èïðîâåðêè èõ êîððåêòíîñòè.ÊÎÍÅÖ ËÅÊÖÈÈ 3.Îñíîâûìàòåìàòè÷åñêîéëîãèêèèëîãè÷åñêîãîïðîãðàììèðîâàíèÿËÅÊÒÎÐ: Â.À.

Çàõàðîâ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, .