Лекция 3. Выполнимые и общезначимые формулы. Модели. Логическое следование. Проблема общезначимости. Семантические таблицы (Лекции)

Îñíîâûìàòåìàòè÷åñêîéëîãèêèèëîãè÷åñêîãîïðîãðàììèðîâàíèÿËÅÊÒÎÐ: Â.À. ÇàõàðîâËåêöèÿ 3.Âûïîëíèìûå è îáùåçíà÷èìûåôîðìóëû.Ìîäåëè. Ëîãè÷åñêîå ñëåäîâàíèå.Ïðîáëåìà îáùåçíà÷èìîñòè.Ñåìàíòè÷åñêèå òàáëèöû.ÂÛÏÎËÍÈÌÛÅ È ÎÁÙÅÇÍÀ×ÈÌÛÅÔÎÐÌÓËÛÔîðìóëà ϕ(x1, . . . , xn ) íàçûâàåòñÿ âûïîëíèìîé â èíòåðïðåòàöèèI , åñëè ñóùåñòâóåò òàêîé íàáîð ýëåìåíòîâ d1 , . . . , dn ∈ DI , äëÿêîòîðîãî èìååò ìåñòî I |= ϕ(x1, . .

. , xn )[d1, . . . , dn ].Ôîðìóëà ϕ(x1, . . . , xn ) íàçûâàåòñÿ èñòèííîé â èíòåðïðåòàöèè I ,åñëè äëÿ ëþáîãî íàáîðà ýëåìåíòîâ d1, . . . , dn ∈ DI èìååò ìåñòîI |= ϕ(x1 , . . . , xn )[d1 , . . . , dn ].Ôîðìóëà ϕ(x1, . . . , xn ) íàçûâàåòñÿ âûïîëíèìîé , åñëè åñòüèíòåðïðåòàöèÿ I , â êîòîðîé ýòà ôîðìóëà âûïîëíèìà.Ôîðìóëà ϕ(x1, . . .

, xn ) íàçûâàåòñÿ îáùåçíà÷èìîé (èëèòîæäåñòâåííî èñòèííîé ), åñëè ýòà ôîðìóëà èñòèííà â ëþáîéèíòåðïðåòàöèè.Ôîðìóëà ϕ(x1, . . . , xn ) íàçûâàåòñÿ ïðîòèâîðå÷èâîé (èëèíåâûïîëíèìîé ), åñëè îíà íå ÿâëÿåòñÿ âûïîëíèìîé.ÂÛÏÎËÍÈÌÛÅ È ÎÁÙÅÇÍÀ×ÈÌÛÅÔÎÐÌÓËÛÏðèìåðû,P(x1 )&¬P(x2 )∀xP(x) → ∃xP(x)∃xP(x) → ∀xP(x), âûïîëíèìûå ôîðìóëû.I1 : DI = {d1 , d2 }, P̄(d1 ) = true, P̄(d2 ) = falseI1 |= P(x1 )&¬P(x2 )[d1 , d2 ],I1 |= ∀xP(x) → ∃xP(x).I2 : DI = {d}, P̄(d) = trueI2 |= ∃xP(x) → ∀xP(x)Ôîðìóëû P(x1)&¬P(x2), ∃xP(x) → ∀xP(x) íåîáùåçíà÷èìûå.I2 6|= P(x1 )&¬P(x2 )[d, d],I1 6|= ∃xP(x) → ∀xP(x).Ôîðìóëà ∀xP(x) → ∃xP(x) ÿâëÿåòñÿ îáùåçíà÷èìîé.Íî ïî÷åìó? È êàê â ýòîì óáåäèòüñÿ?ÂÛÏÎËÍÈÌÛÅ È ÎÁÙÅÇÍÀ×ÈÌÛÅÔÎÐÌÓËÛÂûïîëíèìûå ôîðìóëû ýòî ëîãè÷åñêèå ôîðìû, êîòîðûåñëóæàò äëÿ ïðåäñòàâëåíèÿ çíàíèé. Êàæäàÿ âûïîëíèìàÿôîðìóëà íåñåò îïðåäåëåííóþ èíôîðìàöèþ.Îáùåçíà÷èìûå ôîðìóëû ýòî òðþèçìû, áàíàëüíîñòè,òàâòîëîãèè, íå íåñóùèå íèêàêîé èíôîðìàöèè.Êàêóþ æå ðîëü èãðàþò îáùåçíà÷èìûå ôîðìóëû?ÌÎÄÅËÈ.

