СЕКВЕНЦИИ

    Пример 1. Секвенциите ({j,y},{q}), ({j,y},Ж) и (Ж,Ж), където j, y, q са дадени формули, можем да запишем съответно във вида j,y-:q, j,y-: и -:, а също и във вида q:-j,y, :-j,y и :- (последната от тези три секвенции ще наричаме празна секвенция).

    Забележка. Използването на секвенции като апарат на математическата логика води началото си от изследванията на Герхард Генцен (Gerhard Gentzen). Знака  :-  сме заимствали от езика за програмиране Пролог. В математическата логика по-често се среща използване на стрелка и на обратна стрелка съответно вместо знаците  -:  и  :- , но при нас поне обикновената стрелка е вече ангажирана за означаване на импликация (бихме могли евентуално да използваме някаква по-особена стрелка, но няма да го правим).

    Една секвенция G-:D ще наричаме затворена, ако всички елементи на множествата G и D са затворени формули (разбира се, ако някое от тези две множества е празно, условието всичките му елементи да са затворени формули е изпълнено по тривиални причини; в частност празната секвенция е затворена).

    За една конфигурация (S,v) ще казваме, че опровергава дадена секвенция G-:D, ако всички формули от G са верни в (S,v), а всички формули от D са неверни в (S,v) (разбира се, ако някое от множествата G и D е празно, то съответното условие за вярност или невярност на всички негови формули е изпълнено по тривиални причини). Ще казваме, че секвенцията G-:D е вярна в конфигурацията (S,v), или още, че (S,v) удовлетворява G-:D, ако (S,v) не опровергава G-:D, т.е. ако поне една формула от G е невярна в (S,v) или поне една формула от D е вярна в (S,v). В противен случай, т.е. когато (S,v) опровергава G-:D, ще казваме, че G-:D е невярна в (S,v). Ако дадена секвенция G-:D е затворена, по подобен начин дефинираме кога една структура S опровергава G-:D, кога G-:D е вярна в S и кога G-:D е невярна в S. Ясно е, че ако (S,v) е конфигурация, то една затворена секвенция е вярна в тази конфигурация точно тогава, когато е вярна в съответната структура S. Една секвенция G-:D ще наричаме тъждествено вярна в дадена структура S, ако G-:D е вярна в конфигурацията (S,v) при всяка оценка v в S на променливите. Секвенция, която е тъждествено вярна във всяка структура, ще наричаме тъждествено вярна.

    Пример 2. Ако двете страни на една секвенция имат общ елемент, то секвенцията е тъждествено вярна.

    Уславяме се да наричаме тривиално тъждествено вярна всяка секвенция, на която двете страни имат общ елемент.

    Пример 3. Празната секвенция е невярна във всяка конфигурация (и във всяка структура).

    Пример 4. Нека j е произволна формула. Очевидно секвенцията -:j е вярна точно в онези конфигурации, в които е вярна j, а секвенцията j-: е вярна точно в онези конфигурации, в които е невярна j. Следователно, ако j е например атомарна формула, то всяка от споменатите две секвенции ще бъде вярна в някои конфиурации и невярна в други.

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

    Пример 4 показва, че произволна формула j е еквивалентна на съответната секвенция -:j. Лесно се вижда, че и обратно всяка секвенция е еквивалентна на някоя формула. И наистина при kі1, lі1 секвенциите

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

    Следващите две твърдения се проверяват чрез непосредствено прилагане на нужните дефиниции.

    Закон за отрицание в заключението. За всеки две крайни множества от формули G и D и за всяка формула j, секвенцията G-:DИ{Шj} е еквивалентна на секвенцията GИ{j}-:D.

    Закон за отрицание в предпоставката. За всеки две крайни множества от формули G и D и за всяка формула j, секвенцията GИ{Шj}-:D е еквивалентна на секвенцията G-:DИ{j}.

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

    Сега ще изкажем още няколко лесно доказуеми твърдения, като във всяко от тях G и D означават произволни крайни множества от формули, а j₁ и j₂ - произволни формули.

    Закон за конюнкция в заключението. Секвенцията G-:DИ{j₁&j₂} е еквивалентна на множеството от секвенциите G-:DИ{j₁} и G-:DИ{j₂}.

    Закон за конюнкция в предпоставката. Секвенцията GИ{j₁&j₂}-:D е еквивалентна на секвенцията GИ{j₁,j₂}-:D.

    Закон за дизюнкция в заключението. Секвенцията G-:DИ{j₁Ъj₂} е еквивалентна на секвенцията G-:DИ{j₁,j₂}.

    Закон за дизюнкция в предпоставката. Секвенцията GИ{j₁Ъj₂}-:D е еквивалентна на множеството от секвенциите GИ{j₁}-:D и GИ{j₂}-:D.

    Да докажем например закона за конюнкция в заключението. Да предположим най-напред, че дадена конфигурация (S,v) удовлетворява секвенцията G-:DИ{j₁&j₂}. Това означава, че някоя формула от G е невярна в (S,v) или някоя формула от D е вярна в (S,v) или формулата j₁&j₂ е вярна в (S,v). Очевидно във всеки от тези три случая (S,v) удовлетворява секвенциите G-:DИ{j₁} и G-:DИ{j₂}.  Обратно, да предположим, че дадена конфигурация (S,v) удовлетворява секвенциите G-:DИ{j₁} и G-:DИ{j₂}. Тогава при i=1,2 имаме някой от следните три случая: някоя формула от G е невярна в (S,v) или някоя формула от D е вярна в (S,v) или формулата j_i е вярна в (S,v). Ако при някое от двете i имаме първия или втория случай, то верността на секвенцията G-:DИ{j₁&j₂} в (S,v) е непосредствено ясна, а ако и за двете i имаме третия случай, то конюнкцията j₁&j₂ ще бъде вярна в (S,v) и значи секвенцията G-:DИ{j₁&j₂} пак ще бъде вярна в (S,v).

    Приели сме, че импликацията j₁®j₂ на две формули j₁ и j₂ е формулата Шj₁Ъj₂. Като използваме това и изказаните по-горе твърдения, лесно получаваме при същите предположения за G, D, j₁ и j₂:

    Закон за импликация в заключението. Секвенцията G-:DИ{j₁®j₂} е еквивалентна на секвенцията GИ{j₁}-:DИ{j₂}.

    Закон за импликация в предпоставката. Секвенцията GИ{j₁®j₂}-:D е еквивалентна на множеството от секвенциите G-:DИ{j₁} и GИ{j₂}-:D.

    Секвенция, на която всички членове са безкванторни формули, ще наричаме безкванторна, а секвенция, на която всички членове са атомарни формули - елементарна.

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

    Доказателство. Ще  използваме индукция относно сумарния брой на участията на знаците "Ш", "&" и "Ъ" в членовете на секвенцията (в случаите, когато дадена формула принадлежи и на двете страни на секвенцията, участията на гореизброените знаци в тази формула се броят двукратно). Индукцията ще се състои от следните две неща: проверка, че твърдението е вярно, когато споменатият брой е 0, и доказателство, че ако твърдението е вярно, когато въпросният брой е по-малък от дадено положително цяло число h, то твърдението е вярно и тогава, когато той е равен на h. Когато за една безкванторна секвенция споменатият брой е 0, секвенцията очевидно е елементарна, поради което твърдението е вярно. Нека сега е дадено някое положително цяло число h, такова, че твърдението, което доказваме, е вярно за всяка безкванторна секвенция с по-малко от h участия на знаците "Ш", "&" и "Ъ" в нейните членове. Да разгледаме произволна безкванторна секвенция с h участия на тези знаци. Понеже h е положително, в поне една от страните на секвенцията има формула, която не е атомарна. Следователно разглежданата секвенция има поне един от следните шест вида, където G и D са крайни множества от безкванторни формули, j, j₁, j₂ са безкванторни формули и при означените прибавяния на формула към множество тя не е негов елемент:

    Следствие. Всяка безкванторна формула е еквивалентна на някое непразно крайно множество от непразни елементарни секвенции, на които членовете са измежду атомарните подформули на дадената формула.¹

    Пример 5. Да разгледаме еквиваленцията a«Шa, където a е дадена атомарна формула. Тази еквиваленцияс е неизпълнима и това се вижда съвсем лесно по същия начин, както се вижда, че е неизпълним частният й случай s(b,b)«Шs(b,b), с който се срещнахме при прилагане на метода на Ербран към задачата за бръснаря. Ще покажем все пак, как неизпълнимостта на формулата a«Шa може да се установи и с помощта на горното следствие. Тази формула е еквивалентна на секвенцията -:a«Шa. Като вземем пред вид дефиницията за еквиваленция на две формули и закона за конюнкция в заключението, получаваме, че от своя страна последната секвенция е еквивалентна на множеството от двете секвенции -:a®Шa и -:Шa®a. От закона за импликация в заключението следва, че тези секвенции са еквивалентни съответно на секвенциите a-:Шa и Шa-:a. Като използваме всичко това и още законите за отрицание в заключението и за отрицание в предпоставката, получаваме, че формулата a«Шa е еквивалентна на множеството от двете елементарни секвенции a-: и -:a. Това очевидно още веднаж показва неизпълнимостта на споменатата формула.

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

    Преди това обаче ще отбележим и една друга възможност за използване на свеждането на безкванторна формула към елементарни секвенции, а именно - за да изследваме дали дадена безкванторна формула е тъждествено вярна без да се занимаваме с пресмятане на стойностите на съответната двоична функция и без да свеждаме въпроса до изследване дали е изпълнимо отрицанието на дадената формула. За целта първо нека обърнем внимание на това, че една елементарна секвенция е тъждествено вярна точно тогава, когато тя е тривиално тъждествено вярна (в едната посока твърдението следва от пример 2, а в другата - от основната лема за осъществимост). Да предположим сега, че q е дадена безкванторна формула, за която искаме да проверим дали е тъждествено вярна. За да проверим това, можем да постъпим по следния начин: намираме крайно множество от елементарни секвенции, което е еквивалентно на q, и проверяваме дали всички секвенции от това множество са тривиално тъждествено верни. Ако се окаже, че е така, то формулата q е тъждествено вярна, а в противен случай не е.

    Пример 6. Нека q е формулата (a₁&a₂)Ъa₃®(a₁Ъa₃)&(a₂Ъa₃), където a₁, a₂, a₃ са различни атомарни формули. Като се използват доказаните в този въпрос твърдения, вижда се, че q е еквивалентна на множеството от следните четири елементарни секвенции:

    Пример 7. Нека q е формулата a₁Ъa₂®a₁&a₂, където a₁ и a₂ са различни атомарни формули. Тази формула е еквивалентна на множеството от следните елементарни секвенции:

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

    Пример 8. Да разгледаме отново формулата a«Шa, където a е дадена атомарна формула. Като използваме общия метод за свеждане на безкванторна формула към елементарни секвенции, получаваме, че отрицанието Ш(a«Шa) на споменатата формула е еквивалентно на елементарната секвенция a-:a (преобразованията обаче са по-дълги отколкото преобразованията в пример 5). Тъй като получената елементарна  секвенция е тривиално тъждествено вярна, заключаваме, че въпросното отрицание е тъждествено вярно и значи по още един начин установяваме неизпълнимостта на формулата a«Шa.

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

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