Izsledvane za izpylnimost na mnozhestvo ot formuli

ИЗСЛЕДВАНЕ ЗА ИЗПЪЛНИМОСТ НА МНОЖЕСТВО ОТ ФОРМУЛИ

Ще покажем как скулемизацията може да се използва за изследване на изпълнимостта не само на отделни затворени формули, а и на множества от затворени формули. Можем да се ограничим с множества, състоящи се от затворени формули в пренексен вид, в които всяка от променливите участва само в един от кванторите. За всяка от формулите от такова множество е дефинирано какво значи нейна Скулемова нормална форма. Ще видим, че ако по подходящ начин заменим формулите от такова множество с техни Скулемови нормални форми, изпълнимостта на даденото множество ще бъде равносилна с изпълнимост на новото, което се получава при замяната. Въпросният подходящ начин изисква при скулемизацията на всяка от формулите от множеството да се използват Скулемови функционални символи, които не участват в никоя формула от множеството, и при скулемизцията на различни формули от множеството да се използват различни Скулемови функционални символи. Благодарение на възможностите за разширяване на езика на предикатното смятане с нови функционални символи спазването на тези изисквания е винаги възможно. Това, че тяхното спазване води до желания резултат, се вижда от следното твърдение.

Основна лема за равноизпълнимост. Нека M е множество от затворени формули и нека на всяка формула j от M е поставена в съответствие затворена формула jў по такъв начин, че jў е Скулемово допустима за j и винаги, когато y е формула от M, различна от j, никой от Скулемовите функционални символи на jў относно j не участва във формулата yў. Нека Mў е множеството на формулите jў, съответни на формулите j от M. Тогава изпълнимостта на множеството M е равносилна с изпълнимост на множеството Mў.

Доказателство. Понеже всяка формула j от M следва от съответната си формула jў, ясно е, че всеки модел на Mў е модел и на M; следователно ако множеството Mў е изпълнимо, то M също е изпълнимо. За да докажем, че и обратното е вярно, да предположим, че дадена структура S=(C,I) е модел на множеството M. Ще построим структура Sў=(C,Iў) със същия носител C, която да е модел на Mў. За тази цел най-напред за всяка формула j от M избираме такъв модел S^j=(C,I^j) на съответната формула jў, имащ същия носител C, че интерпретиращото съответствие I^j да съвпада с I за всички функционални символи, участващи във j, и за всички предикатни символи. След това дефинираме интерпретиращото съответствие Iў така, че да имаме равенството Iў(w)=I^j(w) всеки път, когато w е Скулемов функционален символ на jў относно j за някоя формула j от M, и Iў да съвпада с I за всички останали функционални символи и за всички предикатни символи. Тази дефиниция е еднозначна, защото един функционален символ може да бъде Скулемов функционален символ на jў относно j най-много за една формула j от M. За да покажем, че при тази дефиниция на Iў структурата Sў наистина е модел на Mў, ще покажем, че за произволна формула j от M съответната формула jў е вярна в Sў. Нека j е коя да е формула от M. Тъй като съответната формула jў е вярна в структурата S^j, достатъчно е да покажем, че интерпретиращото съответствие Iў съвпада с интерпретиращото съответствие I^j за всички функционални символи, участващи във jў, и за всички предикатни символи. Съвпадането на двете съответствия за предикатните символи е ясно от факта, че за тези символи и двете съответствия съвпадат с I. Да разгледаме сега произволен функционален символ w, който участва във jў. Ако w е Скулемов функционален символ на jў относно j, равенството Iў(w)=I^j(w) разбира се е изпълнено. Ако пък w не е Скулемов функционален символ на jў относно j, то w участва във j. Тогава w не е Скулемов функционален символ на qў относно q за никоя формула q от M и следователно имаме равенството Iў(w)=I(w), а освен това I^j(w) също е равно на I(w), тъй че отново имаме равенството Iў(w)=I^j(w).

Ще дадем някои примери за прилагане на доказаното.

Пример 1. Нека M е множеството, състоящо се от двете формули $x"yp(x,y) и $y"xШp(x,y), където p е двуместен предикатен символ, а x и y са различни променливи. Разглеждаме множеството Mў от формулите "yp(a,y) и "xШp(x,b), където a и b са различни помежду си нулместни функционални символи. Според доказаната лема изпълнимостта на M е равносилна с изпълнимостта на Mў. Тъй като Mў е множество от затворени универсални формули, неговата изпълнимост от своя страна е равносилна с изпълнимостта на множеството на всички конкретизации на формулите от Mў. Можем да считаме, че a и b са единствените функционални символи в сигнатурата на разглеждания език на предикатното смятане. Тогава множеството от всички конкретизации на формулите от Mў ще се състои от следните четири формули: p(a,a), p(a,b), Шp(a,b), Шp(b,b). Очевидно то е неизпълнимо, откъдето виждаме в крайна сметка, че множеството M също е неизпълнимо.

