Диссертация (1104034), страница 3
Текст из файла (страница 3)
. . , xn−1).×åðåç Λ−k ìû îáîçíà÷èì äîïîëíåíèå Λk äî ìíîæåñòâà âñåõ ôóíêöèé σ : {0, . . . , k − 1} → {⊥, >}. Îòìåòèì, ÷òî ñóùåñòâóåò åäèíñòâåííàÿ ôóíêöèÿ σ : ∅ → {⊥, >}, à ñëåäîâàòåëüíî |Λ0 | = 1, åñëèQ0x0 . . . Qn−1xn−1ϕ(x0, . . . , xn−1) èñòèííà è |Λ0| = 0, èíà÷å.Ëåììà 1.1.[8, ëåììà 1] Ïóñòü ξ1 , ξ2 ÿâëÿþòñÿ ïîëèìîäàëüíûìè ôîð-ìóëàìè è s1 , s2 íàòóðàëüíûìè ÷èñëàìè òàêèìè, ÷òî s1 < s2 . Òîãäà1. GLP ` hs2 i(ξ1 ∧ hs1 iξ2 ) ↔ hs2 iξ1 ∧ hs1 iξ2 ;2.
GLP ` hs2 i(ξ1 ∧ ¬hs1 iξ2 ) ↔ hs2 iξ1 ∧ ¬hs1 iξ2 .Ñëåäóþùàÿ ëåììà ìîæåò áûòü ëåãêî ïîëó÷åíà èç ñëåäñòâèÿ 2.7,êîòîðîå áóäåò äîêàçàíî ïîçäíåå:Ëåììà 1.2.Ïóñòü s íàòóðàëüíîå ÷èñëî è ôîðìóëà ϕ èìååò âèähs1 i . . . hsn i>, ãäå si < s äëÿ âñåõ i. ÒîãäàGLP ` hsiϕ ↔ hsi>.Çàìå÷àíèå 1.3.Äèçúþíêöèþ ïóñòîãî ìíîæåñòâà ôîðìóëñ÷èòàåì ðàâíîé ⊥. Êîíúþíêöèþ ïóñòîãî ìíîæåñòâà ôîðìóëξ∈∅Vξ∈∅ñ÷èòàåì ðàâíîé >.Ëåììà 1.4.WÏóñòü k ≤ n. Òîãäà_^ σ(i)GLP `(ηk ∧ θi ) ↔ ψk .i <kσ∈Λk15ξ ìûξ ìûÄîêàçàòåëüñòâî. Ìû äîêàçûâàåì ëåììó èíäóêöèåé ïî n − k.
ÔîðìóëàW V σ(i)( xi ) ÿâëÿåòñÿ ñîâåðøåííîé äèçúþíêòèâíîé íîðìàëüíîé ôîðìîéσ∈Λn i<näëÿ ϕ. Ñëåäîâàòåëüíî ïðåäïîëîæåíèå èíäóêöèè èìååò ìåñòî äëÿ ñëó÷àÿk = n. Äàëåå ìû äîêàçûâàåì ïåðåõîä èíäóêöèè.Ðàññìîòðèì ñëó÷àé Qk = ∃. Ìû äàåì ïîñëåäîâàòåëüíîñòü çàìêíóòûõ ôîðìóë ÿçûêà ëîãèêè GLP è çàòåì ïîêàçûâàåì, ÷òî ñîñåäíèå ôîðìóëû â ýòîé ïîñëåäîâàòåëüíîñòè GLP-äîêàçóåìî ýêâèâàëåíòíû:1. ψk ;2.
h2kih4n − 2k − 1ih2kiψk+1 ;3. h2kih4n − 2k − 1ih2ki(Wσ∈Λk+14.Wσ∈Λk+15.Wσ∈Λk+16.h2kih4n − 2k − 1ih2ki(ηk+1 ∧σ∈Λk+17.Wσ∈Λkσ(i)Vi<k+1Vθiσ(i)θii<k+1σ(k)(h2kih4n − 2k − 1ih2ki(ηk+1 ∧ θk ) ∧(h2kih4n − 2k − 1i> ∧W(ηk+1 ∧(ηk ∧Vi<kσ(i)θiVi <kσ(i)θi)););Vi<kσ(i)θi););).Î÷åâèäíî, ÷òî ïàðû h1.,2.i, h2.,3.i, h3.,4.i è h6.,7.i ÿâëÿþòñÿ ïàðàìè GLPäîêàçóåìî ýêâèâàëåíòíûõ ôîðìóë. Ýêâèâàëåíòíîñòü 4. è 5. ìîæåò áûòüîáîñíîâàíà ñ ïîìîùüþ ìíîãîêðàòíîãî ïðèìåíåíèÿ ëåììû 1.1.
Äëÿ óñòàíîâëåíèÿ GLP-äîêàçóåìîé ýêâèâàëåíòíîñòè 5. è 6. ìû äîêàæåì, ÷òîGLP ` h4n − 2k − 1ih2ki(ηk+1 ∧ θk ) ↔ h4n − 2k − 1i>,GLP ` h4n − 2k − 1ih2ki(ηk+1 ∧ ¬θk ) ↔ h4n − 2k − 1i>.(1.1)(1.2)Èç ëåììû 1.1 ñëåäóåò, ÷òîGLP ` ηk+1 ∧ θk ↔ h2k + 2ih4n − 2k − 3ih2k + 1ih4n − 2k − 2i>. ñèëó ëåììû 1.2GLP ` h4n − 2k − 1ih2kih2k + 2ih4n − 2k − 3ih2k + 1ih4n − 2k − 2i> ↔h4n − 2k − 1i>.Ïîýòîìó ýêâèâàëåíòíîñòü (1.1) âûïîëíÿåòñÿ.16Äîêàæåì, ÷òî GLP ` ¬h2kiηk+1 → ¬θk :GLP ` θk → h2kih4n − 2k − 2i>→ h2kih4n − 2k − 2ih4n − 2k − 3i>→ h2kih2k + 2ih4n − 2k − 3i>→ h2kiηk+1 .Èñïîëüçóÿ àêñèîìó 3 ëîãèêè GLP, ìû âûâîäèìGLP ` h2kiηk+1 → h2ki(ηk+1 ∧ ¬h2kiηk+1 )→ h2ki(ηk+1 ∧ ¬θk ).Ïîýòîìó ìû èìååìGLP ` h4n − 2k − 1ih2kiηk+1 → h4n − 2k − 1ih2ki(ηk+1 ∧ ¬θk ).Ñëåäîâàòåëüíî, â ñèëó ëåììû 1.2 ìû èìååìGLP ` h4n − 2k − 1i> → h4n − 2k − 1ih2kiηk+1→ h4n − 2k − 1ih2ki(ηk+1 ∧ ¬θk )Ñëåäîâàòåëüíî, ýêâèâàëåíòíîñòü (1.2) èìååò ìåñòî.Òàêèì îáðàçîì, ôîðìóëû 5.
è 6. ÿâëÿþòñÿ GLP-äîêàçóåìî ýêâèâàëåíòíûìè.  ðåçóëüòàòå ìû ïîëó÷àåì, ÷òî ôîðìóëû 1. è 7. ýêâèâàëåíòíûâ GLP. Ýòî çàâåðøàåò îáîñíîâàíèå ïåðåõîäà èíäóêöèè â ñëó÷àåÏåðåéäåì ê ñëó÷àþQkQk = ∃.= ∀. Ìû ðàññìàòðèâàåì ñëåäóþùóþ ïî-ñëåäîâàòåëüíîñòü çàìêíóòûõ GLP-ôîðìóë:1. ψk ;2. ηk ∧ ¬h2kih4n − 2k − 1ih2ki(ηk+1 ∧ ¬ψk+1 );3. ηk ∧ ¬h2kih4n − 2k − 1ih2ki(ηk+1 ∧ ¬(Wσ∈Λk+14. ηk ∧ ¬h2kih4n − 2k − 1ih2ki(5. ηk ∧ ¬(W−(ηk ∧σ∈Λk6.Wσ∈Λk(ηk ∧Vi <kσ(i)θiVi<kσ(i)θiWσ∈Λ−k+1));).17(ηk+1 ∧(ηk+1 ∧Vi<k+1σ(i)θiVi<k+1));σ(i)θi)));Äëÿ âñåõ ïàð ñîñåäíèõ ôîðìóë, êðîìå 4.
è 5. î÷åâèäíî, ÷òî ýêâèâàëåíòíîñòü èìååò ìåñòî. Ïîñëåäíÿÿ ýêâèâàëåíòíîñòü îáîñíîâûâàåòñÿ àíàëîãè÷íî ýêâèâàëåíòíîñòè ìåæäó 3. è 7. èç äîêàçàòåëüñòâà ïåðåõîäà èíäóêöèè â ñëó÷àåQk = ∃.Ïî ëåììå 1.4, ìû èìååì GLP ` η0 ↔ ψ0 , åñëè ôîðìóëàQ0x0Q1x1 . . . Qn−1xn−1ϕ(x0, x1, . . . , xn−1)èñòèííà, è GLP ` ⊥ ↔ ψ0 , åñëè ôîðìóëà ëîæíà. Èç êîððåêòíîñòèàðèôìåòè÷åñêîé ñåìàíòèêè [22] äëÿ ëîãèêè GLP ëåãêî âûâîäèòñÿ, ÷òîGLP 6` η0 ↔ ⊥ (òàêæå ýòîò ôàêò ëåãêî äîêàçàòü ñ ïîìîùüþ ìîäåëèÈãíàòüåâà, ÷üå îïèñàíèå ìû ïðèâîäèì â ñëåäóþùåì ðàçäåëå). ÑëåäîâàòåëüíîQ0x0Q1x1 .
. . Qn−1xn−1ϕ(x0, . . . , xn−1)èñòèííà òîãäà è òîëüêî òîãäà, êîãäàGLP ` η0 ↔ ψ0 .Íåñëîæíàÿ ïðîâåðêà ïîêàçûâàåò, ÷òî ìû ìîæåì ïîëó÷èòü ôîðìóëó η0 ↔ ψ0 çà ïîëèíîìèàëüíîå âðåìÿ îò äëèíûQ0x0Q1x1 . . . Qn−1xn−1ϕ(x0, x1, . . . , xn−1).Ýòî äàåò íàì òðåáóåìîå ñâåäåíèå è çàâåðøàåò äîêàçàòåëüñòâî òåîðåìû 1.1.2Çàìêíóòûå ôðàãìåíòû ëîãèêGLPnÏðàâèëüíî ïîñòðîåííûå ôîðìóëû ëîãèêè GLPn ýòî GLP-ôîðìóëû, âêîòîðûõ èç ìîäàëüíûõ ñâÿçîê âñòðå÷àþòñÿ òîëüêî [0], [1], . . .
, [n]. Èñ÷èñëåíèå â ãèëüáåðòîâñêîì ñòèëå äëÿ ëîãèêè GLPn çàäàåòñÿ òåìè àêñèîìàìèè ïðàâèëàìè âûâîäà èñ÷èñëåíèÿ äëÿ GLP, êîòîðûå ëåæàò â ÿçûêå ëîãèêè GLPn . Îòìåòèì, ÷òî ìíîæåñòâî òåîðåì ëîãèêè GLPn ñîâïàäàåò ñîìíîæåñòâîì òåîðåì ëîãèêè GLP, êîòîðûå ÿâëÿþòñÿ GLPn -ôîðìóëàìè[10].18Ìåòîä èñïîëüçîâàííûé â ïðåäûäóùåì ðàçäåëå ñóùåñòâåííî èñïîëüçóåò áåñêîíå÷íî ìíîãî ìîäàëüíîñòåé è, òåì ñàìûì ýòîò ìåòîä íåìîæåò áûòü èñïîëüçîâàí äëÿ äîêàçàòåëüñòâà PSPACE-òðóäíîñòè ïðîáëåìû ðàñïîçíàâàíèÿ âûâîäèìîñòè çàìêíóòûõ ôîðìóë â ëîãèêàõ GLPn .Öåíòðàëüíûì ðåçóëüòàòîì ýòîãî ðàçäåëà ÿâëÿåòñÿ ñëåäóþùàÿòåîðåìà.Òåîðåìà 2.Ïðè âñåõ íàòóðàëüíûõ n ïðîáëåìà ðàñïîçíàâàíèÿ âûâîäè-ìîñòè â ëîãèêå GLPn äëÿ çàìêíóòûõ ôîðìóë ðàçðåøèìà çà ïîëèíîìèàëüíîå âðåìÿ.Íà÷í¼ì ñ ïëàíà äîêàçàòåëüñòâà.
Ìû èñïîëüçóåì ìîäåëü Êðèïêå(îïðåäåëåíèå ïîíÿòèÿ ìîäåëè Êðèïêå ñì. [11]) Uωnn+1 òàêóþ, ÷òî çàìêíóòûé ôðàãìåíò ëîãèêè GLPn ÿâëÿåòñÿ ïîëíûì îòíîñèòåëüíî ýòîé ìîäåëè.Êàæäîé çàìêíóòîé GLPn -ôîðìóëå ìû ñòàâèì â ñîîòâåòñòâèå ìíîæåñòâîìèðîâ ìîäåëè Uωnn+1 , â êîòîðûõ îíà âûïîëíÿåòñÿ. Ïîëíîòà çàìêíóòîãîôðàãìåíòà GLPn îòíîñèòåëüíî ìîäåëè Uωnn+1 îçíà÷àåò, ÷òî âñÿêàÿ çà-ìêíóòàÿ GLPn -ôîðìóëà äîêàçóåìà â GLPn òîãäà è òîëüêî òîãäà, êîãäàýòîé ôîðìóëå ñîîòâåòñòâóåò ìíîæåñòâî âñåõ ìèðîâ ìîäåëè Uωnn+1 . Îòìåòèì, ÷òî äëÿ âñÿêîé çàìêíóòîé GLPn -ôîðìóëû ϕ ñîîòâåòñòâóþùåå åéìíîæåñòâî ìîæåò áûòü ïîëó÷åíî èíòåðïðåòàöèåé ïðîïîçèöèîíàëüíûõêîíñòàíò è ïðîïîçèöèîíàëüíûõ ñâÿçîê èç ϕ, êàê ñïåöèàëüíûõ ìíîæåñòâìèðîâ Uωnn+1 è ñïåöèàëüíûõ îïåðàöèé íà ìíîæåñòâàõ ìèðîâ Uωnn+1 , ñîîòâåòñòâåííî.Ìû èñïîëüçóåì êîäû èç ìíîæåñòâà Cnωn+1 äëÿ ýôôåêòèâíîãî ïðåä-ñòàâëåíèÿ ìíîæåñòâ ìèðîâ ìîäåëè Uωnn+1 (îòìåòèì, ÷òî ñóùåñòâóþò ìíî-æåñòâà ìèðîâ, êîòîðûì íå ñîîòâåòñòâóåò íè îäíîãî êîäà).
 ðàçðåøàþùåì àëãîðèòìå ìû èñïîëüçóåì ñëåäóþùèå âû÷èñëèìûå ôóíêöèè (âïîëíîì äîêàçàòåëüñòâå ó íèõ èìåþòñÿ äîïîëíèòåëüíûå àðãóìåíòû è ïàðàìåòðû):1. Intr : Cnωn+1 × Cnωn+1 → Cnωn+1 ,2. Cmpl : Cnωn+1 → Cnωn+1 ,193. R0 -Inv, . . . , Rn -Inv : Cnωn+1 → Cnωn+1 ,4. IsEmp : Cnωn+1 → {0, 1}.Íàø ðàçðåøàþùèé àëãîðèòì ðàáîòàåò òàêèì îáðàçîì:1. Ìû ïîëó÷àåì íà âõîä çàìêíóòóþ GLPn -ôîðìóëó ϕ.2. Ìû çàìåíÿåì åå íà ôîðìóëó ϕ0 òàêóþ, ÷òîGLP ` ϕ0 ↔ ϕè ϕ0 ñîñòàâëåíà èç ⊥, ∧, ¬, [0], . .
