Автореферат (1104033)
Текст из файла
ÔÃÁÓÍ Ìàòåìàòè÷åñêèé èíñòèòóò èì. Â.À. ÑòåêëîâàÐîññèéñêîé àêàäåìèè íàóêÍà ïðàâàõ ðóêîïèñèÓÄÊ 510.643Ïàõîìîâ Ôåäîð Íèêîëàåâè÷Íåêîòîðûå àëãîðèòìè÷åñêèå âîïðîñûäëÿ ïîëèìîäàëüíûõ ëîãèê äîêàçóåìîñòèÑïåöèàëüíîñòü 01.01.06 ìàòåìàòè÷åñêàÿ ëîãèêà, àëãåáðà è òåîðèÿ ÷èñåëÀÂÒÎÐÅÔÅÐÀÒäèññåðòàöèè íà ñîèñêàíèå ó÷åíîé ñòåïåíèêàíäèäàòà ôèçèêî-ìàòåìàòè÷åñêèõ íàóêÌîñêâà2015Ðàáîòà âûïîëíåíà â îòäåëå ìàòåìàòè÷åñêîé ëîãèêè ÔÃÁÓÍÌàòåìàòè÷åñêèé èíñòèòóò èì. Â.À. Ñòåêëîâà ÐÀÍÍàó÷íûé ðóêîâîäèòåëü:Îôèöèàëüíûå îïïîíåíòû:Áåêëåìèøåâ Ëåâ Äìèòðèåâè÷,÷ëåí-êîðð.
ÐÀÍ,äîêòîð ôèçèêî-ìàòåìàòè÷åñêèõ íàóê,ãëàâíûé íàó÷íûé ñîòðóäíèêîòäåëà ìàòåìàòè÷åñêîé ëîãèêèÔÃÁÓÍ Ìàòåìàòè÷åñêèé èíñòèòóòèì. Â.À. Ñòåêëîâà ÐÀÍ(ñïåöèàëüíîñòü 01.01.06).Âàðäàíÿí Âàëåðèé Àðàìîâè÷,êàíäèäàò ôèçèêî-ìàòåìàòè÷åñêèõ íàóê,ñòàðøèé íàó÷íûé ñîòðóäíèê,ñîâåòíèê äèðåêòîðàÔÃÁÓÍ Âû÷èñëèòåëüíûé öåíòðèì. À.À.
Äîðîäíèöûíà ÐÀÍ(ñïåöèàëüíîñòü 01.01.06);Øåõòìàí Âàëåíòèí Áîðèñîâè÷,äîêòîð ôèçèêî-ìàòåìàòè÷åñêèõ íàóê,ãëàâíûé íàó÷íûé ñîòðóäíèêñåêòîðà 4.1 (Àëãåáðà è òåîðèÿ ÷èñåë)ÔÃÁÓÍ Èíñòèòóò ïðîáëåì ïåðåäà÷èèíôîðìàöèè èì. À.À. Õàðêåâè÷à ÐÀÍ(ñïåöèàëüíîñòü 01.01.06).Âåäóùàÿ îðãàíèçàöèÿ:ÔÃÁÓÍ Èíñòèòóò ìàòåìàòèêèèì. Ñ. Ë.
Ñîáîëåâà ÑÎ ÐÀÍ.Çàùèòà äèññåðòàöèè ñîñòîèòñÿ 22 îêòÿáðÿ 2015 ãîäà â 14 ÷àñîâ 00 ìèíóòíà çàñåäàíèè äèññåðòàöèîííîãî ñîâåòà Ä 002.022.03 ïðè ÌÈÀÍ ïîàäðåñó: ÐÔ, 119991, Ìîñêâà, óë. Ãóáêèíà, ä. 8, êîíôåðåíö-çàë (9 ýòàæ).Ñ äèññåðòàöèåé ìîæíî îçíàêîìèòüñÿ â áèáëèîòåêå ÌÈÀÍ ïî àäðåñó:ÐÔ, 119991, Ìîñêâà, óë. Ãóáêèíà, ä. 8, 8 ýòàæ, à òàêæå íà ñàéòåhttp://www.mi.ras.ru/dis/ref15/pakhomov/pakhomov_dis.pdf.Àâòîðåôåðàò ðàçîñëàí ¾¿ èþëÿ 2015 ãîäà.Ó÷åíûé ñåêðåòàðü äèññåðòàöèîííîãîñîâåòà Ä 002.022.03 ïðè ÌÈÀÍ,äîêòîð ôèçèêî-ìàòåìàòè÷åñêèõ íàóêÈ.Ä. ØêðåäîâÎáùàÿ õàðàêòåðèñòèêà ðàáîòûÄèññåðòàöèÿ ïîñâÿùåíà èçó÷åíèþ ïîíÿòèÿ äîêàçóåìîñòè ñðåäñòâàìè ìîäàëüíîé ëîãèêè.  äèññåðòàöèè èññëåäóþòñÿ àëãîðèòìè÷åñêèå ñâîéñòâàïîëèìîäàëüíîé ëîãèêè äîêàçóåìîñòè Äæàïàðèäçå è åå ôðàãìåíòîâ.Àêòóàëüíîñòü òåìû.
Èäåÿ èçó÷åíèÿ ñâîéñòâ äîêàçóåìîñòè ñðåäñòâàìè ìîäàëüíûõ ëîãèê âîñõîäèò ê Ê. Ãåäåëþ1 . Ê. Ãåäåëü ïðåäëîæèë èíòåðïðåòèðîâàòü ñâÿçêó ìîäàëüíîñòè êàê àðèôìåòè÷åñêóþ ôîðìóëóT,âûðàæàþùóþ äîêàçóåìîñòü â äàííîé ôîðìàëüíîé òåîðèè T.Ëîãèêà Ãåäåëÿ-Ëåáà GL ôîðìàëèçóåòñÿ â ÿçûêå èñ÷èñëåíèÿ âûñêàçûâàíèé, îáîãàùåííîì ñâÿçêîé , è ïîëó÷àåòñÿ äîáàâëåíèåì ê àêñèîìàì èïðàâèëàì âûâîäà èñ÷èñëåíèÿ âûñêàçûâàíèé ñëåäóþùèõ àêñèîì è ïðàâèëâûâîäà:Pr1. (ϕ → ψ) → (ϕ → ψ);2.
(ϕ → ϕ) → ϕ (àêñèîìà Ëåáà);3.ϕ.ϕÈç ðåçóëüòàòîâ Ê. Ãåäåëÿ è Ì.Õ. Ëåáà2 âûòåêàåò, ÷òî äëÿ ïåðå÷èñëèìûõòåîðèé T, ñîäåðæàùèõ ïåðâîïîðÿäêîâóþ àðèôìåòèêó Ïåàíî PA, ëþáàÿòåîðåìà ìîäàëüíîé ëîãèêè GL âûðàæàåò ñâîéñòâî äîêàçóåìîñòè â T, êîòîðîå ìîæíî îáîñíîâàòü ñðåäñòâàìè ñàìîé òåîðèè T. 1976 ãîäó Ð.Ì. Ñîëîâåé3 äîêàçàë òåîðåìó îá àðèôìåòè÷åñêîé ïîëíîòå ëîãèêè GL. Ìîäàëüíàÿ ôîðìóëà ÿâëÿåòñÿ òåîðåìîé ëîãèêè GL, åñëè è òîëüêî åñëè îíà ïåðåâîäèòñÿ â òåîðåìó PA ïðè ëþáîé ïîäñòàíîâêåàðèôìåòè÷åñêèõ ïðåäëîæåíèé âìåñòî ïðîïîçèöèîíàëüíûõ ïåðåìåííûõ èðàñøèôðîâêå êàê PA .Ñ ñåðåäèíû 1970-õ ãîäîâ èññëåäîâàíèþ ëîãèêè GL è äðóãèõ ëîãèê äîêàçóåìîñòè áûëî ïîñâÿùåíî çíà÷èòåëüíîå ÷èñëî ðàáîò.
 1986 ã. Ã.Ê. Äæàïàðèäçå ðàññìîòðåë4 îáîáùåíèå GL ëîãèêó GLP, â êîòîðîé âìåñòîîäíîé ìîäàëüíîé ñâÿçêè èñïîëüçóåòñÿ çàíóìåðîâàííîå íàòóðàëüíûìèPr1 K. Godel. Eine Interpretation des intuitionistischen Aussagenkalkuls. Ergebnisse einesmathematischen Kolloquiums, 4: 3940, 1933. English translation, with an introductorynote by A.S. Troelstra. Kurt Godel, Collected Works, 1:296303, 1986.2 M.H. Lob. Solution of a problem of Leon Henkin. The Journal of Symbolic Logic,20(02):115118, 1955.3 R.M. Solovay.
