Диссертация (1104034), страница 8
Текст из файла (страница 8)
∃yk−1 ∈ Bk−1 ∩ Wα ((A = hk (A) u yk−1 u . . . u y0 )∧ (x = dk (hk (A)) u yk−1 u . . . u y0 )).Ïîðÿäîê <k îïðåäåëÿåòñÿ ÷åðåç ôóíêöèþ dk :A <k B ⇐⇒ B 4 dk (A).487. Èç ïóíêòà 6 ýòîãî ïðåäëîæåíèÿ è ëåììû 2.19 ñëåäóåò, ÷òî â ðàññìàòðèâàåìîé ìîäåëè ïðè k < α ìíîæåñòâî WNk ìîæåò áûòü îïðåäåëåíîñëåäóþùèì îáðàçîì:A ∈ WNk ⇐⇒ A <0 dk+1 (>).Ïðè k = α ìíîæåñòâî WNk îïðåäåëèìî òàê êàê ñîâïàäàåò ñî âñåì óíèâåðñóìîì.Ëåììà 2.21.[9, ëåììà 3.3] Ïóñòü α, β è γ îðäèíàëû. Åñëè β < αè γ < ω `(α) , òî β + γ < α.Äîêàçàòåëüñòâî. Äîêàæåì, ÷òî åñëè β < α, òî β + ω `(α) ≤ α èçýòîãî ôàêòà ñëåäóåò èñêîìîå. Ïóñòü β < α è êàíòîðîâñêàÿ íîðìàëüíàÿôîðìà α èìååò âèä ω α1 + · · · + ω αn−1 + ω αn . Åñëè β < ω α1 + · · · + ω αn−1 ,òî äîêàçûâàåìîå î÷åâèäíî.
Òàêèì îáðàçîì, ìû áóäåì ñ÷èòàòü, ÷òî β =ω α1 + · · · + ω αn−1 + γ , ãäå îðäèíàë γ òàêîâ, ÷òî 0 < γ < ω αn . Ïóñòüêàíòîðîâñêàÿ íîðìàëüíàÿ ôîðìà îðäèíàëà γ èìååò âèä ω γ1 + · · · + ω γm .Çàìåòèì, ÷òî γ1 < αn , à ñëåäîâàòåëüíî ñóùåñòâóåò òàêîé îðäèíàë δ ≥ 1,÷òî γ1 + δ = αn . Òàêèì îáðàçîì, èìåþò ìåñòî ñëåäóþùèå ñîîòíîøåíèÿ:γ + ω `(α) = ω γ1 + · · · + ω γm + ω γ1 +δ ≤ ω γ1 · m + ω γ1 · ω δ= ω γ1 · (m + ω δ ) = ω γ1 · ω δ = ω αn ,β + ω `(α) = ω α1 + · · · + ω αn−1 + γ + ω `(α) ≤ ω α1 + · · · + ω αn−1 + ω αn = α.Èç ïðåäëîæåíèÿ 2.1 è îïðåäåëåíèÿ N F âûòåêàåòËåììà 2.22.Ïóñòü ñëîâà A1 , . . .
, An òàêîâû, ÷òî A1 , . . . , An ∈ Sk+1 ∩NF. Òîãäà A1 kA2 k . . . kAn ∈ NF, åñëè è òîëüêî åñëè ok+1 (A1 ) ≤ ok+1 (A2 ) ≤. . . ≤ ok+1 (An ).Ïðîñòîé ïðîâåðêîé ìû ïîëó÷àåì49Ëåììà 2.23.Ïóñòü íàòóðàëüíûå ÷èñëà n ≥ 1, k, ñëîâî A ∈ Sk \ {>}è ñëîâà A1 ∈ Sk+1 , . . . , An ∈ Sk+1 òàêîâû, ÷òî A = A1 k . . . kAn . Òîãäà äëÿâñÿêîãî m îò 1 äî n èìååò ìåñòî ok (A) = ok (Am k . . . kAn ) + ω ok+1 (Am−1 ) +· · · + ω ok+1 (A1 ) .Ëåììà 2.24.Äëÿ âñÿêîãî îðäèíàëà α ≤ ω è íàòóðàëüíîãî ÷èñëà k < αñóùåñòâóåò ôîðìóëà Inαk (x, y) ÿçûêà ïåðâîãî ïîðÿäêà ìîäåëè Sα , îáëàäàþùàÿ ñëåäóþùèìè ñâîéñòâàìè:1. Äëÿ âñÿêîãî B ∈ Sk ∩ WNα ñóùåñòâóåò ëèøü êîíå÷íîå ÷èñëî A ∈αSk+1 ∩ WNα , äëÿ êîòîðûõ â Sα âûïîëíÿåòñÿ Ink (A, B).2. Äëÿ âñÿêîãî êîíå÷íîãî ìíîæåñòâà A ⊂ Sk+1 ∩ WNα ñóùåñòâóåòB ∈ S k ∩ WNα òàêîå, ÷òî âñÿêîå A ∈ Sk+1 ïðèíàäëåæèò A òîãäàè òîëüêî òîãäà, êîãäà Sα |= Inαk (A, B).Äîêàçàòåëüñòâî.
Îïðåäåëèì Inαk (x, y):Inαk (x, y) y 6= > ∧ ∃z ∈ Sk ∩ WNα (hk+1 (z) = x ∧ z ≤k y <k (x u dk (z))).Óñòàíîâèì, ÷òî äëÿ âñÿêîãî ñëîâà B ∈ Sk ∩ WNα âèäà A1 k . . . kAn ,ãäå Ai ∈ Sk+1 ∩ WNα ïðè i îò 1 äî n, èìååò ìåñòî ðàâåíñòâî {A ∈ Sk+1 ∩ NF |Inαk (A, B)} = {A1 , . . . , An }. Çàìåòèì, ÷òî îòñþäà ñëåäóåò âûïîëíåíèå îáîèõ óñëîâèé íà ïðåäèêàò. Òåïåðü äîêàæåì òðåáóåìîå ïðåäëîæåíèå. ÅñëèB = >, òî îáà ìíîæåñòâà ïóñòû. Ïîêàæåì, ÷òî â ñëó÷àå B 6= > äëÿâñÿêîãî A ∈ Sk+1 ∩ WNα ìû èìååìA ∈ {A1 , . .
. , An } ⇐⇒ Sα |= Inαk (A, B).⇒: Ïóñòü A ∈ {A1 , . . . , An }. Ïîêàæåì, ÷òî Inαk (A, B). Ïóñòü m ìèíèìàëüíûé èíäåêñ èç {1, . . . , n} òàêîé, ÷òî A = Am .  êà÷åñòâå ñëîâà z ,âîçüìåì ñëîâî C = Am k . . . kAn . Òàêèì îáðàçîì, òðåáóåòñÿ äîêàçàòü, ÷òîhk+1 (C) = A, C ≤k B è B <k (A u dk C). Âûïîëíåíèå ïåðâûõ äâóõ óñëîâèéî÷åâèäíî.  ñèëó ëåììû 2.22 è ìèíèìàëüíîñòè m äëÿ âñÿêîãî i îò 1 äîm − 1 ìû èìååì ok+1 (Ai ) < ok+1 (Am ). Ñëåäîâàòåëüíî, ó÷èòûâàÿ ëåììó2.21, ìû ïîëó÷àåì ok (B) = ok (Am k . .
. kAn ) + ω ok+1 (Am−1 ) + · · · + ω ok+1 (A1 ) <50ok (Am k . . . kAn ) + ω ok+1 (Am ) = ok (Am kC) = ok (A u dk (C)). Òàêèì îáðàçîì,âûïîëíÿåòñÿ îñòàâøååñÿ óñëîâèå B <k (A u dk (C)).⇐: Âîçüìåì ñëîâî A ∈ (Sk+1 ∩ WNα ) \ {A1 , . . . , An } è äîêàæåì, ÷òîíå âûïîëíÿåòñÿ Inαk ([A]∼ , [B]∼ ). Ïðåäïîëîæèì ïðîòèâíîå. Òàêèì îáðà-çîì, ñóùåñòâóåò ñëîâî C ∈ Sk ∩ WNα òàêîå, ÷òî hk+1 (C) = A, C ≤k Bè B <k (A u dk (C)).
 ñèëó ëåììû 2.22 ñóùåñòâóåò íàòóðàëüíîå ÷èñëîs ≤ n òàêîå, ÷òî ∀i ≤ s(ok+1 (Ai ) < ok+1 (A)), à ∀i > s(ok+1 (Ai ) > ok+1 (A)).Ïîñêîëüêó C ≤k B è ok (C) ≥ ok (A), ìû èìååì ok (A) ≤ ok (B). Ñëåäîâàòåëüíî, A ≤k+1 An è òåì ñàìûì s < n. Ðàçáåðåì âîçìîæíûå âàðèàíòûñðàâíåíèÿ ok (C) è ok (As+1 k . . . kAn ):1. ok (C) < ok (As+1 k . .
. kAn ). Ó÷èòûâàÿ, ÷òî `(ok (As+1 k . . . kAn )) =ok+1 (As+1 ) è ëåììó 2.21, ìû èìååì ok (A ∧ hkiC) = ok (C) + ω ok+1 (A) <ok (As+1 k . . . kAn ) ≤ ok (B). Òåì ñàìûì ìû ïðèøëè ê ïðîòèâîðå÷èþ ñ óñëîâèåì B <k (A u dk (C)).2. ok (C) = ok (As+1 k . . . kAn ).  ýòîì ñëó÷àå ìû èìååì A =hk+1 (C) = hk+1 (As+1 k . .
. kAn ) = As+1 , íî A ∈ (Sk+1 ∩ WNα ) \ {A1 , . . . , An } ïðîòèâîðå÷èå.3. ok (C) > ok (As+1 k . . . kAn ). Ó÷èòûâàÿ ëåììó 2.21 è òî, ÷òî`(ok (C)) = ok+1 (A), ìû ïîëó÷àåì ok (B) = ok (As+1 k . . . kAn ) + ω ok+1 (As ) +· · · + ω ok+1 (A1 ) < ok (C), à ýòî ïðîòèâîðå÷èò óñëîâèþ C ≤k B.Òàêèì îáðàçîì, íè îäèí èç ñëó÷àåâ íå âîçìîæåí è ìû ïðèøëè êïðîòèâîðå÷èþ, ÷òî çàâåðøàåò äîêàçàòåëüñòâî ëåììû.2.4Íåðàçðåøèìûå òåîðèè ýòîì ðàçäåëå ìû äîêàæåì íåðàçðåøèìîñòü ýëåìåíòàðíûõ òåîðèé ìîäåëåé Sα äëÿ âñåõ îðäèíàëîâ α òàêèõ, ÷òî 2 ≤ α ≤ ω .Ìîäåëè è èíòåðïðåòàöèè.Íàìè áóäóò ðàññìàòðèâàòüñÿ ìíîãîñîðòíûå ìîäåëè.
Ìû ïîëàãàåì, ÷òîìíîãîñîðòíàÿ ñèãíàòóðà σ ñîñòîèò èç1. êîíå÷íîãî ìíîæåñòâà ñîðòîâ îáúåêòîâ T = {t1 , . . . , tn };512. ìíîæåñòâ ïðåäèêàòíûõ ñèìâîëîâ Pred è ôóíêöèîíàëüíûõ ñèìâîëîâFun;3. ôóíêöèè PType ñîïîñòàâëÿþùåé êàæäîìó ïðåäèêàòíîìó ñèìâîëóP ∈ Pred êîíå÷íóþ ïîñëåäîâàòåëüíîñòü (s1 , . . . , sk ) ýëåìåíòîâ T;4. ôóíêöèè FType ñîïîñòàâëÿþùåé êàæäîìó ôóíêöèîíàëüíîìó ñèìâîëó f ∈ Fun ïàðó h(s1 , . . . , sk ), ri, ïåðâûé ýëåìåíò êîòîðîé ÿâëÿåòñÿêîíå÷íîé ïîñëåäîâàòåëüíîñòüþ ýëåìåíòîâ T, à âòîðîé ýëåìåíòîì T;Âî âñåõ ïðèìåðàõ, êîòîðûå âñòðå÷àþòñÿ â ýòîé äèññåðòàöèè ñèãíàòóðûñ÷åòíû è äîïóñêàþò ýôôåêòèâíîå çàäàíèå (âñå ìíîæåñòâà, î êîòîðûõèäåò ðå÷ü â îïðåäåëåíèå ñèãíàòóðû ðàçðåøèìû, à ôóíêöèè ðåêóðñèâíû).Ïîýòîìó äàëåå ìû âñåãäà, ðàññìàòðèâàÿ íåêîòîðóþ ñèãíàòóðó, ïðåäïîëàãàåì, ÷òî îíà ýôôåêòèâíî çàäàíà íè÷åãî äîïîëíèòåëüíî íå îãîâàðèâàÿ.Ìîäåëü A ñèãíàòóðû σ ñîñòîèò èç ñåìåéñòâà èãðàþùèõ ðîëü ïðåäìåòíûõ îáëàñòåé ìíîæåñòâ At , ãäå t ïðîáåãàåò T, îöåíîê I(P ) ïðåäèêàòíûõ ñèìâîëîâ P ∈ Pred è îöåíîê I(f ) ôóíêöèîíàëüíûõ ñèìâîëîâf ∈ Fun .
Ïóñòü P ∈ Pred è PType(P ) = (s1 , . . . , sk ). Òîãäà I(P ) ýòîïîäìíîæåñòâî As1 × . . . × Ask . Ïóñòü f ∈ Fun, FType(f ) = h(s1 , . . . , sk ), ri.Òîãäà I(f ) ýòî ôóíêöèÿ As1 × . . . × Ask → Ar .Äëÿ êàæäîãî ñîðòà ti ∈ T ìû îáîçíà÷àåì ñèìâîëàìè xti , y ti , z ti . . .ïåðâîïîðÿäêîâûå ïåðåìåííûå ýòîãî ñîðòà. Åñòåñòâåííûì îáðàçîì ââîäÿòñÿ ìíîãîñîðòíûå ôîðìóëû ïåðâîãî ïîðÿäêà ñ ðàâåíñòâîì äàííîéìíîãîñîðòíîé ñèãíàòóðû.
Òàêæå åñòåñòâåííûì îáðàçîì ââîäèòñÿ ïîíÿòèå èñòèííîñòè ýòèõ ôîðìóë â ìîäåëÿõ ýòîé ñèãíàòóðû.Äëÿ êëàññà ìîäåëåé A íåêîòîðîé ñèãíàòóðû σ ìû îáîçíà÷àåì÷åðåç Th(A) ýëåìåíòàðíóþ òåîðèþ ýòîãî êëàññà ìîäåëåé ìíîæåñòâî âñåõ ïåðâîïîðÿäêîâûõ ïðåäëîæåíèé ñèãíàòóðû σ èñòèííûõ âî âñåõìîäåëÿõ A ∈ A.  ýòîé äèññåðòàöèè ìû ïðèäåðæèâàåìñÿ òåîðåòèêîìîäåëüíîãî âçãëÿäà íà òåîðèè ïåðâîãî ïîðÿäêà. Ìû íàçûâàåì ìíîæåñòâî ôîðìóë ïåðâîãî ïîðÿäêà ñèãíàòóðû σ òåîðèåé, åñëè îíî ÿâëÿåòñÿýëåìåíòàðíîé òåîðèåé íåêîòîðîãî êëàññà ìîäåëåé A ñèãíàòóðû σ .
Äëÿ52ìîäåëè A åå ýëåìåíòàðíàÿ òåîðèÿ ýòî òåîðèÿ Th({A}).Ìû ãîâîðèì, ÷òî òåîðèÿ ðàçðåøèìà, åñëè îíà ÿâëÿåòñÿ ðàçðåøèìûì ìíîæåñòâîì ôîðìóë.Ìû äëÿ äîêàçàòåëüñòâà ðÿäà ôàêòîâ î ðàçðåøèìîñòè è íåðàçðåøèìîñòè òåîðèé èñïîëüçóåì ìåòîä èíòåðïðåòàöèé [30, 3]. Ìû â öåëîìñëåäóåì òåðìèíîëîãèè èíòåðïðåòàöèé Â. Õîäæåñà [21, ãëàâà 5]. Ðàññìàòðèâàåìûå íàìè â ýòîì ðàçäåëå èíòåðïðåòàöèè îòëè÷àþòñÿ îò èñïîëüçóåìûõ Â.
Õîäæåñîì òåì, ÷òî ìû ðàáîòàåì ñ ìíîãîñîðòíûìè ìîäåëÿìèè îãðàíè÷èâàåìñÿ îäíîìåðíûìè èíòåðïðåòàöèÿìè. Êðàòêî îïèøåì ñâÿçàííûå ñ ýòîé òåõíèêîé ïîíÿòèÿ â òðåáóåìîì íàì ñëó÷àå. Ïóñòü äàíûñèãíàòóðû σ1 è σ2 . Èíòåðïðåòàöèÿ Γ ñîñòîèò èç:1. ôóíêöèè i, ñîïîñòàâëÿþùåé êàæäîìó ñîðòó t èç σ2 ñîðò i(t) ñèãíàòóðû σ1 , â êîòîðîì áóäóò èíòåðïðåòèðîâàòüñÿ îáúåêòû ñîðòà t;2. ôîðìóë Ut (xi(t) ) ñèãíàòóðû σ1 , çàäàþùèõ îáëàñòè èíòåðïðåòàöèéîáúåêòîâ òèïà t è ôîðìóë Eqt (xi(t) , y i(t) ) ñèãíàòóðû σ1 , èíòåðïðåòèðóþùèõ ðàâåíñòâî äëÿ âñåõ ñîðòîâ t èç σ2 ;i(s1 )3. ñåìåéñòâà ôîðìóë P I (xki(sk ), . . .
, xk) ñèãíàòóðû σ1 , ãäå P ïðîáåãàåòPredσ2 è PTypeσ2 (P ) = (s1 , . . . , sk );i(s1 )4. ñåìåéñòâà ôîðìóë Intf (xki(sk ), . . . , xk, y i(r) ) ñèãíàòóðû σ1 , ãäå f ïðî-áåãàåò Funσ2 è FTypeσ2 (P ) = h(s1 , . . . , sk ), ri (äîïóñêàÿ âîëüíîñòü, ìûi(s1 )áóäåì çàïèñûâàòü ýòè ôîðìóëû êàê f I (xki(sk ), . . . , xk) = y i(r) ).Êîãäà ìû ñòðîèì èíòåðïðåòàöèè, åñëè ìû íå îãîâàðèâàåì èíîãî, òîìû ñ÷èòàåì, ÷òî èíòåðïðåòàöèè ðàâåíñòâ Eqt (xi(t) , y i(t) ) ýòî ïðîñòîxi(t) = y i(t) ; òàêèå èíòåðïðåòàöèè ðàâåíñòâ ìû íàçûâàåì àáñîëþòíûìè.Èíòåðïðåòàöèÿ Γ îäíîçíà÷íî çàäàåò trΓ : F 7−→ F? ïåðåâîä ôîðìóëñèãíàòóðû σ2 â ôîðìóëû ñèãíàòóðû σ1 ; ìû íå ïðèâîäèì çäåñü òî÷íîãîçàäàíèÿ trΓ , åãî ïîñòðîåíèå àíàëîãè÷íî ïîñòðîåíèþ ïåðåâîäà ôîðìóë èç[21, ãëàâà 5].
Ïóñòü T1 òåîðèÿ ñèãíàòóðû σ1 è T2 òåîðèÿ ñèãíàòóðû σ2 .Ìû ãîâîðèì, ÷òî Γ ÿâëÿåòñÿ èíòåðïðåòàöèåé T2 â T1 , åñëè äëÿ âñÿêîéF ∈ T2 ìû èìååì F? ∈ T1 .53Ïóñòü åñòü ìîäåëü A ñ óíèâåðñóìàìè A1 , . . . , An . Ìû ãîâîðèì, ÷òîâ ìîäåëè A îïðåäåëèìî ìíîæåñòâî S ⊂ As1 × . . . × Ask , åñëè èìååòñÿôîðìóëà F(xs11 , xs22 , . . .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
