Частично упорядоченные множества (1127207), страница 4
Текст из файла (страница 4)
×àñòü IV: ×àñòè÷íî óïîðÿäî÷åííûå ìíîæåñòâà66 / 85Ìîäåëè ÊðèïêåÊëàññè÷åñêîå èñ÷èñëåíèå âûñêàçûâàíèé ÊÈÂ: îïðåäåëåíèåÅñëè ê ñõåìàì àêñèîì äîáàâèòü åù¼ îäíó:11A ∨ ¬A(ëàò.òî ïîëó÷èì ëîãè÷åñêèé çàêîí TNDtertium non datur, ¾òðåòüåãî íå äàíî¿),êëàññè÷åñêîå èñ÷èñëåíèå âûñêàçûâàíèé ÊÈÂ.Òîãäà êàæäîé ëîãè÷åñêîé ïåðåìåííîé ìîæíî ïðèïèñàòü îäíîèç äâóõ èñòèííîñòíûõ çíà÷åíèé 1 èëè 0, ïîíèìàåìûõ êàê¾èñòèíà¿ è ¾ëîæü¿ ñîîòâåòñòâåííî, è ïî ïðàâèëàì|¬A| = 1 ⇔ |A| = 0;|AN B| = 1 ⇔ |A| = |B| = 1;|A ∨ B| = 0 ⇔ |A| = |B| = 0;|A B| = 1 ⇔ |B| = 1 èëè |A| = 0.ïîëó÷èòü îöåíêó |F | ∈ {1, 0} ëþáîé ôîðìóëû F .ÏÐÈÊËÀÄÍÀß ÀËÃÅÁÐÀ.
×àñòü IV: ×àñòè÷íî óïîðÿäî÷åííûå ìíîæåñòâàÌîäåëè ÊðèïêåÊÈÂ: òàâòîëîãèèÔîðìóëû, èñòèííûå ïðè ëþáûõ èíòåðïðåòàöèÿõ âîçìîæíûõâàðèàíòàõ ïðèïèñûâàíèé ëîãè÷åñêèì ïåðåìåííûì çíà÷åíèé (1èëè 0) íàçûâàþòñÿ òàâòîëîãèÿìè.Ïðèìåðû: âñå àêñèîìû 111, ¬¬x x, ¬(x ∨ y) ¬xN ¬y , ... ÊÈ âûâîäèìûìè îêàçûâàþòñÿ âñå òàâòîëîãèè è òîëüêî îíè⇒ ïðîáëåìà âûâîäèìîñòè ñâîäèòñÿ ê ïðîâåðêå ôîðìóëû íàòàâòîëîãè÷íîñòü. ÈÈ çàäà÷à ðàäèêàëüíî óñëîæíÿåòñÿ: ýòî èñ÷èñëåíèå íåèìååò êîíå÷íîçíà÷íîé èíòåðïðåòàöèè, ò.å.
åñëè â ëþáîìêîíå÷íîì íàáîðå T r = { 0, 1, . . . , k − 1} îáúÿâèâ çíà÷åíèå 0âûäåëåííûì è çàäàâ ïðàâèëà îöåíêè ôîðìóë òàê, ÷òîáû ïðèâñåõ èíòåðïðåòàöèÿõ ïåðåìåííûì èç V ar çíà÷åíèé èç T r âñåàêñèîìû âñåãäà ïðèíèìàëè áû òîëüêî çíà÷åíèå 0, íàéä¼òñÿíåâûâîäèìàÿ ôîðìóëà ÈÈ òàêàÿ, ÷òî å¼ îöåíêà òîæå âñåãäàáóäåò ïðèíèìàòü âûäåëåííîå çíà÷åíèå.67 / 85ÏÐÈÊËÀÄÍÀß ÀËÃÅÁÐÀ. ×àñòü IV: ×àñòè÷íî óïîðÿäî÷åííûå ìíîæåñòâàÌîäåëè ÊðèïêåÈÈÂ: ïðîáëåìà ðàçðåøèìîñòèËþáàÿ âûâîäèìàÿ â ÈÈ ôîðìóëà âûâîäèìà è â ÊÈÂ.Îáðàòíîå íåâåðíî: íàïðèìåð, ôîðìóëû, ïîëó÷àåìûå èçñõåìû TND è ¬¬x x, ¬(x ∨ y) ¬xN ¬y , ... íåâûâîäèìûâ ÈÈÂ.Äëÿ ðàçðåøåíèÿ ïðîáëåìû âûâîäèìîñòè â ÈÈ ïðèìåíèììåòîä, îñíîâàííûé íà ïîñòðîåíèè øêàë Êðèïêå.Ñîë Êðèïêå (Saul Aaron Kripke, 1940) àìåðèêàíñêèé ôèëîñîô è ëîãèê,îäèí èç äåñÿòè âûäàþùèõñÿ ôèëîñîôîâïîñëåäíèõ 200 ëåò.Åù¼ þíîøåé âí¼ñ çíà÷èòåëüíûé âêëàä âìàòåìàòè÷åñêóþ ëîãèêó, ôèëîñîôèþìàòåìàòèêè è òåîðèþ ìíîæåñòâ.68 / 85ÏÐÈÊËÀÄÍÀß ÀËÃÅÁÐÀ.
×àñòü IV: ×àñòè÷íî óïîðÿäî÷åííûå ìíîæåñòâàÌîäåëè ÊðèïêåØêàëû Êðèïêå: ïîñòðîåíèå×òîáû çàäàòü òàêóþ øêàëó íóæíî:óêàçàòü ÷.ó. ìíîæåñòâî h W, 6 i, ýëåìåíòû íîñèòåëÿêîòîðîãî íàçûâàþò ìèðàìè;äëÿ êàæäîãî ìèðà óêàçàòü, êàêèå èç ëîãè÷åñêèõïåðåìåííûõ â í¼ì ÿâëÿþòñÿ èñòèííûìè (îñòàëüíûåïåðåìåííûå â ýòîì ìèðå ëîæíû).Ôàêò èñòèííîñòè ïåðåìåííîé x â ìèðå w çàïèñûâàþòñèìâîëè÷åñêè w x, ëîæíîñòè w 6 x.Ïðè ôîðìèðîâàíèè øêàëû Êðèïêå òðåáóåòñÿ, ÷òîáûu 6 v è u x ⇒ v x,ò.å., êàê ãîâîðÿò, ¾îáëàñòü èñòèííîñòè ïåðåìåííîé íàñëåäóåòñÿââåðõ¿ èëè ¾ñîõðàíÿåòñÿ â áîëüøèõ ìèðàõ¿.69 / 85ÏÐÈÊËÀÄÍÀß ÀËÃÅÁÐÀ. ×àñòü IV: ×àñòè÷íî óïîðÿäî÷åííûå ìíîæåñòâàÌîäåëè ÊðèïêåØêàëû Êðèïêå: èíòåðïðåòàöèÿ ïîðÿäêà è ôîðìàëüíîåîïðåäåëåíèåÍåôîðìàëüíî ïîðÿäîê u 6 v ìåæäó ìèðàìè èíòåðïðåòèðóåòñÿêàê òî, ÷òî ìèð v åñòü ñîñòîÿíèå ìèðà u â ñëåäóþùèé ìîìåíòâðåìåíè, ïîíèìàÿ âðåìÿ íå â ôèçè÷åñêîì, à â ëîãè÷åñêîìñìûñëå: êàæäûé ìèð îïèñûâàåòñÿ ñîñòîÿíèåì çíàíèé â äàííûéìîìåíò è îäíàæäû óñòàíîâëåííàÿ èñòèííîñòü èëè äîêàçàííûéôàêò îñòà¼òñÿ òàêîâûì è âïîñëåäñòâèè.Ëîãè÷åñêîå âðåìÿ íå îáÿçàòåëüíî îáëàäàåò ëèíåéíûìïîðÿäêîì.Îïðåäåëåíèååñòü òðîéêà h W, 6, i, ãäå ðåäóêò h W, 6 i ÷.ó.
ìíîæåñòâî, à ⊆ W ×V ar ñîîòâåòñòâèå ¾îäèí êîìíîãèì¿, ñòàâÿùåå êàæäîìó ìèðó ñîâîêóïíîñòü èñòèííûõ âí¼ì ëîãè÷åñêèõ ïåðåìåííûõ è óäîâëåòâîðÿþùåå óñëîâèþíàñëåäîâàíèÿ èñòèííîñòè.Øêàëà Êðèïêå70 / 85ÏÐÈÊËÀÄÍÀß ÀËÃÅÁÐÀ. ×àñòü IV: ×àñòè÷íî óïîðÿäî÷åííûå ìíîæåñòâàÌîäåëè ÊðèïêåØêàëû Êðèïêå: èñòèííîñòü ôîðìóëû â ìèðàõÄëÿ ïîñòðîåííîé øêàëû Êðèïêå îïðåäåëèì èñòèííîñòü äàííîéôîðìóëû A â ëþáîì ìèðå w:w AN B ⇔ w A è w B ;w A ∨ B ⇔ w A èëè w B ;w A B ⇔ ∀(u > w) u B èëè u 6 A;w ¬A ⇔ ∀(u > w) u 6 A(ò.å.
åñëè ¬A, òî íå ñóùåñòâóåò áîëüøåãî ìèðà, âêîòîðîì áû A).Ââåä¼ííûå øêàëû Êðèïêå çàäàþò ñåìàíòèêó ÈÈÂ, ïðèäàâàÿñìûñë ôîðìóëàì ðàçäåëÿÿ èõ íà èñòèííûå è ëîæíûå âäàííîì ìèðå.71 / 85ÏÐÈÊËÀÄÍÀß ÀËÃÅÁÐÀ. ×àñòü IV: ×àñòè÷íî óïîðÿäî÷åííûå ìíîæåñòâàÌîäåëè ÊðèïêåØêàëû Êðèïêå: èñòèííîñòü ôîðìóëû â ìèðàõ...Èñòèííàÿ â äàííîì ìèðå ôîðìóëà îñòà¼òñÿ èñòèííîé è âñòàðøèõ (áîëüøèõ) ìèðàõ.Ëîæíàÿ â äàííîì ìèðå ôîðìóëà áûëà ëîæíîé è âî âñåõìëàäøèõ (ìåíüøèõ) ìèðàõ.Åñëè ôîðìóëà ñîäåðæèò òîëüêî ñâÿçêè N è ∨, òî å¼èñòèííîñòü â äàííîì ìèðå íå çàâèñèò îò å¼ èñòèííîñòè âäðóãèõ ìèðàõ.Èñòèííîñòè èìïëèêàöèè è îòðèöàíèÿ èñïîëüçóþò ïîðÿäîêíà ìíîæåñòâå ìèðîâ.Ñëåäñòâèåì ïðåäûäóùåãî ÿâëÿåòñÿ ôàêò íåçàâèñèìîñòèèìïëèêàöèè îò äðóãèõ ñâÿçîê: â ÈÈÂ, íàïðèìåð, ôîðìóëûA B è ¬A ∨ B ëîãè÷åñêè íå ýêâèâàëåíòíû.72 / 85ÏÐÈÊËÀÄÍÀß ÀËÃÅÁÐÀ.
×àñòü IV: ×àñòè÷íî óïîðÿäî÷åííûå ìíîæåñòâà73 / 85Ìîäåëè ÊðèïêåØêàëû Êðèïêå: òðè âàðèàíòà èñòèííîñòè ôîðìóëû â øêàëåèç äâóõ ñâÿçàííûõ ìèðîâÏÐÈÊËÀÄÍÀß ÀËÃÅÁÐÀ. ×àñòü IV: ×àñòè÷íî óïîðÿäî÷åííûå ìíîæåñòâàÌîäåëè ÊðèïêåØêàëû Êðèïêå: òåîðåìà êîððåêòíîñòèÒåîðåìà (êîððåêòíîñòè ÈÈ îòíîñèòåëüíî øêàë Êðèïêå)Ôîðìóëà, âûâîäèìàÿ â ÈÈÂ, èñòèíà âî âñåõ ìèðàõ âñåõ øêàëÊðèïêå.ÄîêàçàòåëüñòâîÏîêàæåì, ÷òî (1) âñå àêñèîìû èñòèíû âî âñåõ ìèðàõ è(2) ïðàâèëî MP ñîõðàíÿåò èñòèííîñòü.Âòîðîå î÷åâèäíî: åñëè èBA,èA Bèñòèíû âî âñåõ ìèðàõ, òîáóäåò òàêæå èñòèíà âî âñåõ ìèðàõ.Çàìå÷àíèå: ÷òîáû â ìèðåwïðîâåðèòü îöåíêóA B íàäî óäîñòîâåðèòüñÿ, ÷òîw A ⇒ w B ( w 6 A ýòà èìïëèêàöèÿ ïîäàâíî èñòèíà);ëîæíîñòü èìïëèêàöèè A B íàäî óäîñòîâåðèòüñÿ, ÷òîw A ⇒ w 6 B .èñòèííîñòü èìïëèêàöèè74 / 85ÏÐÈÊËÀÄÍÀß ÀËÃÅÁÐÀ.
×àñòü IV: ×àñòè÷íî óïîðÿäî÷åííûå ìíîæåñòâàÌîäåëè ÊðèïêåØêàëû Êðèïêå: òåîðåìà êîððåêòíîñòèÒåîðåìà (êîððåêòíîñòè ÈÈ îòíîñèòåëüíî øêàë Êðèïêå)Ôîðìóëà, âûâîäèìàÿ â ÈÈÂ, èñòèíà âî âñåõ ìèðàõ âñåõ øêàëÊðèïêå.ÄîêàçàòåëüñòâîÏîêàæåì, ÷òî (1) âñå àêñèîìû èñòèíû âî âñåõ ìèðàõ è(2) ïðàâèëî MP ñîõðàíÿåò èñòèííîñòü.Âòîðîå î÷åâèäíî: åñëè èBA,èA Bèñòèíû âî âñåõ ìèðàõ, òîáóäåò òàêæå èñòèíà âî âñåõ ìèðàõ.Çàìå÷àíèå: ÷òîáû â ìèðåwïðîâåðèòü îöåíêóA B íàäî óäîñòîâåðèòüñÿ, ÷òîw A ⇒ w B ( w 6 A ýòà èìïëèêàöèÿ ïîäàâíî èñòèíà);ëîæíîñòü èìïëèêàöèè A B íàäî óäîñòîâåðèòüñÿ, ÷òîw A ⇒ w 6 B .èñòèííîñòü èìïëèêàöèè75 / 85ÏÐÈÊËÀÄÍÀß ÀËÃÅÁÐÀ. ×àñòü IV: ×àñòè÷íî óïîðÿäî÷åííûå ìíîæåñòâà76 / 85Ìîäåëè ÊðèïêåØêàëû Êðèïêå: òåîðåìà êîððåêòíîñòè...Äîêàçàòåëüñòâî (ïðîäîëæåíèå)Ïðîâåðèì1-þàêñèîìóÅñëè â íåêîòîðîì ìèðåv>u(â òîì ÷èñëå è âA (B A).u èìååò ìåñòî u A, òî âîu) ñïðàâåäëèâî v B A.âñåõ ìèðàõ(A (B C)) ((A B) (A C)).u, ãäå îíà ëîæíà ⇒ â í¼ì äîëæíû áûòüèñòèíû ôîðìóëû A (B C), A B è A, à C ëîæíà.Íî èç u A è u A B ñëåäóåò v B âî âñåõ ìèðàõ v > u.Ïðè u A (B C) ýòî îçíà÷àåò ñïðàâåäëèâîñòü w C âîâñåõ ìèðàõ w > v .Îòñþäà ñëåäóåò ñïðàâåäëèâîñòü u C ïðîòèâîðå÷èå.Ïðîâåðèì2-þàêñèîìóÏóñòü ñóùåñòâóåò ìèðÎñòàëüíûå àêñèîìû ïðîâåðÿþòñÿ àíàëîãè÷íî è åù¼ ïðîùå.ÏÐÈÊËÀÄÍÀß ÀËÃÅÁÐÀ.
×àñòü IV: ×àñòè÷íî óïîðÿäî÷åííûå ìíîæåñòâàÌîäåëè ÊðèïêåØêàëû Êðèïêå: òåîðåìà êîððåêòíîñòè âàæíîå ...ÑëåäñòâèåÄëÿ äîêàçàòåëüñòâà íåâûâîäèìîñòè ôîðìóëû â ÈÈÂäîñòàòî÷íî óêàçàòü øêàëó Êðèïêå, â îäíîì èç ìèðîâ êîòîðîéîíà ëîæíà.Òàêàÿ øêàëà íàçûâàåòñÿêîíòðìîäåëüþäëÿ äàííîé ôîðìóëû.Ñóùåñòâóåò êîíòðìîäåëü, ÿâëÿþùàÿñÿ êîðíåâûì äåðåâîì, âêîòîðîé ìèð ñ ëîæíîé ôîðìóëîé åãî êîðíåì.ÏðèìåðÏîñòîèì øêàëó Êðèïêå, ñîäåðæàùóþ ìèð, â êîòîðîì ôîðìóëàx ∨ ¬x ëîæíà.Âîçüì¼ì äâà ìèðà u è v òàêèå, ÷òî u 6 v , u 6 x è v x.Òîãäà v 6 ¬x, îòêóäà u 6 ¬x, ÷òî, â ñâîþ î÷åðåäü äà¼òu 6 x ∨ ¬x (íî v x ∨ ¬x).77 / 85ÏÐÈÊËÀÄÍÀß ÀËÃÅÁÐÀ.
×àñòü IV: ×àñòè÷íî óïîðÿäî÷åííûå ìíîæåñòâàÌîäåëè ÊðèïêåÊîíòðìîäåëü äëÿ x ∨ ¬x (1)78 / 85ÏÐÈÊËÀÄÍÀß ÀËÃÅÁÐÀ. ×àñòü IV: ×àñòè÷íî óïîðÿäî÷åííûå ìíîæåñòâàÌîäåëè ÊðèïêåÊîíòðìîäåëü äëÿ x ∨ ¬x (2)79 / 85ÏÐÈÊËÀÄÍÀß ÀËÃÅÁÐÀ. ×àñòü IV: ×àñòè÷íî óïîðÿäî÷åííûå ìíîæåñòâàÌîäåëè ÊðèïêåÂèçóàëèçàöèÿ êîíòðìîäåëè äëÿ x ∨ ¬x (3)80 / 85ÏÐÈÊËÀÄÍÀß ÀËÃÅÁÐÀ. ×àñòü IV: ×àñòè÷íî óïîðÿäî÷åííûå ìíîæåñòâàÌîäåëè ÊðèïêåÊîíòðìîäåëü äëÿ x ∨ ¬x (4)81 / 85ÏÐÈÊËÀÄÍÀß ÀËÃÅÁÐÀ.
×àñòü IV: ×àñòè÷íî óïîðÿäî÷åííûå ìíîæåñòâàÌîäåëè ÊðèïêåÊîíòðìîäåëü äëÿ x ∨ ¬x (5)82 / 85ÏÐÈÊËÀÄÍÀß ÀËÃÅÁÐÀ. ×àñòü IV: ×àñòè÷íî óïîðÿäî÷åííûå ìíîæåñòâàÌîäåëè ÊðèïêåÊîíòðìîäåëü äëÿ ¬ x ∨ ¬¬ xÏóñòü â ìèðå u äàííàÿ ôîðìóëà ëîæíà, ò.å. u 6 ¬ x ∨ ¬¬ x.Òîãäà u 6 ¬ x è u 6 ¬¬ x.Ïîñòðîèì äâà íåñðàâíèìûõ ìåæäó ñîáîé ìèðà v è w, áîëüøèåu, â êîòîðûõ:v 6 ¬ x è v ¬¬ x ;w 6 ¬¬ x è w ¬¬ x.Èñêîìàÿ êîíòðìîäåëü ïîëó÷åíà:ïðàâèëà èñòèííîñòè è ëîæíîñòè ôîðìóë â ìîäåëèñîáëþäåíû;ôîðìóëà x áóäåò èñòèííà òîëüêî â ìèðå v .83 / 85ÏÐÈÊËÀÄÍÀß ÀËÃÅÁÐÀ. ×àñòü IV: ×àñòè÷íî óïîðÿäî÷åííûå ìíîæåñòâàÌîäåëè ÊðèïêåÊîíòðìîäåëü äëÿ ¬ x ∨ ¬¬ x...84 / 85ÏÐÈÊËÀÄÍÀß ÀËÃÅÁÐÀ. ×àñòü IV: ×àñòè÷íî óïîðÿäî÷åííûå ìíîæåñòâàÌîäåëè ÊðèïêåØêàëû Êðèïêå: ïðèìåíåíèåÌåòîä àâòîìàòè÷åñêîé âåðèôèêàöèè ïàðàëëåëüíûõâû÷èñëèòåëüíûõ ñèñòåì (àíãë. model checking), ïîçâîëÿåòïðîâåðèòü, óäîâëåòâîðÿåò ëè çàäàííàÿ ìîäåëü ñèñòåìûôîðìàëüíûì ñïåöèôèêàöèÿì.  êà÷åñòâå ìîäåëè îáû÷íîèñïîëüçóþò øêàëû Êðèïêå, à äëÿ ñïåöèôèêàöèèàïïàðàòíîãî è ïðîãðàììíîãî îáåñïå÷åíèÿ òåìïîðàëüíóþ(âðåìåííóþ) ëîãèêó.ôîðìàëèçóþò ñèëüíûå è ñëàáûåâûðàæåíèÿ âèäà ¾íåîáõîäèìî/âîçìîæíî¿,¾âñåãäà/èíîãäà¿, ¾çäåñü/ãäå-òî¿ è ò.ä.
Çàìåíèâ âîïðåäåëåíèè øêàëû Êðèïêå ÷àñòè÷íûé ïîðÿäîê íàÌîäàëüíûå ëîãèêèìîäàëüíûåîòíîøåíèå òîëåðàíòíîñòè ïîëó÷èì ñåìàíòèêó äëÿáðàóýðîâîé ëîãèêè B;àìîðôíîå îòíîøåíèå ñåìàíòèêó äëÿ ëîãèêè S5;äèàãîíàëüíîå ìîäåëü äëÿ ìîäàëüíîé ëîãèêè M.85 / 85.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
