4. Подстановки. Табличный вывод. Корректность табличного вывода (В.А. Захаров - Лекции), страница 2
Описание файла
Файл "4. Подстановки. Табличный вывод. Корректность табличного вывода" внутри архива находится в папке "В.А. Захаров - Лекции". PDF-файл из архива "В.А. Захаров - Лекции", который расположен в категории "". Всё это находится в предмете "математическая логика и логическое программирование" из 7 семестр, которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .
Просмотр PDF-файла онлайн
Текст 2 страницы из PDF
. . , 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..