Диссертация (1104034), страница 7
Текст из файла (страница 7)
Èñõîäÿ èç ïðîöåäóðû ïîñòðîåíèÿ íîðìàëüíîé ôîðìûñëîâà ìû âûâîäèì, ÷òî ëèáî C = C0 kCl k . . . kCm äëÿ íåêîòîðîãî ïîëîæèòåëüíîãî íàòóðàëüíîãî ÷èñëà l ≤ m, ëèáî C = C0 . Ñëåäîâàòåëüíî,hk+1 (C) = C0 ∼ hk+1 (A).Ïðîâåäÿ àíàëîãè÷íîå ðàññóæäåíèå äëÿ B è íîðìàëüíîé ôîðìûñëîâà hk (B), ðàâíîé D, ìû ïîëó÷èì, ÷òî hk+1 (D) ∼ hk+1 (B).  ñèëóåäèíñòâåííîñòè íîðìàëüíîé ôîðìû ñëîâà è ïðåäïîëîæåíèÿ èíäóêöèè41C = D. Òåì ñàìûì hk+1 (A) ∼ hk+1 (B), ÷òî çàâåðøàåò äîêàçàòåëüñòâîëåììû.Ïî ëåììå 2.10 ïðàâàÿ ÷àñòü ðàâåíñòâà (2.1) ñîõðàíÿåò ñâîå çíà÷åíèå ïðè çàìåíå ñëîâà A íà ýêâèâàëåíòíîå, òåì ñàìûì ìû ïîëó÷àåìÑëåäñòâèå 2.11.Åñëè A ∼ B, òî t(A) = t(B).Èç ëåììû 2.3 è ñëåäñòâèÿ 2.11 ìû âûâîäèìÑëåäñòâèå 2.12.Åñëè ñëîâî A ïðèíàäëåæèò Bk , òî è åãî íîðìàëüíàÿôîðìà ïðèíàäëåæèò Bk .Ëåììà 2.13.Äëÿ âñÿêîãî íàòóðàëüíîãî ÷èñëà k è ëþáûõ ñëîâ A è Bhk (A u B) ∼ hk (A) u hk (B).Äîêàçàòåëüñòâî.
Íàéäåì òàêîå ÷èñëî n > k è ñëîâà A0 , B0 ∈ B0 ,A1 , B1 ∈ B1 , . . ., An , Bn ∈ Bn , ÷òî A = An An−1 . . . A0 è B = Bn Bn−1 . . . B0 .Ïðè i îò 0 äî n ïîëîæèì Ci = Ai u Bi . Èç ñëåäñòâèé 2.6 è 2.12 ìû äëÿâñåõ Ci ïîëó÷àåì, ÷òî Ci ∈ Bi . Èñïîëüçóÿ ëåììó 2.4 ìû ïîëó÷àåì ñîîòíîøåíèÿA u B = An u .
. . u A0 u Bn u . . . u B0 = Cn u . . . u C0 ∼ Cn . . . C0 ,hk (A) u hk (B) = An u . . . u Ak u Bn u . . . u Bk = Cn u . . . u Ck ∼ Cn . . . Ck . ñèëó ëåììû 2.10hk (A u B) ∼ hk (Cn . . . C0 ) = Cn . . . Ck ∼ hk (A) u hk (B).Ñëåäñòâèå 2.14.Ïóñòü A è B ñëîâà. Òîãäà t(A ∧ B) = max(t(A), t(B)).Äîêàçàòåëüñòâî.  ñèëó ëåììû 2.13 ïðè ïðîèçâîëüíîì k:hk (A ∧ B) ∼ > ⇐⇒ hk (A) ∼ > è hk (B) ∼ >.Òàêèì îáðàçîì, èñêîìîå ñëåäóåò èç ëåììû 2.9.42Îáîçíà÷èì ÷åðåç B ìíîæåñòâîSn∈ωBn .Íàçîâåì ñëîâî A ðàçëîæèìûì, åñëè ñóùåñòâóþò òàêèå ñëîâà B A è C A, ÷òî B ∧ C ∼ A.Ïðåäëîæåíèå 2.15.Ïóñòü ñëîâî A ∈ NF. Òîãäà A íåðàçëîæèìî, åñëèè òîëüêî åñëè A ∈ B.
Ïðè ýòîì, åñëè A ∈ Wn ðàçëîæèìî, òî ñóùåñòâóþò ñëîâà B, C ∈ Wn òàêèå, ÷òî B ∧ C ∼ A, B A è A.Äîêàçàòåëüñòâî. Ïóñòü A 6∈ B, äîêàæåì, ÷òî A ðàçëîæèìî. ÏðåäñòàâèìA â âèäå A = ht(A) (A)B, ãäå B 6= > è t(B) < t(A). Ðàññìàòðèâàÿ ïðîöåäóðó ïðèâåäåíèÿ ñëîâà ê íîðìàëüíîé ôîðìå (ñì.
ñòð 38), ìû çàìå÷àåì,÷òî äëÿ âñÿêîãî ñëîâà äëèíà åãî íîðìàëüíîé ôîðìû íå ïðåâîñõîäèò åãîñîáñòâåííîé äëèíû. Òåì ñàìûì íîðìàëüíûå ôîðìû ñëîâ ht(A) (A) è B íåñîâïàäàþò ñî ñëîâîì A. Ñëåäîâàòåëüíî, A ht(A) (A) è A B, ïðè òîìA ∼ ht(A) (A) ∧ B. Òàêèì îáðàçîì, A ðàçëîæèìî. Íåñëîæíî âèäåòü, ÷òîåñëè äëÿ íåêîòîðîãî n ìû èìååì A ∈ Wn , òî ht(A) (A), B ∈ Wn .Ïóñòü A ∈ B, äîêàæåì, ÷òî A íåðàçëîæèìî. Âûáåðåì òàêîå íàòóðàëüíîå ÷èñëî k, ÷òî A ∈ Bk .
Ðàññìîòðèì ïðîèçâîëüíûå ñëîâà B è Còàêèå, ÷òî A ∼ B ∧ C. Èç ëåììû 2.13 ìû âûâîäèì, ÷òî hk (B) ∧ hk (C) ∼hk (A) = A. Òàêèì îáðàçîì, â ñèëó ñëåäñòâèÿ 2.14 ìû èìååì t(hk (B)) ≤ kè t(hk (C)) ≤ k. Ñëåäîâàòåëüíî, hk (B) ∈ Bk è hk (C) ∈ Bk . Òåì ñàìûì â ñèëó ñëåäñòâèÿ 2.6 ëèáî hk (B) ∧ hk (C) ∼ hk (B), ëèáî hk (B) ∧ hk (C) ∼ hk (C).Áåç îãðàíè÷åíèÿ îáùíîñòè ìû áóäåì ñ÷èòàòü, ÷òî hk (B) ∧ hk (C) ∼ hk (B).Òàêèì îáðàçîì, ìû èìååì GLP ` A ↔ hk (B), GLP ` B → hk (B) èGLP ` A → B. Ñëåäîâàòåëüíî A ∼ B. Ïîñëåäíåå, â ñèëó ïðîèçâîëüíîñòèâûáîðà ñëîâ B è C, îçíà÷àåò íåðàçëîæèìîñòü ñëîâà A.Ëåììà 2.16.Ïóñòü äëÿ ïàðû ñëîâ hA, Bi âûïîëíÿþòñÿ ñëåäóþùèå äâàóñëîâèÿ:1.
GLP 0 A → B;2. äëÿ âñÿêîãî ñëîâà C A òàêîãî, ÷òî GLP ` C → A èìååò ìåñòîGLP ` C → B.43Òîãäà A <0 B.Äîêàçàòåëüñòâî. Ïðåäñòàâèì ñëîâà A è B â âèäå A = h1 (A)A1 , B =h1 (B)B1 . Çàìåòèì, ÷òî A1 , B1 ∈ B0 .  ñèëó ëåììû 2.4 è ñëåäñòâèÿ 2.6 ìûèìååìGLP ` h1 (A)0A → h1 (A)0h1 (A)A1→ h1 (A) ∧ h0i(h1 (A)A1 )→ h1 (A) ∧ h0i(h1 (A) ∧ A1 )→ h1 (A) ∧ h0iA1→ h1 (A) ∧ A1→ A.Ïîñêîëüêó o0 (h1 (A)0A) > o0 (A), ìû èìååì h1 (A)0A A. Òàêèì îáðàçîì,ïîëüçóÿñü óñëîâèåì 2, ìû ïîëó÷àåì GLP ` h1 (A)0A → B. Òåì ñàìûììû èìååìh1 (A) ∼ h1 (h1 (A)0A) ∼ h1 (h1 (A)0A u B) ∼∼ h1 (h1 (A)0A) u h1 (B) ∼ h1 (A) u h1 (B).Ïðåäïîëîæèì, ÷òî A 6<0 B.
Òàê êàê A B è <0 ÿâëÿåòñÿ îòíîøåíèåì ñòðîãîãî ëèíåéíîãî ïîðÿäêà ìû èìååì B <0 A. Èñïîëüçóÿñëåäñòâèå 2.6 è òî, ÷òî B1 <0 0B ìû ïîëó÷àåì GLP ` h0iB → B1 .Ïîñêîëüêó GLP ` A → h0iB, ìû èìååì GLP ` A → B1 . Êðîìåòîãî GLP ` A → h1 (A) è GLP ` h1 (A) → h1 (B), ñëåäîâàòåëüíîGLP ` A → h1 (B). Òàê êàê B ∼ h1 (B) ∧ B1 , ìû èìååì GLP ` A → B,÷òî ïðîòèâîðå÷èò óñëîâèþ 1. Ñîîòâåòñòâåííî, A <0 B, ÷òî è òðåáîâàëîñüäîêàçàòü.Ëåììà 2.17.Äëÿ âñÿêîãî ñëîâà A ïàðà hA, d0 (A)i óäîâëåòâîðÿåò óñëî-âèÿì ëåììû 2.16.Äîêàçàòåëüñòâî. Äîêàæåì, ÷òî âûïîëíÿåòñÿ óñëîâèå 1.  ñàìîì äåëå,ïî èððåôëåêñèâíîñòè <0 ìû èìååì GLP 0 A → h0iA.Òåïåðü ïîêàæåì, ÷òî âûïîëíÿåòñÿ óñëîâèå 2.
Ðàññìîòðèì ïðîèçâîëüíîå ñëîâî C A, ÷òî GLP ` C → A è äîêàæåì, ÷òî GLP ` C →44h0iA. Ïðåäïîëîæèì, ÷òî C <0 A. Îòñþäà ìû ïîëó÷àåìGLP ` A → h0iC→ h0iA.Ìû ïîêàçàëè, ÷òî A <0 A, à ýòî ïðîòèâîðå÷èò èððåôëåêñèâíîñòè <0 .Òàêèì îáðàçîì, A <0 C, ÷òî è òðåáîâàëîñü äîêàçàòü.Äëÿ ëþáîãî k è A ∈ Sk èìåþò ìåñòî ñëåäóþùèå ôàêòû:Ëåììà 2.18.1. A <0 hkiA;2. åñëè A ∈ Bk , òî ∀B ∈ Sk (A <0 B ⇒ GLP ` B → A);3. åñëè GLP ` hkiA → A, òî A ∈ Bk .Äîêàçàòåëüñòâî. 1. Î÷åâèäíî ñëåäóåò èç àêñèîìû 4 ëîãèêè GLP.2.
Ïóñòü A ∈ Bk , à B ïðîèçâîëüíîå ñëîâî èç Sk òàêîå, ÷òî A <0 B.Äîêàæåì, ÷òî GLP ` B → A.  ñèëó ñîãëàñîâàííîñòè <k è <0 íà Sk ìûèìååì A <k B. Òàê êàê GLP ` B → hkiA è GLP ` hkiA → A ìû èìååìòðåáóåìîå GLP ` B → A.3. Ïóñòü GLP ` hkiA → A. Ñ ïîìîùüþ ñëåäñòâèÿ 2.14 ìû ïîëó÷àåì, ÷òî t(A) ≤ t(kA) = k. Ñëåäîâàòåëüíî ëèáî A íà÷èíàåòñÿ ñ k, ëèáîA = >. Òåì ñàìûì A ∈ Bk .2.3Îïðåäåëèìûå â ïîëóðåøåòêàõ ñëîâ ñâîéñòâàÍàïîìíèì, ÷òî äëÿ α ≤ ω ìû îáîçíà÷àåì ÷åðåç Sα = (WNα ; u). Ïåðåäòåì, êàê â ñëåäóþùåì ðàçäåëå ïåðåéòè ê äîêàçàòåëüñòâó íåðàçðåøèìîñòè ýëåìåíòàðíûõ òåîðèé ìîäåëåé Sα äëÿ α ≥ 2, ìû ïîêàæåì, ÷òî â ýòèõìîäåëÿõ ìîæíî âûðàçèòü ìíîãèå åñòåñòâåííûå ïîíÿòèÿ, îòíîñÿùèåñÿ êñëîâàì.Ëåììà 2.19.Ïóñòü A ñëîâî, à k íàòóðàëüíîå ÷èñëî.
Òîãäà A ∈ Sk ,åñëè è òîëüêî åñëè A <0 hk + 1i>.Äîêàçàòåëüñòâî. Èñïîëüçóÿ îïðåäåëåíèÿ ôóíêöèè o, çàìåòèì, ÷òî íàëè÷èå â A ñèìâîëîâ áîëüøèõ k ðàâíîñèëüíî òîìó, ÷òî o0 (A) ≥ ωk+1 =o0 (hk + 1i>).45Ìû îáîçíà÷àåì ÷åðåç 4 åñòåñòâåííûé ÷àñòè÷íûé ïîðÿäîê íà ñëîâàõ, äëÿ âñÿêèõ A, B ∈ WN ìû ïîëàãàåìdefA 4 B ⇐⇒ GLP ` A → B.Îòìåòèì, ÷òî äëÿ âñåõ α ≤ ω ýòîò ïîðÿäîê, áóäó÷è îãðàíè÷åí íà WNα,ñîâïàäàåò ñ åñòåñòâåííûì ïîðÿäêîì íà ïîëóðåøåòêå Sα :∀A, B ∈ WNα (A u B = A ⇐⇒ A 4 B).Ìû ïðåäïîëàãàåì çíàêîìñòâî ÷èòàòåëÿ ñ ïîíÿòèåì îïðåäåëèìîñòèâ ìîäåëÿõ. Îòìåòèì, ÷òî ìû ïðèâîäèì îáñóæäåíèå ìîäåëåé è îïðåäåëèìîñòè â áîëåå øèðîêîì êîíòåêñòå ìíîãîñîðòíûõ ìîäåëåé â ðàçäåëå2.4.Ïðåäëîæåíèå 2.20.Ïóñòü α ≤ ω .
Òîãäà äëÿ âñåõ íàòóðàëüíûõ k ≤ αâ ìîäåëè Sα ôîðìóëàìè ïåðâîãî ïîðÿäêà îïðåäåëèìû ñëåäóþùèå ôóíêöèè, áèíàðíûå îòíîøåíèÿ è ìíîæåñòâà:1. ìíîæåñòâî B ∩ WNα;2. ôóíêöèÿ d0 è áèíàðíîå îòíîøåíèå <0 ;3. ìíîæåñòâî Bk ∩ WNα;4. ôóíêöèè hk ;5. ìíîæåñòâî Sk ∩ WNα;6. ôóíêöèè hki è áèíàðíûå îòíîøåíèÿ <k ;7. ìíîæåñòâî Wk .Äîêàçàòåëüñòâî. 1. Èç ïðåäëîæåíèÿ 2.15 ñëåäóåò, ÷òî ïðèíàäëåæíîñòüñëîâà A ∈ WNα ê ìíîæåñòâó B ýêâèâàëåíòíà∀x∀y(A = x u y ↔ A = x ∨ A = y).2. Äëÿ âñÿêèõ ñëîâ A è B ìû èìååìB 4 d0 (A) ⇐⇒ GLP ` B → h0iA ⇐⇒ A <0 B.Òåì ñàìûì íàì îñòàëîñü âûðàçèòü ôóíêöèþ d0 .
Äëÿ âñÿêîãî ñëîâà Ad0 (A) = max{x ∈ WNα | x 4 d0 (A)} = max{x ∈ Sα | A <0 x}.4446Çàäàäèì ôîðìóëó A(x, y) ÿçûêà òåîðèè Th(Sα ) òàêóþ, ÷òî âñÿêàÿïàðà ñëîâ hB, Ci óäîâëåòâîðÿåò óñëîâèþ ëåììû 2.16, åñëè è òîëüêî åñëèSα |= A(B, C):A(x, y) x 64 y ∧ ∀z < x(z 4 y).Ïî ëåììå 2.16 ìíîæåñòâî {y ∈ Sα | A(A, y)} âêëþ÷åíî â ìíîæåñòâî {y ∈ Sα | A <0 y}. Ïðè ýòîì, ïî ëåììå 2.17, ìàêñèìóì âòîðîãîìíîæåñòâà ñîäåðæèòñÿ â ïåðâîì. Ñëåäîâàòåëüíî, d0 (A) = max4 ({y |A(A, y)}). Òàêèì îáðàçîì, ôóíêöèÿ d0 , à òåì ñàìûì è îòíîøåíèå <0îïðåäåëèìû â ìîäåëè Sα .3.
Ïîñëåäîâàòåëüíî, â ïîðÿäêå óâåëè÷åíèÿ k, ïîñòðîèì îïðåäåëåNíèÿ ìíîæåñòâ Bk ∩ WNα . Ïóñòü ïîñòðîåíû îïðåäåëåíèÿ ìíîæåñòâ B0 ∩ Wα ,NNB 1 ∩ WNα ,. . .,Bk−1 ∩ Wα . Ïîñòðîèì îïðåäåëåíèå ìíîæåñòâà Bk ∩ Wα . ÏîSNNëîæèì Gk =(Bi ∩ WNα ). ßñíî, ÷òî Bk ∩ Wα ⊂ Gk ⊂ Sk ∩ Wα . Ïðèi≥kòîì,NGk = ((B ∩ Wα ) \[(Bi ∩ WNα )) ∪ {>}i,0≤i<kè òåì ñàìûì ìíîæåñòâî Gk îïðåäåëèìî. Ïîëüçóÿñü ëåììîé 2.18 ìû ïîëó÷àåì, ÷òîNNA ∈ Bk ∩ WNα ⇐⇒ A ∈ Gk ∩ Wα ∧ ∀x ∈ Gk ∩ Wα (A <0 x → x 4 A).4. Ïóñòü A è B ñëîâà èç WNα . Ïîêàæåì, ÷òî óòâåðæäåíèå hk (A) =hk (B) ýêâèâàëåíòíî òîìó, ÷òî â Sα âûïîëíÿåòñÿ ïðåäëîæåíèå:N∃x0 ∈ B0 ∩ WNα .
. . ∃xk−1 ∈ Bk−1 ∩ Wα (A u xk−1 u . . . u x0 =B u xk−1 u . . . u x0 ).(2.2) ñèëó ëåììû 2.13 è òîãî, ÷òî äëÿ âñÿêîãî i < k è x ∈ Bi èìååòìåñòî hk (x) = >, ìû ïîëó÷àåì, ÷òî èç ïðåäëîæåíèÿ (2.2) ñëåäóåò hk (A) =hk (B).Ïóñòü òåïåðü hk (A) = hk (B). Äîêàæåì, ÷òî èìååò ìåñòî (2.2). ÐàñNñìîòðèì ñëîâà A0 , B0 ∈ B0 ∩ WNα , . . ., Ak−1 , Bk−1 ∈ Bk−1 ∩ Wα òàêèå, ÷òîA = hk (A)Ak−1 . . . A0 , B = hk (B)Bk−1 .
. . B0 . Ñ ïîìîùüþ ñëåäñòâèÿ 2.1247ìû ïîëó÷àåì, ÷òî Ai u Bi ∈ Bi ïðè i < k. Çàìåòèì, ÷òîAuu (Ai u Bi) = hk(A) u 0≤ui<k(Ai u Bi) =hk(B) u 0≤ui<k(Ai u Bi) =B u u (Ai u Bi ).0≤i<k0≤i<kÒåì ñàìûì, âûáèðàÿ Ai u Bi â êà÷åñòâå xi , ìû âûâîäèì ïðåäëîæåíèå(2.2). Òàêèì îáðàçîì, ìû äîêàçàëè òðåáóåìóþ ýêâèâàëåíòíîñòü.Çàìåòèì, ÷òî hk (A) = max4 {x ∈ WNα | hk (x) = hk (A)}. Òàêèìîáðàçîì, â ñèëó äîêàçàííîé âûøå ýêâèâàëåíòíîñòè ôóíêöèÿ hk îïðåäåëèìà.5.
Çàìåòèì, ÷òî äëÿ âñÿêîãî ñëîâà A ∈ NFA ∈ Sk ⇐⇒ A = hk (A).Òåì ñàìûì, ìíîæåñòâî Sk ∩ WNα îïðåäåëèìî.6. Ïîêàæåì, ÷òî âûðàçèìà ôóíêöèÿ x 7→ dk (hk (x)). Ïóñòü ñëîâîA ∈ WNα . Òàê êàê hk (A) ∈ Sk è íà ìíîæåñòâå Sk îòíîøåíèÿ <0 è <kñîâïàäàþò, ìû ïîëó÷àåì, ÷òîdk (hk (A)) = min{x ∈ Sk | hk (A) <0 x}.<0Òåì ñàìûì, ìû ïîêàçàëè èñêîìóþ âûðàçèìîñòü.NNÏóñòü ñëîâî A ∈ WNα è ñëîâà A0 ∈ B0 ∩ Wα , . . . , Ak−1 ∈ Bk−1 ∩ Wαòàêîâû, ÷òî A = hk (A) u Ak−1 u . . . u A0 .
 ñèëó ëåììû 1.1 ìû èìååìdk (A) = dk (hk (A) u Ak−1 u . . . u A0 ) = dk (hk (A)) u Ak−1 u . . . u A0 . Êðîìåòîãî çàìåòèì, ÷òî äëÿ äàííîãî A ñóùåñòâóåò ïî êðàéíåé ìåðå îäèí íàáîðA0 , . . . , Ak−1 , îáëàäàþùèé óêàçàííûìè âûøå ñâîéñòâàìè. Òåì ñàìûì ìûìîæåì âûðàçèòü ôóíêöèþ dk òàêèì îáðàçîì:Nx = dk (A) ⇐⇒ ∃y0 ∈ B0 ∩ WNα . . .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
