Автореферат (1104033), страница 2
Текст из файла (страница 2)
. . , h i, . . . Îí ïîêàçàë,÷òî ïðîáëåìà âûâîäèìîñòè ôîðìóë äëÿ ýòîãî ôðàãìåíòà ëåæèò â êëàññåPTIME, â ïðîòèâîïîëîæíîñòü òîìó, ÷òî ëîãèêà GLP è äàæå åå çàìêíóòûé ôðàãìåíò PSPACE-ïîëíû. Îòìåòèì, ÷òî èç ðåçóëüòàòà Å.Â. Äàøêîâà ñëåäóåò ðàçðåøèìîñòü çà ïîëèíîìèàëüíîå âðåìÿ äèàãðàìì ìîäåëåé( /∼; ∧, <0 , >, h0i, h1i, . . .
, h i, . . .) è ( n /∼; ∧, <0 , >, h0i, h1i, . . . , h i). äèññåðòàöèè äîêàçàíî, ÷òî ýëåìåíòàðíàÿ òåîðèÿ ìîäåëè( /∼; <0 , >, h0i, h1i, . . . , h i, . . .) íåðàçðåøèìà. Äîêàçàíî, ÷òî ïðèâñåõ íàòóðàëüíûõ≥ 3 íåðàçðåøèìû ýëåìåíòàðíûå òåîðèè ìîäåëåé( n /∼; <0 , >, h0i, h1i, . . . , h i). Ïðè ýòîì ïîêàçàíî, ÷òî ýëåìåíòàðíàÿòåîðèÿ ìîäåëè ( 2 /∼; <0 , >, h0i, h1i, h2i) ðàçðåøèìà. Äîêàçàíî, ÷òî ÿçûêà ïåðâîãî ïîðÿäêà â ïîëóðåøåòêàõ ( /∼; ∧) è ( n /∼; ∧) äîñòàòî÷íîäëÿ âûðàæåíèÿ âñåõ ðàññìîòðåííûõ âûøå ïðåäèêàòîâ è ôóíêöèé íàòåõ æå íîñèòåëÿõ, è òåì ñàìûì íà ýòè ñòðóêòóðû ïåðåíîñÿòñÿ ðåçóëüòàòû î íåðàçðåøèìîñòè.
Êðîìå ýòîãî, äîêàçàíî, ÷òî íåðàçðåøèìà èýëåìåíòàðíàÿ òåîðèÿ ìîäåëè ( 2 /∼; ∧).WWnWWWnnWWnnnWWWÖåëè ðàáîòû.1. Îïðåäåëèòü àëãîðèòìè÷åñêóþ ñëîæíîñòü ïðîáëåìû ðàñïîçíàâàíèÿâûâîäèìîñòè çàìêíóòûõ ôîðìóë äëÿ ëîãèê GLP è GLPn .2. Èññëåäîâàòü âîïðîñ î ðàçðåøèìîñòè ýëåìåíòàðíûõ òåîðèé ïîëóðåøåòêè GLP-ñëîâ è ïîëóðåøåòîê GLPn -ñëîâ.11 Å.Â. Äàøêîâ. Î ïîçèòèâíîì ôðàãìåíòå ïîëèìîäàëüíîé ëîãèêè äîêàçóåìîñòè GLP.Ìàòåìàòè÷åñêèå çàìåòêè, 91(3):331346, 2012.43. Èññëåäîâàòü âîïðîñ î ðàçðåøèìîñòè ýëåìåíòàðíûõ òåîðèé àëãåáð,ñîîòâåòñòâóþùèõ ïîëíîé ñèñòåìå îðäèíàëüíûõ îáîçíà÷åíèé Áåêëåìèøåâà è åå ôðàãìåíòîâ, ïîðîæäåííûõ ëèøü ïåðâûìè ìîäàëüíîñòÿìè.nÍàó÷íàÿ íîâèçíà. Ðåçóëüòàòû äèññåðòàöèè ÿâëÿþòñÿ íîâûìè è ïîëó÷åíû àâòîðîì ñàìîñòîÿòåëüíî. Îñíîâíûå ðåçóëüòàòû äèññåðòàöèè ñîñòîÿò â ñëåäóþùåì:1.
Ïðîáëåìà ðàñïîçíàâàíèÿ âûâîäèìîñòè äëÿ çàìêíóòûõ ôîðìóë â ëîãèêå GLP ÿâëÿåòñÿ PSPACE-ïîëíîé.n2. Äëÿ êàæäîãî íàòóðàëüíîãî ïðîáëåìà ðàñïîçíàâàíèÿ âûâîäèìîñòèäëÿ çàìêíóòûõ ôîðìóë â ëîãèêå GLPn ðàçðåøèìà çà ïîëèíîìèàëüíîå âðåìÿ.W3. Ïîëóðåøåòêà ( /∼; ∧) è ïîëóðåøåòêè (íåðàçðåøèìûå ýëåìåíòàðíûå òåîðèè.Wn/∼; ∧) äëÿ n ≥ 2, èìåþòW1/∼; ∧) îáëàäàåò ðàçðåøèìîé ýëåìåíòàðíîé òåîðè-4.
Ïîëóðåøåòêà (åé.Wn5. Ýëåìåíòàðíàÿ òåîðèÿ àëãåáðû ( /∼; <0 , >, h0i, h1i, . . . , h i, . . .)íåðàçðåøèìà. Òàêæå äëÿ ≥ 3 íåðàçðåøèìà ýëåìåíòàðíàÿ òåîðèÿàëãåáðû ( n /∼; <0 , >, h0i, h1i, . . . , h i).nWn6. Àëãåáðà (W2 /∼; <0 , >, h0i, h1i, h2i) îáëàäàåò ðàçðåøèìîé ýëåìåíòàðíîé òåîðèåé.Ìåòîäû èññëåäîâàíèÿ.  ðàáîòå èñïîëüçóþòñÿ ìåòîäû òåîðèèñëîæíîñòè âû÷èñëåíèé, ìîäàëüíîé ëîãèêè è òåîðèè ìîäåëåé. Äëÿ äîêàçàòåëüñòâà PSPACE-ïîëíîòû çàìêíóòîãî ôðàãìåíòà ëîãèêè GLP ñòðîèòñÿïîëèíîìèàëüíîå ñâåäåíèå ÿçûêà áóëåâûõ ôîðìóë ñ êâàíòîðàìè ê èñêîìîìó.
Ïîëèíîìèàëüíûå ðàçðåøàþùèå àëãîðèòìû äëÿ çàìêíóòûõ ôðàãìåíòîâ GLPn îñíîâàíû íà ýôôåêòèâíîì êîäèðîâàíèè ïîäìíîæåñòâ ïðåäëîæåííîé Ê.Í. Èãíàòüåâûì12 óíèâåðñàëüíîé ìîäåëè Êðèïêå äëÿ çàìêíóòîãî ôðàãìåíòà ëîãèêè GLP. Ìû äîêàçûâàåì íåðàçðåøèìîñòü ýëåìåíòàðíûõ òåîðèé ïîëóðåøåòîê GLP-ñëîâ, èíòåðïðåòèðóÿ â íèõ íåðàçðåøèìóþ13 ñëàáóþ ìîíàäè÷åñêóþ òåîðèþ íàòóðàëüíûõ ÷èñåë â ñèãíàòóðå,12 K.N. Ignatiev. On strong provability predicates and the associated modal logics. TheJournal of Symbolic Logic, 58(1):249290, 1993.13 C.C.
Elgot and M.O. Rabin. Decidability and undecidability of extensions of second(rst) order theory of (generalized) successor. Journal of Symbolic Logic, 31:169181, 1966.5Hxxâêëþ÷àþùåé â ñåáÿ ôóíêöèþ ñëåäîâàíèÿ è ôóíêöèþ ( ) = 2 . Äëÿ äîêàçàòåëüñòâà ðàçðåøèìîñòè ýëåìåíòàðíîé òåîðèè ïîëóðåøåòêè ( 1 /∼; ∧)ñòðîèòñÿ åå èíòåðïðåòàöèÿ â òåîðèè ñòðóêòóðû (ω ω ; <, +). Ðåçóëüòàòû îíåðàçðåøèìîñòè ýëåìåíòàðíûõ òåîðèé ñèñòåìû îðäèíàëüíûõ îáîçíà÷åíèé Áåêëåìèøåâà è åå ôðàãìåíòîâ äîêàçûâàþòñÿ ïóòåì ïîãðóæåíèÿ òåîðèè êëàññà âñåõ ïàð ëèíåéíûõ ïîðÿäêîâ íà êîíå÷íûõ ìíîæåñòâàõ.
Ðàçðåøèìîñòü ýëåìåíòàðíîé òåîðèè ìîäåëè ( 2 /∼; <0 , >, h0i, h1i, h2i) äîêàçûâàåòñÿ ïðè ïîìîùè ïîñòðîåíèÿ åå èíòåðïðåòàöèè â ðàçðåøèìîé â ñèëó ðåçóëüòàòà Ë. Áðî14 ñëàáîé ìîíàäè÷åñêîé òåîðèè îðäèíàëà ω ω , ñíàáæåííîãîïîðÿäêîì è ïðåäèêàòîì, çàäàþùèì ñòàíäàðòíóþ ñèñòåìó êîôèíàëüíûõïîñëåäîâàòåëüíîñòåé.Òåîðåòè÷åñêàÿ è ïðàêòè÷åñêàÿ öåííîñòü. Ðàáîòà èìååò òåîðåòè÷åñêèé õàðàêòåð. Ïîëó÷åííûå ðåçóëüòàòû ìîãóò íàéòè ïðèìåíåíèå â ìàòåìàòè÷åñêîé ëîãèêå è òåîðåòè÷åñêîé èíôîðìàòèêå. Ðåçóëüòàòû äèññåðòàöèè ìîãóò áûòü ïîëåçíû ñïåöèàëèñòàì, ðàáîòàþùèì â Ìàòåìàòè÷åñêîìèíñòèòóòå èì.
Â.À. Ñòåêëîâà ÐÀÍ, ÌÃÓ èì. Ì.Â. Ëîìîíîñîâà, Èíñòèòóòåìàòåìàòèêè èì. Ñ.Ë. Ñîáîëåâà ÑÎ ÐÀÍ, ÏÎÌÈ èì. Â.À. Ñòåêëîâà ÐÀÍ,ÈÏÏÈ èì. À.À. Õàðêåâè÷à ÐÀÍ, Òâåðñêîì ãîñóäàðñòâåííîì óíèâåðñèòåòå è äð.Àïðîáàöèÿ äèññåðòàöèè. Ðåçóëüòàòû äèññåðòàöèè äîêëàäûâàëèñüíà ñëåäóþùèõ ñåìèíàðàõ è êîíôåðåíöèÿõ:WW1. 1-àÿ è 2-àÿ ìåæäóíàðîäíûå êîíôåðåíöèè ¾International Workshopon Proof Theory, Modal Logic and Reection Principles¿ â Áàðñåëîíå,Èñïàíèÿ, 16 àïðåëÿ 2012 ãîäà è â Ìåõèêî, Ìåêñèêà, 1 îêòÿáðÿ 2014ãîäà, ñîîòâåòñòâåííî;2. Ìåæäóíàðîäíàÿ êîíôåðåíöèÿ ¾Logic Colloquium 2013¿ â Ýâîðå,Ïîðòóãàëèÿ, 22 èþëÿ 2013 ãîäà;3.
Ìåæäóíàðîäíàÿ êîíôåðåíöèÿ ¾Advances in Modal Logic 2012¿ â Êîïåíãàãåíå, Äàíèÿ 22 àâãóñòà 2012 ãîäà ;4. Êîíôåðåíöèÿ ¾Ëîìîíîñîâ 2012¿ â Ìîñêâå, Ðîññèÿ, 11 àïðåëÿ 2012ãîäà;5. Ñåìèíàð ¾Àëãîðèòìè÷åñêèå ïðîáëåìû àëãåáðû è ëîãèêè¿ ïîä ðóêîâîäñòâîì àêàäåìèêà ÐÀÍ Ñ.È. Àäÿíà â Ìîñêâå, Ðîññèÿ, 23 îêòÿáðÿ2012, 9 àïðåëÿ 2013 ãîäà è 24 ôåâðàëÿ 2015 ãîäà;14 L. Braud. Covering of ordinals. In Foundations of Software Technology and TheoreticalComputer Science, pages 97108, 2009.6Ïóáëèêàöèè.
Îñíîâíûå ðåçóëüòàòû äèññåðòàöèè îïóáëèêîâàíû â ðàáîòàõ [1][3], èç íèõ âñå â æóðíàëàõ èç ïåðå÷íÿ ÂÀÊ.Ñòðóêòóðà äèññåðòàöèè. Ðàáîòà ñîñòîèò èç ââåäåíèÿ, òðåõ ãëàâ,ñîäåðæàùèõ 10 ðàçäåëîâ, è ñïèñêà ëèòåðàòóðû. Áèáëèîãðàôèÿ ñîäåðæèò33 íàèìåíîâàíèÿ. Òåêñò äèññåðòàöèè èçëîæåí íà 83 ñòðàíèöàõ.Ñîäåðæàíèå ðàáîòûñîäåðæèò äîêàçàòåëüñòâî PSPACE-ïîëíîòû ïðîáëåìû ðàñïîçíàâàíèÿ âûâîäèìîñòè äëÿ çàìêíóòîãî ôðàãìåíòà ëîãèêè GLP è äîêàçàòåëüñòâà ïîëèíîìèàëüíîé ðàçðåøèìîñòè ïðîáëåì ðàñïîçíàâàíèÿ âûâîäèìîñòè äëÿ çàìêíóòûõ ôðàãìåíòîâ ëîãèê GLPn .Îñíîâíîé ðåçóëüòàò ãëàâû 2 ñîñòîèò â äîêàçàòåëüñòâå íåðàçðåøèìîñòè ýëåìåíòàðíîé òåîðèè ïîëóðåøåòêè GLP-ñëîâ.
Êðîìå òîãî, óñòàíîâëåíî, ÷òî ýëåìåíòàðíàÿ òåîðèÿ ïîëóðåøåòêè GLPn -ñëîâ íåðàçðåøèìà, åñëèè òîëüêî åñëè ≥ 2.Ãëàâà 3 ïîñâÿùåíà èññëåäîâàíèþ ýëåìåíòàðíûõ òåîðèé ñèñòåì îðäèíàëüíûõ îáîçíà÷åíèé íà îñíîâå ëîãèêè GLP. Äîêàçàíî, ÷òî àëãåáðà ñîîòâåòñòâóþùàÿ ïîëíîé ñèñòåìå îðäèíàëüíûõ îáîçíà÷åíèé äëÿ îðäèíàëà ε0îáëàäàåò íåðàçðåøèìîé ýëåìåíòàðíîé òåîðèåé. Òàêæå â ãëàâå 3 äîêàçûâàåòñÿ, ÷òî ýëåìåíòàðíàÿ òåîðèÿ àëãåáðû, ñîîòâåòñòâóþùåé ñèñòåìå îðäèíàëüíûõ îáîçíà÷åíèé, ïîðîæäàåìîé h0i, .
. . , h i, íåðàçðåøèìà ïðè ≥ 3è ðàçðåøèìà ïðè = 2.Ãëàâà 1nnnnßçûê ïîëèìîäàëüíîé ëîãèêè äîêàçóåìîñòè GLP ýòî ÿçûê èñ÷èñëåíèÿ âûñêàçûâàíèé ñ ïðîïîçèöèîíàëüíûìè êîíñòàíòàìè ¾èñòèíà¿ > è¾ëîæü¿ ⊥, îáîãàùåííûé óíàðíûìè ñâÿçêàìè [0], [1], . . . Çàïèñü h iϕ ÿâëÿåòñÿ ñîêðàùåíèåì äëÿ ¬[ ]¬ϕ. GLP çàäàåòñÿ ñëåäóþùèìè àêñèîìàìè èïðàâèëàìè âûâîäà:nnn0. Àêñèîìû è ïðàâèëà âûâîäà ëîãèêè GL äëÿ êàæäîé ñâÿçêè [ ];knk ≤ n;2.
hkiϕ → [n]hkiϕ, ãäå k < n.1. [ ]ϕ → [ ]ϕ, ãäåÌû îáîçíà÷àåì ÷åðåç GLPn ëîãèêó, ÿçûê êîòîðîé ïîëó÷àåòñÿ èç ÿçûêàïðîïîçèöèîíàëüíîé ëîãèêè îáîãàùåíèåì ñâÿçêàìè [0], . . . , [ ], à òåîðåìàìèÿâëÿþòñÿ âñå òåîðåìû GLP â ýòîì ÿçûêå. ãëàâå 1 äîêàçûâàåòñÿn7Ïðîáëåìà ðàñïîçíàâàíèÿ âûâîäèìîñòè çàìêíóòûõ ôîðìóëâ ëîãèêå GLP ÿâëÿåòñÿ PSPACE-ïîëíîé.Òåîðåìà 1.Äàëåå â ýòîé ãëàâå äîêàçûâàåòñÿ, ÷òî íàëè÷èå áåñêîíå÷íîãî ÷èñëà ðàçëè÷íûõ ìîäàëüíûõ ñâÿçîê â ÿçûêå íåîáõîäèìî äëÿ ïîëó÷åíèÿ PSPACEïîëíîòû.Ïðè âñåõ n ïðîáëåìà ðàñïîçíàâàíèÿ âûâîäèìîñòè çàìêíóòûõ ôîðìóë â ëîãèêå GLPn ðàçðåøèìà çà ïîëèíîìèàëüíîå âðåìÿ.Òåîðåìà 2.Äëÿ äîêàçàòåëüñòâà ïîñëåäíåé òåîðåìû ìû ðàññìàòðèâàåì óíèâåðñàëüíóþ ìîäåëü Êðèïêå äëÿ çàìêíóòîãî ôðàãìåíòà ëîãèêè GLP.
Ïîëèíîìèàëüíûé àëãîðèòì îñíîâûâàåòñÿ íà ýôôåêòèâíîì çàäàíèè ïîäìíîæåñòâýòîé ìîäåëè, îïðåäåëèìûõ çàìêíóòûìè GLPn -ôîðìóëàìè.Îäíèì èç öåíòðàëüíûõ äëÿ ãëàâ 2 è 3 ïîíÿòèé ÿâëÿåòñÿ ïîíÿòèå GLPñëîâà. Ðàññìàòðèâàåòñÿ ìíîæåñòâî âñåõ ôîðìóë âèäà h 1 ih 2 i . . .
h k i>.Òàêèå ôîðìóëû íàçûâàþòñÿ GLP. Òàêæå äëÿ êðàòêîñòè â ðàìêàõ äàííîé äèññåðòàöèè ìû íàçûâàåì èõ ïðîñòî. Äëÿ îáîçíà÷åíèÿ ñëîâ ìû èñïîëüçóåì áóêâû A, B, . . .Íà ìíîæåñòâå âñåõ GLP-ôîðìóë îïðåäåëèì áèíàðíûå îòíîøåíèÿ <n :W-ñëîâàìèn nñëîâàìènndefϕ <n ψ ⇐⇒ GLP ` ψ → h iϕ.Ìû îáîçíà÷àåì ÷åðåç ∼ îòíîøåíèå GLP-äîêàçóåìîé ýêâèâàëåíòíîñòèíà ôîðìóëàõ è, â ÷àñòíîñòè, íà ñëîâàõ:defϕ ∼ ψ ⇐⇒ GLP ` ϕ ↔ ψ.Êàê áûëî îòìå÷åíî âûøå, êîíúþíêöèÿ äâóõ ñëîâ â GLP ýêâèâàëåíòíà íåêîòîðîìó ñëîâó.
Òåì ñàìûì, h i è ∧ åñòåñòâåííûì îáðàçîì çàäàþòôóíêöèè íà êëàññàõ ýêâèâàëåíòíîñòè ñëîâ:nnnh i[A]∼ = {B | B ∼ h iA},[A]∼ ∧ [B]∼ = {C | C ∼ A ∧ B}. ãëàâàõ 2 è 3 ìû èçó÷àåì ðàçðåøèìîñòü ýëåìåíòàðíûõ òåîðèé ìîäåëåé ( /∼; ∧, <0 , >, h0i, h1i, . . . , h i, . . .), ( n /∼; ∧, <0 , >, h0i, h1i, . . . , h i) èìîäåëåé, ïîëó÷àåìûõ èç íèõ îïóñêàíèåì íåêîòîðûõ ïðåäèêàòîâ è ôóíêöèé. Îòìåòèì, ÷òî ôàêòè÷åñêè èç ñîîáðàæåíèé òåõíè÷åñêîãî óäîáñòâàìû ðàáîòàåì íå íåïîñðåäñòâåííî ñ ýòèìè ìîäåëÿìè, à ñ èçîìîðôíûìèìîäåëÿìè, íîñèòåëè êîòîðûõ ñîñòàâëåíû èç ñëîâ â íîðìàëüíîé ôîðìåWkW8n(êàíîíè÷åñêèõ ïðåäñòàâèòåëåé êëàññîâ ýêâèâàëåíòíîñòè GLP-ñëîâ ïî îòíîøåíèþ ∼).Îñíîâíîé ðåçóëüòàò ãëàâû 2, â êîòîðîé ìû èçó÷àåì âîïðîñû î ðàçðåøèìîñòè ýëåìåíòàðíûõ òåîðèé ïîëóðåøåòîê óêàçàííîãî âûøå âèäà, ñîñòîèò â ñëåäóþùåì.Ýëåìåíòàðíàÿ òåîðèÿ íèæíåé ïîëóðåøåòêè (W/∼; ∧)íåðàçðåøèìà.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
