БЕЗКВАНТОРНИ ФОРМУЛИ

    БФ1. Всяка атомарна формула е безкванторна формула.
    БФ2. Ако j е безкванторна формула, то Шj също е безкванторна формула.
    БФ3,4. Ако j₁ и j₂ са безкванторни формули, то (j₁&j₂) и (j₁Ъj₂) също са безкванторни формули.

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

    Безкванторните формули образуват един важен клас от формули, защото, както ще видим по-късно, въпросът за изпълнимост на произволно множество от формули може да се сведе до въпрос за изпълнимост на подходящо множество от безкванторни формули.

    Всяка от атомарните формули, използвани при получаването на дадена формула (не непременно безкванторна), ще наричаме нейна атомарна подформула (атомарна компонента). Това уславяне оформяме във вид на следната индуктивна дефиниция, която определя на кои формули дадена атомарна формула a е атомарна подформула:

    АП1. a е атомарна подформула на a.
    АП2. Ако a е атомарна подформула на j, то a е атомарна подформула и на Шj.
    АП3,4. Ако a е атомарна подформула на j₁ или на j₂, то a е атомарна формула на (j₁&j₂) и на (j₁Ъj₂).
    АП5,6. Ако a е атомарна подформула на j, а x е произволна променлива, то a е атомарна подформула на "xj и на $xj.

    От тази дефиниция, като се използва еднозначният синтактичен анализ на формулите, се получава, че една атомарна формула има за атомарна подформула себе си и само себе си, че атомарните подформули на коя да е от формулите Шj, "xj и $xj са същите както на j и че множеството на атомарните подформули на коя да е от формулите (j₁&j₂) и (j₁Ъj₂) е обединение на множеството на атомарните подформули на j₁ и множеството на атомарните подформули на j₂. Това позволява индуктивно да покажем, че множеството на атомарните подформули на коя да е формула е непразно крайно множество от атомарни формули, а също че всяка нейна свободна променлива е свободна променлива на някоя формула от въпросното множество. Чрез индукция, съобразена с дефиницията за безкванторна формула, и с използване на точки АП1, АП2 и АП3,4 от следващата дефиниция се показва, че за безкванторни формули е вярно и обратното - когато дадена променлива е свободна променлива на някоя от атомарните подформули на една безкванторна формула, тя е свободна променлива и на самата формула. Оттук е ясно, че една безкванторна формула е затворена точно тогава, когато е затворена всяка от атомарните й подформули (за произволни формули положението е друго - например, ако p е едноместен предикатен символ и x е променлива, то формулата "xp(x) е затворена, но нейната атомарна подформула p(x) не е затворена).

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

    Лема за двоични функции, съответни на безкванторни формули. Нека a₁, ..., a_n (nі1) са различни атомарни формули, а j е безкванторна формула, на която атомарните подформули са измежду a₁, ..., a_n. Тогава съществува такава двоична функция F на n променливи, че за всяка конфигурация (S,v) е в сила равенството j^S,v=F(a₁^S,v,...,a_n^S,v).

    Доказателство. Индукция, съобразена с дефиницията на понятието безкванторна формула.

    Следствие. Нека j е безкванторна формула, а (S,v) и (Sў,vў) са такива конфигурации, че за всяка атомарна подформула a на j е изпълнено равенството a^S,v=a^Sў,vў. В такъв случай имаме и равенството j^S,v=j^Sў,vў.

    Забележка 1. Ако при предположенията на горната лема дадените атомарни формули a₁, ..., a_n са затворени, то и формулата j ще бъде затворена, тъй че всъщност за всяка структура S ще имаме равенството j^S=F(a₁^S,...,a_n^S).

    Забележка 2. Функцията, чието съществуване се твърди в доказаната лема, е единствена. Това е така, защото за всяка n-ка (t₁,...,t_n) от елементи на множеството {0,1}, съществува такава конфигурация (S,v), че да бъдат в сила равенствата a_i^S,v=t_i, i=1,...,n. За да се убедим в последното, достатъчно е да приложим основната лема за осъществимост и да изберем конфигурацията (S,v) така. че атомарните формули a_i, отговарящи на номер`а i, за които t<sub>i</sub>=1, да бъдат верни в (S,v), а атомарните формули a<sub>i</sub>, отговарящи на номер`а i, за които t_i=0, да бъдат неверни в (S,v).

    Забележка 3. Доказаната лема допуска следното обръщане: ако a₁, ..., a_n (nі1) са различни атомарни формули, а F е двоична функция на n променливи, то съществува такава безкванторна формула j, че атомарните подформули на j са измежду a₁, ..., a_n и за всяка конфигурация (S,v) е в сила равенството от лемата (доказателството може да се извърши като се използва теоремата на Бул за пълнота на множеството от двоичните функции отрицание, конюнкция и дизюнкция).

    Следното твърдение ще ни бъде от полза по-нататък:

    Лема за Ербранова изпълнимост на множество от безкванторни формули. За всяко изпълнимо множество M от безкванторни формули съществува Ербранова конфигурация, която го удовлетворява, а ако M е от затворени формули и съществува поне един нулместен функционален символ, то съществува и Ербранова структура, която е модел на M.

    Доказателство. Нека M е изпълнимо множество от безкванторни формули. Разглеждаме конфигурация (S,v), която удовлетворява M, и с помощта на основната лема за осъществимост строим такава Ербранова конфигурация (Sў,vў), че всички атомарни формули, верни в (S,v), да бъдат верни в (Sў,vў), а всички атомарни формули, неверни в (S,v), да бъдат неверни в (Sў,vў). Като приложим следствието от лемата за двоични функции, съответни на безкванторни формули, и използваме, че (S,v) удовлетворява M, заключаваме, че (Sў,vў) също удовлетворява M. В случай, че формулите от M са затворени и съществува поне един нулместен функционален символ, можем да разсъждаваме по подобен начин, като разгледаме структура S, която е модел на M, и с помощта на основната лема за осъществимост построим такава Ербранова структура Sў, че всички затворени атомарни формули, верни в S, да бъдат верни в Sў, а всички затворени атомарни формули, неверни в S, да бъдат неверни в Sў.

    Лемата за двоичните функции, съответни на безкванторни формули, показва един начин, чрез който за произволно крайно множество M от безкванторни формули може да се изследва дали е изпълнимо (при условие, че е налице списък на елементите на M). Начинът е следният (при непразно M): съставяме списък на атомарните формули, които са подформули на поне една формула от M, и ако този списък се състои от формулите a₁, ..., a_n, то за всяка формула j от M разглеждаме съответната двоична функция F със свойството от лемата и изследваме дали съществува n-ка от елементи на множеството {0,1}, за която всички така получени съответни функции приемат едновременно стойност 1 (ако такава n-ка съществува, то M е изпълнимо, а ако не съществува, то M е неизпълнимо). Използването на този начин понякога е удобно, но в други случаи изисква прекалено много труд. Освен това начинът се отнася само за крайни множества от безкванторни формули. По тези причини ние скоро ще разгледаме и един друг подход.

    Засега ще отбележим още едно свойство на безкванторните формули. В неговата формулировка ще участва едно понятие, което сега ще дефинираме. Нека са дадени две конфигурации (S,v) и (Sў,vў), където S=(C,I), Sў=(Cў,Iў). Нека B е релация между елементи на C и елементи на Cў, т.е. B е подмножество на декартовото произведение CґCў; за да изразим, че дадена двойка (c,cў) от CґCў принадлежи на B, ще пишем cBcў (когато е изпълнено условието cBcў, можем да разглеждаме елементите c и cў като съответни един на друг). Ще казваме, че B е бисимулация между дадените две конфигурации, ако са изпълнени следните условия:
    а₀) за всеки елемент w на W₀ е изпълнено съотношението I(w)BIў(w);
    а₁) всеки път, когато wОW_n, където n>0, и за дадени елементи c₁, ..., c_n на C и дадени елементи c₁ў, ..., c_nў на Cў са изпълнени съотношенията c₁Bc₁ў, ..., c_nBc_nў, в сила е и съотношението I(w)(c₁,...,c_n)BIў(w)(c₁ў,...,c_nў);
    б₀) за всеки елемент p на P₀ е изпълнено равенството I(p)=Iў(p);
    б₁) всеки път, когато pОP_n, където n>0, и за дадени елементи c₁, ..., c_n на C и дадени елементи c₁ў, ..., c_nў на Cў са изпълнени равенствата c₁Bc₁ў, ..., c_nBc_nў, в сила е и съотношението I(p)(c₁,...,c_n)=Iў(p)(c₁ў,...,c_nў);
    в) за всяка променлива x е изпълнено съотношението v(x)Bvў(x).
