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

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

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

òàáë.R¬?yT3çàêð. òàáë.?Ty4çàêð. òàáë.ÒÀÁËÈ×ÍÛÉ ÂÛÂÎÄÎïðåäåëåíèå òàáëè÷íîãî âûâîäàÒàáëè÷íûé âûâîä áóäåì íàçûâàòü óñïåøíûì (èëè òàáëè÷íûìîïðîâåðæåíèåì ), åñëè äåðåâî âûâîäà êîíå÷íîå, è âñå ëèñòüÿäåðåâà çàêðûòûå òàáëèöû.Ñóùåñòâîâàíèå óñïåøíîãî âûâîäà îçíà÷àåò, ÷òî êîðíåâàÿñåìàíòè÷åñêàÿ òàáëèöà T0 íåâûïîëíèìà.Åñëè T0 = h ∅ | ϕ i, òî ýòî îçíà÷àåò, ÷òî |= ϕ.T0 = h ∅ | ∀x(P(x) → B(x)) → (∀xP(x) → ∀xB(x)) iT0 = h ∅ | ∀x(P(x) → B(x)) → (∀xP(x) → ∀xB(x)) iR→(?)T1 = h ∀x(P(x) → B(x)) | ∀xP(x) → ∀xB(x) iT0 = h ∅ | ∀x(P(x) → B(x)) → (∀xP(x) → ∀xB(x)) iR→()?T1 = h ∀x(P(x) → B(x)) | ∀xP(x) → ∀xB(x) iR→(?)T2 = h ∀x(P(x) → B(x)), ∀xP(x) | ∀xB(x) iT0 = h ∅ | ∀x(P(x) → B(x)) → (∀xP(x) → ∀xB(x)) iR→()?T1 = h ∀x(P(x) → B(x)) | ∀xP(x) → ∀xB(x) iR→()?T2 = h ∀x(P(x) → B(x)), ∀xP(x) | ∀xB(x) iR∀( )?T3 = h ∀x(P(x) → B(x)), ∀xP(x) | B(c) iT0 = h ∅ | ∀x(P(x) → B(x)) → (∀xP(x) → ∀xB(x)) iR→()?T1 = h ∀x(P(x) → B(x)) | ∀xP(x) → ∀xB(x) iR→()?T2 = h ∀x(P(x) → B(x)), ∀xP(x) | ∀xB(x) iR∀( )?T3 = h ∀x(P(x) → B(x)), ∀xP(x) | B(c) iL∀( )?T4 = h ∀x(P(x) → B(x)), ∀xP(x), P(c) | B(c) iT0 = h ∅ | ∀x(P(x) → B(x)) → (∀xP(x) → ∀xB(x)) iR→()?T1 = h ∀x(P(x) → B(x)) | ∀xP(x) → ∀xB(x) iR→()?T2 = h ∀x(P(x) → B(x)), ∀xP(x) | ∀xB(x) iR∀( )?T3 = h ∀x(P(x) → B(x)), ∀xP(x) | B(c) iL∀( )?T4 = h ∀x(P(x) → B(x)), ∀xP(x), P(c) | B(c) iL∀( )?T5 = h ∀x(P(x) → B(x)), P(c) → B(c), ∀xP(x), P(c) | B(c) iT0 = h ∅ | ∀x(P(x) → B(x)) → (∀xP(x) → ∀xB(x)) iR→()?T1 = h ∀x(P(x) → B(x)) | ∀xP(x) → ∀xB(x) iR→()?T2 = h ∀x(P(x) → B(x)), ∀xP(x) | ∀xB(x) iR∀( )?T3 = h ∀x(P(x) → B(x)), ∀xP(x) | B(c) iL∀( )?T4 = h ∀x(P(x) → B(x)), ∀xP(x), P(c) | B(c) iL∀( )?T5 = h ∀x(P(x) → B(x)), P(c) → B(c), ∀xP(x), P(c) | B(c) iPPL→PP)()qPT6 = h∀x(P(x) → B(x)), |B(c)i T7 = h∀x(P(x) → B(x)), |B(c), P(c)i∀xP(x), B(c), P(c)∀xP(x), P(c)T0 = h ∅ | ∀x(P(x) → B(x)) → (∀xP(x) → ∀xB(x)) iR→()?T1 = h ∀x(P(x) → B(x)) | ∀xP(x) → ∀xB(x) iR→()?T2 = h ∀x(P(x) → B(x)), ∀xP(x) | ∀xB(x) iR∀( )?T3 = h ∀x(P(x) → B(x)), ∀xP(x) | B(c) iL∀( )?T4 = h ∀x(P(x) → B(x)), ∀xP(x), P(c) | B(c) iL∀( )?T5 = h ∀x(P(x) → B(x)), P(c) → B(c), ∀xP(x), P(c) | B(c) iPPL→PP)()qPT6 = h∀x(P(x) → B(x)), |B(c)i T7 = h∀x(P(x) → B(x)), |B(c), P(c)i∀xP(x), B(c), P(c)∀xP(x), P(c)T0 = h ∅ | ∀x(P(x) → B(x)) → (∀xP(x) → ∀xB(x)) iR→()?T1 = h ∀x(P(x) → B(x)) | ∀xP(x) → ∀xB(x) iR→()?T2 = h ∀x(P(x) → B(x)), ∀xP(x) | ∀xB(x) iR∀( )?T3 = h ∀x(P(x) → B(x)), ∀xP(x) | B(c) iL∀( )?T4 = h ∀x(P(x) → B(x)), ∀xP(x), P(c) | B(c) iL∀( )?T5 = h ∀x(P(x) → B(x)), P(c) → B(c), ∀xP(x), P(c) | B(c) iPPL→PP)()qPT6 = h∀x(P(x) → B(x)), |B(c)i T7 = h∀x(P(x) → B(x)), |B(c), P(c)i∀xP(x), B(c), P(c)∀xP(x), P(c)çàêðûòàÿ òàáëèöàçàêðûòàÿ òàáëèöàT0 = h ∅ | ∃x(P(x) → ∀xP(x) iT0 = h ∅ | ∃x(P(x) → ∀xP(x) iR→(?)T1 = h ∃xP(x) | ∀xP(x) iT0 = h ∅ | ∃x(P(x) → ∀xP(x) iR→()?T1 = h ∃xP(x) | ∀xP(x) iL∃( )?T2 = h P(c1 ) | ∀xP(x) iT0 = h ∅ | ∃x(P(x) → ∀xP(x) iR→()?T1 = h ∃xP(x) | ∀xP(x) iL∃( )?T2 = h P(c1 ) | ∀xP(x) iR∀( )?T3 = h P(c1 ) | P(c2 ) iT0 = h ∅ | ∃x(P(x) → ∀xP(x) iR→()?T1 = h ∃xP(x) | ∀xP(x) iL∃( )?T2 = h P(c1 ) | ∀xP(x) iR∀( )?T3 = h P(c1 ) | P(c2 ) iàòîìàðíàÿ òàáëèöàT0 = h ∅ | ∀y ∃xP(x, y ) → ∃x∀yP(x, y ) iT0 = h ∅ | ∀y ∃xP(x, y ) → ∃x∀yP(x, y ) iR→(?)T1 = h ∀y ∃xP(x, y ) | ∃x∀yP(x, y ) iT0 = h ∅ | ∀y ∃xP(x, y ) → ∃x∀yP(x, y ) iR→()?T1 = h ∀y ∃xP(x, y ) | ∃x∀yP(x, y ) iL∀( )?T2 = h ∀y ∃xP(x, y ), ∃xP(x, c1 ) | ∃x∀yP(x, y ) iT0 = h ∅ | ∀y ∃xP(x, y ) → ∃x∀yP(x, y ) iR→()?T1 = h ∀y ∃xP(x, y ) | ∃x∀yP(x, y ) iL∀( )?T2 = h ∀y ∃xP(x, y ), ∃xP(x, c1 ) | ∃x∀yP(x, y ) iR∃( )?T3 = h ∀y ∃xP(x, y ), ∃xP(x, c1 ) | ∀yP(c2 , y ), ∃x∀yP(x, y ) iT0 = h ∅ | ∀y ∃xP(x, y ) → ∃x∀yP(x, y ) iR→()?T1 = h ∀y ∃xP(x, y ) | ∃x∀yP(x, y ) iL∀( )?T2 = h ∀y ∃xP(x, y ), ∃xP(x, c1 ) | ∃x∀yP(x, y ) iR∃( )?T3 = h ∀y ∃xP(x, y ), ∃xP(x, c1 ) | ∀yP(c2 , y ), ∃x∀yP(x, y ) iL∃( )?T4 = h ∀y ∃xP(x, y ), P(c3 , c1 ) | ∀y P(c2 , y ), ∃x∀yP(x, y ) iT0 = h ∅ | ∀y ∃xP(x, y ) → ∃x∀yP(x, y ) iR→()?T1 = h ∀y ∃xP(x, y ) | ∃x∀yP(x, y ) iL∀( )?T2 = h ∀y ∃xP(x, y ), ∃xP(x, c1 ) | ∃x∀yP(x, y ) iR∃( )?T3 = h ∀y ∃xP(x, y ), ∃xP(x, c1 ) | ∀yP(c2 , y ), ∃x∀yP(x, y ) iL∃( )?T4 = h ∀y ∃xP(x, y ), P(c3 , c1 ) | ∀y P(c2 , y ), ∃x∀yP(x, y ) iR∀( )?T5 = h ∀y ∃xP(x, y ), P(c3 , c1 ) | P(c2 , c4 ), ∃x∀yP(x, y ) iT0 = h ∅ | ∀y ∃xP(x, y ) → ∃x∀yP(x, y ) iR→()?T1 = h ∀y ∃xP(x, y ) | ∃x∀yP(x, y ) iL∀( )?T2 = h ∀y ∃xP(x, y ), ∃xP(x, c1 ) | ∃x∀yP(x, y ) iR∃( )?T3 = h ∀y ∃xP(x, y ), ∃xP(x, c1 ) | ∀yP(c2 , y ), ∃x∀yP(x, y ) iL∃( )?T4 = h ∀y ∃xP(x, y ), P(c3 , c1 ) | ∀y P(c2 , y ), ∃x∀yP(x, y ) iR∀( )?T5 = h ∀y ∃xP(x, y ), P(c3 , c1 ) | P(c2 , c4 ), ∃x∀yP(x, y ) i?∞ÊÎÐÐÅÊÒÍÎÑÒÜ ÒÀÁËÈ×ÍÎÃÎ ÂÛÂÎÄÀËåììà î êîððåêòíîñòè ïðàâèë âûâîäàÊàêîâî áû íè áûëî ïðàâèëî òàáëè÷íîãî âûâîäàL&, R&, L∨, R∨, L →, R →, L¬, R¬, L∀, R∀, L∃, R∃T0 ,T1 , (T2 )òàáëèöà T0 âûïîëíèìà òîãäà è òîëüêî òîãäà, êîãäàâûïîëíèìà òàáëèöà T1 (èëè âûïîëíèìà òàáëèöà T2 ).ÊÎÐÐÅÊÒÍÎÑÒÜ ÒÀÁËÈ×ÍÎÃÎ ÂÛÂÎÄÀÄîêàçàòåëüñòâî ëåììûϕ → ψ|∆iÐàññìîòðèì ïðàâèëî L →: hΓ,hΓ,ψ|∆i,.hΓ|ϕ, ∆iÒàáëèöà hΓ, ϕ → ψ|∆i âûïîëíèìà ⇐⇒ñóùåñòâóåò èíòåðïðåòàöèÿ I è íàáîð d̄ = hd1, .

. . , dn i çíà÷åíèéñâîáîäíûõ ïåðåìåííûõ, äëÿ êîòîðûõ I |= Γ[d̄],I 6|= ∆[d̄],I |= (ϕ → ψ)[d̄]⇐⇒ I |= Γ[d̄],I 6|= ∆[d̄],I |= ψ[d̄]⇐⇒èëè I |= Γ[d̄],I 6|= ∆[d̄],I |= ψ[d̄] èëè I 6|= ϕ[d̄] I |= Γ[d̄],I 6|= ∆[d̄],I 6|= ϕ[d̄]⇐⇒⇐⇒îäíà èç òàáëèö T1 = hΓ, ψ|∆i èëè T2 = hΓ|ϕ, ∆i âûïîëíèìà.ÊÎÐÐÅÊÒÍÎÑÒÜ ÒÀÁËÈ×ÍÎÃÎ ÂÛÂÎÄÀÄîêàçàòåëüñòâî ëåììûÀíàëîãè÷íî äîêàçûâàåòñÿ êîððåêòíîñòü îñòàëüíûõ 7 ïðàâèëäëÿ ëîãè÷åñêèõ ñâÿçîêÊÎÐÐÅÊÒÍÎÑÒÜ ÒÀÁËÈ×ÍÎÃÎ ÂÛÂÎÄÀÄîêàçàòåëüñòâî ëåììû∀x0 ϕ(x0 )|∆i.Ðàññìîòðèì ïðàâèëî L∀: hΓ, ∀x0hΓ,ϕ(x0 ), ϕ(x0 ){x0 /t}|∆iÒàáëèöà hΓ, ∀x0ϕ(x0)|∆i âûïîëíèìà ⇐⇒ ñóùåñòâóåòèíòåðïðåòàöèÿ I è íàáîð d1, .

. . , dn çíà÷åíèé ñâîáîäíûõïåðåìåííûõ, äëÿ êîòîðûõ I |= Γ[d1 , . . . , dn ],I 6|= ∆[d1 , . . . , dn ],I |= (∀x0 ϕ)[d1 , . . . , dn ]Ïóñòü d0 = t[d1, . . . , dn ]. ÒîãäàI |= (∀x0 ϕ)[d1 , . . . , dn ] ⇒ I |= ϕ[d0 , d1 , . . . , dn ] ⇒.Ñëåäîâàòåëüíî, òàáëèöàâûïîëíèìà â èíòåðïðåòàöèè .Íà êàêîì ýòàïå äîêàçàòåëüñòâà ñóùåñòâåííî èñïîëüçóåòñÿ òîòôàêò, ÷òî ïåðåìåííàÿ x0 ñâîáîäíà äëÿ òåðìà t â ôîðìóëå ϕ ?⇒ I |= ϕ[t[d1 , . . . , dn ], d1 , .

. . , dn ] ⇒ I |= ϕ{x0 /t}[d1 , . . . , dn ]hΓ, ∀x0 ϕ(x0 ), ϕ(x0 ){x0 /t}|∆iIÊÎÐÐÅÊÒÍÎÑÒÜ ÒÀÁËÈ×ÍÎÃÎ ÂÛÂÎÄÀÄîêàçàòåëüñòâî ëåììû∃xϕ(x)|∆i.Ðàññìîòðèì ïðàâèëî L∃: hΓ,hΓ,ϕ(x){x/c}|∆iÎ÷åâèäíî, ÷òî âûïîëíèìîñòü òàáëèöû hΓ, ϕ(x){x/c}|∆i âëå÷åòâûïîëíèìîñòü òàáëèöû hΓ, ∃xϕ(x)|∆iÄîïóñòèì, ÷òî âûïîëíèìà òàáëèöà hΓ, ∃xϕ(x)|∆i. Òîãäàñóùåñòâóåò èíòåðïðåòàöèÿ I è íàáîð d1, . . . , dn çíà÷åíèéñâîáîäíûõ ïåðåìåííûõ, äëÿ êîòîðûõ I |= Γ[d1 , . . . , dn ],I 6|= ∆[d1 , . .

. , dn ],I |= (∃xϕ)[d1 , . . . , dn ]Âûïîëíèìîñòü ∃xϕ[d1, . . . , dn ] îçíà÷àåò, ÷òî ñóùåñòâóåò òàêîéýëåìåíò d0 ∈ DI , ÷òî I |= ϕ[d0, d1, . . . , dn ].ÊÎÐÐÅÊÒÍÎÑÒÜ ÒÀÁËÈ×ÍÎÃÎ ÂÛÂÎÄÀÄîêàçàòåëüñòâî ëåììûÐàññìîòðèì èíòåðïðåòàöèþ J , êîòîðàÿ îòëè÷àåòñÿ îò I , òîëüêîòåì, ÷òî â J êîíñòàíòà c èìååò äðóãîå çíà÷åíèå, à èìåííîc̄ = d0 .Òîãäà J |= (ϕ{x/c})[d1, . . . , dn ].Êðîìå òîãî, J |= Γ[d1, .

. . , dn ] è J 6|= ∆[d1, . . . , dn ].Ñëåäîâàòåëüíî, òàáëèöà hΓ, ϕ(x){x/c}|∆i âûïîëíèìà âèíòåðïðåòàöèè J .Íà êàêîì ýòàïå äîêàçàòåëüñòâà ñóùåñòâåííî èñïîëüçóåòñÿ òîòôàêò, ÷òî êîíñòàíòà c íå âõîäèò â ñîñòàâ ôîðìóë èç Γ, ∆ èôîðìóëû ϕ ?ÊÎÐÐÅÊÒÍÎÑÒÜ ÒÀÁËÈ×ÍÎÃÎ ÂÛÂÎÄÀÒåîðåìà êîððåêòíîñòè òàáëè÷íîãî âûâîäàÅñëè äëÿ ñåìàíòè÷åñêîé òàáëèöû T0 ñóùåñòâóåòóñïåøíûé òàáëè÷íûé âûâîä, òî òàáëèöà T0íåâûïîëíèìà.ÄîêàçàòåëüñòâîÑëåäóåò èçI îïðåäåëåíèÿ òàáëè÷íîãî âûâîäà,I ëåììû î êîððåêòíîñòè ïðàâèë òàáëè÷íîãî âûâîäà,I è óòâåðæäåíèÿ î íåâûïîëíèìîñòè çàêðûòûõ òàáëèö.ÑëåäñòâèåÅñëè äëÿ òàáëèöû Tϕ = h ∅ |ϕ i ìîæíî ïîñòðîèòü óñïåøíûéòàáëè÷íûé âûâîä, òî |= ϕ.ÊÎÍÅÖ ËÅÊÖÈÈ 4.Основыматематическойлогики и логическогопрограммированияЛЕКТОР: В.А.

Захаровzakh@cs.msu.suhttp://mathcyb.cs.msu.su/courses/logprog.htmlЛекция 5.Полнота табличного вывода.Теорема Левенгейма-Сколема.Теорема компактности Мальцева.Автоматическое доказательствотеорем.ПОЛНОТА ТАБЛИЧНОГО ВЫВОДАТеорема полноты табличного выводаЕсли семантическая таблица T0 невыполнима, то для T0существует успешный табличный вывод.Доказательство.Проведем для упрощенного частного случая таблицы T0 , вкоторойIимеется лишь конечное число формул,Iвсе формулы замкнутые,Iв формулах нет функциональных символов.Пусть T0 = h Γ0 | ∆0 i — невыполнимая таблица. Будемстроить табличный вывод для T0 , руководствуясь следующейстратегией.ПОЛНОТА ТАБЛИЧНОГО ВЫВОДА1). Каждая незакрытая таблица в дереве вывода получаетпорядковый номер, и правила табличного выводаприменяются к таблицам в порядке возрастания ихномеров.ПОЛНОТА ТАБЛИЧНОГО ВЫВОДА1). Каждая незакрытая таблица в дереве вывода получаетпорядковый номер, и правила табличного выводаприменяются к таблицам в порядке возрастания ихномеров.yT0ПОЛНОТА ТАБЛИЧНОГО ВЫВОДА1).

Каждая незакрытая таблица в дереве вывода получаетпорядковый номер, и правила табличного выводаприменяются к таблицам в порядке возрастания ихномеров.Ty1yT0@@@R yT@2ПОЛНОТА ТАБЛИЧНОГО ВЫВОДА1). Каждая незакрытая таблица в дереве вывода получаетпорядковый номер, и правила табличного выводаприменяются к таблицам в порядке возрастания ихномеров.yT0@@@R yT@2Ty3Ty1@@@R yT@4ПОЛНОТА ТАБЛИЧНОГО ВЫВОДА1). Каждая незакрытая таблица в дереве вывода получаетпорядковый номер, и правила табличного выводаприменяются к таблицам в порядке возрастания ихномеров.Ty3yT0@@@R yT@Ty12@@@@@@R yT@R yT@4закр. табл.ПОЛНОТА ТАБЛИЧНОГО ВЫВОДА1).

Каждая незакрытая таблица в дереве вывода получаетпорядковый номер, и правила табличного выводаприменяются к таблицам в порядке возрастания ихномеров.Ty3yT0@@@R yT@Ty12@@@@@@R yT@R yT@4закр. табл.?yTзакр. табл.ПОЛНОТА ТАБЛИЧНОГО ВЫВОДА1). Каждая незакрытая таблица в дереве вывода получаетпорядковый номер, и правила табличного выводаприменяются к таблицам в порядке возрастания ихномеров.Ty3yT0@@@R yT@Ty12@@@@@@R yT@R yT@4закр. табл.?yTзакр. табл.?yT5и. т. д.ПОЛНОТА ТАБЛИЧНОГО ВЫВОДА2).

Таблицы состоят из упорядоченных множеств формул(списков). Правила применяются к формулам в порядке ихрасположения в списках. Формулы, участвующие вприменении правил, помещаются в хвост нужного списка.Атомарные формулы просто переходят из головы списка вего хвост.ПОЛНОТА ТАБЛИЧНОГО ВЫВОДА2). Таблицы состоят из упорядоченных множеств формул(списков).

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

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