СКУЛЕМОВА НОРМАЛНА ФОРМА

    Най-напред ще извършим известна подготвителна работа, а именно ще дефинираме по един естествен начин кога един функционален символ участва в даден терм или дадена формула. Дефиницията е индуктивна и се състои от следните точки:
    ФСУ1. Ако w е нулместен функционален символ, то w участва в терма w.
    ФСУ1а. Ако w е n-местен функционален символ, където n>0, а t₁, ..., t_n са термове, то w участва в терма w(t₁,..., t_n).
    ФСУ2. Ако w е n-местен функционален символ, където n>0, а t₁, ..., t_n са термове, то всеки функционален символ, който участва в някой от термовете t₁, ..., t_n, участва и в терма w(t₁,..., t_n).
    ФСУ3. Ако p е n-местен предикатен символ, където n>0, а t₁, ..., t_n са термове, то всеки функционален символ, който участва в някой от термовете t₁, ..., t_n, участва и в атомарната формула p(t₁,..., t_n).
    ФСУ4. Ако j е формула, то всеки функционален символ, участващ във j, участва и във формулата Шj.
    ФСУ5,6. Ако j и y са формули, то всеки функционален символ, който участва в някоя от тях, участва също във формулата j&y и във формулата jЪy.
    ФСУ7,8. Ако j е формула, а x е променлива, то всеки функционален символ, който участва във j, участва също във формулата "xj и във формулата $xj.

    Забележка 1. По подобен (малко по-кратък) начин може да се дефинира и какво значи даден предикатен символ да участва в дадена формула. Пропускаме тази дефиниция, защото няма да ни потрябва.

    Да предположим сега, че са дадени две структури S=(C,I) и Sў=(C,Iў), имащи един и същ носител C. Чрез индукция, съобразена с дефиницията на понятието терм, лесно се доказва, че ако интерпретиращите съответствия I и Iў съвпадат за всички функционални символи, участващи в даден терм t, то за всяко изображение v на множеството X на променливите в множеството C е изпълнено равенството t^S,v=t^Sў,v. С помощта на това твърдение и на индукция, съобразена с дефиницията на понятието формула, не е трудно да се докаже, че ако интерпретиращите съответствия I и Iў съвпадат за всички функционални символи, участващи в дадена формула q, и за всички предикатни символи, то за всяко изображение v на множеството X в множеството C е изпълнено равенството q^S,v=q^Sў,v.

    С помощта на индукция, съобразена с дефинициите на понятията терм и формула, се доказва още, че ако q е терм или формула, а qў е резултат от прилагане на някоя субституция s към q, то един функционален символ участва в qў точно тогава, когато участва в q или в някой терм от вида s(z), където z е свободна променлива на q.

    Ако j и jў са две затворени формули, ще казваме, че jў е Скулемово допустима за j, когато са изпълнени следните условия: а) всеки функционален символ, участващ във j, участва и във jў; б) jўj; в) за всеки модел на j съществува такъв модел на jў, че носителите на двата модела съвпадат, а интерпретиращите им съответствия съвпадат за всички функционални символи, участващи във j, и за всички предикатни символи. Когато j и jў са такива затворени формули, че jў е Скулемово допустима за j, функционалните символи, които участват във jў, но не участват във j, ще наричаме Скулемови функционални символи на jў по отношение на j. Ясно е, че ако jў е Скулемово допустима за j и някоя от двете формули j и jў е изпълнима, то другата също е изпълнима. Прост пример за Скулемова допустимост получаваме, ако разгледаме две еквивалентни затворени формули, в които участват едни и същи функционални символи - всяка от двете формули е Скулемово допустима за другата без да са налице Скулемови функционални символи. Сега ще разгледаме един по-интересен случай на Скулемова допустимост.

    Нека j е затворена формула от вида "x₁..."x_n$hq, където n е неотрицателно цяло число, x₁, ..., x_n, h са различни помежду си променливи и q е формула. Скулемово усилване на j ще наричаме всяка формула от вида вида "x₁..."x_nqў, където qў е частен случай на q, получен от q чрез прилагане на някоя субституция s, дефинирана по следния начин: избран е някой n-местен функционален символ w, неучастващ в q, и в качеството на s е взета субституцията (h:=w(x₁,...,x_n)), ако n>0, и субституцията (h:=w) при n=0. Разбира се, за да притежава една формула j от горния вид Скулемово усилване, необходимо е да съществува поне един n-местен функционален символ w, неучастващ в q, но това условие винаги бихме могли да удовлетворим чрез добавяне на нов функционален символ към сигнатурата на езика на предикатното смятане. При n=0 горното необходимо условие е и достатъчно, защото съответната субституция s не привнася променливи в q и следователно е приложима към q. При n>0 то е достатъчно например в случая, когато никоя от променливите x₁, ..., x_n не е свързана променлива на формулата q, тъй като съответната субституция s не привнася в q променливи, различни от x₁, ..., x_n.

    Пример 1. Нека p и q са съответно едноместен и двуместен предикатен символ, а x и y са различни променливи. Тогава, ако a е нулместен функционален символ, то формулата p(a)®"xq(x,a) е Скулемово усилване на формулата $y(p(y)®"xq(x,y)).

    Пример 2. При същите предположения както в пример 1, ако f е едноместен функционален символ, то формулата "x(q(x,f(x))&p(f(x))) е Скулемово усилване на формулата "x$y(q(x,y)&p(y)).

    Теорема за въвеждане на Скулемови функционални символи. Нека j е затворена формула от вида "x₁..."x_n$hq, където n е неотрицателно цяло число, x₁, ..., x_n, h са различни помежду си променливи и q е формула. Нека jў е формула, която е Скулемово усилване на j. Тогава jў е Скулемово допустима за j.

    Доказателство. Ще използваме означенията qў, s и w от дефиницията за Скулемово усилване. Щом j е затворена, ясно е, че СВО(q)Н{x₁,...,x_n,h}, а това гарантира, че СВО(qў)Н{x₁,...,x_n} и следователно jў е затворена. От дефиницията за това, кога един функционален символ участва в дадена формула, е ясно, че всеки функционален символ, участващ във j, непременно участва в q, а оттук се получава, че всеки такъв символ ще участва и във формулата jў. При n=0 свойството б) от дефиницията за Скулемова допустимост следва направо от теоремата за семантичната връзка между генерализация, частен случай и екзистенциализация (по-точно от връзката между частен случай и екзистенциализация). При n>0 споменатото свойство следва от същата теорема и от обстоятелството, че ако за две формули y и c имаме съотношението yc, то при всеки избор на променливата z имаме също и съотношението "zy"zc. Остава да покажем, че за формулите j и jў е изпълнено свойството в) от дефиницията. За целта да предположим, че S=(C,I) е модел на j. Ще се стремим да построим модел Sў=(C,Iў) на jў, свързан с модела S на j по нужния начин. За да направим това, първо отбелязваме, че при направеното предположение формулата $hq ще бъде тъждествено вярна в структурата S (при n=0 това означава просто, че споменатата формула е вярна в S). В такъв случай за всяка оценка v в S на променливите ще съществува такъв елемент d на C, че формулата q да бъде вярна в S при h,d-модификацията на v. Да означим с G множеството на всички n+1-орки от вида (vў(x₁),...,vў(x_n),vў(h)), където vў е такава оценка в S на променливите, че q да е вярна в S при оценка vў. От казаното преди малко е ясно, че при n=0 множеството G има поне един елемент, а когато n е положително, при всеки избор на елементите c₁, ..., c_n на C има елемент d на C, за който n+1-орката (c₁,...,c_n,d) принадлежи на G. Като използваме включването СВО(q)Н{x₁,...,x_n,h}, лесно съобразяваме още, че при (c₁,...,c_n,d)ОG формулата q е вярна в S при всяка оценка vў, удовлетворяваща условията