ËÎÃÈ×ÅÑÊÎÅ ÑËÅÄÑÒÂÈÅÏóñòü Γ íåêîòîðîå ìíîæåñòâî çàìêíóòûõ ôîðìóë, Γ ⊆ CForm.Òîãäà êàæäàÿ èíòåðïðåòàöèÿ I , â êîòîðîé âûïîëíÿþòñÿ âñåôîðìóëû ìíîæåñòâà Γ, íàçûâàåòñÿ ìîäåëüþ äëÿ ìíîæåñòâà Γ.Ìîäåëü äëÿ ìíîæåñòâà ôîðìóë Γ ýòî èíòåðïðåòàöèÿ(ðåàëüíûé èëè âèðòóàëüíûé ìèð), óñòðîéñòâî êîòîðîãîàäåêâàòíî âñåì ïðåäëîæåíèÿì èç ìíîæåñòâà Γ.ÏðèìåðI : DI = {d1 , d2 }, P̄(d1 ) = true, P̄(d2 ) = falseI ìîäåëü äëÿ ìíîæåñòâà ôîðìóë Γ = {∃xP(x), ∃x¬P(x)}.Çàìå÷àíèåÀ êàêàÿ èíòåðïðåòàöèÿ ÿâëÿåòñÿ ìîäåëüþ ïóñòîãî ìíîæåñòâàôîðìóë Γ = ∅?Ïðàâèëüíûé îòâåò: ëþáàÿ èíòåðïðåòàöèÿ . Ïî÷åìó ?ÌÎÄÅËÈ. ËÎÃÈ×ÅÑÊÎÅ ÑËÅÄÑÒÂÈÅÏðèìåð ¾x êâàäðàò¿;S(x) ¾x øàð¿;B(x) ¾x ÷åðíûé ïðåäìåò¿;W (x) ¾x áåëûé ïðåäìåò¿;U(x, y ) ¾ïðåäìåò x ëåæèò ïîä ïðåäìåòîì y ¿.C (x)ÌÎÄÅËÈ. ËÎÃÈ×ÅÑÊÎÅ ÑËÅÄÑÒÂÈÅÊàæäûé áåëûé êóá ëåæèò ïîä êàêèì-òî ÷åðíûì øàðîì.∀x (W (x) & C (x) → ∃y (B(y ) & S(y ) & U(x, y )))~Ìîäåëü~~I∀x (W (x) & C (x) & ∃y (B(y ) & S(y ) & U(x, y )))Êàæäûé ïðåäìåò ÿâëÿåòñÿ áåëûì êóáîìè ëåæèò ïîä êàêèì-òî ÷åðíûì øàðîì.ÌÎÄÅËÈ.

ËÎÃÈ×ÅÑÊÎÅ ÑËÅÄÑÒÂÈÅÊàêîé-òî áåëûé êóá ëåæèò ïîä âñåìè ÷åðíûìè øàðàìè.ÌÎÄÅËÈ. ËÎÃÈ×ÅÑÊÎÅ ÑËÅÄÑÒÂÈÅÊàêîé-òî áåëûé êóá ëåæèò ïîä âñåìè ÷åðíûìè øàðàìè.∃x (W (x) & C (x) & ∀y (B(y ) & S(y ) → U(x, y )))ÌÎÄÅËÈ. ËÎÃÈ×ÅÑÊÎÅ ÑËÅÄÑÒÂÈÅÊàêîé-òî áåëûé êóá ëåæèò ïîä âñåìè ÷åðíûìè øàðàìè.∃x (W (x) & C (x) & ∀y (B(y ) & S(y ) → U(x, y )))~ÌîäåëüIÌÎÄÅËÈ.

ËÎÃÈ×ÅÑÊÎÅ ÑËÅÄÑÒÂÈÅÊàêîé-òî áåëûé êóá ëåæèò ïîä âñåìè ÷åðíûìè øàðàìè.∃x (W (x) & C (x) & ∀y (B(y ) & S(y ) → U(x, y )))~ÌîäåëüI∃x (W (x) & C (x) → ∀y (B(y ) & S(y ) → U(x, y )))ÌÎÄÅËÈ. ËÎÃÈ×ÅÑÊÎÅ ÑËÅÄÑÒÂÈÅÊàêîé-òî áåëûé êóá ëåæèò ïîä âñåìè ÷åðíûìè øàðàìè.∃x (W (x) & C (x) & ∀y (B(y ) & S(y ) → U(x, y )))~ÌîäåëüI∃x (W (x) & C (x) → ∀y (B(y ) & S(y ) → U(x, y )))Êàêîé-òî ïðåäìåò ëèáî íå ÿâëÿåòñÿ áåëûì êóáîì,ëèáî ëåæèò ïîä êàæäûì ÷åðíûì øàðîì.ÌÎÄÅËÈ.

