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

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

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

Òîãäà äîëæíàñóùåñòâîâàòü èíòåðïðåòàöèÿ 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 Åñëè òðåáîâàíèÿ, êîòîðûå ïðåäúÿâëÿþòñÿ ê êîíòðìîäåëè,îêàçûâàþòñÿ íåñîâìåñòíûìè, çíà÷èò, ïðîâåðÿåìàÿôîðìóëà íåîïðîâåðæèìà, ò. å. îáùåçíà÷èìà.ÑÅÌÀÍÒÈ×ÅÑÊÈÅ ÒÀÁËÈÖÛÑåìàíòè÷åñêàÿ òàáëèöà ýòî óïîðÿäî÷åííàÿ ïàðà ìíîæåñòâôîðìóë 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..

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

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