. , [n].3. Ìû ñòðîèì êîä c(ϕ0 ) äëÿ ìíîæåñòâà, ñîîòâåòñòâóþùåãî ôîðìóëå ϕ0 .Äëÿ ýòîãî ìû îïðåäåëÿåì êîäû c(ψ) äëÿ âñåõ ïîäôîðìóë ψ ôîðìóëûϕ0 , èñïîëüçóÿ ñëåäóþùèå ïðàâèëà:(a) c(⊥) ÿâëÿåòñÿ êîíñòàíòîé, îáîçíà÷àþùåé ïóñòîå ìíîæåñòâî;(b) c(ψ1 ∧ ψ2 ) ðàâíî Intr(c(ψ1 ), c(ψ2 ));(c) c(¬ψ) ðàâíî Cmpl(c(ψ));(d) c(hkiψ) ðàâíî Rk -Inv(c(ψ)).4. Ìû äàåì ïîëîæèòåëüíûé îòâåò íà ôîðìóëó ϕ, åñëè è òîëüêî åñëèôóíêöèÿ IsEmp âîçâðàùàåò 1 íà âõîäå Cmpl(c(ϕ0 )).Òåïåðü îïèøåì íàø ìåòîä îöåíêè âðåìåíè ðàáîòû àëãîðèòìà.
Ìû ââîäèì ôóíêöèè cnωn+1 è wωnn+1 äëÿ èçìåðåíèÿ ñëîæíîñòè êîäîâ, ïåðåäàííûõíà âõîä. Äàëåå ìû ïîëó÷àåì îöåíêè âðåìåíè ðàáîòû è ñëîæíîñòè ðåçóëüòèðóþùèõ êîäîâ äëÿ ôóíêöèé Cmpl, Intr, R0 -Inv, R1 -Inv,. . ., Rn -Invâ òåðìèíàõ ñëîæíîñòè êîäîâ íà âõîäå. Ýòî äàåò íàì ïîëèíîìèàëüíóþîöåíêó íà ñëîæíîñòè èñïîëüçóåìûõ êîäîâ, â ñìûñëå óêàçàííûõ âûøåôóíêöèé, è íà âðåìÿ ðàáîòû ðàçðåøàþùåãî àëãîðèòìà.  áîëüøèíñòâåëåìì ýòîãî ðàçäåëà ìû îäíîâðåìåííî äàåì îïèñàíèå àëãîðèòìà è âåðõíþþ îöåíêó íà âðåìÿ åãî ðàáîòû.Òåïåðü ìû ïåðåõîäèì ê òî÷íîìó îïèñàíèþ òðåáóåìîé íàì ìîäåëèÊðèïêå.Îáîçíà÷èì ÷åðåç On êëàññ âñåõ îðäèíàëîâ.20Òåîðåìà Êàíòîðà î íîðìàëüíîé ôîðìå îðäèíàëîâ óòâåðæäàåò, ÷òîêàæäûé îðäèíàë α > 0 ìîæåò áûòü åäèíñòâåííûì îáðàçîì ïðåäñòàâëåíâ âèäå ñóììûα = ω β0 + · · · + ω βn−1òàêîé, ÷òî β0 ≥ β1 ≥ . . . ≥ βn−1 è n ≥ 0.Ïóñòü ` : On → On çàäàåòñÿ, êàê• `(0) = 0;• `(α) = βn−1 , ãäå α > 0 è ÊÍÔ (êàíòîðîâñêàÿ íîðìàëüíàÿ ôîðìà) αðàâíà ω β0 + · · · + ω βn−1 .Îïðåäåëèì ìîäåëü Èãíàòüåâà U = (U, R0 , R1 , .
. . , Rn , . . .) [22].Ìíîæåñòâî U ÿâëÿåòñÿ ìíîæåñòâîì âñåõ ïîñëåäîâàòåëüíîñòåé(α0 , α1 , α2 , . . .)òàêèõ, ÷òî âñå αi ÿâëÿþòñÿ îðäèíàëàìè, α0 < ε0 è αi+1 ≤ `(αi ), äëÿ âñåõi ∈ ω . Äëÿ êàæäîãî íàòóðàëüíîãî k áèíàðíîå îòíîøåíèå Rk çàäàåòñÿ,êàêdef(α0 , α1 , . . .) Rk (β0 , β1 , . . .) ⇐⇒ βk < αk ∧ ∀i < k(αi = βi ).Ìîäåëü U ÿâëÿåòñÿ óíèâåðñàëüíîé ìîäåëüþ äëÿ çàìêíóòîãî ôðàãìåíòàëîãèêè GLP [22, 23, 9].
Ýòî îçíà÷àåò, ÷òî äëÿ âñÿêîé çàìêíóòîé GLPôîðìóëû ϕ ìû èìååìGLP ` ϕ ⇐⇒ U |= ϕ (ϕ âåðíà â U).Ëåãêî âèäåòü, ÷òî äëÿ âñÿêîé ïîñëåäîâàòåëüíîñòè (α0 , α1 , . . .) ∈ U ìûèìååì αi = 0 äëÿ äîñòàòî÷íî áîëüøèõ i.Íà ñàìîì äåëå, íàì ïîòðåáóþòñÿ ¾ìåíüøèå¿ ìîäåëè Uαn =(Uαn , R0 , R1 , . . . , Rn ) äëÿ âñåâîçìîæíûõ 1 ≤ α < ε0 è n ≥ −1. Îòìåòèì,÷òî âñå Uα−1 áóäóò ìîäåëÿìè èñ÷èñëåíèÿ âûñêàçûâàíèé PC = GLP−1 ñåäèíñòâåííûì ìèðîì è áåç îòíîøåíèé äîñòèæèìîñòè.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