(1)                            vў(x₁)=c₁, ..., vў(x_n)=c_n, vў(h)=d.

    Ще дефинираме интерпретиращото съответствие Iў на модела Sў поотделно в случая, когато n=0, и в случая, когато n>0.

    При n=0 избираме някой елемент d на множеството G и означаваме с Iў интерпретиращото съответствие, което на символа w съпоставя елемента d, а за всички останали функционални символи и за всички предикатни символи съвпада с I. Ако v е произволна оценка в S на променливите, а vў е h,d-модификацията на v, то верността на jў в Sў се вижда от равенствата
                               jў^Sў=qў^Sў,v=q^s(Sў,v)=q^Sў,vў=q^S,vў=1, 
като в последните три от тях са използвани равенството w^Sў=d, обстоятелството, че символът w не участва в q, и равенството vў(h)=d.

    Да предположим сега, че числото n е положително. Ако за всяка n-орка (c₁,...,c_n) от елементи на C изберем по един елемент d, такъв, че n+1-орката (c₁,...,c_n,d) да принадлежи на множеството G, ще получим n-местна операция F в C със свойството, че
                               (c₁,...,c_n,F(c₁,...,c_n))ОG
при всеки избор на c₁, ..., c_n в C. Нека сега Iў е интерпретиращото съответствие, което на символа w съпоставя операцията F, а за всички останали функционални символи и за всички предикатни символи съвпада с I. Ще покажем, че формулата jў е вярна в Sў, като покажем, че в Sў е тъждествено вярна формулата qў. За целта да означим с v произволна оценка в S на променливите и да положим
                               c₁=v(x₁), ..., c_n=v(x_n), d=F(c₁,...,c_n).
