1611678200-36438fb4f1ee6f855c93dc4a315ea8eb (826633), страница 41
Текст из файла (страница 41)
7.1А такова,интерпреи Qt р Ф[,о]. Но тогда !В р Ф[,о]доказано.алгебраическая система и Ф, Ф-DRQ-формулы соответствующей сигнатуры.Определение. Формула Ф называется-следствием формулы Ф на Qt (обозначается Ф==>21 Ф),для любой интерпретацииА из Qtследует Qt р Ф[,];1:FV(Ф)U FV(Ф)----,еслиF Ф[1]§ 5. 7.RQ-формулы и L--формулы195семантическим следствием формулы Ф (обозначается Ф ==='?s Ф),-если Ф ==='?21 Ф для любой алгебраической системы21..Определение. Формулы Ф и Ф называются21.-эквивалентными-(обозначается Ф =21 Ф), если Ф ==='? 21 ФиФ ==='?21 Ф;семантически эквивалентными-Ф =21 Ф для всех(обозначается Ф =s Ф), если21..Укажем ряд легко проверяемых семантических эквивалентностейи импликаций:''Ф =s Ф,Ф-+ Ф =s'ФVФ,'3хФ =s \lх"Ф,'\lхФ =s 3х·Ф,'(Ф V Ф) =s 'Ф Л 'Ф,'(Ф Л Ф) =s 'Ф V 'Ф,'3х::;; tФ =s \lx ::;; ГФ,'\lx ::;; tФ =s 3х ::;; ГФ,3х3у ::;; tФ =s 3у::;; t3хФ,\lx\ly ::;; tФ =s \ly ::;; NхФ,3х::;; tФ =s 3у(у::;; t Л (Ф);), если у не встречается в t и Ф,\lx::;; tФ =s'v'y(y::;; t-+ (Ф);), если у не встречается в t и Ф,Ф ==='?s 3хФ,\lхФ==='?s Ф,3х::;; tФ ==='?s 3хФ,\lхФ==='?s\lx::;; tФ.В качестве следствий приведем две леммы.Лемма5.
7 .2.Для любой RQ-формулы Ф можно эффективноуказать RQ-формулу Ф такую, что Ф =s Ф, и формула Ф не содержит-+,а отрицания встречаются в ней лишь перед атомарнымиформулами.Замечание5. 7 .3.Еслидо-формула(I:-формула),(I:-формулой).7*RQ-формулатоФможноФвлеммевыбрать5. 7.2естьдо-формулойГл.196Лемма5. 7 .4.5.Теория моделейДля любой RQ-формулы Ф можно эффективноуказать формулу Ф языка ипа такую, что Ф=s Ф.Для ~:>формулы Ф и переменной и, не встречающейся в Ф, определим Ло-формулу ф(и) как формулу, полученную из Ф заменой каждоговхождениявФнеограниченного кванторасуществованиявида:3хвхождением ограниченного квантора существования Зх ~ и.Предложение5.
7 .5.Для любой Е-формулы Ф справедлива импликация ЗuФ(и) ==='?s Ф.До к аз ат ел ь ст в о. Установим индукцией по построению Ф импликацию ф(и) ==='?s Ф. Для Ло-формулы Ф имеем ф(и) = Ф и Ф ==='?s Ф.Кроме того,ФЬи)==='?sФо}Фiи)==='?sФ1(и)ФOФЬи)==='? s Фо ==='?==='?sФо(Фо V Ф1)(и)(= Ф6и) V Фiи))==='?sФо V Ф1,(Фо /\ Ф1 )(и) (= ФЬи) 1\ Фiи))==='?sФо 1\ Ф1,{ (:3х ~ tФо)(и)(= Зх ~ tФЬи))==='?sЗх ~ tФо,(\/х ~ tФо)(и)(= \/х ~ tФЬи))==='?s\/х ~ tФо,==='?(:3хФ)(и)(= Зх ~ иФЬи))==='?==='?s:3хФ6и)==='?sЗхФо.Так как ф(и) ==='?s Ф и и не свободна в Ф, то ЗuФ(и) ==='?s Ф.Предложение5.7.6 (монотонность ф(и)). Если вО2( отношениетранзитивно, Ф - Е-формула, FV(Ф) ~ Х, и 1- Х и 1 : Х U {и}-+А - интерпретация такая, что 2(ф(и)[,], то 2(ф(и)[,о] для.~ 21--+Fлюбой интерпретации ,о: Хu {и} --+ Атакой, что ,оFr Х = 1 rХи,(и) ~ 21 ,о(и).До к аз ат ел ь ст в о.Утверждение устанавливается индукцией попостроению Ф и следует из сформулированных и доказанных нижеутверждений(1)(1)-(4).Если Ф-Ло-формула, то Ф удовлетворяет свойству монотонности.Действительно, тогда Ф не содержит неограниченных кванторовсуществования, ф(и) = Ф и и не входит свободно в Ф.
Следовательно,2(ф(и) [,] ==='? 2(Ф[,] ==='? 2(Ф[,о] ==='? 2(ф(и) [,о].F(2)FЕсли Фо и Ф1-FFЕ-формулы, удовлетворяющие свойству монотонности, то формулы (ФоV Ф1)и (Фо/\Ф1) также удовлетворяютэтому свойству.Пусть FV(ФoV Ф1) ~ Х, и 1- Х, -у: Х U {и}-+ А, 2t F (ФоV Ф1)(и)[,],,о: Х U {и}--+ А и ,о Х = 1Х, ,(и) ~ 21 ,о(и). Из равенстваrrRQ-формулы и "Г,-формулы§ 5. 7.197(Фа V Ф1)Си) = Фьи) V Ф\и) следует, что 21. р Фiи)['У] для некоторогоF Фiи)['Уо] и 21. F (Фа V Ф1)Си)['Уо]. Для формулыi = О, 1. Но тогда 21.(Фа Л Ф1) рассуждения аналогичны.Если Фа(3)-'У:,-формула, удовлетворяющая свойству монотонности, то формулы :3х ~ tФо и \:/х ~ tФо также удовлетворяютсвойству монотонности.FV(Фo)Пусть21.FцияU FV(t)(Vx ~ tФо)Си)['У]такая,(Vx ~ tФа)Си),'Очтоr~ Х,иtf.Х,,.,:ХU{и}--+А,интерпрета10: Х U {и} --+ АиХ = 'У r Х и 1(и) ~ 21 'Уо(и). Так как= Vx ~ tФьи) и, следовательно, 21.
F 1;/х ~ tФьи)ы,Фьи)['У'] для любой интерпретации 1': Х U {х,и}--+ Аr (Х \ {х}) U {и}= 'У r (Х \ {х}) U {и}, 1'(х) ~ 21 t 21 [1].чтотакая,интерпретация'Уо: х u {Х, и} --+ АПусть'Уо r (Х \ {х}) U {и}= 'Уа r (Х \ {х}) U {и} и 'Уо(х) ~ 21 t 21 ['Y] (так каки (j. FV(t) и 'Уа r Х = 'У r Х). Пусть интерпретация 1': Х U {х,и}--+ Атакова, что ,'1 r х u {х} = 'Уо r х u {х}, 'У'(и) = ,'(и) ~ 21 ,'о(и) = 'Уо(и).Тогда 21. F Фьи) [1'] и 21. F ф~и) [16] ввиду монотонности формулы Фа.Следовательно, 21. F \:/х ~ tФ 0и)['Уо]. Для формулы :3х ~ tФо рассуждеимеем 21.Fтакой, что 1'ния аналогичны.(4)Если Фа-'У:,-формула, удовлетворяющая свойству монотонности, то формула :3хФо также удовлетворяет свойству монотонности.,.,: Х U {и} --+ А,и tf. Х,х Е Х,FV(Фo) ~ Х,Пусть21.
F (:3хФа)Си) ['У] и ,'о: Х U {и} --+ А - интерпретация такая, что'Уа r Х = 'У r Х и 1(и) ~ 21 'Уо(и). Имеем (:3хФа)Си) = :3х ~ иФЬи)_ Так как21. F :3х ~ иФьи) ['У], существует интерпретация ,.,, ; х u {и} --+ А такая,что 1' r ~Х \ {х}) u {и}= 'У r (Х \ {х}) U {и}, 1'(х) ~ 21 1'(и) = 1(и),21. F Фьи ['У']. Пусть 'Уо; х u {и} --+ А - интерпретация, определенная так, что 'Уо r Х = 'У' r Х и 10 (и) = 'Уо(и). Тогда'У'(и) = 1(и) ~ 21 'Уо(и) = 'Уо(и). В силу монотонности формулы Фаполучаем 21. F Фьи)['Уо]- Кроме того, 'Уо(х) = ,' 1 (х) ~ 21 'У'(и) ~ 21 'Уо(и), и10 (х) ~ 21 10 (и) ввиду транзитивности отношения ~ 21 . Следовательно,21. F :3х ~ иФьи)[,'о] и 21.
F (:3х ~ иФа)Си)['Уо].Таким образом, предложение5. 7.6Следствие 5. 7. 7. Если в системедоказано.о21. отношение ~ 21 транзитивно,Ф есть 'У:,-формула, переменные и =f. v не входят в Ф и т FV(Ф) UU {v}--+ А, то 21. l;/u ~ v(Ф(и)--+ ф(v))['У].FГл.1985.Теория моделейСледствие 5. 7 .8. Если в системе 21. отношение ( 21 транзитивно, Ф есть 'Г,-формула и переменные и -/=- v не входят в Ф, то:3иvФ(и) ===}21 ф(v).(Доказательство.тация такая, что 21.FПустьт FV(Ф)U {v}-+Аинтерпре-:3и ( vФ(и)[1]. Тогда существует интерпреU {и,v} -+ А такая, что 1' r FV(Ф) U {v} = 1,и 21.
F ф(и)[1']. Пусть 1 11 : FV(Ф) U {v}-+ А интерпретация такая, что 1" r FV(Ф) = 1 r FV(Ф) и 1"(v) = 1'(и). Таккак 21. F ф(и)[1'], имеем 21. F ф(v)[1"]. с другой стороны, 1" r FV(Ф) == 1 r FV(Ф) и 1"(v) = 1'(и) ( 21 1'(v) = 1(v). Следовательно, по монотонности 21. F Фv['У].Отация1':FV(Ф)1'(и) ( 21 1'(v)= 1(v)Определение. Алгебраическая система21.называется ограничен-ной, если выполнены следующие условия:отношение21.(21 является транзитивным и направленным на А, т. е.F \/x\/y\/z(x (у/\ у( z-+ х ( z) /\ \/x\/y:3z(x ( z /\ у ( z),для любой Ла-формулы Ф имеет место принцип Ла-ограниченности: \/х(ЗамечаниелыФ)t:3уФ ===} 215.
7 .9.:3v\/x ( t:3y (ПринципvФ.Ла-ограниченностиэквивалентен соотношению \/х(t:3уФ =21(дляЛа-формуvФ.:3v\/x ( t:3y (Действительно, для любой RQ-формулы Ф справедливы импликации(vФ===}s :3уФ,( t:3y (vФ===}s \/х (:3у\/х:3v\/x ( t:3y (vФ===}s \/х (t:3уФ,t:3уФ.Для ограниченных систем верны два важных утверждения (принцип 'Г,-рефлексии и принцип 'Г,-ограниченности).Принцип:Е-рефлексии. Еслисистема21.ограниченаиФ-'Г,-формула, то справедлива эквивалентность Ф =2t :3uФ(и).До к аз ат ель ст в о.
Имеем :3иФ(и) ===} s Ф согласно предложению5. 7.5. Поэтому достаточно доказать импликацию Ф ===} 21 :3uФ(и). Онаследует из нижеприведенных утверждений (1)-(5) индукцией по построению формулы Ф.(1) Если Ф - Ла-формула, то Ф===}s :3иФ<и)_Действительно, в этом случае ф(и)=Ф.(2) Если для 'Г,-формул Фа и Ф, верны импликации Фii=0,1,mo(Фа V Ф1) ===},11 :3и(Фа V Ф,)(и),(Фа/\ Ф1)===}21:3и( Фа /\ Ф 1 )(и).===} 21:3иФ;и!§ 5. 7.Рассмотримще).Пусть,:RQ-формулы и "Е,-формулыформулу(Фа А Ф1)FV(Фa А Ф1)--.А199(случай(Фа V Ф1)интерпретация-такая,прочтоF (Фа А Ф1)[1].
Тогда Q{ 1= Фа['У], Q{ F Ф1[1]. По предположениюQ{ F :3иФьи)[,'], Q{ F :3иФ\и)[,.,J. Поэтому существуют интерпретации 'Yi: FV(Фa А Ф1) U {и}--. А, 'Yi r FV(Фa А Ф1) = 'У, i = О, 1,такие, что Q{ F Фьи)['Уа], Q{ F Ф\и)[11]. Так как отношение ( 21Q{направленное, существует элемент а Е А такой, что 'Уа(и) ( 21 а и11(и) ( 21 а.
Пусть 1*: FV(Фa А Ф1) U {и}--. А интерпретациятакая,ЧТО'У*r FV(ФaА Ф1)= ,'И'У*(и)=а.Ввидумонотонности имеем Q{ F Фьи)['У*], Q{ F Ф\и)['У*] и Q{ F (Фьи) А Ф\и))[1*],(Фаи) А Ф\и)) = (Фа А Ф1)(и)_ Следовательно, Q{ р :3и(Фа А Ф1)(и)['У], Иимпликация (Фа А Ф1)===>21 :3и(Фа А Ф1)(и) установлена.(3) Если Фа - 'Г,-формула и Фа ===>21 :3иФ6и), то :3х ( tФа ===>21===>21 :3и(:3х ( tФа)(и).В силу основных свойств отношений===>21, =2t, ===>s, =sимеем:3х ( tФа ===>21 :3х ( t:3иФ6и),:3х ( t:3иФ6и) =s :3и:3х ( tФаи)Следовательно, :3х ( tФа= :3и(:3х ( tФа)(и).===> 21 :3и(:3х ( tФа)(и).(4) Если Фа - 'Г,-формула и Фа ===>21 :3иФьи), то \/х ( tФа ===>21===>21 :3u(Vx ( tФа)(и).Соотношения\/х ( tФа ===>21 \/х ( t:3иФаи),\/х ( t:3иФ6и) =21 :3w\/x ( t:3u ( wФаи),справедливы ввиду ограниченности системы Qt и того факта, что ФЬи) да-формула.
Из следствия 5. 7.8 следует импликация :3и ( wФ 0 ===>*21 ФЬw). Получаем \/х ( tФа ===>21 :3u(Vx ( tФа)Си) в силу соотношения:3w\/x ( t:3u ( wФЬи) ===>21 :3w\/x ( tФaw) =s=s :3и\/х ( tФаи)=:3и(\/х ( tФа)(и).(5) Если Фа ===>21 :3иФаи), то :3хФа ===>21 :3и(:3хФа)(и).Справедливы следующие импликации::3хФа ===>21 :3х:3иФьи),:3х:3иФ6и) ===> 21 :3и:3х ( и Фаи).200Гл.5.Теория моделейДействительно,пусть ,: FV(Фo) -.
Аинтерпретацията21. 1== 3х3иФ6и)['"У].Тогда существует интерпретация'У': FV(Фo) U {х, и} -. Атакая,что'У' f FV(Фo) = 'У,21. 1== Ф6и)['"У']. Рассмотрим элемент а Е А такой, что 1'(х) ~ 21 а,1'(и) ~ 21 а, и интерпретацию 'У": FV(Фo) U {х, и} -. А такую, чтокая,f'У"чтоFV(Фo) U {х}='У'fFV(Фo) U {х}, 1"(и)=а. Тогдав силумонотонности ИЗ 21. 1== Ф6и)['"У'] следует 21. 1== Фьи)['"У"]. Заметим, что1"(х) = 1'(х) ~ 21 а = 1"(и). Тогда 21. 1== 3и3х ~ иФ6и)['"У]. Поэтому3хФо =?2( 3и3х ~ иФ6и) = 3и(3хФо)(и).Таким образом, принцип :Е-рефлексии установлен.оПриведем одно из следствий принципа :Е-рефлексии для случаяконечной сигнатуры а, не содержащей функциональных символов.Следствиенатурыа,5.
7 .10.неПустьсодержащейограниченная21. -функциональных:Е-формула сигнатуры а и)': FV(Ф)-. АчтоФ[1].21. 1==а ;=се {а'Тогдасуществует-системасимволов,сигФ-интерпретация такая,элемента Е Атакой,чтоа' ~ 21 а} содержит все значения констант сигнатуры а,1(FV(Ф)) ~аи 21.