Диссертация (1104034), страница 12
Текст из файла (страница 12)
. . 0An äëÿ íåêîòîðîãî k îò 2 äî n + 1. Ïðèòîì k òàêîâî, ÷òî äëÿ âñåõ i îò k äî n èìååòìåñòî 2A1 ≤0 Ai è äëÿ âñåõ i îò 2 äî k − 1 èìååò ìåñòî Ai <0 2A1 . Îòñþäàñëåäóåò ïðàâèëüíîñòü ïîñòðîåííîãî îïðåäåëåíèÿ.Ëåììà 3.10.Ïóñòü α çàìêíóòûé îòíîñèòåëüíî ψ îðäèíàë. Òîãäàâ ìîäåëè (α; <, ψ)0 èíòåðïðåòèðóåòñÿ ìîäåëü (α; <, ψ)+ .Äîêàçàòåëüñòâî. Âñÿêèé îðäèíàë β ∈ α ìû áóäåì èíòåðïðåòèðîâàòüîðäèíàëîì β I = ω · β , íåñëîæíî âèäåòü, ÷òî òåì ñàìûì ìû ïîñòðîèìèíúåêöèþ α â ñåáÿ. Äëÿ äàííîãî ìóëüòèìíîæåñòâà A ∈ M<ω (α) ïîñòðîèì ìíîæåñòâî AI ∈ P <ω (α) èíòåðïðåòàöèþ A.
Ïóñòü íàáîð β1 , . . . , βnïîïàðíî ðàçëè÷íûõ îðäèíàëîâ ìåíüøèõ α ñîäåðæèò âñå îðäèíàëû âõîäÿùèå â A ñ íåíóëåâîé êðàòíîñòüþ. Ïðèòîì, ïóñòü k1 , . . . , kn ∈ ω åñòüêðàòíîñòè âõîæäåíèé â A îðäèíàëîâ β1 , . . . , βn ñîîòâåòñòâåííî. Ïîëîæèì AI = {ω · βi + (ki − 1) | i ∈ {1, . . . , n}}.Çàìåòèì, ÷òî îòîáðàæåíèå (β, k) 7−→ ω · β + (k − 1) åñòü áèåêöèÿìåæäó ìíîæåñòâàìè α × (ω \ {0}) è α. Òåì ñàìûì, ïîñòðîåííîå îòîáðàæåíèå A 7−→ AI ÿâëÿåòñÿ èíúåêòèâíûì. Ïîêàæåì, ÷òî ìíîæåñòâî U1âñåõ èíòåðïðåòàöèé îðäèíàëîâ îïðåäåëèìî â (α; <, ψ)0 .  ñàìîì äåëå,73äëÿ âñÿêîãî β ∈ αβ ∈ U1 ⇐⇒ β ∈ Lim ∨ β = 0.Òåïåðü ïîêàæåì, ÷òî ìíîæåñòâî U2 âñåõ èíòåðïðåòàöèé ìóëüòèìíîæåñòâîïðåäåëèìî â (α; <, ψ)0 .
 ñàìîì äåëå, äëÿ âñÿêîãî A ∈ P <ω (α) ìû èìååìA ∈ U2 ⇐⇒ ∀β ∈ α∀γ ∈ α((β ∈ X ∧ γ ∈ X) → (FinDif(β, γ) ↔ β = γ)).Çàäàäèì ∈IM , ⊂IM , <I , ψ I èíòåðïðåòàöèè ∈M , ⊂M , <, ψ ñîîòâåòñòâåííî.x ∈IM X x ∈ U1 ∧ X ∈ U2 ∧ ∃y ∈ X(FinDif(x, y));x <I y x ∈ U1 ∧ y ∈ U1 ∧ x < y;ψ I (x) = y x ∈ U1 ∧y ∈ U1 ∧(x = 0 → y = ψ(ψ(0)))∧(x 6= 0 → y = ψ(x));X ⊂IM Y X, Y ∈ U2 ∧ ∀x ∈ X∃y ∈ Y(FinDif(x, y) ∧ x ≤ y).Íåñëîæíî âèäåòü, ÷òî ýòè îïðåäåëåíèÿ çàäàþò òðåáóåìóþ èíòåðïðåòàöèþ.Êîôèíàëüíîé ïîñëåäîâàòåëüíîñòüþ äëèíû ω äëÿ îðäèíàëà α íàçûâàåòñÿ ïðîèíäåêñèðîâàííàÿ íàòóðàëüíûìè ÷èñëàìè ïîñëåäîâàòåëüíîñòü α1 , α2 , .
