1611678200-36438fb4f1ee6f855c93dc4a315ea8eb (826633), страница 42
Текст из файла (страница 42)
f a(~end 21.) 1== Ф[1].1До к аз ат ель ст в о. Так как Ф =2t 3uФСи), существует интерпретация 1': FV(Ф) U {и}-. А такая, что 'У' f FV(Ф) = 'У и 21. 1== ф(и) [1']. Используя направленность отношения ~ 21 • находим элемент а Е А такой,что {с 21 1 с Е а} U )' 1 ( FV ( Ф) U {и}) ~ а. Система 21. является концевым,расширением 21.
f а, а ФСи) - до-формулой. Согласно предложению5.7.l получаем 21. 1== ф(и)['"У'] ~ 21. f а 1== ф(и)['"У'], 21. f а 1== ф(и)['"У'],21. f а 1== 3uФСи)['"У], 21. f а 1== Ф['"У], так как 3uФСи) =*s Ф в силу предложенияО5. 7.5.Принцип :Е-ограниченности. Если система:Е-формула, то \/х ~ t3уФ =21До к аз ат ель ст в о.ция3v\/x~t3y3v\/x~t3y21.ограничена и Ф-~ vФ.Как отмечено выше, всегда верна имплика~ vФ =?S \/х ~ t3уФ. Поэтому требуется установитьимпликацию \/х ~ t3уФ =*213v\/x~t3y~ vФ. По принципу рефлексии3уФ =? 21 3w(3yФ)Cw)_ Далее, \/х ~ t3уФ ==;- 21 \/х ~ t3w(3yФ)(w).
Попринципу да-ограниченностиКроме того,3w ~ v(3yФ)(w)=*21(3уФ?)[следствие 5.7.8],§ 5. 7.RQ-формулы и 'Е,-формулы:3v\fx ~ t:3w ~ v(:3yФ)(w)(:3уФ)(v)==}Q! :3v\fx ~ t(:3yФ)(v),= :3у:3у ~ vФ(v) ==}s :3у ~ vФ:3v\fx ~ t(:3yФ)(v)Итак, \fx ~ t:3уФ201~ vФ(v),[предложение 5.7.5],==}s :3v\fx ~ t:3y ~ vФ.~ t:3y ~ vФ. Принцип ~-ограниченности==}Q! :3v\fxустановлен.ОСледствие5. 7 .11.Если система Q( ограничена и Ф-~-формула,то справедливо следующее соотношение:До к аз ат ель ст в о. Установим утверждение дляшихkрассужденияаналогичны.Справедливыk= 1;для больследующие соотношения:\fx1 ~ t,:3уФ==}Q! :3v\fx1\fxo ~ to\fx1 ~ t,:3уФ\fxo ~ to:3v\fx1 ~ t,:3y ~ vФ==}Q! \fxo\fxo ~ to\fx1 ~ ti=JyФ~ to:3v\fx1 ~ t1:3y ~ vФ,==}Q! :3w\fxo~ w\fx1 ~ t1:3y ~ vФ:3v~ t1:3y ~ vФ,~ to:3v ~ w\fx1 ~ t,:3y ~ vФ,==}Q! \fx1==}Qt :3w\fxo~ t,:3y ~ wФ,~ to\fx, ~ t,:3y ~ wФ =s=s :3v\fxo ~ to\fx1 ~ t1:3y ~ vФ.Таким образом, следствие5.
7.11доказано.оВ заключение параграфа укажем без доказательства, как естественно расширить исчисление ИПf до исчисления языка RQ-формул так,чтобы теорема о полноте оставалась справедливой.Гильбертовское исчисление RQ-формул получается из ИПf добавлением следующих новых схем аксиом и правил вывода.Определение. Новые аксиомы:11')12')\fx ~ tФ /\ to ~ t--. (Ф)f0 , где хне входит в t;(Ф)f0/\to ~ t--. :3х ~ tФ, где хне входит в t.Новые правила вывода:2')3')(х ~t /\(х ~t /\Ф:3Ф)--. Ф\fФ--. x~tx~tФ)Ф--.--.ФФ, если х не входит свободно в Ф и не входит в t;, если х не входит свободно в Ф и не входит в t.Гл.2025.Теория моделейУпражнение1.Доказать, что система(Z, +,О,::;;)не является ограниченной.(Указание.
Рассмотреть формулу \:/х :;;; 03у х +у~ О.)§ 5.8.Формульная определимостьИспользуя формулы (RQ-формулы) сигнатуры а, можно определятьпредикаты на алгебраических системах сигнатуры а.Пусть Фформула сигнатуры а и Уо,-... , Yk-l -список попарноразличных переменных такой, что FV(Ф) <;;;; {Уо, ... , Yk-1}- Тогда длялюбой алгебраической системы Q! соответствующей сигнатуры на Аопределяется k-местный предикатФ2![у] ~{ (ао, ... , ak-1) 1 ai Е А, i < k; Q! р Ф[')'а:], где интерпретация')'а::{yo,---,Yk-1}--+А такая, чтоr'a(Yi) = ai,i < k}.Замечание 5.8.1. Можно рассматривать конструкцию Ф2![у] и безусловия FV(Ф) <;;;; {Yo,---,Yk-1}.
Тогда <<предикат,> Ф2![у] зависит отпараметров FV(Ф)\ {yo,--·,Yk-1} и имеет однозначный смысл, лишькогда задана интерпретация т FV(Ф) \{у}--+ А и имеет место соотношениеФ2![у][r'] ~{а= (ао, ... ,ak-1) 1 а Е A\Qt р Ф[,аU')']}.Определение. Предикаты вида Ф 21 [у] называются а-формульныминаQ!.Предложение5.8.2.Пусть Q! -алгебраическая система сигнатуры а, а' = а U (P0ko, •.. , P}s), Qt' = (Q!, Qo, ... , Q 8 ) - обогащение Q!до сигнатуры а' такое, что Qi, i :;;; s, - а-формульный предикат на Q!.
ЕслиQ -а' -формульный предикат на Qt', тоа-формульный предикат наДо к аз ат ел ь ст в о проведем для случая sполучается индукцией поQ -Q!.=О; общий случайs.Пусть ер формула сигнатуры а такая, что Qo = ср2![у], иФ - формула сигнатуры а U (Ро) такая, что Q = ф(2!.Qо) [z]. Предполагая, что все связанные переменные формулы ер не встречаютсяв Ф, определим синтаксическую операцию подстановки (Ф):[il] следующим образом: формула (Ф):[у] сигнатуры а получается из формулы Ф сигнатуры а U (Ро) заменой каждой атомарной подформулыyk0-1 Зф ормулы ф вида р,о (to, ...
, tko-l ) ф ормулои• (ер )yo,.....10 ... ,tko-' . аметим, чтоFV((Ф):rи)<;;;;FV(Ф).§ 5.8. Формульная определимость203Индукцией по построению формулы Ф устанавливается следующееутверждение: для любой интерпретации т FV(Ф)-А имеет местосоотношение-Единственный нетривиальный случайвидкогда Ф атомарна и имеетPo(to, ... , tk0 -1):(Qt,F Ф[1]Qo)~~ (t~bl.
· .. , tro-1 [1]) Е Qo ~F <p[1I21[,J], где 1I21[,J(Yi) = tl[1],i < ko,~ Qt F (<р)Л1] ~ Qt F (Po(t))'P[Y1[1].Qt~р,Из указанного свойства сразу вытекает, что для любой формулы Фсигнатуры аU (Ро)имеет место соотношениеф (Q!,Qo) [z] = (( ф (о_) Q( [z] '<р[у]из которого следует заключение предложенияЗамечание5.8.2(для s=О).D5.8.3. Как отмечалось выше, конструкцию <pQ![y] можбез условия FV(cp) ~ {у}. Это же справедлино использовать ивоидляподстановки.Предположим,чтовсепеременныеформулы <р не встречаются в Ф.
Тогда формула (Ф):[у]' определеннаявыше,1:обладаетFV(Ф)следующимU (FV(cp) \(12t,cpQ([VH1'J)FФ{у})-~ 12tсвойством:длялюбойинтерпретацииА справедливо соотношениеF (Ф):1и[1],1' ~ 1 ~ (FV(cp) \ {у}).Наряду с понятием формульного предиката можно ввести и понятиеформульной функции. Пусть Qt -алгебраическая система сигнатуры а.Определение. Функция g: А 1 - А называется а-формульной на Qt,если ее график Га = {(а, Ь) 1 а Е А 1 , Ь Е А, g(a) = Ь} ~ Al+ 1 являетсяа-формульным предикатом на Qt.Справедливо естественное обобщение предложенияПредложение5.8.4.Пусть Qt -5.8.2.алгебраическая система сигна-U (J,lol,,, , P.koО , ... ' f тО , ...
' pks)в, '"~ / -_ ("''~, go, ... , gm, QО, ..... . , Qs) - а'-обогащение Qt такое, что gi, i ~ т - а-формульныефункции, Q1 ,j ~ s, а-формульные предикаты. Тогда любойтурыа,а' -_аа' -формульный предикат (а' -формульная функция) на Qt' являетсяа-формульным предикатом (а-формульной функцией) на Qt.204Гл.5.Теория моделейУстановим сначала следующее общее утверждение.Лемма5.8.5.Для любой формулы Ф можно эффективно найтиформулу Ф той же сигнатуры такую, что Ф =sФ, FV(Ф) = FV(Ф),любая атомарная подформула формулы Ф является атомной, а любой ограниченный квантор формулы Ф имеет вид :3х:;;; у или \/х:;;; у.До к аз ат ель ст в о.Легко проверяется справедливость следующих эквивалентностей::3х:;;; tФ=s :3у(у~t /\ :3х:;;;уФ),уr:J_FV(Ф)\/х:;;; tФ=s :3у(у~t /\ \/х:;;;уФ),уr:J_FV(Ф) UU FV(t),FV(t),P(to, ...
, tk-1) =s :3хо ... :Jxk-1 ( Л xi ~ ti /\ Р(хо, ... , Xk-1)),i<kXir:J_u FV(tj),j <k,j<kt~f(to, ... , t1-1) =s f(to, ... , t1-1)~t =s=s :3х:3хо ... :3х1-1 ( х ~ t /\ Л Xi ~ ti /\ х ~ f(xo, ... , х1-1)),i<lгде х, Xi r:J_ U FV(tj) U FV(t), i < l. Если формула Ф содержит подфорj<kмулы вида :3х :;;; tФ (\/х :;;; tФ), где терм t отличен от переменной, то, последовательно заменяя их на :3у(у ~ t /\ :3х:;;; уФ) (:3у(у ~ t /\ \/х:;;; уФ)),добьемся того, что Ф не будет содержать таких подформул.Определим рангp(t)р(х) = О,термаtпо индукции:p(f(to, ... , t1-1)) = maxp(ti)i<l+ 1,и ранг р(Ф) атомарной формулы Ф:-когда Ф естьP(to, ... , tk-1),= ...
= p(tk-1) = О,и р(Ф)полагаем р(Ф)= maxp(ti) + 1,i<k=О, еслиp(to) =i<kесли существуетp(ti) > О;- когда Ф есть to ~ ti, полагаем р(Ф) = О, если p(to) = p(ti) =и р(Ф) = p(to) + p(t 1) - 1, если p(to) > О или p(ti) > О.такое, чтоЗаметим, что для атомарной формулы Ф равенство р( Ф)=ОО,выполняется тогда и только тогда, когда Ф атомная.Наконец, определим ранг р( Ф) для произвольной формулы Ф какмаксимум рангов ее атомарных подформул.§ 5.8. Формульная определимость>Если р(Ф)О, то каждую атомарную подформулу видаформулы Ф такую, что р( Р( to.
. . , tk- l)лой205... , tk- l)) >P(to, ...О, заменим форму-:3хо ... :3xk-l ( Л xi ~ ti /\ Р(хо, ... , Xk-l)),i<kа каждую атомарную подформулу вида~tтакую,f(to, ... , t1-1)(илиf(to, ... , tн)~t),чтоp(f(to, ... ,t1-1)) > 1 (или p(t) =p(f(to, ... ,t1-1)) = 1),заменим формулой:3х:3хо ... :3х1-1 ( х ~ t /\ Л Xi ~ ti /\ х ~ f(xo, ... , Х1-1)).i<lВ результате получим формулу Ф' такую, чтоФ=s Ф',FV(Ф)= FV(Ф')и р(Ф')р(Ф).<Если р(Ф') = О, то Ф:::::; Ф' удовлетворяет заключению леммы. Еслир( Ф')> О,то, образуя последовательностьФ, Ф', (Ф')', ...
'ф(n+l} :':::::; (Ф(п))', ... 'находим п ~ р(Ф) такое, что р(Ф(п)) =О.Тогда Ф:::::; ф(п) удовлетворяетзаключению леммы5.8.5.DДо к аз ат ель ст в о предложен и я(JJ5.8.4.Достаточно рассмотреть случай а'= а u 0 ).Пусть ер - формула сигнатуры а такая, что Г 90 = ep2l [у], и Ф формула сигнатуры а' такая, что Q = ф(2t, 9о) [z].
Согласно лемме 5.8.5можно считать, что любая атомарная подформула формулы Ф являетсяатомной.ОпределимпоформуламФиерформулуменив в Ф всякую атомную подформулу видаu()YO,····Ylo-1,Ylo)) ф( f (,JO Xi 0в•••,Xi10 _ 1~доказательствеXiормулоипредложенияфакт: для любой интерпретацииwXiер х, 0 , ••• ,х, 1 о- 1 ,х,.сигнатуры~а,заfo(Xi 0 , ••• , Xi 10 _ 1 )тоrда(такжекак5.8.2) устанавливается следующий1 : FV(Ф) - А справедливы соотношения(Qt, go)F Ф[,]Следовательно, ф2l, 9o[z]~ QtF wы(Ф '=(2l,go)w).= w2t[:z].
Предложение 5.8.4 доказано.DГл.206ПустьТеория моделей5.алгебраическая система.Qt -Определение.k-местныйпредикат Q ~ Akна Аназывается"'5:.-предикатом (на Qt), если существуют "'5:.-формула Ф и переменныеУо, ... , Yk-l такие, что Q= ФQl[y].Определение. У:.-предикат Q ~ Ak называется Л-предикатом(на Qt), если предикат Ak \ Q является "'5:.-предикатом.Определение. Функция g: А 1---.А называется "'5:.-функцией (на Qt),если ее график Г 9 является "'5:.-предикатом.Заметим, что если g: А 1 ---. А является "'5:.-функцией, то ее графикбудет даже Л-предикатом.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