Пример 2. Нека M е множеството от формулите

"x$y"zp(x,y,z), "z$y"xШp(x,y,z), "x"z(p(x,x,z)®p(x,z,z)), където p е триместен предикатен символ, а x, y, z са различни помежду си променливи. Основната лема за равноизпълнимост показва, че изпълнимостта на M е равносилна с изпълнимост на множеството Mў, състоящо се от формулите "x"zp(x,f(x),z), "z"xШp(x,g(z),z), "x"z(p(x,x,z)®p(x,z,z)), където f и g са различни помежду си едноместни функционални символи. Можем да считаме, че съществува поне един нулместен функционален символ. Множеството на всички конкретизации на формулите от Mў ще се състои от формулите, имащи някой от следните три вида, където X и Z са затворени термове: p(X,f(X),Z), Шp(X,g(Z),Z), p(X,X,Z)®p(X,Z,Z). Тези формули са еквивалентни съответно на елементарните секвенции -:p(X,f(X),Z), p(X,g(Z),Z)-:, p(X,X,Z)-:p(X,Z,Z). На въпроса за изпълнимостта на M можем да отговорим, ако установим дали от секвенции от тези три вида би могла чрез някакъв брой прилагания на съществено сечение да се получи празната секвенция. За да имат някои две секвенции от разглежданите видове съществено сечение, необходимо е да съществуват такива затворени термове X, Z, Xў, Zў, че да е в сила някое от равенствата p(X,g(Z),Z)=p(Xў,f(Xў),Zў), p(X,X,Z)=p(Xў,f(Xў),Zў), p(X,g(Z),Z)=p(Xў,Zў,Zў). Лесно се вижда обаче, че никое от тези равенства не е възможно. Значи няма възможност от секвенции от разглежданите видове чрез някакъв брой прилагания на съществено сечение да се получи празната секвенция. Поради това множеството на секвенциите от тези видове е изпълнимо. Оттук, връщайки се обратно, заключаваме, че и множеството M е изпълнимо.

Пример 3. Нека p да бъде двуместен предикатен символ и x и y да бъдат две различни променливи. Нека освен тях са дадени още безбройно много други променливи x₁, x₂, x₃, ..., две по две различни помежду си. Ще изследваме дали формулата $y"xp(x,y) следва от безкрайното множество, състоящо се от формулите

"x₁"x₂..."x_n$y(p(x₁,y)&p(x₂,y)&...&p(x_n,y)), n=1,2,3,.... Така поставеният въпрос е равносилен с въпроса дали е неизпълнимо множеството M, получено от споменатото безкрайно множество чрез добавяне на формулата Ш$y"xp(x,y). Лесно можем да видим, че отговорът на последния въпрос, а значи и на първоначалния е отрицателен - множеството M е изпълнимо, защото един негов модел е например структурата (C,I), където C е множеството на естествените числа, а равенството I(p)(c,cў)=1 е в сила точно за онези естествени числа c и cў, които удовлетворяват неравенството c<cў. Ще покажем, че изпълнимостта на M би могла да бъде установена и с помощта на разгледаните дотук общи методи, без да има нужда да се досещаме за някакъв модел на множеството. И наистина, след като заменим формулата Ш$y"xp(x,y) с еквивалентната й формула "y$xШp(x,y) и направим скулемизация, получаваме, че изпълнимостта на M е равносилна с изпълнимостта на множеството, състоящо се от формулите "x₁..."x_n(p(x₁,f_n(x₁,...,x_n))&...&p(x_n,f_n(x₁,...,x_n))), n=1,2,3,..., и от формулата "yШp(g(y),y), където f_n е n-местен функционален символ при n=1,2,3,... и g е едноместен функционален символ, различен от f₁. Отново можем да считаме, че съществува поне един нулместен функционален символ. В такъв случай изпълнимостта на M ще бъде равносилна с изпълнимостта на множеството, състоящо се от всички формули p(X₁,f_n(X₁,...,X_n))&...&p(X_n,f_n(X₁,...,X_n))), n=1,2,3,..., и всички формули Шp(g(Y),Y), където X₁,...,X_n,Y са затворени термове. Заменяйки всяка от конюнкциите в последното множество с множеството на нейните членове, получаваме, че изпълнимостта на M е равносилна с изпълнимостта на множеството, състоящо се от всички формули p(X_i,f_n(X₁,...,X_n)), 1ЈiЈn, и всички формули Шp(g(Y),Y), където X₁,...,X_n,Y са затворени термове. За да бъде неизпълнимо последното множество, необходимо и достатъчно е да имаме равенството p(X_i,f_n(X₁,...,X_n))=p(g(Y),Y) при някой избор на целите числа n и i, удовлетворяващи неравенствата 1ЈiЈn, и на затворените термове X₁,...,X_n,Y. Последното равенство обаче е равносилно с двойката равенства X_i=g(Y), f_n(X₁,...,X_n)=Y, а те не могат да бъдат едновременно в сила, защото от тях следват противоречащи си заключения за дължините на термовете X_i и Y. С това е показано, че множеството M е изпълнимо.