ËÎÃÈ×ÅÑÊÎÅ ÑËÅÄÑÒÂÈÅÊàêîé-òî áåëûé êóá ëåæèò ïîä âñåìè ÷åðíûìè øàðàìè.∃x (W (x) & C (x) & ∀y (B(y ) & S(y ) → U(x, y )))~ÌîäåëüJ∃x (W (x) & C (x) → ∀y (B(y ) & S(y ) → U(x, y )))Êàêîé-òî ïðåäìåò ëèáî íå ÿâëÿåòñÿ áåëûì êóáîì,ëèáî ëåæèò ïîä êàæäûì ÷åðíûì øàðîì.ÌÎÄÅËÈ. ËÎÃÈ×ÅÑÊÎÅ ÑËÅÄÑÒÂÈÅÎáùèé ïðèíöèï ïðàâèëüíîãî ïîñòðîåíèÿ ôîðìóë.Êàæäûé ïðåäìåò, íàäåëåííûé àòðèáóòîì A, îáëàäàåòñâîéñòâîì B :∀x (A(x) → B(x))Íåêîòîðûé ïðåäìåò, íàäåëåííûé àòðèáóòîì A, îáëàäàåòñâîéñòâîì B :∃x (A(x) & B(x))ÌÎÄÅËÈ. ËÎÃÈ×ÅÑÊÎÅ ÑËÅÄÑÒÂÈÅÎïðåäåëåíèåΓÏóñòü íåêîòîðîå ìíîæåñòâî çàìêíóòûõ ôîðìóë, è ϕ çàìêíóòàÿ ôîðìóëà.

Ôîðìóëà ϕ íàçûâàåòñÿ ëîãè÷åñêèìñëåäñòâèåì ìíîæåñòâà ïðåäëîæåíèé (áàçû çíàíèé) Γ, åñëèêàæäàÿ ìîäåëü äëÿ ìíîæåñòâà ôîðìóë Γ ÿâëÿåòñÿ ìîäåëüþäëÿ ôîðìóëû ϕ, ò. å.äëÿ ëþáîé èíòåðïðåòàöèè I : I |= Γ =⇒ I |= ϕËîãè÷åñêèå ñëåäñòâèÿ ýòî ¾ïðîèçâîäíûå¿ çíàíèÿ, êîòîðûåíåèçáåæíî ñîïóòñòâóþò ¾áàçîâûì¿ çíàíèÿì Γ, íàõîäÿòñÿ âïðè÷èííî-ñëåäñòâåííîé çàâèñèìîñòè îò ïðåäëîæåíèé Γ. Îäíàèç ãëàâíûõ çàäà÷ (è îäíîâðåìåííî íàèáîëåå õàðàêòåðíîåïðîÿâëåíèå) èíòåëëåêòóàëüíîé äåÿòåëüíîñòè ýòî èçâëå÷åíèåëîãè÷åñêèõ ñëåäñòâèé èç áàç çíàíèé.ÌÎÄÅËÈ.

ËÎÃÈ×ÅÑÊÎÅ ÑËÅÄÑÒÂÈÅÎáîçíà÷åíèÿÇàïèñü Γ |= ϕ îáîçíà÷àåò, ÷òî ϕ ëîãè÷åñêîå ñëåäñòâèå Γ .À êàêèå ôîðìóëû ÿâëÿþòñÿ ëîãè÷åñêèìè ñëåäñòâèÿìè ïóñòîéáàçû çíàíèé Γ = ∅? Ïðàâèëüíûé îòâåò: îáùåçíà÷èìûå .Ïîýòîìó äëÿ îáîçíà÷åíèÿ îáùåçíà÷èìîñòè ôîðìóëû ϕ áóäåìèñïîëüçîâàòü çàïèñü |= ϕ .ÌÎÄÅËÈ. ËÎÃÈ×ÅÑÊÎÅ ÑËÅÄÑÒÂÈÅÒåîðåìà î ëîãè÷åñêîì ñëåäñòâèèÏóñòüΓ = {ψ1 , . . . , ψn } ⊆ CForm, ϕ ∈ CForm. ÒîãäàΓ |= ϕ ⇐⇒ |= ψ1 & . . . &ψn → ϕ.Äîêàçàòåëüñòâî. ⇒ Ïóñòü I ïðîèçâîëüíàÿ èíòåðïðåòàöèÿ.Åñëè I 6|= ψ1& . . .

