1611678200-36438fb4f1ee6f855c93dc4a315ea8eb (826633), страница 35
Текст из файла (страница 35)
ТогдаСледовательно, Q( р t ~ с. ПустьгдеЕ~ с Е Sw.базисный терм, с Е С. Если в Q( ложно~t~ с,§ 5. 4.Механизм совместностито по определению Qt имеем с~167(*) и (С9), б) получаем5.4.2, б) это противоречит (Cl).истинность (5.5), если Ф - атомарноеtЕ Sw. Из~с~ с Е Sw. В силу(*) и предложенияТаким образом, мы показалипредложение или отрицание атомарного и число п( Ф) символов сигнатуры Е, входящих в Ф, не больше1.Пусть Ф Е> 1.предложение или отрицание атомарного и п( Ф)базисный термФ. По свойствамимеем d ~С.
ИзtЕt .j. С, входящий вsw для некоторого d Еформула Ф1, полученная из Ф заменойп(Ф 1 )<tнаатомарноеsw -Тогда существуети (С9), а)(*)и (С9), б) следует, что(*)d, принадлежит Sw. Так какп(Ф), то по индукционному предположению Ф истинно в Qt.Для остальных предложений Ф сигнатуры Ее утверждениечается непосредственно изОпределение.
Множествополу(5.5)и (С2)-(С7) индукцией по длине Ф.(*)SDконечных или счетных множеств предложений сигнатуры Ее называется механизмом совместности сигнатуры Е без равенства, еслиSудовлетворяет условиямпредложения, входящие в элементыТеорема5.4.4.ций и констант,S,(Cl)-(C7)ине содержат равенства.Пусть сигнатура Е не содержит символов функмеханизм совместности сигнатуры Е безS -равенства. Тогда любоеs*ЕSимеет каноническую модель сигнатуры Ее.До к аз ат ель ст в о.и классS'= {s U Х I sРассмотрим множество ХЕОчевидно, чтоS}.совместности сигнатуры Е.
По теоремеS'= {смножество5.4.3~ сIс ЕС}является механизмомs* U Химеетканоническую модель сигнатуры Ее.DСледующая теорема является обобщением теоремыкоторое5.4.3,нам понадобится в дальнейшем.ТеоремаЕ,Xi, iЕ5.4.5.ПустьS -механизм совместности сигнатурыконечные или счетные множества предложенийw, -сигнатуры Ее и Т - непротиворечивая теория сигнатуры Е.
Пустьдля любыхчтоsUsЕS, Ф Еs,.{Ф, Ф} ~Т иiЕ w существуют такие Ф ЕТогда для любогоs*ЕSмножество Х предложений сигнатуры Е, чтоканоническую модель Qt и Хn Xi=f.1о для любогоДо к аз ат ель ст в о. Рассмотрим класспроверяется, чтоS' -Е s U Т и s Е S.U Т ~ s 1 U Т дляS'Xiиs,ЕS,существует такоеs* U Х Ui Е w.= {s U Т I sЕТ имеетS}.Легкомеханизм совместности. Например, пусть :3хФ ЕЕсли :3хФ Еs, то в силу (С7) имеем s U {(Ф)~} Us, Е S. Если :3хФ Е Т, то по условиютеоремы существует такое s, Е S, что s U {:3хФ} ~ s,. Опять по (С7)имеем S[ U {(Ф)n ~ s2 для некоторых СЕ С И s2 Е S. Следовательно,sUTU{(Ф)~} ~s2UT. Пусть Фо,Ф1, ...
,Фn,··· (nEw) и to, ... ,tn,···некоторогоГл.168Теория моделей5.(п Е w) - нумерации всех предложений сигнатуры Ее и всех базисныхтермов сигнатуры Ее.ПоS'строим множествоSw= USn следующим образом. Множе-пЕwU Т, и sn+l для п, равных 4k, 4k + 1 или 4k + 2,так же, как по S в теореме 5.4.3 строятся sn+Iдля п, равных 3k, 3k + 1 или 3k + 2 соответственно. Для п = 4k + 3поступаем следующим образом: если sn = s~ U Т, s~ Е S то по условиютеоремы существуют такие Ф Е Xk и sn Е S, что s~ U {Ф} ~ s'; полагаем sn+I = s' U Т. Построение модели Qt то же самое, что и в теореме5.4.3.
В качестве Х берем множество Sw.Оство s0 равно s*определяем поS'Следствие (еще одно доказательство теоремы4.4.2о существовании модели). Если множество Г формул сигнатуры Е непротиворечиво, то Г имеет модель.До к аз ат ел ь ст в о.В силу теоремыкомпактности достаточнодоказать теорему для конечного множества Г= {Ф1, ... , Фk}.Выполнимость и совместность Г равносильна соответственно выполнимости и совместности предложения Фх 1 , ••• , Хп -{ Ф}=3х,... 3хп(Ф, /\ ... /\непротиворечиво, то из предложенияствует механизм совместностиняем теорему=5.4.3 для s*S,5.4.1S.Теперь приме{Ф}.Определение. МножествоZп-типом сигнатуры Е. Если ТZполучаем, что сущедля которого {Ф} ЕОформул сигнатуры Е, свободные переменные которых содержатся в множествеЕ, то n-типФk), гдевсе свободные переменные, входящие в Ф 1, ..• , Ф k.
Если-{ v,, ... , vn}, называетсянепротиворечивая теория сигнатурысигнатуры Е называется главным в Т, если существуеттакая формула Ф( v,,... , vn) сигнатуры Е, что Т U {3v, ... 3vn Ф} совместно и Т 1> Ф----, Ф для любой Ф ЕZ.Будем говорить, что п-типZсигнатуры Е реализуется в алгебраической системе Q( сигнатуры Е,если существуют такие элементы а 1, .•. , ап Е А, что Q(F Ф (а 1, .•. , ап)для любой формулы Ф( v,,реализуется в системе... , vn) Е Z. Если n-тип Z сигнатуры Е неQt сигнатуры Е, то говорим, что Z опускается в Qt.Следующая теорема называется теоремой об опускании типов.ТеоремаиZi, iЕw, -5.4.6.Если Т-непротиворечивая теория сигнатуры Енеглавные в Т ni-munы сигнатуры Е, то существуетмодель Т сигнатуры Е, опускающая все типыДо к аз ат ель ст в о.РассмотримZi, iсовокупностьЕw.S таких конечных множеств s предложений сигнатуры Ее, что s U Т совместно.
По предложению 5.4.1 множество S является механизмом совместности. Пусть fi, i Е w, - разнозначные отображения w на сп,§ 5.4.и g -Механизм совместностиразнозначное отображениеu1169на w 2 . Определим множества Xk,k Е w, следующим образом: если g(k) = (i,j) и fi(j) = (с1, ... ,спJ,то полагаем Xk = {·(Ф)~::::::~:: 1 Ф Е Zi}- Предположим, что условие теоремы 5.4.5 не выполнено. Тогда существуют такие so Е S иka Е w, что sa U Т U {Ф} несовместно для любого '11 Е Xko· Пустьg(ko) = (ia, l), fi 0 (l) = (с1, ... ,и Фа - конъюнкция всех элемен-Cn,Jтовsa.Тогда {Фа}Ф(v1, ...
,Vn;0 ) Еот с1,... , сп, 0Zio·UТv1, ... ,vпсовместно и Т [>Фа-+ (Ф)с,, ... ,сn:оПусть Cn; 0 +J,···,cm-'Одля всехвсе элементы С, отличныеи содержащиеся в Фа. Пусть Ф1предложение, конгру--энтное предложению Фа, не содержащее переменныхv1, ... , Vm,и пустьФ2- формула сигнатуры Е, для которой (Ф2)~!:::::~;;: = Ф1. Покажем,что Т [> 3vn, 0 +1 ...
::3vmФ2-+ Ф для всех Ф Е Zio· В самом деле, пустьQ(F Ф2[1']для некоторой модели Q( теории Т, имеющей сигнатуру Е, иинтерпретации -у: {v1, ... , Vm} -+ А. Рассмотрим такое обогащение Qt'системы Q( до сигнатуры Ее, что vQ!' (с1) = -у( v1 ), ...
, vQI' ( ст) = -у( vm).Тогда Qt'FФ1Taк как Qt' образом, Q(и из эквивалентности Ф1= Фаv,, ... ,Vn-получаем Qt'модель Т и Т [>Фа-+ (Ф)с,, ... ,сn:о, то Q(F (::3vn;'ОF Ф[-у].FФо.Таким+1 ... ::3vmФ2-+ Ф)[-у] для любой модели Q( теории Т,любой формулы Ф Е Zio и любой интерпретации -у: {v1, ... , Vn; 0 } -+ А.Из следствия 4.5.8 тогда вытекает, что Т [> 3vn +1 ...
3vm Ф2 -+ Ф длялюбого Ф Е Zio. Так как sa U Т совместно, то Т U {::Jv1 ... 3vm Ф2} такжесовместно. Это противоречит тому, что Zio - неглавный пi 0 -тип. Такимобразом, условия теоремы 5.4.5 выполнены, значит, существует такоемножество Х предложений сигнатуры Ее, что Х n Xi f:. 125, i Е w,и существует система Q( сигнатуры Ее, являющаяся моделью Т U Х,0•оу которой любой элемент а Е А является значением некоторой константы с Е С. Так как для любогоi Е u1 и любого кортежа (с1, ... , Сп;) Е сп;что Х k = {• (Ф )~; :::::~:: 1 Ф Е Zi}, то Qt ~ Есуществует такое k Е u1,опускает все типы Zi, i Е w.DТеорема об опускании типов является очень важным методом построения моделей. Она дополняет теорему компактности, которая применяется,восновном,тогда,типы.
Применения теоремыВхождение символаqкогда5.4.6нужнореализовыватьбудут даны всовместные§ 5.6.в формулу Ф, не содержащую связки-+,назовем положительным (отрицательным), если число различныхподформул формулы Ф вида ·ir,, содержащих это вхождение, является четным (нечетным). Обозначим через Е+(Ф) и Е-(Ф) множествасимволов отношений сигнатуры Е, имеющих соответственно положительные и отрицательные вхождения в Ф.
Например, если= Vv1 ('(::Jv2r(t1, v2) V 's(v2)) /\ '('r(vз, t2) /\ v1t1,t2 - термы, то Е+(Ф) = {r,s}, Е-(Ф) = {r}.Фгде~t1)),Гл.170Следующаятеорема5.Теория моделейназываетсяинтерполяционнойтеоремойКрейга-Линдона.Теорема5.4.7.Пусть Ф, Фсодержащие связки---;, и Фпредложения сигнатуры :Е, не-Ф. Тогдаt>а) существует такое предложение Х сигнатуры :Е, не содержащее связки:r;-(x)~ :r;-(Ф)---;, что Ф t>n :r;-(w);Х, ХФ, :Е+(Х) ~ :Е+(Ф)t>n :Е+(Ф)иб} если :Е не содержит символов функций и констант, Ф, Ф несодержат равенства, а ~Ф и Ф обе недоказуемы, то в а) можнопотребовать, чтобы Х не содержало равенства.До к аз ат ел ь ст в о. Предложение Х, удовлетворяющее условиямутверждения а}, назовем интерполирующим для пары (Ф, Ф).а).
Пустьмножество конечных множеств s предложений сигS -натуры :r;c, не содержащих символа импликации, которые удовлетворяют следующему условию: существуют такие-1- 125 и s2 -1- 125, чтоss,= s, U s2(Л s1, ~(ли не существует интерполирующего предложения для пары(Через Л S мы обозначаем КОНЪЮНКЦИЮ элементовs2)).s1Множествопри этом будем называть началом, аОтметим, что начало и конецПроверим условия(Cl}-(C9)определяются поss2 sконцомs.}s.неоднозначно.механизма совместности.
Так как импликация не входит в элементы s ЕS,то (СЗ) тривиально выполнено. Еслипредложение 8 1 сигнатуры :r;c эквивалентно предложению 8 2 Е s Е Sи :r;т (81)=:r;т (82), т Е{+, -}, то очевидно,получаем условия (С2) и (С8). Пусть s Еs.(CI).чтоs U {81}S, s, -ЕS.Отсюданачало s, аs2 -конецце)Пусть{8, ~0}то предложениеs,~s.Если{8, ~0}содержится в начале (кон\lv1 ~v, ~ v, (предложение \lv1 v 1 ~ v,) будетинтерполирующим для (Лs1, ~(Лs2)), что противоречит условию.