. . òàêàÿ, ÷òî αi < αi+1 è α = sup{αi | i ∈ ω}. Òàê êàê ìûíå ðàññìàòðèâàåì êîôèíàëüíûõ ïîñëåäîâàòåëüíîñòåé äëèí îòëè÷íûõ îòω ìû áóäåì íàçûâàòü èõ ïðîñòî êîôèíàëüíûìè ïîñëåäîâàòåëüíîñòÿìè.Èìååòñÿ îáùåïðèíÿòàÿ ñèñòåìà êîôèíàëüíûõ ïîñëåäîâàòåëüíîñòåé äëÿîðäèíàëîâ èç Lim ìåíüøèõ ε0 . Äëÿ êàæäîãî íàòóðàëüíîãî ÷èñëà n èîðäèíàëà α ∈ Lim ñ êàíòîðîâñêîé íîðìàëüíîé ôîðìîé ω α1 + · · · + ω αkñëåäóþùèì îáðàçîì çàäàåòñÿ n-ûé ÷ëåí êîôèíàëüíîé ïîñëåäîâàòåëüíîñòè α[n]:1.
α[n] = ω α1 + · · · + ω αk−1 + ω β (n + 1), åñëè αk 6∈ Lim è αk = β + 1;2. α[n] = ω α1 + · · · + ω αk−1 + ω αk [n] , åñëè αk ∈ Lim.74Íà îñíîâå êîôèíàëüíûõ ïîñëåäîâàòåëüíîñòåé ââîäèòñÿ áèíàðíîå îòíîøåíèå R íà îðäèíàëàõ ìåíüøèõ ε0 :defαRβ ⇐⇒ β = α + 1 ∨ ∃n ∈ ω(α = β[n]).Íåñëîæíî âèäåòü, ÷òî òðàíçèòèâíîå çàìûêàíèåì áèíàðíîãî îòíîøåíèÿR ñîâïàäàåò ñî ñòàíäàðòíûì ïîðÿäêîì íà îðäèíàëàõ <.Ëîðåíîì Áðî [13] áûëî äîêàçàíî ñëåäóþùåå ïðåäëîæåíèå.Ïðåäëîæåíèå3.11.Ïðè âñåõ α∈[1, ε0 ) ðàçðåøèìà òåîðèÿTh((α; <, R)0 ).Ëåììà 3.12. ìîäåëè (α; R)0 èíòåðïðåòèðóåòñÿ ìîäåëü (α; <, ψ)0Äîêàçàòåëüñòâî. Äëÿ äîêàçàòåëüñòâà ëåììû íàì äîñòàòî÷íî âûðàçèòüîïåðàöèþ ψ â (ωα ; <, R)0 , íèæå ìû ñòðîèì òàêîå âûðàæåíèå. Ïóñòü β ∈ωα íåíóëåâîé îðäèíàë.
Ïîêàæåì, ÷òî ψ(β) åñòü âòîðîé îðäèíàë γòàêîé, ÷òî β Rγ . Ïóñòü êàíòîðîâñêàÿ íîðìàëüíàÿ ôîðìà β èìååò âèäβkω β1 +· · ·+ω βk−1 +ω· · + ω β}k , ãäå k, n ≥ 1 è β1 ≥ β2 ≥ . . . ≥ βk−1 > βk .| + ·{zn ñëàãàåìûõßñíî, ÷òî ψ(β) = ω β1 + · · · + ω βk−1 + ω βk +1 . Î÷åâèäíî èìååò ìåñòî β Rψ(β)è β R(β + 1). Îò ïðîòèâíîãî äîêàæåì, ÷òî äëÿ âñåõ γ ∈ (β + 1, ψ(β)) íåâûïîëíÿåòñÿ β Rγ . Ïðåäïîëîæèì γ ∈ (β + 1, ψ(β)) è β Rγ . Îðäèíàë γèìååò êàíòîðîâñêóþ íîðìàëüíóþ ôîðìóω β1 + · · · + ω βk−1 + |ω βk + ·{z· · + ω β}k +ω γ1 + · · · + ω γs , ãäå s ≥ 1 è βk > γ1 .n ñëàãàåìûõÈç îïðåäåëåíèÿ îòíîøåíèÿ R ñëåäóåò, ÷òî γ ∈ Lim è äëÿ íåêîòîðîãî nìû èìååì γ[n] = β .
Íîβkγ[n] = ω β1 + · · · + ω βk−1 + ω· · + ω β}k +ω γ1 + · · · + ω γs−1 + ω γs [n]| + ·{zn ñëàãàåìûõè ω γs [n] 6= 0. Òåì ñàìûì, γ[n] > β è ìû ïðèøëè ê ïðîòèâîðå÷èþ ñíàøèì ïðåäïîëîæåíèåì β Rγ . Ñëåäîâàòåëüíî, ψ(β) äåéñòâèòåëüíî ÿâëÿåòñÿ âòîðûì îðäèíàëîì γ òàêèì, ÷òî β Rγ .75 ñèëó äîêàçàííîãî â ïðåäûäóùåì àáçàöå, ÿñíî ÷òî äëÿ âñÿêèõβ, γ < ωα ðàâåíñòâî ψ(β) = γ âûïîëíåíî òîãäà è òîëüêî òîãäà, êîãäà(β = 0 → γ ∈ Lim ∧ ∀δ < γ(δ 6∈ Lim))∧(β 6= 0 → β Rγ ∧ ∃!δ < γ(β Rδ))Ñëåäîâàòåëüíî, ôóíêöèÿ ψ âûðàæàåòñÿ â (ωα ; <, R)0 , ÷òî çàâåðøàåò äîêàçàòåëüñòâî ëåììû.Èç ëåìì 3.9, 3.10, 3.12 è óòâåðæäåíèÿ 3.11, äîêàçàííîãî â [13], ìûïîëó÷àåìÒåîðåìà 6.Ïðè âñåõ α ∈ [2, ω) òåîðèÿ Th(WNα ; <0 , >, h0i, h1i, h2i) ðàç-ðåøèìà.3.3Ýëåìåíòàðíàÿ ýêâèâàëåíòíîñòü íåêîòîðûõ ìîäåëåé ýòîì ðàçäåëå ìû ïîêàæåì, ÷òî ñòðóêòóðû (WNω ; <0 , >, h0i, h1i, h2i) è(WN3 ; <0 , >, h0i, h1i, h2i) ýëåìåíòàðíî ýêâèâàëåíòíû.
Òåì ñàìûì ìû ïîêàæåì ðàçðåøèìîñòü Th(WNω ; <0 , >, h0i, h1i, h2i) è óñèëèì òåîðåìó 6. Äëÿýòîãî ìû âîñïîëüçóåìñÿ êëàññè÷åñêèì ðåçóëüòàòîì À. Ýðåíôîéõòà [17]îá ýëåìåíòàðíîé ýêâèâàëåíòíîñòè.Çàìå÷àíèå 3.13.Äàëåå ìû ðàññìàòðèâàåì ïîíÿòèÿ îðäèíàëà, ïàðû,ôóíêöèè è ïîñëåäîâàòåëüíîñòè â òåîðåòèêî-ìíîæåñòâåííîì ñòèëå.Ìû èñïîëüçóåì îðäèíàëû ïî ôîí Íåéìàíó α = {β | β < α}. Ìû èñïîëüçóåì ïàðû ïî Êóðàòîâñêîìó (x, y) = {{x}, {x, y}}.
Ìû ðàññìàòðèâàåì ôóíêöèè f , êàê ìíîæåñòâà ïàð {(x, f (x)) | x ∈ dom(f )}.Ìû ðàññìàòðèâàåì ïîñëåäîâàòåëüíîñòè haβ | β < αi, êàê ôóíêöèè{(β, aβ ) | β < α}.Ïóñòü A ñòðóêòóðà áåç ôóíêöèîíàëüíûõ ñèìâîëîâ â ñèãíàòóðå.Ìû îïðåäåëÿåì ìîäåëüHF(A)ñ ñèãíàòóðîé ðàñøèðÿþùåé ñèãíàòóðó76ìîäåëè A áèíàðíûì ïðåäèêàòíûì ñèìâîëîì ∈ è óíàðíûì ïðåäèêàòíûìñèìâîëîì Ur.
Ïóñòü óíèâåðñóìîì A ÿâëÿåòñÿ ìíîæåñòâî A. Íåêîòîðûìôèêñèðîâàííûì îáðàçîì âûáåðåì ìíîæåñòâî B ðàâíîìîùíîå A, íî íåñîäåðæàùåå êîíå÷íûõ ìíîæåñòâ è áèåêöèþ eA : A → B. Óíèâåðñóì ìî-äåëè HF(A) ýòî ìíîæåñòâî HF(B). Ìíîæåñòâî HF(B) ýòî ìèíèìàëüíîå ìíîæåñòâî òàêîå, ÷òî B ⊂ HF(B) è P <ω (HF(B)) ⊂ HF(B). Î÷åâèäíî,HF(B) ñóùåñòâóåò è åäèíñòâåííî. Îöåíêà âñÿêîãî ïðåäèêàòíîãî ñèìâîëàP(x1 , . . .
, xn ) èç ñèãíàòóðû A â ìîäåëè HF(A) òàêîâà:HF(A) |= P(a1, . . . , an)def⇐⇒ a1 , . . . , an ∈ B è−1A |= P(e−1A (a1 ), . . . , eA (an )).Äëÿ êàæäîãî a ∈ HF(B)HF(A) |= Ur(a)def⇐⇒ a ∈ B.Äëÿ êàæäîãî a1 , a2 ∈ HF(B)HF(A) |= a1 ∈ a2def⇐⇒ a2 6∈ B è a1 ∈ a2 .HF(A). Åñëè a ∈ HF(A) òàêîâ, ÷òîHF(A) |= Ur(a), òîãäà ìû íàçûâàåì a ∈ HF(A) óðýëåìåíòîì.Òåì ñàìûì, ìû îïðåäåëèëè ìîäåëüËåììà 3.14.Äëÿ âñÿêîãî α ∈ Lim ìîäåëü (ω α ; <, ψ)0 èíòåðïðåòèðó-åòñÿ â HF(α; <).Äîêàçàòåëüñòâî. Íåñëîæíî âèäåòü, ÷òîHF(α; <)óäîâëåòâîðÿåò âñåìàêñèîìàì òåîðèè ZF, êðîìå àêñèîìû áåñêîíå÷íîñòè è àêñèîìû îáúåìíîñòè.
Ïðè ýòîì HF(α; <) óäîâëåòâîðÿåò åñòåñòâåííîé ìîäèôèêàöèè àêñèîìû îáúåìíîñòè∀x, y(¬Ur(x) ∧ ¬Ur(y) ∧ ∀z(z ∈ x ↔ z ∈ y) → x = y).Ïîýòîìó, âHF(α; <)âûðàçèìû ïîíÿòèÿ èç çàìå÷àíèÿ 3.13 (ïî-äðîáíåå ñì. [6]).77Ïóñòü β ∈ ω α è åãî êàíòîðîâñêàÿ íîðìàëüíàÿ ôîðìà èìååò âèäω β1 + · · · + ω βn . Òîãäà åãî èíòåðïðåòàöèÿ β I ðàâíà êîíå÷íîé ïîñëåäîâàòåëüíîñòè (eα (β1 ), . . . , eα (βn )). ÂHF(α; <)ìíîæåñòâî âñåõ èíòåð-ïðåòàöèé îðäèíàëîâ îïðåäåëèìî, êàê ìíîæåñòâî âñåõ ìîíîòîííî íåâîçðàñòàþùèõ ïîñëåäîâàòåëüíîñòåé óðýëåìåíòîâ. Èíòåðïðåòàöèåé ìíîæåñòâà A ∈ P <ω (ω α ) ÿâëÿåòñÿ AI = {β I | β ∈ A}.
Ìíîæåñòâî âñåõèíòåðïðåòàöèé êîíå÷íûõ ìíîæåñòâ îðäèíàëîâ î÷åâèäíî îïðåäåëèìî âHF(α; <). Ïðåäèêàò ∈ èíòåðïðåòèðóåòñÿ òðèâèàëüíûì îáðàçîì. Ïðåäèêàò <I , èíòåðïðåòèðóþùèé <, çàäàåòñÿ, êàê ëåêñèêîãðàôè÷åñêèé ïîðÿäîê íà êîíå÷íûõ ïîñëåäîâàòåëüíîñòÿõ àòîìîâ. Çàäàäèì èíòåðïðåòàöèþψ ôóíêöèþ ψ I . ψ I ((eα (β1 ), . . . , eα (βn ))) ðàâíà ëåêñèêîãðàôè÷åñêè ìèíèìàëüíîé ïîñëåäîâàòåëüíîñòè, çàêàí÷èâàþùåéñÿ íà eα (βn + 1) è ëåêñèêîãðàôè÷åñêè áîëüøåé, ÷åì (eα (β1 ), .
. . , eα (βn )).Îïðåäåëèì ïîíÿòèå ω -õâîñòà îðäèíàëà α ñ êàíòîðîâñêîé íîðìàëüíîé ôîðìîé ω α1 + ω α2 + · · · + ω αn . Åñëè α < ω ω , òî ω -õâîñò α ñîâïàäàåò ñ α. Åñëè α ≥ ω ω , òî ω -õâîñòîì α áóäåò îðäèíàë ω ω +ω αk +· · ·+ω αn ,ãäå k ìèíèìàëüíîå íàòóðàëüíîå ÷èñëî òàêîå, ÷òî αi < ω äëÿ âñåõ i òàêèõ,÷òî k ≤ i ≤ n.Èçâåñòåí ðåçóëüòàò À. Ýðåíôîéõòà î ýëåìåíòàðíîé ýêâèâàëåíòíîñòè ìîäåëåéHF(α1; <) è HF(α2; <) äëÿ α1è α2 ó êîòîðûõ ñîâïàäàåòω -õâîñò [17].
Çàìåòèì, ÷òî ïðè α ∈ [2, ω] ó âñåõ ωα ñîâïàäàþò ω -õâîñòû.Çàìåòèì, ÷òî ïåðåâîäû ôîðìóë, èçâëåêàåìûå èç äîêàçàòåëüñòâëåìì 3.9, 3.10 è 3.14, íå çàâèñÿò îò ïàðàìåòðîâ ïàð òåîðèé. Îòñþäà èëåììû 3.14 ïîñëåäîâàòåëüíî âûâîäÿòñÿ ñëåäóþùèå ñëåäñòâèÿ:Ñëåäñòâèå 3.15.Äëÿ âñÿêèõ α1 , α2 ∈ [3, ω] ìîäåëè (ωα1 ; <, ψ)0 è(ωα2 ; <, ψ)0 ýëåìåíòàðíî ýêâèâàëåíòíû.Ñëåäñòâèå 3.16.Äëÿ âñÿêèõ α1 , α2 ∈ [3, ω] ìîäåëè (ωα1 ; <, ψ)+ è(α2 ; <, ψ)+ ýëåìåíòàðíî ýêâèâàëåíòû.78Ñëåäñòâèå3.17.Ïóñòü îðäèíàë α∈[3, ω].
Òîãäà ìîäåëèN(WNα ; <0 , >, h0i, h1i, h2i) è (W3 ; <0 , >, h0i, h1i, h2i) ýëåìåíòàðíî ýêâèâà-ëåíòíû.Èç ñëåäñòâèÿ 3.17 è òåîðåìû 6 ìû çàêëþ÷àåì ñëåäóþùóþ óñèëåííóþ âåðñèþ òåîðåìû 6:Òåîðåìà 7.Äëÿ âñåõ îðäèíàëîâ α òàêèõ, ÷òî 2 ≤ α ≤ ω òåîðèÿTh(WNα ; <0 , >, h0i, h1i, h2i) ðàçðåøèìà.79Ëèòåðàòóðà[1] Å.Â. Äàøêîâ. Î ïîçèòèâíîì ôðàãìåíòå ïîëèìîäàëüíîé ëîãèêè äîêàçóåìîñòè GLP.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
