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

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

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

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

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

    Тъй като множеството на всички формули е изброимо, формулите от Γ могат да бъдат подредени в редица - крайна или безкрайна. Случаят, когато тази редица е крайна, е ясен, затова да предположим, че тя е безкрайна. Нека нейните членове са φ1, φ2, φ3, … Една крайна редица от литерали (λ1,…,λn) ще наричаме допустима относно редицата (φ1,φ2,φ3,…), ако λi е член на дизюнкцията φi при i=1,…,n и никой член на редицата (λ1,…,λn) не е отрицание на друг неин член (понеже редицата (φ1,φ2,φ3,…) ще бъде една и съща в рамките на това доказателство, по-нататък допустимите относно нея редици ще наричаме просто допустими). От тази дефиниция следва веднага, че всяка редица, която е начало на допустима крайна редица от литерали, също е допустима, и че всяка n-членна допустима редица от литерали има най-много краен брой n+1-членни допустими продължения. Освен това поради локалната изпълнимост на множеството Γ съществуват допустими редици с произволно голям брой членове. Тези свойства на множеството на допустимите редици позволяват да приложим едно твърдение (вж. накрая), известно като лема на Кьониг, и да заключим, че съществува безкрайна редица от литерали, на която всяка крайна начална част е допустима. Множеството на членовете на тази безкрайна редица е точно такова множество, каквото търсим.  □

    Следствие (втора форма на теоремата за компактност за безкванторни формули). Всяко неизпълнимо множество от безкванторни формули има неизпълнимо крайно подмножество.

    Когато е дадена такава безкрайна редица (φ1,φ2,φ3,…) от елементарни дизюнкции, че да разполагаме с алгоритъм за намиране на последователните нейни членове, може да се посочи алгоритъм, който в случай, че множеството на членовете й е неизпълнимо, дава нейна крайна начална част с неизпълнимо множество на членовете. Един такъв алгоритъм може да бъде описан по следния начин: последователно изброяваме всичките едночленни, всичките двучленни, всичките тричленни и т.н. допустими относно (φ1,φ2,φ3,…) редици от литерали и действаме по този начин, докато евентуално намерим естествено число n, за което няма нито една n-членна редица, допустима относно (φ1,φ2,φ3,…). Намерим ли такова n, можем да сме сигурни, че множеството {φ1,…,φn} не е изпълнимо. В случай, че безкрайното множество {φ1,φ2,φ3,…} е неизпълнимо, съществуването на такова n е гарантирано от изказаното преди малко следствие.

    Лемата на Кьониг най-често се формулира в терминологията на теорията на графите, но може да се изкаже и като следното твърдение, непосредствено приложимо в ситуацията от горното доказателство: ако L е някакво множество, а F е такова множество от крайни редици от елементи на L, че всяка редица, която е начало на редица от F, също принадлежи на F, всяка n-членна редица от F има най-много краен брой n+1-членни продължения, принадлежащи на F, и в множеството F има редици с произволно голям брой членове, то съществува безкрайна редица от елементи на L, на която всяка крайна начална част принадлежи на множеството F. Така изказаното твърдение може да се докаже по следния начин. Нека са дадени множества L и F, удовлетворяващи предположенията на твърдението. Да се условим да наричаме обещаваща такава редица от F, която има в F продължения с произволно голям брой членове. От направените предположения е ясно, че празната редица принадлежи на F и е обещаваща, а лесно се съобразява още, че всяка n-членна обещаваща редица има поне едно n+1-членно обещаващо продължение (можем да се убедим в това чрез допускане на противното). От тези две свойства следва, че можем да изберем елемент l1 на L, за който редицата с единствен член l1 е обещаваща, след това да изберем елемент l2 на L, за който двучленната редица (l1,l2) е обещаваща, после да изберем елемент l3, за който тричленната редица (l1,l2,l3) е обещаваща, и така нататък до безкрайност. Получаващата се по този начин безкрайна редица (l1,l2,l3,…) от елементи на L има желаното свойство.

    Забележка 1. В общия случай изложеното по-горе доказателство използва аксиомата за избора. Нейното използване може да се избегне, когато множеството L е изброимо (такъв е интересуващият ни тук случай - в него можем да вземем в качеството на L множеството на всички литерали). Действително, ако L е изброимо, то можем да подредим неговите елементи в една безкрайна редица, след това на всяка n-членна обещаваща редица да съпоставим онова нейно обещаващо n+1-членно обещаващо продължение, чийто последен член е с най-малък възможен номер при подреждането на елементите на L, и при построяването на безкрайната редица (l1,l2,l3,…) да си служим само с така съпоставени продължения. В конкретния случай, който ни интересува, има и друга възножност да се избегне използването на аксиомата за избора - това, че във всяка от елементарните дизюнкции φ1, φ2, φ3, … има подредба на нейните членове и можем при образуването на n+1-членно обещаващо продължение на дадена n-членна обещаваща редица да добавяме към нея като нов член първия подходящ за целта измежду членовете на дизюнкцията φn+1.

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

 

Последно изменение във файла:  7 ноември 2005 г.