&ψn , òî I |= ψ1& . . . &ψn → ϕ.Åñëè I |= ψ1& . . . &ψn , òî I |= ψi , 1 ≤ i ≤ n, ò. å. I ìîäåëüäëÿ Γ.Ïîñêîëüêó Γ |= ϕ, ïîëó÷àåì I |= ϕ. Çíà÷èò,I |= ψ1 & . . . &ψn → ϕ.Òàêèì îáðàçîì, äëÿ ëþáîé èíòåðïðåòàöèè I èìååò ìåñòîI |= ψ1 & . . . &ψn → ϕ.Çíà÷èò, ψ1& . . . &ψn → ϕ îáùåçíà÷èìàÿ ôîðìóëà.ÌÎÄÅËÈ. ËÎÃÈ×ÅÑÊÎÅ ÑËÅÄÑÒÂÈÅÒåîðåìà î ëîãè÷åñêîì ñëåäñòâèèÏóñòüΓ = {ψ1 , . . . , ψn } ⊆ CForm, ϕ ∈ CForm. ÒîãäàΓ |= ϕ ⇐⇒ |= ψ1 & . . . &ψn → ϕ.Äîêàçàòåëüñòâî. ⇐ Ïóñòü I ìîäåëü äëÿ ìíîæåñòâàïðåäëîæåíèé Γ, ò.

å. I |= ψi , 1 ≤ i ≤ n.Òîãäà I |= ψ1& . . . &ψn .Òàê êàê |= ψ1& . . . &ψn → ϕ, âåðíî I |= ψ1& . . . &ψn → ϕ.Çíà÷èò, I |= ϕ.Òàê êàê I ïðîèçâîëüíàÿ ìîäåëü äëÿ Γ, ïðèõîäèì êçàêëþ÷åíèþ Γ |= ϕ.ÏÐÎÁËÅÌÀ ÎÁÙÅÇÍÀ×ÈÌÎÑÒÈ ÔÎÐÌÓËÎáùåçíà÷èìûå ôîðìóëû ýòî êàíàëû ïðè÷èííî-ñëåäñòâåííîéñâÿçè, ïî êîòîðûì ïåðåäàþòñÿ çíàíèÿ, ïðåäñòàâëåííûå â âèäåëîãè÷åñêèõ ôîðìóë, ïðåîáðàçóÿñü ïðè ýòîì èç îäíîé ôîðìû âäðóãóþ.Ïðàêòè÷åñêè âàæíî óìåòü îïðåäåëÿòü ýòè êàíàëû èíàñòðàèâàòü èõ íà èçâëå÷åíèå íóæíûõ çíàíèé.I Áàçà çíàíèé ìíîæåñòâî ïðåäëîæåíèé Γ;I Çàïðîñ ê áàçå çíàíèé ïðåäëîæåíèå ϕ;I Ïîëó÷åíèå îòâåòà íà çàïðîñ ïðîâåðêà ëîãè÷åñêîãîñëåäñòâèÿ Γ |= ϕ.Åñëè Γ êîíå÷íîå ìíîæåñòâî, òî ïðîâåðêà ëîãè÷åñêîãîñëåäñòâèÿ ñâîäèòñÿ ê ïðîâåðêå îáùåçíà÷èìîñòè ôîðìóëûψ1 & .

. . &ψn → ϕÏÐÎÁËÅÌÀ ÎÁÙÅÇÍÀ×ÈÌÎÑÒÈ ÔÎÐÌÓËÒàêèì îáðàçîì, âîçíèêàåò ïðîáëåìàîáùåçíà÷èìîñòè ôîðìóë:Äëÿ çàäàííîé ôîðìóëûϕïðîâåðèòü åå îáùåçíà÷èìîñòü:|= ϕ?ÏÐÎÁËÅÌÀ ÎÁÙÅÇÍÀ×ÈÌÎÑÒÈ ÔÎÐÌÓËÓòâåðæäåíèå.Äëÿ ëþáîé ôîðìóëû1.2.|= ϕ(x1 , . . . , xn )ϕ(x1 , . . . , xn )⇐⇒âåðíî, ÷òî|= ∀x1 . . . ∀xn ϕ(x1 , . . . , xn ); âûïîëíèìàÿϕ(x , . . . , x ) âûïîëíèìàÿ;ϕ(x1 , . . . , xn )⇐⇒∃x1 . .