По аналогичен начин се дефинира кога B е бисимулация между две структури S=(C,I) и Sў=(Cў,Iў) - изисква се да са изпълнени горните условия без последното.

    Важен специален вид бисимулации са изоморфизмите. Под изоморфизъм между две конфигурации или две структури с носители съответно C и Cў се разбира такава бисимулация B между тези конфигурации или структури, че за всяко c от C условието cBcў е изпълнено точно за един елемент cў на Cў и за всеки елемент cў на Cў същото условие е изпълнено точно за един елемент c на C. Един по-общ вид бисимулации са тоталните - при тях изискването е за всяко c от C условието cBcў да е изпълнено поне за един елемент cў на Cў и за всеки елемент cў на Cў същото условие да е изпълнено поне за един елемент c на C. Ето и един прост вид нетотални бисимулации. Ще казваме, че една структура (Cў,Iў) е разширение на дадена структура (C,I), ако CНCў, съответствията I и Iў съвпадат за всички елементи на W₀ИP₀, а за всеки елемент s на W_nИP_n изображението (операция или предикат) Iў(s) е продължение на изображението I(s). Не представлява трудност да се провери, че ако една структура Sў=(Cў,Iў) е разширение на дадена структура S=(C,I) и означим с B множеството на двойките от вида (c,c), където cОC, то B е бисимулация между S и Sў, а също между (S,v) и (Sў,v) при всеки избор на оценката v в S на променливите. Очевидно тази бисимулация ще бъде тотална само в случая, когато C=Cў (в този случай тя ще бъде даже и изоморфизъм).

    Свойството, за което стана дума, се изказва чрез следното твърдение.

    Бисимулационна лема. Ако B е бисимулация между две конфигурации (S,v) и (Sў,vў), то за всеки терм t е изпълнено съотношението t^S,vBt^Sў,vў и за всяка безкванторна формула j е в сила равенството j^S,v=j^Sў,vў. Ако B е бисимулация между две структури S и Sў, то за всеки затворен терм t е изпълнено съотношението t^SBt^Sў и за всяка затворена безкванторна формула j е в сила равенството j^S=j^Sў.

    Доказателство. Твърденията за случая на терм се доказват чрез индукция, съобразена с дефиницията на понятието терм, и, като се използват те, чрез индукция съобразена с дефиницията на понятието безкванторна формула се доказват твърденията за случая на безкванторна формула.

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

    Пример. Да разгледаме формулата "xp(x), където p е едноместен предикатен символ, а x е променлива. Лесно могат да се посочат такива две структури, че да съществува бисимулация между тях и въпреки това споменатата формула да бъде вярна в едната от двете структури и невярна в другата. За целта е достатъчно да вземем два различни обекта c и d и след това да построим структури ({c},I) и ({c,d},Iў), такива, че втората да е разширение на първата и да са изпълнени равенствата I(p)(c)=1, Iў(p)(d)=0.

    Забележка. От горния пример и бисимулационната лема следва, че разгледаната в примера формула не е еквивалентна на никаква безкванторна формула.

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