3. Выполнимые и общезначимые формулы. Модели. Логическое следование. Проблема общезначимости. Семантические таблицы (1158018)
Текст из файла
Îñíîâûìàòåìàòè÷åñêîéëîãèêèèëîãè÷åñêîãîïðîãðàììèðîâàíèÿËÅÊÒÎÐ: Â.À. ÇàõàðîâËåêöèÿ 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)).Ïðåäïîëîæèì, ÷òî ϕ íåîáùåçíà÷èìà. Òîãäà äîëæíàñóùåñòâîâàòü èíòåðïðåòàöèÿ I (êîíòðìîäåëü), îïðîâåðãàþùàÿϕ.
Èçó÷èì ýòó êîíòðìîäåëü.I |= ∀x (P(x) → R(x))I |= ∀x P(x)IIII6|= ϕ6|= ∀x P(x) → ∀x R(x)6|= ∀x R(x)6|= R(x)[d]ÏÐÎÁËÅÌÀ ÎÁÙÅÇÍÀ×ÈÌÎÑÒÈ ÔÎÐÌÓËÏðèìåð.Ïðîâåðèòü îáùåçíà÷èìîñòü ôîðìóëûϕ = ∀x (P(x) → R(x)) → (∀x P(x) → ∀x R(x)).Ïðåäïîëîæèì, ÷òî ϕ íåîáùåçíà÷èìà. Òîãäà äîëæíàñóùåñòâîâàòü èíòåðïðåòàöèÿ I (êîíòðìîäåëü), îïðîâåðãàþùàÿϕ. Èçó÷èì ýòó êîíòðìîäåëü.I |= ∀x (P(x) → R(x))I |= ∀x P(x)I |= (P(x) → R(x))[d]IIII6|= ϕ6|= ∀x P(x) → ∀x R(x)6|= ∀x R(x)6|= R(x)[d]ÏÐÎÁËÅÌÀ ÎÁÙÅÇÍÀ×ÈÌÎÑÒÈ ÔÎÐÌÓËÏðèìåð.Ïðîâåðèòü îáùåçíà÷èìîñòü ôîðìóëûϕ = ∀x (P(x) → R(x)) → (∀x P(x) → ∀x R(x)).Ïðåäïîëîæèì, ÷òî ϕ íåîáùåçíà÷èìà. Òîãäà äîëæíàñóùåñòâîâàòü èíòåðïðåòàöèÿ I (êîíòðìîäåëü), îïðîâåðãàþùàÿϕ. Èçó÷èì ýòó êîíòðìîäåëü.I |= ∀x (P(x) → R(x))I |= ∀x P(x)I |= (P(x) → R(x))[d]I |= P(x)[d]IIII6|= ϕ6|= ∀x P(x) → ∀x R(x)6|= ∀x R(x)6|= R(x)[d]ÏÐÎÁËÅÌÀ ÎÁÙÅÇÍÀ×ÈÌÎÑÒÈ ÔÎÐÌÓËÏðèìåð.Ïðîâåðèòü îáùåçíà÷èìîñòü ôîðìóëûϕ = ∀x (P(x) → R(x)) → (∀x P(x) → ∀x R(x)).Ïðåäïîëîæèì, ÷òî ϕ íåîáùåçíà÷èìà.
Характеристики
Тип файла PDF
PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.
Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