От това полагане получаваме, че n+1-орката (c₁,...,c_n,d) принадлежи на G. Нека vў е h,d-модификацията на v. Тогава имаме равенствата
                               qў^Sў,v=q^s(Sў,v)=q^Sў,vў=q^S,vў=1, 
като в последните три от тях използваме равенството w(x₁,...,x_n)^Sў,v=d, обстоятелството, че w не участва в q, и изпълнените в случая равенства (1).

    Следствие. При предположенията на горната теорема формулата j е изпълнима точно тогава, когато е изпълнима формулата jў.

    Забележка 2. Лесно се проверява, че когато са изпълнени предположенията на доказаната теорема и h е свободна променлива на q, формулата jў има точно един Скулемов функционален символ по отношение на j, а именно символа w, с помощта на който е дефинирана съответната субституция s.

    Забележка 3. В случая, когато числото n е положително, изложеното доказателство на теоремата използва тъй наречената аксиома за избора, която дълго време е била една от най-оспорваните аксиоми на теорията на множествата (въпросната аксиома се използва обаче и в многобройни други математически доказателства - например при доказателството за еквивалентност на двете най-често прилагани дефиниции за непрекъснатост на функция).

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

    Пример 3. Задачата за бръснаря, която разглеждахме по-рано, би могла да се формулира и като въпрос дали е изпълнима форнулата $y"x(s(y,x)«Шs(x,x)), където y и x са различни помежду си променливи, а s е двуместен предикатен символ. Според споменатото следствие този въпрос е равносилен с въпроса дали е изпълнима формулата "x(s(b,x)«Шs(x,x)), където b е нулместен функционален символ. За тази формула вече сме показали, че не е изпълнима.

    Пример 4. Ще изследваме дали е тъждествено вярна формулата
                               $x"y$z(p(x,y)®p(y,z)),
където x, y, z са различни помежду си променливи, а p е двуместен предикатен символ. За да бъде тъждествено вярна тази формула, необходимо и достатъчно е да е неизпълнимо нейното отрицание, а то е еквивалентно на формулата
                               "x$y"z(p(x,y)&Шp(y,z)).
Според следствието от теоремата изпълнимостта на последната формула е равносилна с изпълнимостта на формулата
                               "x"z(p(x,f(x))&Шp(f(x),z)),
