Диссертация (1104034)
Текст из файла
ÔÃÁÓÍ Ìàòåìàòè÷åñêèé èíñòèòóò èì. Â.À. ÑòåêëîâàÐîññèéñêîé àêàäåìèè íàóêÍà ïðàâàõ ðóêîïèñèÓÄÊ 510.643ÏàõîìîâÔåäîð Íèêîëàåâè÷Íåêîòîðûå àëãîðèòìè÷åñêèå âîïðîñûäëÿ ïîëèìîäàëüíûõ ëîãèê äîêàçóåìîñòèÑïåöèàëüíîñòü 01.01.06 ìàòåìàòè÷åñêàÿ ëîãèêà, àëãåáðàè òåîðèÿ ÷èñåëÄÈÑÑÅÐÒÀÖÈßíà ñîèñêàíèå ó÷åíîé ñòåïåíè êàíäèäàòà ôèçèêî-ìàòåìàòè÷åñêèõ íàóêÍàó÷íûé ðóêîâîäèòåëü:÷ëåí-êîðð.
ÐÀÍ Ëåâ Äìèòðèåâè÷ ÁåêëåìèøåâÌÎÑÊÂÀ 2015ÎãëàâëåíèåÂâåäåíèå1233Àëãîðèòìè÷åñêàÿ ñëîæíîñòü çàìêíóòûõ ôðàãìåíòîâ121.1Ëîãèêà GLP è åå çàìêíóòûé ôðàãìåíò . . . . . . . . . . . 121.2Çàìêíóòûå ôðàãìåíòû ëîãèê GLPn . . . . . . . . . . . . . 18Ýëåìåíòàðíûå òåîðèè ïîëóðåøåòîêGLP-ñëîâ362.1GLP-ñëîâà . . . . . .
. . . . . . . . . . . . . . . . . . . . . . 362.2Íåêîòîðûå ñâîéñòâà ïîëóðåøåòîê ñëîâ . . . . . . . . . . . . 402.3Îïðåäåëèìûå â ïîëóðåøåòêàõ ñëîâ ñâîéñòâà . . . . . . . . 452.4Íåðàçðåøèìûå òåîðèè . . . . . . . . . . . . . . . . . . . . . 512.5Ñëîâà èç äâóõ ñèìâîëîâ . . . . . .
. . . . . . . . . . . . . . 58Ýëåìåíòàðíûå òåîðèè ñèñòåìû îðäèíàëüíûõ îáîçíà÷åíèé Áåêëåìèøåâà è åå ôðàãìåíòîâ3.161Ñèñòåìû îðäèíàëüíûõ îáîçíà÷åíèé ñ íåðàçðåøèìûìèýëåìåíòàðíûìè òåîðèÿìè . . . . . . . . . . . . . . . . . . . 613.2Íåêîòîðûå òåîðèè îðäèíàëîâ è ñëîâ . . . . . . . . . . .
. . 673.3Ýëåìåíòàðíàÿ ýêâèâàëåíòíîñòü íåêîòîðûõ ìîäåëåé . . . . 76Ëèòåðàòóðà802ÂâåäåíèåÄèññåðòàöèÿ ïîñâÿùåíà èçó÷åíèþ ïîíÿòèÿ äîêàçóåìîñòè ñðåäñòâàìè ìîäàëüíîé ëîãèêè.  äèññåðòàöèè èññëåäóþòñÿ àëãîðèòìè÷åñêèå ñâîéñòâàïîëèìîäàëüíîé ëîãèêè äîêàçóåìîñòè Äæàïàðèäçå è åå ôðàãìåíòîâ.Èäåÿ èçó÷åíèÿ ñâîéñòâ äîêàçóåìîñòè ñðåäñòâàìè ìîäàëüíûõ ëîãèê âîñõîäèò ê Ê.
Ãåäåëþ [20]. Ãåäåëü ïðåäëîæèë èíòåðïðåòèðîâàòü ñâÿçêó ìîäàëüíîñòè 2 êàê àðèôìåòè÷åñêóþ ôîðìóëó PrT , âûðàæàþùóþ äîêàçóåìîñòü â äàííîé ôîðìàëüíîé òåîðèè T.Èç ðåçóëüòàòîâ Ãåäåëÿ è Ëåáà [25] âûòåêàåò, ÷òî äëÿ ïåðå÷èñëèìûõ òåîðèé T, ñîäåðæàùèõ ïåðâîïîðÿäêîâóþ àðèôìåòèêó Ïåàíî PA,ëþáàÿ òåîðåìà ìîäàëüíîé ëîãèêè GL âûðàæàåò ñâîéñòâî äîêàçóåìîñòè â T, êîòîðîå ìîæíî îáîñíîâàòü ñðåäñòâàìè ñàìîé òåîðèè T. ËîãèêàÃåäåëÿ-Ëåáà GL ôîðìàëèçóåòñÿ â ÿçûêå èñ÷èñëåíèÿ âûñêàçûâàíèé, îáîãàùåííîì ñâÿçêîé 2, è ïîëó÷àåòñÿ äîáàâëåíèåì ê àêñèîìàì è ïðàâèëàìâûâîäà èñ÷èñëåíèÿ âûñêàçûâàíèé ñëåäóþùèõ àêñèîì è ïðàâèë âûâîäà:1. 2(ϕ → ψ) → (2ϕ → 2ψ);2.
2(2ϕ → ϕ) → 2ϕ (àêñèîìà Ëåáà);3.ϕ.2ϕ 1976 ãîäó Ð.Ì. Ñîëîâåé [27] äîêàçàë òåîðåìó îá àðèôìåòè÷åñêîéïîëíîòå ëîãèêè GL. Ìîäàëüíàÿ ôîðìóëà ÿâëÿåòñÿ òåîðåìîé ëîãèêè GL,åñëè è òîëüêî åñëè îíà ïåðåâîäèòñÿ â òåîðåìó PA ïðè ëþáîé ïîäñòàíîâêåàðèôìåòè÷åñêèõ ïðåäëîæåíèé âìåñòî ïðîïîçèöèîíàëüíûõ ïåðåìåííûõè ðàñøèôðîâêå 2 êàê PrPA .Ñ ñåðåäèíû 1970-õ ãîäîâ èññëåäîâàíèþ ëîãèêè GL è äðóãèõ ëîãèê äîêàçóåìîñòè áûëî ïîñâÿùåíî çíà÷èòåëüíîå ÷èñëî ðàáîò.  1986 ã.3Ã.Ê. Äæàïàðèäçå ðàññìîòðåë [2] îáîáùåíèå GL ëîãèêó GLP, â êîòîðîé âìåñòî îäíîé ìîäàëüíîé ñâÿçêè 2 èñïîëüçóåòñÿ çàíóìåðîâàííîåíàòóðàëüíûìè ÷èñëàìè ñåìåéñòâî ìîäàëüíûõ ñâÿçîê [0], [1], .
. . , [n], . . .Äæàïàðèäçå äîêàçàë àíàëîã òåîðåìû Ñîëîâåÿ îá àðèôìåòè÷åñêîé ïîëíîòå, â êîòîðîì ñâÿçêè [n] èíòåðïðåòèðóþòñÿ êàê äîêàçóåìîñòü èç àêñèîì PA ñ èñïîëüçîâàíèåì âûâîäîâ ñ ω -ïðàâèëàìè c ãëóáèíîé âëîæåííîñòèω -ïðàâèë, íå ïðåâîñõîäÿùåé n. íàñòîÿùåå âðåìÿ ëîãèêà GLP àêòèâíî èçó÷àåòñÿ â ñâÿçè ñ ååïðèìåíåíèÿìè â îðäèíàëüíîì àíàëèçå àðèôìåòè÷åñêèõ òåîðèé [7]. Âîïðîñ î õàðàêòåðèçàöèè ôîðìàëüíûõ òåîðèé îðäèíàëàìè ÿâëÿåòñÿ îäíèìèç öåíòðàëüíûõ âîïðîñîâ â òåîðèè äîêàçàòåëüñòâ. Èññëåäîâàíèÿ òàêîãîðîäà âîñõîäÿò ê Ã.
Ãåíöåíó [19], êîòîðûé äîêàçàë íåïðîòèâîðå÷èâîñòüPA ñ ïîìîùüþ òðàíñôèíèòíîé èíäóêöèè äî îðäèíàëà ε0 . Ïðèìåíåíèåëîãèêè GLP îñíîâàíî íà èñïîëüçîâàíèè çàìêíóòûõ ôîðìóë (ôîðìóëáåç ïðîïîçèöèîíàëüíûõ ïåðåìåííûõ) äëÿ îáîçíà÷åíèÿ àðèôìåòè÷åñêèõòåîðèé è äëÿ ïîñòðîåíèÿ åñòåñòâåííîé ñèñòåìû îðäèíàëüíûõ îáîçíà÷åωω ···íèé äëÿ îðäèíàëà ε0 = sup{ω| {z } | n ∈ ω}.n ðàç äèññåðòàöèè ðàññìàòðèâàþòñÿ äâà êðóãà àëãîðèòìè÷åñêèõ âîïðîñîâ, ñâÿçàííûõ ñ çàìêíóòûì ôðàãìåíòîì ëîãèêè GLP.1.
Àëãîðèòìè÷åñêàÿ ñëîæíîñòü ïðîáëåìû ðàñïîçíàâàíèÿ âûâîäèìîñòè.2. Ðàçðåøèìîñòü ýëåìåíòàðíûõ òåîðèé àëãåáð åñòåñòâåííûõ ñèñòåì îðäèíàëüíûõ îáîçíà÷åíèé.Âîïðîñ îá àëãîðèòìè÷åñêîé ñëîæíîñòè ïðîáëåìû âûâîäèìîñòèäëÿ ìîäàëüíûõ ëîãèê èçó÷àëñÿ Ð.Å. Ëàäíåðîì [24]. Îí ïîêàçàë, ÷òîìíîãèå êëàññè÷åñêèå ìîäàëüíûå ëîãèêè, âêëþ÷àÿ S4, K, T, îáëàäàþòPSPACE-ïîëíûìè ïðîáëåìàìè ðàñïîçíàâàíèÿ âûâîäèìîñòè ôîðìóë. Õîòÿ ëîãèêà GL íå áûëà ðàññìîòðåíà â ýòîé ðàáîòå Ëàäíåðà, íî èñïîëüçîâàííûé òàì ìåòîä ëåãêî ïîçâîëÿåò ïîëó÷èòü àíàëîãè÷íûé ðåçóëüòàò èäëÿ íåå.  äàëüíåéøåì, È.Á. Øàïèðîâñêèé äîêàçàë, ÷òî è ëîãèêà GLP4îáëàäàåò PSPACE-ïîëíîé ïðîáëåìîé ðàñïîçíàâàíèÿ âûâîäèìîñòè [26].À.Â.
×àãðîâûì è Ì.Í. Ðûáàêîâûì ðàññìàòðèâàëèñü ôðàãìåíòûìîäàëüíûõ ëîãèê ñ îãðàíè÷åíèåì íà ÷èñëî ðàçëè÷íûõ ïðîïîçèöèîíàëüíûõ ïåðåìåííûõ â ôîðìóëàõ è âîïðîñ îá àëãîðèòìè÷åñêîé ñëîæíîñòèäëÿ ýòèõ ôðàãìåíòîâ [15]. Èìè áûëî ïîêàçàíî, ÷òî äàæå ôðàãìåíòëîãèêè GL ñ îäíîé ïðîïîçèöèîíàëüíîé ïåðåìåííîé ÿâëÿåòñÿ PSPACEïîëíûì; òàì æå áûëè ïîëó÷åíû àíàëîãè÷íûå ðåçóëüòàòû äëÿ ëîãèê S4è Grz.
Ïðè ýòîì îíè ïîêàçàëè, ÷òî çàìêíóòûé ôðàãìåíò ëîãèêè GL ðàçðåøèì çà ïîëèíîìèàëüíîå âðåìÿ.  òî æå âðåìÿ çàìêíóòûå ôðàãìåíòûëîãèê K4 è K ÿâëÿþòñÿ PSPACE-ïîëíûìè. Òàêæå Ô. Áîó è É. Éîîñòåíäîêàçàëè, ÷òî çàìêíóòûé ôðàãìåíò ëîãèêè èíòåðïðåòèðóåìîñòè IL, ðàñøèðÿþùåé GL, ÿâëÿåòñÿ PSPACE-òðóäíûì [12]. äèññåðòàöèè äîêàçàíà PSPACE-ïîëíîòà çàìêíóòîãî ôðàãìåíòàëîãèêè GLP.Ìû îáîçíà÷àåì ÷åðåç GLPn ôðàãìåíò ëîãèêè GLP ñ ìîäàëüíîñòÿìè [0], [1], . . . , [n]. Òàêæå äîêàçàíî, ÷òî äëÿ âñÿêîãî íàòóðàëüíîãî nçàìêíóòûé ôðàãìåíò ëîãèêè GLPn ðàçðåøèì çà ïîëèíîìèàëüíîå âðåìÿ.Ïåðåéäåì ê âîïðîñàì ðàçðåøèìîñòè ýëåìåíòàðíûõ òåîðèé àëãåáð,ñâÿçàííûõ ñ êîíñòðóêòèâíûìè ñèñòåìàìè îðäèíàëüíûõ îáîçíà÷åíèé.Íàèáîëåå èçâåñòíîé ñèñòåìîé îáîçíà÷åíèé äëÿ îðäèíàëà ε0 ÿâëÿåòñÿòàê íàçûâàåìàÿ êàíòîðîâñêàÿ ñèñòåìà.
Îáîçíà÷åíèÿìè äëÿ îðäèíàëîââ ýòîé ñèñòåìå ÿâëÿþòñÿ çàìêíóòûå òåðìû, ñîñòàâëåííûå èç êîíñòàíòû0, ôóíêöèè + è ôóíêöèè f : x 7−→ ω x . Êàíòîðîâñêàÿ ñèñòåìà ñîîòâåòñòâóåò àëãåáðå (ε0 ; <, 0, +, f ); çàìåòèì, ÷òî â ýòîé àëãåáðå âñÿêèé îðäèíàë ìåíüøèé ε0 ðàâåí çíà÷åíèþ íåêîòîðîãî çàìêíóòîãî òåðìà. Èçâåñòíî,÷òî ýëåìåíòàðíàÿ òåîðèÿ ìîäåëè (ε0 ; <, 0, +, f ) ÿâëÿåòñÿ àëãîðèòìè÷åñêè íåðàçðåøèìîé.Åñòåñòâåííûé, ñâÿçàííûé ñ îðäèíàëüíûì àíàëèçîì ñïîñîá îáîçíà÷åíèÿ îðäèíàëîâ íà îñíîâå çàìêíóòîãî ôðàãìåíòà ëîãèêè GLP áûëïðåäëîæåí Ë.Ä. Áåêëåìèøåâûì [7].
Îðäèíàëû îáîçíà÷àþòñÿ ôîðìóëà-5ìè âèäà hn1 ihn1 i . . . hnk i>, íàçûâàåìûìè ñëîâàìè. Ìû îáîçíà÷àåì ìíîæåñòâî âñåõ ñëîâ W. Áèíàðíîå îòíîøåíèå <0 íà ñëîâàõ ñîîòâåòñòâóåòïîðÿäêó íà îðäèíàëàõ:defA <0 B ⇐⇒ GLP ` A → h0iB.Îòíîøåíèå ðàâåíñòâà îðäèíàëîâ ñîîòâåòñòâóåò îòíîøåíèþ GLPäîêàçóåìîéíàëüíûõýêâèâàëåíòíîñòèîáîçíà÷åíèéäëÿñëîâ∼.îðäèíàëàÏîëíîéε0(W/∼; <0 , >, h0i, h1i, . . .
, hni, . . .).Òàêæååñòåñòâåííûõñèñòåìûôðàãìåíòîâýòîéñèñòåìåñîîòâåòñòâóåòìûîðäèàëãåáðàðàññìàòðèâàåìîðäèíàëüíûõðÿäîáîçíà÷å-íèé. Îáîçíà÷èì ÷åðåç Wn ìíîæåñòâî âñåõ ñëîâ ñîñòàâëåííûõ èç> è h0i, . . . , hni; ìû íàçûâàåì òàêèå ñëîâà GLPn -ñëîâàìè. Ìîäåëü(Wn /∼; <0 , >, h0i, h1i, . . . , hni) ÿâëÿåòñÿ ñèñòåìîé îðäèíàëüíûõ îáîçíà÷åíèé äëÿ îðäèíàëîâ ωn+1 ; çäåñüω0 = 1,ωn+1 = ω ωn .Îòìåòèì, ÷òî êîíúþíêöèÿ âñÿêèõ äâóõ ñëîâ GLP-äîêàçóåìî ýêâèâàëåíòíà íåêîòîðîìó GLP-ñëîâó [7].
Ýòî äàåò âîçìîæíîñòü åñòåñòâåííûì îáðàçîì ðàññìàòðèâàòü ïîëóðåøåòêè (W/∼; ∧) è (Wn /∼; ∧).Å.Â. Äàøêîâ [1] ðàññìîòðåë ôðàãìåíò ëîãèêè GLP, ñîñòîÿùèéèç èìïëèêàöèé ìåæäó ñòðîãî ïîçèòèâíûìè ôîðìóëàìè, òî åñòü ìåæäó ôîðìóëàìè ïîñòðîåííûìè èç ïåðåìåííûõ, ∧, > è h0i, h1i, . . .
hni.Îí ïîêàçàë, ÷òî ïðîáëåìà âûâîäèìîñòè ôîðìóë äëÿ ýòîãî ôðàãìåíòà ëåæèò â êëàññå PTIME, â ïðîòèâîïîëîæíîñòü òîìó, ÷òî ëîãèêà GLP è äàæå åå çàìêíóòûé ôðàãìåíò PSPACE-ïîëíû. Îòìåòèì,÷òî èç ðåçóëüòàòà Å.Â. Äàøêîâà ñëåäóåò ðàçðåøèìîñòü çà ïîëèíîìèàëüíîå âðåìÿ äèàãðàìì ìîäåëåé (W/∼; ∧, <0 , >, h0i, h1i, . . . , hni, . . .) è(Wn /∼; ∧, <0 , >, h0i, h1i, . . .
, hni).Âëèäèññåðòàöèèäîêàçàíî,÷òî(W/∼; <0 , >, h0i, h1i, . . . , hni, . . .)ïðè âñåõ n≥ýëåìåíòàðíàÿíåðàçðåøèìà.òåîðèÿÄîêàçàíî,ìîäå÷òî3 íåðàçðåøèìû ýëåìåíòàðíûå òåîðèè ìîäåëåé6(Wn /∼; <0 , >, h0i, h1i, . . . , hni). Ïðè ýòîì ïîêàçàíî, ÷òî ýëåìåíòàðíàÿ òåîðèÿ ìîäåëè (W2 /∼; <0 , >, h0i, h1i, h2i) ðàçðåøèìà. Äîêàçàíî,÷òî ÿçûêà ïåðâîãî ïîðÿäêà â ïîëóðåøåòêàõ (W/∼; ∧) è (Wn /∼; ∧)äîñòàòî÷íî äëÿ âûðàæåíèÿ âñåõ ðàññìîòðåííûõ âûøå ïðåäèêàòîâ èôóíêöèé íà òåõ æå íîñèòåëÿõ, è òåì ñàìûì íà ýòè ñòðóêòóðû ïåðåíîñÿòñÿ ðåçóëüòàòû î íåðàçðåøèìîñòè. Íî, áîëåå òîãî, äîêàçàíî, ÷òîíåðàçðåøèìà è ýëåìåíòàðíàÿ òåîðèÿ ìîäåëè (W2 /∼; ∧).Ìåòîäû èññëåäîâàíèÿ. ðàáîòå èñïîëüçóþòñÿ ìåòîäû òåîðèèñëîæíîñòè âû÷èñëåíèé, ìîäàëüíîé ëîãèêè è òåîðèè ìîäåëåé. Äëÿ äîêàçàòåëüñòâà PSPACE-ïîëíîòû çàìêíóòîãî ôðàãìåíòà ëîãèêè GLP ñòðîèòñÿ ïîëèíîìèàëüíîå ñâåäåíèå ÿçûêà áóëåâûõ ôîðìóë ñ êâàíòîðàìèê èñêîìîìó.
Ïîëèíîìèàëüíûå ðàçðåøàþùèå àëãîðèòìû äëÿ çàìêíóòûõ ôðàãìåíòîâ GLPn îñíîâàíû íà ýôôåêòèâíîì êîäèðîâàíèè ïîäìíîæåñòâ ïðåäëîæåííîé Ê.Í. Èãíàòüåâûì [22] óíèâåðñàëüíîé ìîäåëè Êðèïêå äëÿ çàìêíóòîãî ôðàãìåíòà ëîãèêè GLP. Ìû äîêàçûâàåì íåðàçðåøèìîñòü ýëåìåíòàðíûõ òåîðèé ïîëóðåøåòîê GLP-ñëîâ, èíòåðïðåòèðóÿ âíèõ íåðàçðåøèìóþ [18] ñëàáóþ ìîíàäè÷åñêóþ òåîðèþ íàòóðàëüíûõ ÷èñåë â ñèãíàòóðå, âêëþ÷àþùåé â ñåáÿ ôóíêöèþ ñëåäîâàíèÿ è ôóíêöèþH(x) = 2x. Äëÿ äîêàçàòåëüñòâà ðàçðåøèìîñòè ýëåìåíòàðíîé òåîðèè ïîëóðåøåòêè (W1 /∼; ∧) ñòðîèòñÿ åå èíòåðïðåòàöèÿ â òåîðèè ñòðóêòóðû(ω ω ; <, +).
Ðåçóëüòàòû î íåðàçðåøèìîñòè ýëåìåíòàðíûõ òåîðèé ñèñòåìû îðäèíàëüíûõ îáîçíà÷åíèé Áåêëåìèøåâà è åå ôðàãìåíòîâ äîêàçûâàþòñÿ ïóòåì ïîãðóæåíèÿ òåîðèè êëàññà âñåõ ïàð ëèíåéíûõ ïîðÿäêîâ íàêîíå÷íûõ ìíîæåñòâàõ. Ðàçðåøèìîñòü òåîðèè ýëåìåíòàðíîé òåîðèè ìîäåëè (W2 /∼; <0 , >, h0i, h1i, h2i) äîêàçûâàåòñÿ ïðè ïîìîùè ïîñòðîåíèÿ ååèíòåðïðåòàöèè â ñëàáîé ìîíàäè÷åñêîé òåîðèè îðäèíàëà ω ω , ñíàáæåííîãîïîðÿäêîì è ïðåäèêàòîì çàäàþùèì ñòàíäàðòíóþ ñèñòåìó êîôèíàëüíûõïîñëåäîâàòåëüíîñòåé, ðàçðåøèìîñòü êîòîðîé áûëà óñòàíîâëåíà Ë. Áðî[13].7Ñîäåðæàíèå ðàáîòûÃëàâà 1ñîäåðæèò äîêàçàòåëüñòâî PSPACE-ïîëíîòû ïðîáëåìû ðàñïî-çíàâàíèÿ âûâîäèìîñòè äëÿ çàìêíóòîãî ôðàãìåíòà ëîãèêè GLP è äîêàçàòåëüñòâà ïîëèíîìèàëüíîé ðàçðåøèìîñòè ïðîáëåì ðàñïîçíàâàíèÿ âûâîäèìîñòè äëÿ çàìêíóòûõ ôðàãìåíòîâ ëîãèê GLPn .Îñíîâíîé ðåçóëüòàòãëàâû 2ñîñòîèò â äîêàçàòåëüñòâå íåðàç-ðåøèìîñòè ýëåìåíòàðíîé òåîðèè ïîëóðåøåòêè GLP-ñëîâ. Êðîìå òîãî,óñòàíîâëåíî, ÷òî ýëåìåíòàðíàÿ òåîðèÿ ïîëóðåøåòêè GLPn -ñëîâ íåðàçðåøèìà, åñëè è òîëüêî åñëè n ≥ 2.Ãëàâà 3ïîñâÿùåíà èññëåäîâàíèþ ýëåìåíòàðíûõ òåîðèé ñèñòåìîðäèíàëüíûõ îáîçíà÷åíèé íà îñíîâå ëîãèêè GLP.
Характеристики
Тип файла PDF
PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.
Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.















