Лекции 2-11. Математическая логика (до колка) (Лекции 2014), страница 4

Тогда существуетинтерпретация I (контрмодель), которая опровергает ϕ.I 6|= ∃x (P(x) → ∀x P(x))I |= ∃x (P(x) I 6|= ∀x P(x)ПРОБЛЕМА ОБЩЕЗНАЧИМОСТИ ФОРМУЛПример.Проверить общезначимость формулыϕ = ∃x (P(x) → ∀x P(x)) .Предположим, что ϕ необщезначима. Тогда существуетинтерпретация I (контрмодель), которая опровергает ϕ.I 6|= ∃x (P(x) → ∀x P(x))I |= ∃x (P(x) I 6|= ∀x P(x)I |= P(x)[d1 ]ПРОБЛЕМА ОБЩЕЗНАЧИМОСТИ ФОРМУЛПример.Проверить общезначимость формулыϕ = ∃x (P(x) → ∀x P(x)) .Предположим, что ϕ необщезначима.

Тогда существуетинтерпретация I (контрмодель), которая опровергает ϕ.I 6|= ∃x (P(x) → ∀x P(x))I |= ∃x (P(x) I 6|= ∀x P(x)I |= P(x)[d1 ]I 6|= P(x)[d2 ]ПРОБЛЕМА ОБЩЕЗНАЧИМОСТИ ФОРМУЛПример.Проверить общезначимость формулыϕ = ∃x (P(x) → ∀x P(x)) .Предположим, что ϕ необщезначима. Тогда существуетинтерпретация I (контрмодель), которая опровергает ϕ.I 6|= ∃x (P(x) → ∀x P(x))I |= ∃x (P(x) I 6|= ∀x P(x)I |= P(x)[d1 ]I 6|= P(x)[d2 ]Противоречия нет.I = hDI , Predi: DI = {d1 , d2 }, P(d1 ) = true, P(d2 ) = false,I 6|= ϕ.Следовательно, 6|= ϕ.СЕМАНТИЧЕСКИЕ ТАБЛИЦЫПопробуем систематизировать этот способ проверкиобщезначимости формул.IОбщезначимость формулы доказываем «от противного»,пытаясь построить контрмодель.IКонтрмодель строим, указывая, какие формулы должны вней выполняться, а какие нет.

Требования(не)выполнимости формул, предъявляемые к контрмодели,сводим в таблицу и последовательно их уточняем.IЕсли требования, которые предъявляются к контрмодели,оказываются несовместными, значит, проверяемаяформула неопровержима, т. е. общезначима.СЕМАНТИЧЕСКИЕ ТАБЛИЦЫСемантическая таблица — это упорядоченная пара множествформул h Γ ; ∆ i , Γ, ∆ ⊆ Form.Γ — это множество формул, которые мы хотим считатьистинными,∆ — это множество формул, которые мы хотим считатьложными.Пусть {x1 , x2 , . . .

, xn } — множество свободных переменных вформулах множеств Γ, ∆.Семантическая таблица h Γ ; ∆ i называется выполнимой ,если существует такая интерпретация I и такой набор значенийd1 , d2 , . . . , dn ∈ DI свободных переменных, для которыхII |= ϕ(x1 , x2 , . . . , xn )[d1 , d2 , . . . , dn ] для любой формулы ϕ,ϕ ∈ Γ,II 6|= ψ(x1 , x2 , . . .

, xn )[d1 , d2 , . . . , dn ] для любой формулы ψ,ψ ∈ ∆.СЕМАНТИЧЕСКИЕ ТАБЛИЦЫПримерыСемантическая таблицаT = h {∃x P(x), ¬P(y )} ; {∀xP(x), P(x) & ¬P(x)} iвыполнима. Ее выполнимость подтверждает интерпретацияI = hDI , Predi: DI = {d1 , d2 }, P(d1 ) = true, P(d2 ) = false, инабор d1 , d2 значений свободных переменных x, y.Семантическая таблицаT = 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.Îñíîâûìàòåìàòè÷åñêîéëîãèêèèëîãè÷åñêîãîïðîãðàììèðîâàíèÿËÅÊÒÎÐ: Â.À.

Çàõàðîâzakh@cs.msu.suËåêöèÿ 4.Ïîäñòàíîâêè.Òàáëè÷íûé âûâîä.Êîððåêòíîñòü òàáëè÷íîãî âûâîäà.ÏÎÄÑÒÀÍÎÂÊÈÏîäñòàíîâêà ýòî âñÿêîå îòîáðàæåíèå θ : Var → Term,ñîïîñòàâëÿþùåå êàæäîé ïåðåìåííîé íåêîòîðûé òåðì.Ïîäñòàíîâêè íóæíû äëÿ òîãî, ÷òîáû èìåòü âîçìîæíîñòüïåðåõîäèòü îò îáùèõ óòâåðæäåíèé ∀x∀yP(x, y ) ê èõ ÷àñòíûìâàðèàíòàì P(f (z), c).Ìíîæåñòâî Domθ = {x : θ(x) 6= x} íàçûâàåòñÿ îáëàñòüþïîäñòàíîâêè .

Åñëè îáëàñòü ïîäñòàíîâêè ýòî êîíå÷íîåìíîæåñòâî ïåðåìåííûõ, òî òàêàÿ ïîäñòàíîâêà íàçûâàåòñÿêîíå÷íîé. Ìíîæåñòâî êîíå÷íûõ ïîäñòàíîâîê îáîçíà÷èì Subst .Åñëè θ ∈ Subst è Domθ = {x1, x2, . . . , xn }, òî ïîäñòàíîâêà θîäíîçíà÷íî îïðåäåëÿåòñÿ ìíîæåñòâîì ïàð{x1 /θ(x1 ), x2 /θ(x2 ), .

. . , xn /θ(xn )}.Êàæäàÿ ïàðà xi /θ(xi ) íàçûâàåòñÿ ñâÿçêîé .ÏÎÄÑÒÀÍÎÂÊÈÄëÿ çàäàííîãî ëîãè÷åñêîãî âûðàæåíèÿ E è ïîäñòàíîâêè θçàïèñü E θ îáîçíà÷àåò ðåçóëüòàò ïðèìåíåíèÿ ïîäñòàíîâêè θ ê E ,êîòîðûé îïðåäåëåòñÿ òàê:Åñëè E = x, x ∈ Var , òî E θ = θ(x);Åñëè E = c, c ∈ Const , òî E θ = c ;Åñëè E = f (t1, t2, . . . , tk ), òî E θ = f (t1θ, t2θ, . .

. , tn θ);Åñëè E = P(t1, t2, . . . , tk ), òî E θ = P(t1θ, t2θ, . . . , tn θ);Åñëè E = ϕ&ψ, òî E θ = ϕθ & ψθ(àíàëîãè÷íî äëÿ ôîðìóë ϕ ∨ ψ, ϕ → ψ, ¬ϕ);Åñëè E = ∀x0 ϕ, òî E θ = ∀x0 (ϕθ0), ãäå η íîâàÿïîäñòàíîâêà, óäîâëåòâîðÿþùàÿ óñëîâèþθ0 (x) =x0 , åñëè x = x0 ,θ(x), åñëè x 6= x0 ,∃x0 ϕ(àíàëîãè÷íî äëÿ ôîðìóë).ÏÎÄÑÒÀÍÎÂÊÈÏðèìåðϕ : ∀x(P(x) → ¬R(y )) → R(f (x)) ∨ ∃yP(y )θ = { x/g (x, c), y /x, z/f (z) }Âûäåëÿþòñÿ âñå ñâîáîäíûå âõîæäåíèÿ ïåðåìåííûõ â ϕϕ : ∀x(P(x) → ¬R(y )) → R(f (x)) ∨ ∃yP(y )Ê ñâîáîäíûì âõîæäåíèÿì ïåðåìåííûõ ïðèìåíÿåòñÿ θϕθ : ∀x(P(x) → ¬R(x)) → R(f (g (x, c))) ∨ ∃yP(y )ÏÎÄÑÒÀÍÎÂÊÈ ðåçóëüòàòå ïðèìåíåíèÿ íåêîòîðûõ ïîäñòàíîâîê ñìûñëóòâåðæäåíèé (ôîðìóë) ìîæåò çíà÷èòåëüíî èñêàçèòüñÿ.¾Åñëè ó êàæäîãî åñòü äåä, òî ó ñóáúåêòà x òîæå åñòü äåä¿ϕ(x) : ∀x∃yP(x, y ) → ∃yP(x, y )Î÷åâèäíî, |= ϕ(x)Ïðèìåíèì ê ϕ(x) ïîäñòàíîâêó θ = { x/y }ϕ(x)θ : ∀x∃yP(x, y ) → ∃yP(y , y )¾Åñëè ó êàæäîãî åñòü äåä, òî åñòü è òàêèå, êîòîðûå ïðèõîäÿòñÿäåäîì ñàìèì ñåáå¿Î÷åâèäíî, 6|= ϕ(x)θÊàê ñòðàííî: îáùåå óòâåðæäåíèå ϕ(x) âåðíî, à åãî ÷àñòíûéñëó÷àé ϕ(x)θ íåò.ÏÎÄÑÒÀÍÎÂÊÈÏåðåìåííàÿ x íàçûâàåòñÿ ñâîáîäíîé äëÿ òåðìà t â ôîðìóëåϕ(x), åñëè ëþáîå ñâîáîäíîå âõîæäåíèå ïåðåìåííîé x âôîðìóëå ϕ(x) íå ëåæèò â îáëàñòè äåéñòâèÿ íè îäíîãîêâàíòîðà, ñâÿçûâàþùåãî ïåðåìåííóþ èç ìíîæåñòâà Vart .Ïîäñòàíîâêà θ = { x1/t1, .

. . , xn /tn } íàçûâàåòñÿ ïðàâèëüíîé äëÿôîðìóëû ϕ, åñëè äëÿ ëþáîé ñâÿçêè xi /ti ïåðåìåííàÿ xiñâîáîäíà äëÿ òåðìà ti â ôîðìóëå ϕ.ÏðèìåðÏåðåìåííàÿ y íå ÿâëÿåòñÿ ñâîáîäíîé äëÿ òåðìà f (x, z) âôîðìóëå ϕϕ : ∀x(P(x) → ¬R(y )) → R(f (x)) ∨ ∃yP(y )À âîò äëÿ òåðìà f (y , z) ïåðåìåííàÿ y â ôîðìóëå ϕ ñâîáîäíà.ÒÀÁËÈ×ÍÛÉ ÂÛÂÎÄÏðàâèëà òàáëè÷íîãî âûâîäà èìåþò âèäT0 ,T0èëèT1T1, T2ãäå T0, T1, T2 ñåìàíòè÷åñêèå òàáëèöû. Ïðî÷òåíèå ïðàâèëàòàêîâî:Òàáëèöà T0 âûïîëíèìà òîãäà è òîëüêî òîãäà, êîãäàâûïîëíèìà òàáëèöà T1 (èëè T2 ). òåõ ñëó÷àÿõ, êîãäà òàáëèöà T0 ðåäóöèðóåòñÿ â ïàðó òàáëèöT1 , T2 , áóäåì ãîâîðèòü, ÷òî ïðàâèëî èìååò àëüòåðíàòèâû.ÒÀÁËÈ×ÍÛÉ ÂÛÂÎÄÏðàâèëà òàáëè÷íîãî âûâîäàL&hΓ, ϕ&ψ|∆ihΓ, ϕ, ψ|∆iL∨hΓ, ϕ ∨ ψ|∆iR∨hΓ, ϕ|∆i, hΓ, ψ|∆iL→hΓ, ϕ → ψ|∆ihΓ|∆, ϕ → ψiR→hΓ, ψ|∆i, hΓ|ϕ, ∆ihΓ, ϕ|∆, ψiL¬hΓ, ¬ϕ|∆ihΓ|∆, ϕiR&R¬hΓ|∆, ϕ&ψihΓ|∆, ϕi, hΓ | ∆, ψihΓ|∆, ϕ ∨ ψihΓ|∆, ϕ, ψihΓ|∆, ¬ϕihΓ, ϕ|∆iÒÀÁËÈ×ÍÛÉ ÂÛÂÎÄÏðàâèëà òàáëè÷íîãî âûâîäàL∀hΓ, ∀xϕ(x)|∆ihΓ, ∀xϕ(x), ϕ(x){x/t}|∆ix ñâîáîäíàϕ(x)ïåðåìåííàÿâ ôîðìóëåR∀äëÿ òåðìàthΓ|∆, ∀xϕ(x)ihΓ|∆, ϕ(x){x/c}iêîíñòàíòàèçΓ, ∆cíå ñîäåðæèòñÿ â ôîðìóëàõè â ôîðìóëåϕ(x)ÒÀÁËÈ×ÍÛÉ ÂÛÂÎÄÏðàâèëà òàáëè÷íîãî âûâîäàL∃hΓ, ∃xϕ(x)|∆ihΓ, ϕ(x){x/c}|∆iêîíñòàíòàèçR∃Γ, ∆cíå ñîäåðæèòñÿ â ôîðìóëàõè â ôîðìóëåϕ(x)hΓ|∆, ∃xϕ(x)ihΓ|∆, ∃xϕ(x), ϕ(x){x/t}ix ñâîáîäíàϕ(x)ïåðåìåííàÿâ ôîðìóëåäëÿ òåðìàtÒÀÁËÈ×ÍÛÉ ÂÛÂÎÄÇà÷åì íóæíû îãðàíè÷åíèÿ íà ïîäñòàâëÿåìûå òåðìûâ ïðàâèëàõ L∀, R∀, L∃, R∃?Åñëè â ïðàâèëå òàáëè÷íîãî âûâîäà L∀ íå ïðèäåðæèâàòüñÿïðàâèëüíûõ ïîäñòàíîâîê, òî âûïîëíèìàÿ òàáëèöà− L∀ :h ∀x∃yR(x, y ) | ∃yR(y , y ) ih ∀x∃yR(x, y ), ∃yR(y , y ) | ∃yR(y , y ) iïðåîáðàçóåòñÿ â çàêðûòóþ, ò.å.

íåâûïîëíèìóþ òàáëèöó .Ïðè÷èíà â òîì, ÷òî ïåðåìåííàÿ x íåñâîáîäíà äëÿ òåðìà y âôîðìóëå ∃yR(x, y ).ÒÀÁËÈ×ÍÛÉ ÂÛÂÎÄÇà÷åì íóæíû îãðàíè÷åíèÿ íà ïîäñòàâëÿåìûå òåðìûâ ïðàâèëàõ L∀, R∀, L∃, R∃?Åñëè â ïðàâèëå òàáëè÷íîãî âûâîäà L∃ ïîäñòàâèòü ¾íåñâåæóþ¿êîíñòàíòó, òî âûïîëíèìàÿ òàáëèöà− L∃ :h ∃x P(x) | P(c) ih P(c) | P(c) iïðåîáðàçóåòñÿ â çàêðûòóþ, ò.å. íåâûïîëíèìóþ òàáëèöó .Ïðè÷èíà â òîì, ÷òî êîíñòàíòà, ïîäñòàâëÿåìàÿ âìåñòîïåðåìåííîé x, äîëæíà áûòü îòëè÷íà îò âñåõ ðàíååèñïîëüçîâàííûõ êîíñòàíò.ÒÀÁËÈ×ÍÛÉ ÂÛÂÎÄÎïðåäåëåíèå òàáëè÷íîãî âûâîäàÒàáëè÷íûé âûâîä äëÿ òàáëèöû T0 ýòî êîðíåâîå äåðåâî,âåðøèíàìè êîòîðîãî ñëóæàò ñåìàíòè÷åñêèå òàáëèöû è ïðè ýòîì1) êîðíåì äåðåâà ÿâëÿåòñÿ òàáëèöà T0;yT0@Tyj?yT3@@TR yT@y1i@@@@@@R yT@R yT@2k?yT4ÒÀÁËÈ×ÍÛÉ ÂÛÂÎÄÎïðåäåëåíèå òàáëè÷íîãî âûâîäà2)èç âåðøèíû Ti èñõîäÿò äóãè â âåðøèíû Tj (Tk )⇐⇒TiTj , (Tk ) ïðàâèëî òàáëè÷íîãî âûâîäà;TyjL∃yT0@L→ @@TR yT@y1i@@R& @L∀ @@@R yT@R yT@2kR¬?yT3?Ty4ÒÀÁËÈ×ÍÛÉ ÂÛÂÎÄÎïðåäåëåíèå òàáëè÷íîãî âûâîäà3) ëèñòüÿìè äåðåâà ìîãóò áûòü òîëüêî çàêðûòûå èàòîìàðíûå òàáëèöû.TyjyT0@L→ @@TR yT@y1i@@R& @L∀ @@@R yT@R yT@2kL∃àòîì.