където f е едноместен функционален символ. Без ограничение на общността можем да считаме, че съществува поне един нулместен функционален символ. При това положение, тъй като последната формула е универсална, нейната изпълнимост е равносилна с изпълнимост на множеството, състоящо се от всички нейни конкретизации, т.е. от всички формули от вида p(X,f(X))&Шp(f(X),Z), където X и Z са затворени термове. За да бъде така описаното множество изпълнимо, необходимо и   достатъчно е да съществува структура, в която са верни всички формули от вида p(X,f(X)), където X е затворен терм, и са неверни всички формули от вида p(f(X),Z), където X и Z са затворени термове. Формулите от двата посочени вида са затворени атомарни формули. Поради това съществуването на такава структура е равносилно с изискването множеството на формулите от първия вид и множеството на формулите от втория вид да нямат общи елементи. Въпросното изискване ще бъде нарушено точно тогава, когато за някои затворени термове X, Xў и Z е в сила равенството p(X,f(X))=p(f(Xў),Z). Това равенство е равносилно със системата от двете равенства X=f(Xў), f(X)=Z, а за нея лесно се вижда, че се удовлетворява при подходящ избор на затворените термове X, Xў и Z (а именно при X=f(Xў), Z=f(f(Xў)), където Xў е произволен затворен терм). И така, споменатите две множества от атомарни формули имат общ елемент, а това позволява, като се върнем обратно назад, да заключим, че отрицанието на формулата, дадена в началото, не е изпълнимо, следователно самата формула е тъждествено вярна.

    Пример 5. Ще изследваме дали е тъждествено вярна формулата
                               $x"y$z"u(p(x,y,z)®p(u,z,y)),
където x, y, z, u са различни помежду си променливи, а p е триместен предикатен символ. За да бъде тъждествено вярна тази формула, необходимо и достатъчно е да е неизпълнимо нейното отрицание, а то е еквивалентно на формулата
(2)                            "x$y"z$u(p(x,y,z)&Шp(u,z,y)).
Като приложим следствието от теоремата за въвеждане на Скулемови функционални символи, виждаме, че изпълнимостта на последната формула е равносилна с изпълнимост на формулата
                               "x"z$u(p(x,f(x),z)&Шp(u,z,f(x))),
