1611678200-36438fb4f1ee6f855c93dc4a315ea8eb (826633), страница 34
Текст из файла (страница 34)
Тогда Q(-теория сигнатуры Е, S:В1Е -<S:В-I Е.б). Любая алгебраическая система Q( имеет некоторую скулемизацию Qt 8 .До к аз ат ель ст в о.а) следует непосредственно из предложения5.1.4. Докажем б). Если Ф=:3Ф(х,xi, ... , хп),то для а1, ... , an Е Аберем в качестве значения v 21 (JФ)(a,, ... ,an) элемент ао Е А, длякоторого Qt F Ф(ао, ai, ...
, ап), если такой ао Е А существует, и произвольный элемент а Е А, если такой ао не существует.Из предложения5.3.2сразу получается теоремаS:В в этой теореме нужно взять s:811 Е,где s:81 -D5.1.9.В качествеподсистема Qt 8 ,порожденная множеством Х.Скулемизация позволяет <<убирать» кванторы у формул старой сигнатуры Е. Однако в формулах новой сигнатуры Е 8 они <<остаются>>.Чтобы избежать этого неудобства, «замкнем,> процесс скулемизации.§ 5.4.Механизм совместностиОпределение. Пусть :Есигнатура и Т-:Е. Определим сигнатуры :Ens и теории тns,1;os =:Ecs =:Е, тоsU=Т,I;(n+l)S = (:Ens)s,:Ens (теория тсs= Uт(n+l)S163- теория сигнатурыn Е w, по индукции:=(Tns)s.
Сигнатуратns) называется полной скулемиза-nEwnЕwцией сигнатуры :Е (теории Т). Алгебраическая система21cs сигнату-ры :Ecs называется полной скулемизацией системы 21 сигнатуры :Е,если21csr :Е = 21 и 21csПредложение- модель (Th(21) )cs.5.3.3.а). Любая алгебраическая системанекоторую полную скулемизациюб}. Пусть Т21имеет21cs.непротиворечивая теория сигнатуры :Е. Тогда-теория тсs является универсально аксиоматизируемым модельнополным расширением Т и для любой моделимодель211 теории тсs такая что 21121r :Е = 21.теории Т существуетДоказательство.
а). В силу предложения 5.3.2,б} существуюттакие системы 21пs,21° 8 = 21 и 21Cп+l)S является скулемизасистема сигнатуры :EcS, где 1/Q(cSна символах из :Ens_ Ясно, что 21cs будет полнойnцией 21пs. Пусть 21csсовпадает сvQ!nsскулемизациейЕ w, что= (А,1/Q(cS)21.б}. Пусть 21 - модель тсs сигнатуры :Ecs и S:В <:;:; 21. Из предложения 5.3.2, а) получаем, ЧТО S:В :EnS --< 21 1;ns для любого n Е w.Так как :Ecs = UnEw 1;ns, то получаем S:В --< 21.
Следовательно, тсsмодельно полна и в силу теоремы 5.2.7 класс K'f:.cs (тсs) является\f-аксиоматизируемым, т. е. K'E,cS (тсs) = K'E,cS (Z), где z - множество\!-предложений сигнатуры :Ecs_ Тогда Z - система аксиом для тсs.rrВторое утверждение в б} следует из а).DУпражнение1.Показать, что для того чтобы, все скулемизации системы21былиэлементарно эквивалентными, необходимо и достаточно, чтобы21было одноэлементно. {Указание.
Рассмотреть различные значенияvQ! 8(/Ф) для Ф = Эvo(vo ~ vo А v1 ~ v1).)§ 5.4.Механизм совместностиМеханизм совместности имеет, в основном, методическое значение.Он позволяет выделить общую часть в многих теоремах, доказательство которых связано с построением моделей. В этом параграфе мыдокажем несколько таких теорем. Всюду в дальнейшем предполагается,что сигнатура :Е имеет конечную или счетную мощность.6*Гл.164Теория моделей5.Определение.
Для формулы Ф сигнатуры :Е определим формулу Ф·следующим образом:1) если Ф - атомарная формула,2) (·Ф)· = Ф,3) (Ф1 - t Ф2)· = Ф1 Л 'Ф2,4) (Ф1 Л Ф2)·5) (Ф1 V Ф2)·6) (:JхФ) •7) (VхФ)·то Ф'=·Ф,= 'Ф1 V 'Ф2,= 'Ф1 Л ·Ф2,= Vx· Ф,= :Jх·Ф.Из определения Ф' видно, что Ф'натуру, полученную из сигнатуры :Е= ·Ф.=Обозначим через :Ее сиг(R, F, µ)добавлением счетногомножества С новых констант. Константу сигнатуры :Ее и терм видаf(c,, ... ,cn),где с,,...
,спЕ С иfЕбудем называть базиснымF,термом сигнатуры :Ее.Определение. МножествоSконечных или счетных множеств предложений сигнатуры :Ее называется механизмом совместности сигнатуры :Е, если для каждогоs(С 1) включениеs не имеет места ни для какого предложе{ Ф, ·ф} ~ЕSвыполняются следующие условия:ния Ф;(С2) ·ф Еs ==> (s U {Ф·} ~ s, для некоторого s, Е S);s ==> (s U {Ф} ~ s, или s U {'Ф} ~ s, для некоторогоЕ S);(С4) Ф Л Ф Е s ==> (sU {Ф} ~ s, и sU {Ф} ~ s2 для некоторых s1,s2 ЕЕ S);(С5) Ф V Ф Е s ==> (s U {Ф} ~ s, или s U {Ф} ~ s 1 для некоторого s, ЕЕ S);(Сб) \lхФ Е s ==>(для любого с Е С существует такое s, Е S, что s U(СЗ) Фs,-tФ ЕU {(Ф)n ~ s,);s ==> (s U {(Ф)~} ~ s, для некоторого с Е С и некоторого(С7) :JхФ Еs,s,Е S);(С8) (с1,с2 Е С и с,~ с2 ЕЕs) ==> (s U {с2 ~с,}~ s, для некоторогоS);(С9} если с Е С ибазисный терм сигнатуры :Ее, то выполняютсяt -два условия:а)s U {dб} {с~Множество~t}~t, (Ф)f}Ss,~для некоторогоdЕ С и некоторогоs,ЕS,s ==> (s U {(Ф)~} ~ s, для некоторого s, Е S).будем называть механизмом совместности, если оноявляется механизмом совместности некоторой сигнатуры :Е.Механизм совместности§ 5.4.ПредложениенатурыI;_Пусть Т5.4.
t.Тогда множествожений сигнатуры165непротиворечивая теория сиг-таких конечных множествs предлоI;c, что Т U s совместно, является механизмомSсовместности.До к аз ат ель ст в о.ныхусловийПроверим условие (С7).оставляемчитателювкачествеПроверку остальлегкогоупражнения.Пусть множество Т U s U {(Ф)n несовместно для константы с Е С,не входящей в элементы s U { Ф}, и D - доказательство секвенции(Ф);: f-W1, ...
, Wn,Jгде{W1, ... , Wn} <:: :ТU s.Используя обычный прием: заменяя константу с во всех секвенциях изу,не встречающуюся в элементахD,Dна переменнуюполучаем доказательствоDiW1, ... , Wп, ( Ф )~ f- J. Применяя правило 16, получаем доказуемость W1, ... , Wn, :3у(Ф)~ f- J. Так как :3хФ и :3у(Ф)~ конгруэнтны,то множество Т U s несовместно, если :3хФ Е s.ОсеквенцииПредложениеа). {Ф, Ф-,5.4.2.W} <:: : sПусть==}S -механизм совместности и(s U {W} <:: : s1в).Е С и {с~d, dS).{s' s' <:: : s Е S} -торогог).S'=si~ е}<:: : s)==}siЕsi Е S).S, что s U {с~S.для некоторогоб). Для любого с Е С существует такое<:: : S[.(c,d,eЕs(s U {с~е}<:: : s1с}<:::::для некоЕ1механизм совместности.Доказательство.
г) очевидно, а) следует из (СЗ) ив) сле(Cl),дует из (С9), б), если в качестве Ф взять х ~ е, а в качествеt -константу d. Докажем б). В силу (С9),а) имеем sдлянекоторой константы d Е С иs1U {d~с}<:::::Е S. Из (С8) получаем s~d} <:: : s1 для некоторого s1 Е S. Теперь применяемs U {d ~ с,с ~ d,c ~с}<::::: s1, для некоторого s1 Е S.s1U {d ~с, с~в) и получаемОАлгебраическую систему Qt сигнатуры I;c назовем канонической,если vщ ( С) = А, т. е. любой элемент а Е А является значением некоторой константы с Е С.Теорема5.4.3.ЕслиS -механизм совместности сигнатурыI;и s* Е S, то s* имеет каноническую модель Qt сигнатуры I;c_Доказательство.торый по предложениюРассмотрим класс5.4.2, г)S'= {s' <:: : s I sПустьФо,Ф1,ЕS},коявляется механизмом совместности....
,Фn,···(nЕш)- нумерация всех предложении сигнатуры I;c иto, t 1, ... , tп, . . . (nЕw)Гл.166Теория моделей5.- нумерация всех базисных термов сигнатуры Ее. Индукцией поп Е wбудем строить последовательностьSO ~элементовS'.Полагаем so~S[= s*.~ Sn ~ ......Если п= Зk,то по (С9), а) находимS', и полагаем sn+l = sn UU {с~ tk}. При п = Зk + 1 полагаем Sn+I = sn U {Фk}, если sn U {Фk} ЕЕ S', и sn+l = Sn в противном случае. Пусть п = Зk + 2. Если Фk == ЭхФ и Фk Е Sn, то полагаем Sn+I = Sn U {(Ф)~} Е S' для некоторойтакую константу с Е С, что SnU {с~tk} Ес Е С. В противном случае полагаем sn+I= USw= Sn.Рассмотрим множествоsn.
Из построения Sw вытекает следующий факт:nEw( *) одноэлементное множество {Sw} является механизмом совместности.На множестве С определим отношениеС"'dС~{=}В силу (С8) и предложения5.4.2, б),d"':Е Sw.в) отношениевивалентностью на множестве С. На множестве Аэквивалентности по отношениюинтерпретациюv 21 (f)(ct, ... , с;,.)= с= (R, ре, µе)гдеfЕре, r ЕR, µe(f)с~{=}(ci, ... ,c;,.) Е v 21 (r){сIс -класссодержащий с Е С} определяем"',v 21 сигнатуры Ееявляется эк"'={=}следующим образом:f (с1, ...
, Сп)r(c1, ... ,cn) ЕЕSw,Sw,= µe(r) = п. Из (*) и (С9),б) следует,что эти определения корректны. Пусть, например, с1 ~f(c2, сз), с4 ~cs и сз ~ Cf, принадлежат Sw. Применяя (*) и (С9), б),получаем С4 ~ f(c2, Сб) Е Sw. Еще два раза применяя (*) и (С9), б),получаем с4 ~ f (c2, сз) Е Sw и С4 ~ с1 Е Sw.~f(cs,Сб), с2 ~Так как v21 (c)= с дляс Е С, то Q(=(А, v21 ) является каноническойсистемой.
Покажем теперь, что для любого предложения Ф сигнатурыЕе имеет место(5.5)Отсюда будет вытекать,базисного термаt,что Q( -с Е С, Фмодель s*.= r(c1, ... ,cn)дляЕсли ФrЕR,=С\,с ~ t для... ,сп Е С,или Ф есть отрицание таких формул, тоv 21 , (*) иизпо~t(*)(*)(Cl). Если t ~ с Еи (С9), а) получаеми (С9), б) имеем~ с Е Sw, гдеt -ddSw,~t(5.5) следует из определенияt - базисный терм, с Е С, тоSw для некоторого d Е С.