Диссертация (1104034), страница 2
Текст из файла (страница 2)
Äîêàçàíî, ÷òî àëãåáðà ñîîòâåòñòâóþùàÿ ïîëíîé ñèñòåìå îðäèíàëüíûõ îáîçíà÷åíèé äëÿ îðäèíàëà ε0 îáëàäàåò íåðàçðåøèìîé ýëåìåíòàðíîé òåîðèåé. Òàêæå â ãëàâå3 äîêàçûâàåòñÿ, ÷òî ýëåìåíòàðíàÿ òåîðèÿ àëãåáðû, ñîîòâåòñòâóþùåé ñèñòåìå îðäèíàëüíûõ îáîçíà÷åíèé, ïîðîæäàåìîé h0i, . . . , hni, íåðàçðåøèìà ïðè n ≥ 3 è ðàçðåøèìà ïðè n = 2.ßçûê ïîëèìîäàëüíîé ëîãèêè äîêàçóåìîñòè GLP ýòî ÿçûê èñ÷èñëåíèÿ âûñêàçûâàíèé ñ ïðîïîçèöèîíàëüíûìè êîíñòàíòàìè ¾èñòèíà¿> è ¾ëîæü¿ ⊥, îáîãàùåííûé óíàðíûìè ñâÿçêàìè [0], [1], . . ..
Çàïèñü hniϕÿâëÿåòñÿ ñîêðàùåíèåì äëÿ ¬[n]¬ϕ. GLP çàäàåòñÿ ñëåäóþùèìè àêñèîìàìè è ïðàâèëàìè âûâîäà:0. Àêñèîìû è ïðàâèëà âûâîäà ëîãèêè GL äëÿ êàæäîé ñâÿçêè [n];1. [k]ϕ → [n]ϕ, ãäå k ≤ n;2. hkiϕ → [n]hkiϕ, ãäå k < n.Ìû îáîçíà÷àåì ÷åðåç GLPn ëîãèêó, ÿçûê êîòîðîé ïîëó÷àåòñÿ èçÿçûêà ïðîïîçèöèîíàëüíîé ëîãèêè îáîãàùåíèåì ñâÿçêàìè [0], . . . , [n], àòåîðåìàìè ÿâëÿþòñÿ âñå òåîðåìû GLP â ýòîì ÿçûêå. ãëàâå 1 äîêàçûâàåòñÿ8Òåîðåìà 1.Ïðîáëåìà ðàñïîçíàâàíèÿ âûâîäèìîñòè çàìêíóòûõ ôîðìóëâ ëîãèêå GLP ÿâëÿåòñÿ PSPACE-ïîëíîé.Äàëåå â ýòîé ãëàâå äîêàçûâàåòñÿ, ÷òî íàëè÷èå áåñêîíå÷íîãî ÷èñëà ðàçëè÷íûõ ìîäàëüíûõ ñâÿçîê â ÿçûêå íåîáõîäèìî äëÿ ïîëó÷åíèÿPSPACE-ïîëíîòû.Òåîðåìà 2.Ïðè âñåõ n ïðîáëåìà ðàñïîçíàâàíèÿ âûâîäèìîñòè çàìêíó-òûõ ôîðìóë â ëîãèêå GLPn ðàçðåøèìà çà ïîëèíîìèàëüíîå âðåìÿ.Äëÿ äîêàçàòåëüñòâà ïîñëåäíåé òåîðåìû ìû ðàññìàòðèâàåì óíèâåðñàëüíóþ ìîäåëü Êðèïêå äëÿ çàìêíóòîãî ôðàãìåíòà ëîãèêè GLP.Ïîëèíîìèàëüíûé àëãîðèòì îñíîâûâàåòñÿ íà ýôôåêòèâíîì çàäàíèå ïîäìíîæåñòâ ýòîé ìîäåëè, îïðåäåëèìûõ çàìêíóòûìè GLPn -ôîðìóëàìè.Îäíèì èç öåíòðàëüíûì äëÿ ãëàâ 2 è 3 ïîíÿòèåì ÿâëÿåòñÿ ïîíÿòèå GLP-ñëîâà.
Ðàññìàòðèâàåòñÿ ìíîæåñòâî W âñåõ ôîðìóë âèäàhn1 ihn2 i . . . hnk i>. Òàêèå ôîðìóëû íàçûâàþòñÿ GLP-ñëîâàìè òàêæå äëÿêðàòêîñòè â ðàìêàõ äàííîé äèññåðòàöèè ìû íàçûâàåì èõ ïðîñòî ñëîâàìè. Äëÿ îáîçíà÷åíèÿ ñëîâ ìû èñïîëüçóåì áóêâû A, B, . . ..Íà ìíîæåñòâå âñåõ GLP-ôîðìóë îïðåäåëèì áèíàðíûå îòíîøåíèÿ<n :defϕ <n ψ ⇐⇒ GLP ` ψ → hniϕ.Ìû îáîçíà÷àåì ÷åðåç ∼ îòíîøåíèå GLP-äîêàçóåìîé ýêâèâàëåíòíîñòè íà ôîðìóëàõ è, â ÷àñòíîñòè, íà ñëîâàõ:defϕ ∼ ψ ⇐⇒ GLP ` ϕ ↔ ψ.Êàê áûëî îòìå÷åíî âûøå, êîíúþíêöèÿ äâóõ ñëîâ â GLP ýêâèâàëåíòíà íåêîòîðîìó ñëîâó. Òåì ñàìûì, ñâÿçêè hni è ∧ åñòåñòâåííûìîáðàçîì çàäàþò ôóíêöèè íà êëàññàõ ýêâèâàëåíòíîñòè ñëîâ:hni[A]∼ = {B | B ∼ hniA},[A]∼ ∧ [B]∼ = {C | C ∼ A ∧ B}.9Âãëàâàõòàðíûõ2òåîðèéè3ìûèçó÷àåìðàçðåøèìîñòüýëåìåí-(W/∼; ∧, <0 , >, h0i, h1i, .
. . , hki, . . .),ìîäåëåé(Wn /∼; ∧, <0 , >, h0i, h1i, . . . , hni) è ìîäåëåé, ïîëó÷àåìûõ èç íèõ îïóñêàíèåì íåêîòîðûõ ïðåäèêàòîâ è ôóíêöèé. Îòìåòèì, ÷òî ôàêòè÷åñêè èçñîîáðàæåíèé òåõíè÷åñêîãî óäîáñòâà ìû ðàáîòàåì íå íåïîñðåäñòâåííîñ ýòèìè ìîäåëÿìè, à ñ èçîìîðôíûìè ìîäåëÿìè, íîñèòåëè êîòîðûõñîñòàâëåíû èç ñëîâ â íîðìàëüíîé ôîðìå (êàíîíè÷åñêèõ ïðåäñòàâèòåëåéêëàññîâ ýêâèâàëåíòíîñòè GLP-ñëîâ ïî îòíîøåíèþ ∼).Îñíîâíîé ðåçóëüòàò ãëàâû 2, â êîòîðîé ìû èçó÷àåì ýëåìåíòàðíûåòåîðèè ïîëóðåøåòîê óêàçàííîãî âûøå âèäà, ñîñòîèò â ñëåäóþùåì.Òåîðåìà 3.Ýëåìåíòàðíàÿ òåîðèÿ íèæíåé ïîëóðåøåòêè (W/∼; ∧)íåðàçðåøèìà. Ïðè âñåõ n ≥ 2 íåðàçðåøèìû ýëåìåíòàðíûå òåîðèè ïîëóðåøåòîê (Wn /∼; ∧).Îòìåòèì, ÷òî ïðè äîêàçàòåëüñòâå ýòîé òåîðåìû ìû óñòàíàâëèâàåì, ÷òî â (W/∼; ∧) ôîðìóëàìè ïåðâîãî ïîðÿäêà âûðàçèìû âñå áèíàðíûåîòíîøåíèÿ <k è âñå ôóíêöèè hki.
Áîëåå òîãî ìû äîêàçûâàåì, ÷òî äëÿâñåõ íàòóðàëüíûõ n â (Wn /∼; ∧) ôîðìóëàìè ïåðâîãî ïîðÿäêà âûðàçèìûâñå áèíàðíûå îòíîøåíèÿ <k è âñå ôóíêöèè hki ïðè k ≤ n.Òåîðåìà 4.Ýëåìåíòàðíàÿ òåîðèÿ íèæíåé ïîëóðåøåòêè (W1 /∼; ∧)ðàçðåøèìà. ãëàâå 3 ìû èçó÷àåì âîïðîñ îá ðàçðåøèìîñòè ýëåìåíòàðíûõ òåîðèé ìîäåëåé ñ íîñèòåëÿìè W/∼ èëè Wn /∼ è ñèãíàòóðå ìîãóùåé âêëþ÷àòü ëèøü ïðåäèêàò <0 , êîíñòàíòó > è ôóíêöèè hki. Îòìåòèì, ÷òî ìîäåëü (W/∼; <0 , >, h0i, h1i, . . . , hki, . . .) è (Wn /∼; <0 , h0i, h1i, . .
. , hni) ÿâëÿþòñÿ åñòåñòâåííûìè êîíñòðóêòèâíûìè ïðåäñòàâëåíèÿìè îðäèíàëîâ ε0è ωn+1 , ñîîòâåòñòâåííî.Òåîðåìà 5.Ïóñòü p, q è n íàòóðàëüíûå ÷èñëà òàêèå, ÷òî 0 < p èp + 1 < q ≤ n. Òîãäà ýëåìåíòàðíûå òåîðèè ìîäåëåé (W/∼; <0 , hpi, hqi)è (Wn /∼; <0 , hpi, hqi) íåðàçðåøèìû.10Ìîäåëü (W/∼; <0 , >, h0i, h1i, . . . , hki, . . .), â ñèëó òåîðåìû 5, èìååò íåðàçðåøèìóþ ýëåìåíòàðíóþ òåîðèþ.
Òàêæå, èç ýòîé òåîðåìû ñëåäóåò, ÷òî ïðè âñåõ n ≥ 3 íåðàçðåøèìà ýëåìåíòàðíàÿ òåîðèÿ ìîäåëè(Wn /∼; <0 , >, h0i, h1i, . . . , hni).Êðîìå òîãî ìû óñòàíàâëèâàåì ñëåäóùèå òåîðåìû.Òåîðåìà 6.Äëÿ ìîäåëè (Wn /∼; <0 , >, h0i, h1i, h2i) ýëåìåíòàðíàÿ òåî-ðèÿ ðàçðåøèìà ïðè âñåõ n ≥ 2.Òåîðåìà 7.Ýëåìåíòàðíàÿ òåîðèÿ ìîäåëè (W/∼; <0 , >, h0i, h1i, h2i)ðàçðåøèìà. Ïðè âñåõ n≥2 ýëåìåíòàðíàÿ òåîðèÿ ìîäåëè(Wn /∼; <0 , >, h0i, h1i, h2i) ðàçðåøèìà.Äëÿ äîêàçàòåëüñòâà òåîðåìû 7 ìû ïîêàçûâàåì, ÷òî âñåñòðóêòóðû (Wn /∼; <0 , >, h0i, h1i, h2i), ãäå n≥3, è ñòðóêòóðà(W/∼; <0 , >, h0i, h1i, h2i) ïîïàðíî ýëåìåíòàðíî ýêâèâèâàëåíòû, à äàëååïðèìåíÿåì òåîðåìó 6.ß âûðàæàþ ãëóáîêóþ áëàãîäàðíîñòü ñâîåìó íàó÷íîìó ðóêîâîäèòåëþ ÷ëåíó-êîððåñïîíäåíòó ÐÀÍ Ë.Ä.
Áåêëåìèøåâó çà ïîñòàíîâêó çàäà÷ è ïîääåðæêó â ðàáîòå. ß áëàãîäàðþ ó÷àñòíèêîâ ñåìèíàðîâ ¾Ëîãè÷åñêèå ïðîáëåìû èíôîðìàòèêè¿ è ¾Àëãîðèòìè÷åñêèå ïðîáëåìû àëãåáðûè ëîãèêè¿ çà êîíñòðóêòèâíîå îáñóæäåíèå. Êðîìå òîãî, ÿ áëàãîäàðþ çàïîëåçíûå çàìå÷àíèÿ àíîíèìíûõ ðåöåíçåíòîâ ñâîèõ ñòàòåé ïî òåìå äèññåðòàöèè.11Ãëàâà 1Àëãîðèòìè÷åñêàÿ ñëîæíîñòüçàìêíóòûõ ôðàãìåíòîâ1.1ËîãèêàËîãèêàGLPè åå çàìêíóòûé ôðàãìåíòGLP.Ñîâîêóïíîñòü âñåõ ïðàâèëüíî ïîñòðîåííûõ GLP-ôîðìóë ïîðîæäàåòñÿïðîïîçèöèîíàëüíûìè ïåðåìåííûìè x1 , x2 , . . . , xn , . .
., äâóìåñòíûìè ïðîïîçèöèîíàëüíûìè ñâÿçêàìè ∧, ∨, →, îäíîìåñòíîé ïðîïîçèöèîíàëüíîéñâÿçêîé ¬, ïðîïîçèöèîíàëüíûìè êîíñòàíòàìè > (èñòèíà), ⊥ (ëîæü) èóíàðíûìè ìîäàëüíûìè ñâÿçêàìè [0], [1], . . . , [n], . . . Ìû ââîäèì ñâÿçêèhni ñëåäóþùèì îáðàçîì:hniϕ ¬[n]¬ϕ.Ëîãèêà GLP çàäàåòñÿ ñëåäóþùèìè ñõåìàìè àêñèîì è ïðàâèëàìèâûâîäà:1. Ñõåìû àêñèîì èñ÷èñëåíèÿ âûñêàçûâàíèé â ðàñøèðåííîì ÿçûêå;2. [n](ϕ → ψ) → ([n]ϕ → [n]ψ);3. [n]([n]ϕ → ϕ) → [n]ϕ;4.
[k]ϕ → [n]ϕ, ãäå k ≤ n;5. hkiϕ → [n]hkiϕ, ãäå k < n;6.ϕ7.ϕ.[n]ϕϕ→ψ;ψ12Ìû íàçûâàåì GLP-ôîðìóëó çàìêíóòîé, åñëè â íåé íå ñîäåðæàòñÿïðîïîçèöèîíàëüíûå ïåðåìåííûå. ýòîì ðàçäåëå ìû äîêàçûâàåì ñëåäóþùóþ òåîðåìó.Òåîðåìà 1.Ïðîáëåìà ðàñïîçíàâàíèÿ âûâîäèìîñòè â ëîãèêå GLP äëÿçàìêíóòûõ ôîðìóë ÿâëÿåòñÿ PSPACE-ïîëíîé.Èç òåîðåìû Øàïèðîâñêîãî [26] î PSPACE-ïîëíîòå ïðîáëåìû ðàñïîçíàâàíèÿ âûâîäèìîñòè â ëîãèêå GLP ñëåäóåò ïðèíàäëåæíîñòü ïðîáëåìû èç òåîðåìû 1 ê êëàññó PSPACE.  ñèëó ýòîãî, äëÿ äîêàçàòåëüñòâà òåîðåìû 1 äîñòàòî÷íî ïîêàçàòü, ÷òî ïðîáëåìà ÿâëÿåòñÿ PSPACE-òðóäíîé.Îáîçíà÷èì ÷åðåç QBF ïðîáëåìó ðàñïîçíàâàíèÿ èñòèííîñòè áóëåâûõ ôîðìóë ñ êâàíòîðàìè.
Èçâåñòíî, ÷òî QBF ÿâëÿåòñÿ PSPACE-ïîëíîé[28]. Äëÿ äîêàçàòåëüñòâà PSPACE-ñëîæíîñòè ïðîáëåìû ðàñïîçíàâàíèÿâûâîäèìîñòè â GLP çàìêíóòûõ ôîðìóë ìû ñòðîèì ïîëèíîìèàëüíóþðåäóêöèþ ïðîáëåìû QBF ê äàííîé.Ïóñòü èìåþòñÿ ôîðìóëûQ0x0Q1x1 . . . Qn−1xn−1ϕ(x0, . . . , xn−1),ãäåQi ∈ {∀, ∃}, à ϕ(x0, . . . , xn−1) áóëåâà ôîðìóëà, ïåðåìåííûå÷ âõîäÿ-ùèå â êîòîðóþ èñ÷åðïûâàþòñÿ íàáîðîì x0 , . . . , xn−1 . Ìû ïîñòðîèì ïîëèìîäàëüíûå ôîðìóëû η0 è ψ0 òàêèå, ÷òî áóëåâà ôîðìóëà ñ êâàíòîðàìèQ0x0Q1x1 . .
. Qn−1xn−1ϕ(x0, . . . , xn−1)èñòèííà, åñëè è òîëüêî åñëèGLP ` η0 ↔ ψ0 .Îòìåòèì, ÷òî â ÿçûêå GLP íåò ñâÿçêè ↔, è ìû âûðàæàåì åå ñ ïîìîùüþñâÿçîê ∧ è →. Êðàòêî îïèøåì èäåþ ïîñòðîåíèÿ ôîðìóëû ψ0 .1. Ìû íà÷èíàåì ñî ñïåöèàëüíî ïîäîáðàííûõ, ïîëíîñòüþ ëîãè÷åñêèíåçàâèñèìûõ ôîðìóë θ0 , . . . , θn−1 , ò.å. òàêèõ ôîðìóë, ÷òî äëÿ âñÿêîéôîðìóëû ξ(x0 , . . . , xn−1 ) ÿçûêà èñ÷èñëåíèÿ âûñêàçûâàíèé ξ ÿâëÿåòñÿòàâòîëîãåé åñëè è òîëüêî åñëè GLP ` ξ[θ0 , . . .
, θn−1 /x0 , . . . , xn−1 ].132. Äàëåå ìû ðàññìàòðèâàåì ôîðìóëóψn ϕ[θ0 , . . . , θn−1 /x0 , . . . , xn−1 ].Îòìåòèì, ÷òî åñëè áû íàøåé ïðîáëåìîé áûëî ñâåäåíèå ïðîáëåìûðàñïîçíàâàíèÿ äîêàçóåìîñòè ôîðìóë â èñ÷èñëåíèè âûñêàçûâàíèé êïðîáëåìå ðàñïîçíàâàíèÿ äîêàçóåìîñòè çàìêíóòûõ ôîðìóë â ëîãèêåGLP, òî ïðîäåëàííîãî áûëî áû äîñòàòî÷íî.3. Íàøà öåëü ñîñòîèò â ïîñòðîåíèè ôîðìóë ψ0 , . .
. , ψn−1 . Äëÿ êàæäîãîi îò 1 äî n ôîðìóëà ψi , â íåêîòîðîì ñìûñëå, ïðåäñòàâëÿåò ôîðìóëóQixi . . . Qn−1xn−1ϕ(x0, . . . , xi−1, xi, . . . , xn−1) ñ x0, . . . , xi−1 çàìåíåííûìèíà θ0 , . . . , θi−1 ñîîòâåòñòâåííî.4. Ìû ïîëó÷àåì ôîðìóëó ψi êàê ξ[ψi+1 /x], ãäå ξ ýòî íåêîòîðàÿ êîðîòêàÿ ôîðìóëà. Êîíêðåòíûé âèä ξ çàâèñèò îò òîãî, êàêèì èìåííîêâàíòîðîì ÿâëÿåòñÿQi, à òàêæå ÷èñåë n è i. Êðîìå òîãî, x ÿâëÿåòñÿåäèíñòâåííîé ïåðåìåííîé â ξ , ïðè ýòîì x âñòðå÷àåòñÿ â ξ ðîâíî îäèíðàç è ïðè ýòîì ïîçèòèâíî.5. Îêàçûâàåòñÿ, ÷òî èìååò ìåñòî ðîâíî îäíà èç äâóõ àëüòåðíàòèâ:(a) ôîðìóëà ψ0 ÿâëÿåòñÿ GLP-îïðîâåðæèìîé (ò.å. GLP ` ¬ψ0 ) èQ0x0Q1x1 .
. . Qn−1xn−1ϕ(x0, . . . , xn−1)ëîæíà,(b) ôîðìóëà ψ0 îêàçûâàåòñÿ GLP-äîêàçóåìî ýêâèâàëåíòíîé ñïåöèàëüíîé ôîðìóëå η0 èQ0x0Q1x1 . . . Qn−1xn−1ϕ(x0, . . . , xn−1)èñòèííà.Ìû îïðåäåëÿåì ñëåäóþùèå ôîðìóëû1. ηn >;2. ηi h2iih4n − 2i − 1i> äëÿ 0 ≤ i < n;3. θi h2i + 1ih4n − 2i − 2i> äëÿ 0 ≤ i < n;144.
ψn ϕ[θ0 , . . . , θn−1 /x0 , . . . , xn−1 ];5. ψi h2iih4n − 2i − 1ih2iiψi+1 äëÿ 0 ≤ i < n, â ñëó÷àåQi = ∃.6. ψi ηi ∧ ¬h2iih4n − 2i − 1ih2ii(ηi+1 ∧ ¬ψi+1 ) äëÿ 0 ≤ i < n, â ñëó÷àåQi = ∀.Äëÿ âñÿêîé ôîðìóëû ξ ïîëîæèì ξ > ξ è ξ ⊥ ¬ξ .Äëÿ êàæäîãî 0 ≤ k ≤ n îáîçíà÷èì ÷åðåç Λk ìíîæåñòâî âñåõ ôóíêöèé σ : {0, . . . , k − 1} → {⊥, >} òàêèõ, ÷òî èñòèííà áóëåâà ôîðìóëà ñêâàíòîðàìèQkxk . . . Qn−1xn−1ϕ(σ(0), . . . , σ(k − 1), xk, .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