Дотук видяхме как може да се изследва дали е изпълнимо едно множество от затворени формули. Сега ще покажем как може да се сведе към този случай въпросът за изпълнимост на произволно множество от формули. Това ще направим като докажем следното твърдение.

Допълнителна лема за равноизпълнимост. Нека M е произволно множество от формули, а s е такава субституция, че за всяка променлива x, която е свободна променлива на някоя формула от M, s(x) е нулместен функционален символ, неучастващ в никоя формула от M, и при това за всеки две различни помежду си такива променливи x съответните им s(x) също са различни помежду си. Тогава s е приложима към всяка формула от M и я преобразува в затворена формула, а изпълнимостта на M е равносилна с изпълнимостта на множеството от така получените затворени формули.

Доказателство. Приложимостта на s към формулите от M и затвореността на формулите, които се получават от тях при прилагането на s, следват от обстоятелството, че s преобразува свободните променливи на формулите от M в затворени термове. С оглед на по-нататъшните разсъждения да означим със СВО(M) обединението на множествата на свободните променливи на формулите от M, а с Mў - множеството на формулите s(j), където j принадлежи на M. Лесно се вижда, че ако една структура S е модел на множеството Mў, то при подходяща оценка v в S на променливите конфигурацията (S,v) удовлетворява M. Действително, достатъчно е да изберем v така, че за всяка променлива x от множеството СВО(M) да имаме равенството v(x)=s(x)^S - тогава за произволна формула j от M ще бъдат в сила равенствата

1=s(j)^S=s(j)^S,v=j^s(S,v)=j^S,v (последното от тях е налице благодарение на това, че за някоя оценка w в S на променливите имаме равенството s(S,v)=(S,w), като за всяка свободна променлива x на j имаме w(x)=s(x)^S,v=s(x)^S=v(x)). По този начин показахме, че ако множеството Mў е изпълнимо, то и множеството M е изпълнимо. За да докажем обратното, да допуснем сега, че множеството M е изпълнимо. Нека (S,v), където S=(C,I), е конфигурация, удовлетворяваща M. Ще построим структура Sў=(C,Iў) със същия носител C както S, която да е модел на Mў. За целта дефинираме интерпретиращото съответствие Iў така, че за всяка променлива x от СВО(M) да имаме равенството Iў(s(x))=v(x), а за всички функционални символи, нямащи вида s(x), където xОСВО(M), и за всички предикатни символи Iў да съвпада с I (да дефинираме такова Iў можем благодарение на обстоятелството, че за различни x от СВО(M) съответните функционални символи s(x) са различни). Нека j е произволна формула от M. Тогава ще имаме равенствата s(j)^Sў=s(j)^Sў,v=j^s(Sў,v)=j^Sў,w, където w е оценката в Sў на променливите, определена чрез равенството w(x)=s(x)^Sў,v. Когато x е свободна променлива на j, последното равенство дава, че w(x)=s(x)^Sў=Iў(s(x))=v(x). Поради това може да се твърди, че j^Sў,w=j^Sў,v. От друга страна интерпретиращите съответствия I и Iў съвпадат за функционалните символи, участващи във j, и за всички предикатни символи (различие между I и Iў е възможно само върху функционалните символи от вида s(x), където xОСВО(M), а никой от тези символи не участва във j). Следователно имаме още и равенствата j^Sў,v=j^S,v=1, тъй че в крайна сметка се оказва, че s(j)^Sў=1. Понеже j беше произволна формула от M, с това е доказано, че наистина Sў е модел на Mў и значи Mў е изпълнимо.

Забележка. В хода на доказателството показахме, че ако една структура S е модел на множеството от формулите, получени чрез прилагането на s към формулите от M, то при подходяща оценка v в S на променливите конфигурацията (S,v) удовлетворява M.

Последно изменение: 26.07.1999 г.

Contents