Лекции В.А. Захарова (1157993), страница 3

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

Текст из файла (страница 3)

. , xn ) и набор d1 , d2 , . . . , dn элементов(предметов) из области интерпретации DI .Отношение выполнимости I |= ϕ(x1 , x2 , . . . , xn )[d1 , d2 , . . . , dn ]формулы ϕ в интерпретации I на наборе d1 , d2 , . . . , dnопределяется рекурсивно.IЕсли ϕ(x1 , x2 , . . . , xn ) = P(t1 , . . . , tm ), тоI |= ϕ(x1 , x2 , . .

. , xn )[d1 , d2 , . . . , dn ]⇐⇒P̄(t1 [d1 , d2 , . . . , dn ], . . . , tm [d1 , d2 , . . . , dn ]) = true;СЕМАНТИКА: ВЫПОЛНИМОСТЬ ФОРМУЛОтношение выполнимости формулIЕсли ϕ(x1 , x2 , . . . , xn ) = ψ1 &ψ2 , тоII |= ϕ(x1 , x2 , . . . , xn )[d1 , d2 , . . . , dn ]⇐⇒I |= ψ1 (x1 , x2 , . . . , xn )[d1 , d2 , . . . , dn ]I |= ψ2 (x1 , x2 , . .

. , xn )[d1 , d2 , . . . , dn ]Если ϕ(x1 , x2 , . . . , xn ) = ψ1 ∨ ψ2 , тоI |= ϕ(x1 , x2 , . . . , xn )[d1 , d2 , . . . , dn ]⇐⇒I |= ψ1 (x1 , x2 , . . . , xn )[d1 , d2 , . . . , dn ]илиI |= ψ2 (x1 , x2 , . . . , xn )[d1 , d2 , . . . , dn ]СЕМАНТИКА: ВЫПОЛНИМОСТЬ ФОРМУЛОтношение выполнимости формулIЕсли ϕ(x1 , x2 , . . . , xn ) = ψ1 → ψ2 , тоI |= ϕ(x1 , x2 , .

. . , xn )[d1 , d2 , . . . , dn ]⇐⇒I 6|= ψ1 (x1 , x2 , . . . , xn )[d1 , d2 , . . . , dn ]илиI |= ψ2 (x1 , x2 , . . . , xn )[d1 , d2 , . . . , dn ]IЕсли ϕ(x1 , x2 , . . . , xn ) = ¬ψ, тоI |= ϕ(x1 , x2 , . . . , xn )[d1 , d2 , . . . , dn ]⇐⇒I 6|= ψ(x1 , x2 , . . . , xn )[d1 , d2 , .

. . , dn ]СЕМАНТИКА: ВЫПОЛНИМОСТЬ ФОРМУЛОтношение выполнимости формулIЕсли ϕ(x1 , x2 , . . . , xn ) = ∀x0 ψ(x0 , x1 , x2 , . . . , xn ), тоI |= ϕ(x1 , x2 , . . . , xn )[d1 , d2 , . . . , dn ]⇐⇒для любого элемента d0 , d0 ∈ DI , имеет местоI |= ψ(x0 , x1 , x2 , . . . , xn )[d0 , d1 , d2 , . .

. , dn ]IЕсли ϕ(x1 , x2 , . . . , xn ) = ∃x0 ψ(x0 , x1 , x2 , . . . , xn ), тоI |= ϕ(x1 , x2 , . . . , xn )[d1 , d2 , . . . , dn ]⇐⇒для некоторого элемента d0 , d0 ∈ DI , имеет местоI |= ψ(x0 , x1 , x2 , . . . , xn )[d0 , d1 , d2 , . . . , dn ]СЕМАНТИКА: ВЫПОЛНИМОСТЬ ФОРМУЛИнтерпретацияI = hDI , Const, Func, PrediОбласть интерпретацииОценка константDI = {d1 , d2 , d3 };c1 = d1 , c2 = d3 ;Оценка функциональных и предикатныхf(x)P(x)R(x, y )yxfxPd1xd1 d2d1 trued1 trued2 d3d2 falsed2 trued3 d1d3 trued3 falseсимволовd2truefalsetrued3falsetruetrueФормулаϕ = ∀x1 (P(x1 ) → ∃x2 (R(x1 , x2 ) & ¬P(f (x2 ))))СЕМАНТИКА: ВЫПОЛНИМОСТЬ ФОРМУЛf(x)xd1d2d3fd2d3d1P(x)xd1d2d3I |= R(x1 , x2 )[d1 , d1 ]PtruefalsetrueR(x, y )yd1xd1 trued2 trued3 falsed2truefalsetrued3falsetruetrueСЕМАНТИКА: ВЫПОЛНИМОСТЬ ФОРМУЛf(x)xd1d2d3fd2d3d1P(x)xd1d2d3I |= R(x1 , x2 )[d1 , d1 ]I 6|= P(f (x2 ))[d1 ]PtruefalsetrueR(x, y )yd1xd1 trued2 trued3 falsed2truefalsetrued3falsetruetrueСЕМАНТИКА: ВЫПОЛНИМОСТЬ ФОРМУЛf(x)xd1d2d3fd2d3d1P(x)xd1d2d3PtruefalsetrueR(x, y )yd1xd1 trued2 trued3 falseI |= R(x1 , x2 )[d1 , d1 ]I 6|= P(f (x2 ))[d1 ] ⇒ I |= ¬P(f (x2 ))[d1 ]d2truefalsetrued3falsetruetrueСЕМАНТИКА: ВЫПОЛНИМОСТЬ ФОРМУЛf(x)xd1d2d3fd2d3d1P(x)xd1d2d3PtruefalsetrueR(x, y )yd1xd1 trued2 trued3 falseI |= R(x1 , x2 )[d1 , d1 ]I 6|= P(f (x2 ))[d1 ] ⇒ I |= ¬P(f (x2 ))[d1 ]I |= R(x1 , x2 ) & ¬P(f (x2 ))[d1 , d1 ]d2truefalsetrued3falsetruetrueСЕМАНТИКА: ВЫПОЛНИМОСТЬ ФОРМУЛf(x)xd1d2d3fd2d3d1P(x)xd1d2d3PtruefalsetrueR(x, y )yd1xd1 trued2 trued3 falseI |= R(x1 , x2 )[d1 , d1 ]I 6|= P(f (x2 ))[d1 ] ⇒ I |= ¬P(f (x2 ))[d1 ]I |= R(x1 , x2 ) & ¬P(f (x2 ))[d1 , d1 ]I |= ∃x2 (R(x1 , x2 ) & ¬P(f (x2 )))[d1 ]d2truefalsetrued3falsetruetrueСЕМАНТИКА: ВЫПОЛНИМОСТЬ ФОРМУЛf(x)xd1d2d3fd2d3d1P(x)xd1d2d3PtruefalsetrueR(x, y )yd1xd1 trued2 trued3 falsed2truefalsetrued3falsetruetrueI |= R(x1 , x2 )[d1 , d1 ]I 6|= P(f (x2 ))[d1 ] ⇒ I |= ¬P(f (x2 ))[d1 ]I |= R(x1 , x2 ) & ¬P(f (x2 ))[d1 , d1 ]I |= ∃x2 (R(x1 , x2 ) & ¬P(f (x2 )))[d1 ]I |= P(x1) → ∃x2(R(x1, x2)&¬P(f (x2)))[d1]СЕМАНТИКА: ВЫПОЛНИМОСТЬ ФОРМУЛf(x)xd1d2d3fd2d3d1P(x)xd1d2d3I 6|= P(x1 )[d2 ]PtruefalsetrueR(x, y )yd1xd1 trued2 trued3 falsed2truefalsetrued3falsetruetrueСЕМАНТИКА: ВЫПОЛНИМОСТЬ ФОРМУЛf(x)xd1d2d3fd2d3d1P(x)xd1d2d3PtruefalsetrueR(x, y )yd1xd1 trued2 trued3 falsed2truefalsetrued3falsetruetrueI 6|= P(x1 )[d2 ]I |= P(x1) → ∃x2(R(x1, x2)&¬P(f (x2)))[d2]СЕМАНТИКА: ВЫПОЛНИМОСТЬ ФОРМУЛf(x)xd1d2d3fd2d3d1P(x)xd1d2d3I |= P(x1 )[d3 ]PtruefalsetrueR(x, y )yd1xd1 trued2 trued3 falsed2truefalsetrued3falsetruetrueСЕМАНТИКА: ВЫПОЛНИМОСТЬ ФОРМУЛf(x)xd1d2d3fd2d3d1P(x)xd1d2d3PtruefalsetrueI |= P(x1 )[d3 ]I 6|= R(x1 , x2 )[d3 , d1 ]R(x, y )yd1xd1 trued2 trued3 falsed2truefalsetrued3falsetruetrueСЕМАНТИКА: ВЫПОЛНИМОСТЬ ФОРМУЛf(x)xd1d2d3fd2d3d1P(x)xd1d2d3PtruefalsetrueR(x, y )yd1xd1 trued2 trued3 falsed2truefalsetrued3falsetruetrueI |= P(x1 )[d3 ]I 6|= R(x1 , x2 )[d3 , d1 ] ⇒ I 6|= R(x1 , x2 ) & ¬P(f (x2 ))[d3 , d1 ]СЕМАНТИКА: ВЫПОЛНИМОСТЬ ФОРМУЛf(x)xd1d2d3fd2d3d1P(x)xd1d2d3PtruefalsetrueR(x, y )yd1xd1 trued2 trued3 falsed2truefalsetrued3falsetruetrueI |= P(x1 )[d3 ]I 6|= R(x1 , x2 )[d3 , d1 ]I 6|= ¬P(f (x2 ))[d2 ]⇒ I 6|= R(x1 , x2 ) & ¬P(f (x2 ))[d3 , d1 ]СЕМАНТИКА: ВЫПОЛНИМОСТЬ ФОРМУЛf(x)xd1d2d3fd2d3d1P(x)xd1d2d3PtruefalsetrueR(x, y )yd1xd1 trued2 trued3 falsed2truefalsetrued3falsetruetrueI |= P(x1 )[d3 ]I 6|= R(x1 , x2 )[d3 , d1 ]⇒ I 6|= R(x1 , x2 ) & ¬P(f (x2 ))[d3 , d1 ]I 6|= ¬P(f (x2 ))[d2 ] ⇒ I 6|= R(x1 , x2 ) & ¬P(f (x2 ))[d3 , d2 ]СЕМАНТИКА: ВЫПОЛНИМОСТЬ ФОРМУЛf(x)xd1d2d3fd2d3d1P(x)xd1d2d3PtruefalsetrueR(x, y )yd1xd1 trued2 trued3 falsed2truefalsetrued3falsetruetrueI |= P(x1 )[d3 ]I 6|= R(x1 , x2 )[d3 , d1 ]I 6|= ¬P(f (x2 ))[d2 ]I 6|= ¬P(f (x2 ))[d3 ]⇒ I 6|= R(x1 , x2 ) & ¬P(f (x2 ))[d3 , d1 ]⇒ I 6|= R(x1 , x2 ) & ¬P(f (x2 ))[d3 , d2 ]СЕМАНТИКА: ВЫПОЛНИМОСТЬ ФОРМУЛf(x)xd1d2d3fd2d3d1P(x)xd1d2d3PtruefalsetrueR(x, y )yd1xd1 trued2 trued3 falsed2truefalsetrued3falsetruetrueI |= P(x1 )[d3 ]I 6|= R(x1 , x2 )[d3 , d1 ]I 6|= ¬P(f (x2 ))[d2 ]⇒ I 6|= R(x1 , x2 ) & ¬P(f (x2 ))[d3 , d1 ]⇒ I 6|= R(x1 , x2 ) & ¬P(f (x2 ))[d3 , d2 ]I 6|= ¬P(f (x2 ))[d3 ] ⇒ I 6|= R(x1 , x2 ) & ¬P(f (x2 ))[d3 , d3 ]СЕМАНТИКА: ВЫПОЛНИМОСТЬ ФОРМУЛf(x)xd1d2d3fd2d3d1P(x)xd1d2d3PtruefalsetrueR(x, y )yd1xd1 trued2 trued3 falsed2truefalsetrued3falsetruetrueI |= P(x1 )[d3 ]I 6|= R(x1 , x2 )[d3 , d1 ]⇒ I 6|= R(x1 , x2 ) & ¬P(f (x2 ))[d3 , d1 ]I 6|= ¬P(f (x2 ))[d2 ]⇒ I 6|= R(x1 , x2 ) & ¬P(f (x2 ))[d3 , d2 ]I 6|= ¬P(f (x2 ))[d3 ]⇒ I 6|= R(x1 , x2 ) & ¬P(f (x2 ))[d3 , d3 ]I 6|= ∃x2 (R(x1 , x2 ) & ¬P(f (x2 )))[d3 ]СЕМАНТИКА: ВЫПОЛНИМОСТЬ ФОРМУЛf(x)xd1d2d3fd2d3d1P(x)xd1d2d3PtruefalsetrueR(x, y )yd1xd1 trued2 trued3 falsed2truefalsetrued3falsetruetrueI |= P(x1 )[d3 ]I 6|= R(x1 , x2 )[d3 , d1 ]⇒ I 6|= R(x1 , x2 ) & ¬P(f (x2 ))[d3 , d1 ]I 6|= ¬P(f (x2 ))[d2 ]⇒ I 6|= R(x1 , x2 ) & ¬P(f (x2 ))[d3 , d2 ]I 6|= ¬P(f (x2 ))[d3 ]⇒ I 6|= R(x1 , x2 ) & ¬P(f (x2 ))[d3 , d3 ]I 6|= ∃x2 (R(x1 , x2 ) & ¬P(f (x2 )))[d3 ]I 6|= P(x1) → ∃x2(R(x1, x2)&¬P(f (x2)))[d3]СЕМАНТИКА: ВЫПОЛНИМОСТЬ ФОРМУЛИтак, мы имеемI |= (P(x1 ) → ∃x2 (R(x1 , x2 ) & ¬P(f (x2 ))))[d1 ]I |= (P(x1 ) → ∃x2 (R(x1 , x2 ) & ¬P(f (x2 ))))[d2 ]I 6|= (P(x1 ) → ∃x2 (R(x1 , x2 ) & ¬P(f (x2 ))))[d3 ]Значит,I 6|= ∀x1 (P(x1) → ∃x2(R(x1, x2) & ¬P(f (x2))))КОНЕЦ ЛЕКЦИИ 2.Îñíîâûìàòåìàòè÷åñêîéëîãèêèèëîãè÷åñêîãîïðîãðàììèðîâàíèÿËÅÊÒÎÐ: Â.À.

ÇàõàðîâËåêöèÿ 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 )))Êàêîé-òî ïðåäìåò ëèáî íå ÿâëÿåòñÿ áåëûì êóáîì,ëèáî ëåæèò ïîä êàæäûì ÷åðíûì øàðîì.ÌÎÄÅËÈ.

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

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