Provability interpretations of modal logic. Israel Journal of Mathematics,25(3-4):287304, 1976.4 Ã.Ê. Äæàïàðèäçå. Ìîäàëüíî-ëîãè÷åñêèå ñðåäñòâà èññëåäîâàíèÿ äîêàçóåìîñòè.Äèññ. êàíä. ôèëîñ. íàóê, Ìîñêâà, ÌÃÓ, 1986.1n÷èñëàìè ñåìåéñòâî ìîäàëüíûõ ñâÿçîê [0], [1], . . . , [ ], . . . Ã.Ê.
Äæàïàðèäçåäîêàçàë àíàëîã òåîðåìû Ñîëîâåÿ îá àðèôìåòè÷åñêîé ïîëíîòå, â êîòîðîìêàæäàÿ ñâÿçêà [ ] èíòåðïðåòèðóåòñÿ êàê äîêàçóåìîñòü èç àêñèîì PA ñ èñïîëüçîâàíèåì âûâîäîâ ñ ω -ïðàâèëàìè c ãëóáèíîé âëîæåííîñòè ω -ïðàâèë,íå ïðåâîñõîäÿùåé . íàñòîÿùåå âðåìÿ ëîãèêà GLP àêòèâíî èçó÷àåòñÿ â ñâÿçè ñ åå ïðèìåíåíèÿìè â îðäèíàëüíîì àíàëèçå àðèôìåòè÷åñêèõ òåîðèé5 . Âîïðîñ îõàðàêòåðèçàöèè ôîðìàëüíûõ òåîðèé îðäèíàëàìè ÿâëÿåòñÿ îäíèì èç öåíòðàëüíûõ âîïðîñîâ â òåîðèè äîêàçàòåëüñòâ.
Èññëåäîâàíèÿ òàêîãî ðîäàâîñõîäÿò ê Ã. Ãåíöåíó6 , êîòîðûé äîêàçàë íåïðîòèâîðå÷èâîñòü PA ñ ïîωω ···ìîùüþ òðàíñôèíèòíîé èíäóêöèè äî îðäèíàëà ε0 = sup{ω| {z } | ∈ ω}.nnn ðàçnÏðèìåíåíèå ëîãèêè GLP îñíîâàíî íà èñïîëüçîâàíèè çàìêíóòûõ ôîðìóë(ôîðìóë áåç ïðîïîçèöèîíàëüíûõ ïåðåìåííûõ) äëÿ îáîçíà÷åíèÿ àðèôìåòè÷åñêèõ òåîðèé è äëÿ ïîñòðîåíèÿ åñòåñòâåííîé ñèñòåìû îðäèíàëüíûõîáîçíà÷åíèé äëÿ îðäèíàëà ε0 . äèññåðòàöèè ðàññìàòðèâàþòñÿ äâà êðóãà àëãîðèòìè÷åñêèõ âîïðîñîâ,ñâÿçàííûõ ñ çàìêíóòûì ôðàãìåíòîì ëîãèêè GLP.1.
Àëãîðèòìè÷åñêàÿ ñëîæíîñòü ïðîáëåìû ðàñïîçíàâàíèÿ âûâîäèìîñòèäëÿ çàìêíóòûõ ôîðìóë.2. Ðàçðåøèìîñòü ýëåìåíòàðíûõ òåîðèé àëãåáð åñòåñòâåííûõ ñèñòåì îðäèíàëüíûõ îáîçíà÷åíèé.Âîïðîñ îá àëãîðèòìè÷åñêîé ñëîæíîñòè ïðîáëåìû âûâîäèìîñòè äëÿìîäàëüíûõ ëîãèê èçó÷àëñÿ Ð.Ý. Ëàäíåðîì7 . Îí ïîêàçàë, ÷òî ìíîãèåêëàññè÷åñêèå ìîäàëüíûå ëîãèêè, âêëþ÷àÿ S4, K, T, îáëàäàþò PSPACEïîëíûìè ïðîáëåìàìè ðàñïîçíàâàíèÿ âûâîäèìîñòè ôîðìóë. Õîòÿ ëîãèêàGL íå áûëà ðàññìîòðåíà â ýòîé ðàáîòå Ð.Ý. Ëàäíåðà, èñïîëüçîâàííûéòàì ìåòîä ëåãêî ïîçâîëÿåò ïîëó÷èòü àíàëîãè÷íûé ðåçóëüòàò è äëÿ íåå. äàëüíåéøåì, È.Á. Øàïèðîâñêèé äîêàçàë, ÷òî è ëîãèêà GLP îáëàäàåòPSPACE-ïîëíîé ïðîáëåìîé ðàñïîçíàâàíèÿ âûâîäèìîñòè8 .5 L.D.
Beklemishev. Provability algebras and proof-theoretic ordinals, I. Annals of Pureand Applied Logic, 128:103123, 2004.6 G. Gentzen. Die Widerspruchsfreiheit der reinen Zahlentheorie. MathematischeAnnalen, 112:493565, 1936.7 R.E. Ladner. The computational complexity of provability in systems of modalpropositional logic. SIAM Journal on Computing, 6(3):467480, 1977.8 I.B. Shapirovsky. PSPACE-decidability of Japaridze's polymodal logic. In Advances inModal Logic 2008, pages 289304, 2008.2À.Â. ×àãðîâûì è Ì.Í. Ðûáàêîâûì ðàññìàòðèâàëèñü ôðàãìåíòû ìîäàëüíûõ ëîãèê ñ îãðàíè÷åíèåì íà ÷èñëî ðàçëè÷íûõ ïðîïîçèöèîíàëüíûõïåðåìåííûõ â ôîðìóëàõ è âîïðîñ îá àëãîðèòìè÷åñêîé ñëîæíîñòè äëÿ ýòèõôðàãìåíòîâ9 .
Èìè áûëî ïîêàçàíî, ÷òî äàæå ôðàãìåíò ëîãèêè GL ñ îäíîé ïðîïîçèöèîíàëüíîé ïåðåìåííîé ÿâëÿåòñÿ PSPACE-ïîëíûì; òàì æåáûëè ïîëó÷åíû àíàëîãè÷íûå ðåçóëüòàòû äëÿ ëîãèê S4 è Grz. Ïðè ýòîìîíè ïîêàçàëè, ÷òî çàìêíóòûé ôðàãìåíò ëîãèêè GL ðàçðåøèì çà ïîëèíîìèàëüíîå âðåìÿ.  òî æå âðåìÿ çàìêíóòûå ôðàãìåíòû ëîãèê K4 è Kÿâëÿþòñÿ PSPACE-ïîëíûìè. Òàêæå Ô. Áîó è É. Éîîñòåí äîêàçàëè, ÷òîçàìêíóòûé ôðàãìåíò ëîãèêè èíòåðïðåòèðóåìîñòè IL, ðàñøèðÿþùåé GL,ÿâëÿåòñÿ PSPACE-òðóäíûì10 . äèññåðòàöèè äîêàçàíà PSPACE-ïîëíîòà çàìêíóòîãî ôðàãìåíòà ëîãèêè GLP.Ìû îáîçíà÷àåì ÷åðåç GLPn ôðàãìåíò ëîãèêè GLP ñ ìîäàëüíîñòÿìè[0], [1], .
. . , [ ]. Äîêàçàíî, ÷òî äëÿ âñÿêîãî íàòóðàëüíîãî çàìêíóòûé ôðàãìåíò ëîãèêè GLPn ðàçðåøèì çà ïîëèíîìèàëüíîå âðåìÿ.Ïåðåéäåì ê âîïðîñàì ðàçðåøèìîñòè ýëåìåíòàðíûõ òåîðèé àëãåáð, ñâÿçàííûõ ñ êîíñòðóêòèâíûìè ñèñòåìàìè îðäèíàëüíûõ îáîçíà÷åíèé. Íàèáîëåå èçâåñòíîé ñèñòåìîé îáîçíà÷åíèé äëÿ îðäèíàëà ε0 ÿâëÿåòñÿ òàê íàçûâàåìàÿ êàíòîðîâñêàÿ ñèñòåìà. Îáîçíà÷åíèÿìè äëÿ îðäèíàëîâ â ýòîé ñèñòåìå ÿâëÿþòñÿ çàìêíóòûå òåðìû, ñîñòàâëåííûå èç êîíñòàíòû 0, ôóíêöèè+ è ôóíêöèè f : x 7−→ ω x . Êàíòîðîâñêàÿ ñèñòåìà ñîîòâåòñòâóåò àëãåáðå(ε0 ; <, 0, +, f ); çàìåòèì, ÷òî â ýòîé àëãåáðå âñÿêèé îðäèíàë ìåíüøèé ε0 ðàâåí çíà÷åíèþ íåêîòîðîãî çàìêíóòîãî òåðìà.
Èçâåñòíî, ÷òî ýëåìåíòàðíàÿòåîðèÿ ìîäåëè (ε0 ; <, 0, +, f ) ÿâëÿåòñÿ àëãîðèòìè÷åñêè íåðàçðåøèìîé.Åñòåñòâåííûé, ñâÿçàííûé ñ îðäèíàëüíûì àíàëèçîì ñïîñîá îáîçíà÷åíèÿ îðäèíàëîâ íà îñíîâå çàìêíóòîãî ôðàãìåíòà ëîãèêè GLP áûë ïðåäëîæåí Ë.Ä. Áåêëåìèøåâûì â åãî óêàçàííîé âûøå ðàáîòå5 . Îðäèíàëû îáîçíà÷àþòñÿ ôîðìóëàìè âèäà h 1 ih 1 i .
. . h k i>, íàçûâàåìûìè ñëîâàìè. Ìûîáîçíà÷àåì ìíîæåñòâî âñåõ ñëîâ . Áèíàðíîå îòíîøåíèå <0 íà ñëîâàõ ñîîòâåòñòâóåò ïîðÿäêó íà îðäèíàëàõ:nnn nWndefA <0 B ⇐⇒ GLP ` A → h0iB.Îòíîøåíèåäîêàçóåìîéðàâåíñòâà îðäèíàëîâ ñîîòâåòñòâóåò îòíîøåíèþýêâèâàëåíòíîñòè ñëîâ ∼. Ïîëíîé ñèñòåìåGLPîðäè-9 A.V. Chagrov and M.N. Rybakov. How many variables does one need to prove PSPACEhardness of modal logics? In Advances in Modal Logic 2002, pages 7182. King's CollegePublications, 2003.10 F. Bou and J.J.
Joosten. The closed fragment of IL is PSPACE hard. Electronic Notesin Theoretical Computer Science, 278:4754, 2011.3íàëüíûõ îáîçíà÷åíèé äëÿ îðäèíàëà ε0 ñîîòâåòñòâóåò àëãåáðà( /∼; <0 , >, h0i, h1i, . . . , h i, . . .). Òàêæå ìû ðàññìàòðèâàåì ðÿä åñòåñòâåííûõ ôðàãìåíòîâ ýòîé ñèñòåìû îðäèíàëüíûõ îáîçíà÷åíèé.
Îáîçíà÷èì÷åðåç n ìíîæåñòâî âñåõ ñëîâ ñîñòàâëåííûõ èç > è h0i, . . . , h i; ìû íàçûâàåì òàêèå ñëîâà GLPn -ñëîâàìè. Ìîäåëü ( n /∼; <0 , >, h0i, h1i, . . . , h i)ÿâëÿåòñÿ ñèñòåìîé îðäèíàëüíûõ îáîçíà÷åíèé äëÿ îðäèíàëîâ ωn+1 ; çäåñüWnWnWω0 = 1,nωn+1 = ω ωn .Îòìåòèì, ÷òî â óêàçàííîé âûøå ðàáîòå5 Ë.Ä. Áåêëåìèøåâà áûëî ïîêàçàíî, ÷òî êîíúþíêöèÿ âñÿêèõ äâóõ ñëîâ GLP-äîêàçóåìî ýêâèâàëåíòíàíåêîòîðîìó GLP-ñëîâó. Ýòî äàåò âîçìîæíîñòü åñòåñòâåííûì îáðàçîì ðàññìàòðèâàòü ïîëóðåøåòêè ( /∼; ∧) è ( n /∼; ∧).Å.Â. Äàøêîâ11 ðàññìîòðåë ôðàãìåíò ëîãèêè GLP, ñîñòîÿùèé èç èìïëèêàöèé ìåæäó ñòðîãî ïîçèòèâíûìè ôîðìóëàìè, òî åñòü ìåæäó ôîðìóëàìè ïîñòðîåííûìè èç ïåðåìåííûõ, ∧, > è h0i, h1i, .
Характеристики
Тип файла PDF
PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.
Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