където f е едноместен функционален символ. Нейната изпълнимост, пак по същото следствие, от своя страна е равносилна с изпълнимост на универсалната формула
(3)                            "x"z(p(x,f(x),z)&Шp(g(x,z),z,f(x))),
където g е двуместен функционален символ. И така, за да бъде тъждествено вярна формулата в началото на примера, необходимо и достатъчно е да е неизпълнима току-що получената универсална формула. Изследването дали тази универсална формула е изпълнима може да се извърши аналогично на изследването за изпълнимост на универсалната формула, получена в пример 4. В хода на изследването се установява, че за да бъде формулата (3) неизпълнима, необходимо и достатъчно е да съществуват затворени термове X, Xў, Z, Zў, такива, че да са в сила равенствата X=g(Xў,Zў),  f(X)=Zў,  Z=f(Xў). Тъй като от първите две от тези равенства следват противоречащи си заключения по въпроса за дължините на думите X и Zў, виждаме, че такива термове не могат да съществуват и следователно формулата (3) е изпълнима. Това показва, че първоначално дадената формула не е тъждествено вярна.

    Ако в пример 5 бяхме приложили два пъти не следствието от теоремата за въвеждане на Скулемови функционални символи, а самата теорема, би се получило положение, когато от три затворени формули втората е Скулемово допустима за първата, а третата е Скулемово допустима за втората. Следващата лема позволява да се заключи, че при такова положение третата формула е Скулемово допустима за първата.

    Лема за транзитивност на Скулемовата допустимост. Нека j, jў и jІ са такива затворени формули, че jў е Скулемово допустима за j, а jІ е Скулемово допустима за jў. Тогава jІ е Скулемово допустима за j.

    Доказателство. От направените предположения е ясно, че всички функционални символи, участващи във j, участват и във jІ, и че jІj. За да покажем, че за j и jІ е изпълнено и третото изискване от дефиницията за Скулемова допустимост, да предположим, че дадена структура S=(C,I) е модел на формулата j. Поради това, че формулата jў е Скулемово допустима за j, съществува такъв модел Sў=(C,Iў) на jў със същия носител C, че Iў съвпада с I за всички функционални символи, участващи във j, и за всички предикатни символи. От този модел, като използваме, че jІ е Скулемово допустима за jў, можем да получим пък такъв модел SІ=(C,IІ) на jІ със същия носител C, че IІ да съвпада с Iў за всички функционални символи, участващи във jў, и за всички предикатни символи. Благодарение на това, че функционалните символи, участващи във j, участват и във jў, и на това, че Iў съвпада с I за тези функционални символи, виждаме, че и IІ съвпада с I за тях. Очевидно IІ съвпада с I и за всички предикатни символи. С това проверката на твърдението, че jІ е Скулемово допустима за j, е завършена.

    Сега ще дефинираме важното понятие Скулемова нормална форма. Да предположим, че е дадена една произволна затворена формула j в пренексен вид, в която кванторите са по отношение на различни променливи. Лесно се вижда, че ако поне един от тези квантори е квантор за съществуване и заменим дадената формула с някое нейно Скулемово усилване, то новата формула ще бъде пак в пренексен вид с квантори по отношение на различни променливи, но ще има един квантор за съществуване по-малко. Това е ясно от следното твърдение, което може да се докаже чрез индукция относно участващото в него число k: ако y е безкванторна формула, h е променлива, k₁, k₂, ..., k_k са квантори по отношение на променливи, различни помежду си и различни от h, а t е такъв терм, че никоя от променливите на споменатите квантори не е негова свободна променлива, то субституцията (h:=t) е приложима към формулата k₁k₂...k_ky и резултатът от прилагането е k₁k₂...k_k(h:=t)(y) (при доказателството се използва, че за всяка променлива z, различна от h, субституцииите (h:=t) и (h:=t)_z съвпадат). Нека m е броят на кванторите за съществуване във формулата j. Тогава всяка формула, получена от j чрез m-кратно преминаване от формула към нейно Скулемово усилване, се нарича Скулемова нормална форма на j. От казаното дотук е ясно, че такава формула е затворена универсална формула, Скулемово допустима за j. Оттук в частност виждаме, че ако j^. е Скулемова нормална форма на j, то j е изпълнима точно тогава, когато j^. е изпълнима.

    Пример 5ў. Формулата (3) от пример 5 е Скулемова нормална форма на формулата (2) от същия пример.

    Забележка 4. По тривиални причини всяка универсална формула, в която кванторите са по отношение на различни променливи, е Скулемова нормална форма на себе си.

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

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

    Пример 6. Ще изследваме дали е изпълнима формулата
                               $s("t$u$v"wp(s,t,u,v,w)&"w"x$y"zШp(w,s,z,x,y)),
където p е 5-местен предикатен символ, а s, t, u, v, w, x, y, z са различни променливи (очевидно тази формула е затворена). Тя е еквивалентна на следната формула в пренексен вид:
(4)                            $s"t$u$v"x$y"z(p(s,t,u,v,z)&Шp(t,s,z,x,y)).
Преминавайки четири пъти от формула към нейно Скулемово усилване, получаваме последователно формулите
                               "t$u$v"x$y"z(p(a,t,u,v,z)&Шp(t,a,z,x,y)),
                               "t$v"x$y"z(p(a,t,f(t),v,z)&Шp(t,a,z,x,y)),
                               "t"x$y"z(p(a,t,f(t),g(t),z)&Шp(t,a,z,x,y)),
                               "t"x"z(p(a,t,f(t),g(t),z)&Шp(t,a,z,x,h(t,x))),
където a е нулместен функционален символ, f и g са различни едноместни функционални символи, h е двуместен функционален символ. Последната от тези формули е Скулемова нормална форма на формулата (4). Следователно изпълнимостта на първоначално дадената формула е равносилна с изпълнимостта на последната формула, а значи и с изпълнимостта на множеството на нейните конкретизации. То се състои от всички формули от вида
                               p(a,T,f(T),g(T),Z)&Шp(T,a,Z,X,h(T,X)),
където T, X, Z са затворени термове. За да бъде така описаното множество изпълнимо, необходимо и достатъчно е да съществува структура, в която са верни всички формули от вида p(a,T,f(T),g(T),Z), където T и Z са затворени термове, и са неверни всички формули от вида p(T,a,Z,X,h(T,X)), където T, X и Z са затворени термове. Съществуването на такава структура е равносилно с изискването множеството на формулите от първия вид и множеството на формулите от втория вид да нямат общи елементи. Въпросното изискване ще бъде нарушено точно тогава, когато за някои затворени термове T, Tў, X, Z и Zў е в сила равенството
                               p(a,T,f(T),g(T),Z)=p(Tў,a,Zў,X,h(Tў,X)).
То от своя страна е равносилно със системата от петте равенства
                               a=Tў,  T=a,  f(T)=Zў,  g(T)=X,  Z=h(Tў,X).
С прости разсъждения се вижда, че тя е равносилна със системата
                               T=a,  Tў=a,  X=g(a),  Z=h(a,g(a)),  Zў=f(a)
и следователно има решение. Значи разглежданите две множества от формули имат общ елемент. Връщайки се назад, заключаваме, че дадената формула е неизпълнима.

    Методите, които изучихме, дават алгоритъм, с помощта на който чрез извършване на краен брой действия да можем да установяваме тъждествената вярност на една формула на предикатното смятане винаги, когато такава тъждествена вярност е налице, стига множествата на променливите, на функционалните и на предикатните символи да са избрани по достатъчно конструктивен начин. А именно, тъждествената вярност на една формула е равносилна с тъждествена вярност на затворена формула, получена от нея чрез поставяне на квантори за общност по отношение на всичките й свободни променливи. Отрицанието на въпросната затворена формула е пак затворена формула и тъждествената вярност на дадената формула е равносилна с неизпълнимост на това отрицание. Чрез привеждане в пренексен вид и скулемизация можем да заменим споменатото отрицание с подходяща затворена универсална формула, а по теоремата на Ербран неизпълнимостта на тази формула е равносилна с неизпълнимост на някое крайно множество от нейни конкретизации, стига да се погрижим да съществува поне един нулместен функционален символ. От друга страна при наличието на такова неизпълнимо крайно множество от конкретизации търсенето му би могло поне по принцип да стане като в някаква ефективна последователност се строят всевъзможните крайни множества от конкретизации и за всяко построено такова множество се проверява дали е изпълнимо (в много случаи можем да използваме и значително по-удобни начини за търсене).

    Разбира се описаният по-горе алгоритъм не може да даде резултат в случаите, когато дадената формула не е тъждествено вярна, а споменатата съответна затворена универсална формула има безбройно много конкретизации. Изучените методи позволяват все пак в някои такива случаи (като да речем в пример 5 по-горе) да установим, че отрицанието на дадената формула е изпълнимо и значи тя не е тъждествено вярна, но няма гаранция, че винаги бихме могли да направим това. Нещо повече - една теорема, доказана от Алонзо Чърч (Alonzo Church), показва, че при подходяща сигнатура с краен брой функционални и предикатни символи общ алгоритмичен начин за разпознаване на тъждествената вярност на формулите на предикатното смятане е по принцип невъзможен. За съжаление нямаме възможност да се занимаем по-подробно с този резултат. Ще отбележим само една равносилна негова формулировка, дадена от Алън Тюринг (Alan MathisonTuring). Тя, ако си служим със съвременната терминология, би могла да се изкаже например така: при подходяща сигнатура с краен брой функционални и предикатни символи не съществува машина на Тюринг, която при всяко стартиране върху лента със записана на нея формула на предикатното смятане да завършва работата си така, че наблюдаваната клетка от лентата при завършването на работата да бъде празна точно тогава, когато дадената формула е тъждествено вярна.

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

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