. ∃xn3.ϕ(x1 , . . . , xn )⇐⇒1n âûïîëíèìà â ëþáîé èíòåðïðåòàöèè|= ∃x1 . . . ∃xn ϕ(x1 , . . . , xn ).ÄîêàçàòåëüñòâîÑàìîñòîÿòåëüíî. Ýòî ïðîñòî.ÏÐÎÁËÅÌÀ ÎÁÙÅÇÍÀ×ÈÌÎÑÒÈ ÔÎÐÌÓËÊàê æå ðåøàòü ïðîáëåìóîáùåçíà÷èìîñòè|= ϕ ?Ìîæåò áûòü ïðîâåðÿòü âñåèíòåðïðåòàöèè ïî î÷åðåäè ?ÏÐÎÁËÅÌÀ ÎÁÙÅÇÍÀ×ÈÌÎÑÒÈ ÔÎÐÌÓËÍåò, òàêîé ïîäõîä çàâåäîìî îáðå÷åí íà íåóäà÷ó. Ïî÷åìó?Ïîòîìó, ÷òî âåðíîÓòâåðæäåíèå.Ñóùåñòâóåò òàêàÿ çàìêíóòàÿ ôîðìóëàâ ëþáîé èíòåðïðåòàöèèîáëàñòüþDI ,Iñ êîíå÷íîéϕ,êîòîðàÿ èñòèííàïðåäìåòíîéíî íå ÿâëÿåòñÿ îáùåçíà÷èìîé .∀x¬R(x, x) &∀x∀y ∀z(R(x, y )&R(y , z) → R(x, z)) →∃x∀y ¬R(x, y ).ÏÐÎÁËÅÌÀ ÎÁÙÅÇÍÀ×ÈÌÎÑÒÈ ÔÎÐÌÓËÄîêàçàòåëüñòâî.: ¾ñóáúåêò y íà÷àëüíèê ñóáúåêòà x¿;1). ∀x¬R(x, x): ¾íèêòî íå êîìàíäóåò ñàìèì ñîáîé¿;2).

∀x∀y ∀z (R(x, y )&R(y , z) → R(x, z)): ¾íà÷àëüíèê ìîåãîíà÷àëüíèêà ìîé íà÷àëüíèê¿;3). ∃x∀y ¬R(x, y ): ¾êòî-òî íèêîìó íå ïîä÷èíÿåòñÿ¿. êàæäîé êîìïàíèè ñ êîíå÷íûì ìíîæåñòâîì ñîòðóäíèêîâ, âêîòîðîé äåéñòâóþò çàêîíû 1) è 2), âûïîëíÿåòñÿ è çàêîí 3).Çíà÷èò, íàøà ôîðìóëà èñòèííà âî âñåõ èíòåðïðåòàöèÿõ ñêîíå÷íîé ïðåäìåòíîé îáëàñòüþ.R(x, y )ÏÐÎÁËÅÌÀ ÎÁÙÅÇÍÀ×ÈÌÎÑÒÈ ÔÎÐÌÓËÄîêàçàòåëüñòâî.Íî íàøà ôîðìóëà íå ÿâëÿåòñÿ îáùåçíà÷èìîé.R(x, y ): ¾íàòóðàëüíîå ÷èñëî y áîëüøå íàòóðàëüíîãî ÷èñëà x¿1). ∀x¬R(x, x);2). ∀x∀y ∀z (R(x, y )&R(y , z) → R(x, z));âûïîëíÿþòñÿ íà ìíîæåñòâå íàòóðàëüíûõ ÷èñåë.3).

