586 слайдов лекций, страница 4
Описание файла
PDF-файл из архива "586 слайдов лекций", который расположен в категории "". Всё это находится в предмете "математическая логика и логическое программирование" из 7 семестр, которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .
Просмотр PDF-файла онлайн
Текст 4 страницы из PDF
ËÎÃÈ×ÅÑÊÎÅ ÑËÅÄÑÒÂÈÅÎáùèé ïðèíöèï ïðàâèëüíîãî ïîñòðîåíèÿ ôîðìóë.Êàæäûé ïðåäìåò, íàäåëåííûé àòðèáóòîì 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)).Ïðåäïîëîæèì, ÷òî ϕ íåîáùåçíà÷èìà.
Òîãäà äîëæíàñóùåñòâîâàòü èíòåðïðåòàöèÿ I (êîíòðìîäåëü), îïðîâåðãàþùàÿϕ. Èçó÷èì ýòó êîíòðìîäåëü.I |= ∀x (P(x) → R(x))I |= ∀x P(x)I |= (P(x) → R(x))[d]I |= P(x)[d]I |= R(x)[d]IIII6|= ϕ6|= ∀x P(x) → ∀x R(x)6|= ∀x R(x)6|= R(x)[d]Ïîëó÷èëè ïðîòèâîðå÷èå. Çíà÷èò, êîíòðìîäåëè I íå ñóùåñòâóåò.ÏÐÎÁËÅÌÀ ÎÁÙÅÇÍÀ×ÈÌÎÑÒÈ ÔÎÐÌÓËÏðèìåð.Ïðîâåðèòü îáùåçíà÷èìîñòü ôîðìóëûϕ = ∀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]I |= R(x)[d]IIII6|= ϕ6|= ∀x P(x) → ∀x R(x)6|= ∀x R(x)6|= R(x)[d]Ïîëó÷èëè ïðîòèâîðå÷èå.
Çíà÷èò, êîíòðìîäåëè I íå ñóùåñòâóåò.Çíà÷èò, |= ϕ.ÏÐÎÁËÅÌÀ ÎÁÙÅÇÍÀ×ÈÌÎÑÒÈ ÔÎÐÌÓËÏðèìåð.Ïðîâåðèòü îáùåçíà÷èìîñòü ôîðìóëûϕ = ∃x P(x) → ∀x P(x).ÏÐÎÁËÅÌÀ ÎÁÙÅÇÍÀ×ÈÌÎÑÒÈ ÔÎÐÌÓËÏðèìåð.Ïðîâåðèòü îáùåçíà÷èìîñòü ôîðìóëû.Ïðåäïîëîæèì, ÷òî ϕ íåîáùåçíà÷èìà. Òîãäà ñóùåñòâóåòèíòåðïðåòàöèÿ I (êîíòðìîäåëü), êîòîðàÿ îïðîâåðãàåò ϕ.ϕ = ∃x P(x) → ∀x P(x)ÏÐÎÁËÅÌÀ ÎÁÙÅÇÍÀ×ÈÌÎÑÒÈ ÔÎÐÌÓËÏðèìåð.Ïðîâåðèòü îáùåçíà÷èìîñòü ôîðìóëû.Ïðåäïîëîæèì, ÷òî ϕ íåîáùåçíà÷èìà. Òîãäà ñóùåñòâóåòèíòåðïðåòàöèÿ I (êîíòðìîäåëü), êîòîðàÿ îïðîâåðãàåò ϕ.ϕ = ∃x P(x) → ∀x P(x)I 6|= ∃x P(x) → ∀x P(x)ÏÐÎÁËÅÌÀ ÎÁÙÅÇÍÀ×ÈÌÎÑÒÈ ÔÎÐÌÓËÏðèìåð.Ïðîâåðèòü îáùåçíà÷èìîñòü ôîðìóëû.Ïðåäïîëîæèì, ÷òî ϕ íåîáùåçíà÷èìà. Òîãäà ñóùåñòâóåòèíòåðïðåòàöèÿ I (êîíòðìîäåëü), êîòîðàÿ îïðîâåðãàåò ϕ.ϕ = ∃x P(x) → ∀x P(x)I |= ∃x P(x)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 (êîíòðìîäåëü), êîòîðàÿ îïðîâåðãàåò ϕ.ϕ = ∃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 Åñëè òðåáîâàíèÿ, êîòîðûå ïðåäúÿâëÿþòñÿ ê êîíòðìîäåëè,îêàçûâàþòñÿ íåñîâìåñòíûìè, çíà÷èò, ïðîâåðÿåìàÿôîðìóëà íåîïðîâåðæèìà, ò.