∃x∀y ¬R(x, y ) íà ìíîæåñòâå íàòóðàëüíûõ ÷èñåë íåâûïîëíÿåòñÿ: íåâåðíî, ÷òî ñóùåñòâóåò ìàêñèìàëüíîåíàòóðàëüíîå ÷èñëî.ÏÐÎÁËÅÌÀ ÎÁÙÅÇÍÀ×ÈÌÎÑÒÈ ÔÎÐÌÓËÍå òîëüêî ïåðåáîð âñåõ èíòåðïðåòàöèé, íî äàæå ïðîâåðêóèñòèííîñòè ôîðìóëû â èíòåðïðåòàöèè ñ áåñêîíå÷íîéïðåäìåòíîé îáëàñòüþ îñóùåñòâèòü çàòðóäíèòåëüíî.Çíà÷èò, íåîáõîäèìî ïðèäóìàòü áîëåå èçîùðåííûé ñïîñîáïðîâåðêè.ÏÐÎÁËÅÌÀ ÎÁÙÅÇÍÀ×ÈÌÎÑÒÈ ÔÎÐÌÓËÏðèìåð.Ïðîâåðèòü îáùåçíà÷èìîñòü ôîðìóëûϕ = ∀x (P(x) → R(x)) → (∀x P(x) → ∀x R(x)).ÏÐÎÁËÅÌÀ ÎÁÙÅÇÍÀ×ÈÌÎÑÒÈ ÔÎÐÌÓËÏðèìåð.Ïðîâåðèòü îáùåçíà÷èìîñòü ôîðìóëûϕ = ∀x (P(x) → R(x)) → (∀x P(x) → ∀x R(x)).Ïðåäïîëîæèì, ÷òî ϕ íåîáùåçíà÷èìà.

Òîãäà äîëæíàñóùåñòâîâàòü èíòåðïðåòàöèÿ I (êîíòðìîäåëü), îïðîâåðãàþùàÿϕ. Èçó÷èì ýòó êîíòðìîäåëü.ÏÐÎÁËÅÌÀ ÎÁÙÅÇÍÀ×ÈÌÎÑÒÈ ÔÎÐÌÓËÏðèìåð.Ïðîâåðèòü îáùåçíà÷èìîñòü ôîðìóëûϕ = ∀x (P(x) → R(x)) → (∀x P(x) → ∀x R(x)).Ïðåäïîëîæèì, ÷òî ϕ íåîáùåçíà÷èìà. Òîãäà äîëæíàñóùåñòâîâàòü èíòåðïðåòàöèÿ I (êîíòðìîäåëü), îïðîâåðãàþùàÿϕ. Èçó÷èì ýòó êîíòðìîäåëü.I 6|= ϕÏÐÎÁËÅÌÀ ÎÁÙÅÇÍÀ×ÈÌÎÑÒÈ ÔÎÐÌÓËÏðèìåð.Ïðîâåðèòü îáùåçíà÷èìîñòü ôîðìóëûϕ = ∀x (P(x) → R(x)) → (∀x P(x) → ∀x R(x)).Ïðåäïîëîæèì, ÷òî ϕ íåîáùåçíà÷èìà.

Òîãäà äîëæíàñóùåñòâîâàòü èíòåðïðåòàöèÿ I (êîíòðìîäåëü), îïðîâåðãàþùàÿϕ. Èçó÷èì ýòó êîíòðìîäåëü.I |= ∀x (P(x) → R(x))I |6 = ϕI 6|= ∀x P(x) → ∀x R(x)ÏÐÎÁËÅÌÀ ÎÁÙÅÇÍÀ×ÈÌÎÑÒÈ ÔÎÐÌÓËÏðèìåð.Ïðîâåðèòü îáùåçíà÷èìîñòü ôîðìóëûϕ = ∀x (P(x) → R(x)) → (∀x P(x) → ∀x R(x)).Ïðåäïîëîæèì, ÷òî ϕ íåîáùåçíà÷èìà. Òîãäà äîëæíàñóùåñòâîâàòü èíòåðïðåòàöèÿ I (êîíòðìîäåëü), îïðîâåðãàþùàÿϕ. Èçó÷èì ýòó êîíòðìîäåëü.I |= ∀x (P(x) → R(x))I |= ∀x P(x)I |6 = ϕI 6|= ∀x P(x) → ∀x R(x)I 6|= ∀x R(x)ÏÐÎÁËÅÌÀ ÎÁÙÅÇÍÀ×ÈÌÎÑÒÈ ÔÎÐÌÓËÏðèìåð.Ïðîâåðèòü îáùåçíà÷èìîñòü ôîðìóëûϕ = ∀x (P(x) → R(x)) → (∀x P(x) → ∀x R(x)).Ïðåäïîëîæèì, ÷òî ϕ íåîáùåçíà÷èìà.