Previous  Next  Contents

 

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

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

    Лема за разширяване на локално изпълнимо множество. Нека M е произволно локално изпълнимо множество от формули, а q е произволна формула. Тогава поне едно от множествата MИ{q} и MИ{Шq} също е локално изпълнимо.

    Доказателство. Да допуснем, че никое от множествата MИ{q} и MИ{Шq} не е локално изпълнимо. Тогава всяко от тях ще притежава неизпълнимо крайно подмножество. Нека K и L са неизпълними крайни подмножества съответно на MИ{q} и на MИ{Шq}. Да означим с P сечението на KИL с M. Очевидно KНPИ{q}, LНPИ{Шq}. Множеството P е крайно и се съдържа в M, следователно P е изпълнимо, т.е. съществува конфигурация, която удовлетворява P. Разглеждаме една такава конфигурация. Ако формулата q е вярна в нея, получава се, че тази конфигурация удовлетворява K, а ако q не е вярна в нея - че тя удовлетворява L. Тъй като нито K, нито L е изпълнимо, достигаме до противоречие, следователно направеното в началото на доказателството допускане е погрешно.

    Сега вече можем да изпълним обещаното преди горната лема.

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

    Доказателство. Нека M е дадено локално изпълнимо множество от безкванторни формули. Ще покажем, че M е изпълнимо. Разглеждаме обединението на множествата от атомарните подформули на всевъзможните формули от M. Това обединение е едно множество от атомарни формули и то, като всяко множество от думи, е крайно или изброимо. Подреждаме въпросните атомарни формули в една редица (крайна или безкрайна) c1, c2, c3, ..., значи тези формули ще имат вида cj при jОJ, където J е или някой начален отрез {1,2,...,n} от множеството на целите положителни числа, или множеството на всички цели положителни числа (тривиалният случай, когато множеството M е празно, също се обхваща, ако считаме, че споменатият преди малко начален отрез е празен при n=0). За всяко j от множеството {0}ИJ ще дефинираме едно множество Mj по следния индуктивен начин: полагаме M0=M и след това за всеки номер j от J, за който Mj-1 вече е определено, полагаме

Mj  = {
 		 Mj-1 И{cj},  ако Mj-1 И{cj} е локално изпълнимо,
Mj-1 И{Шcj}  в противен случай.
Очевидно Mj-1 Н Mj за всяко j от J, и следователно Mj Н Mk винаги, когато j,kО{0}ИJ и j<k. Лемата за разширяване на локално изпълнимо множество позволява да докажем индуктивно, че Mj е локално изпълнимо за всяко jО{0}ИJ (ако Mj-1 е локално изпълнимо, то поне едно от множествата Mj-1 И{cj} и Mj-1 И{Шci} също е локално изпълнимо). Нека MС е обединението на всички множества Mj, където jО{0}ИJ (разбира се, ако отрезът J е краен, то MС е всъщност онова от множествата Mj, което има най-голям номер). Лесно се вижда, че всяко крайно подмножество на това обединение се съдържа в някое от множествата Mj и следователно е изпълнимо. Освен това всеки път, когато a е атомарна подформула на формула от M, някоя от формулите a и Шa принадлежи на MС. Да означим с T множеството на онези атомарни формули, които принадлежат на MС, а с F - множеството на всички останали атомарни формули. Основната лема за осъществимост позволява да твърдим, че съществува Ербранова конфигурация (S,v), в която всички формули от T са верни, а всички формули от F са неверни. Ще покажем, че тази конфигурация удовлетворява множеството M. За целта да разгледаме произволна формула j от M. Образуваме множеството Q, състоящо се от формулата j, от нейните атомарни подформули, принадлежащи на MС, и от отрицанията на останалите й атомарни подформули. Това множество е изпълнимо, защото е крайно подмножество на MС. Значи има някаква конфигурация (Sў,vў), удовлетворяваща Q. Не е трудно да се провери, че за всяка атомарна подформула a на j е изпълнено равенството aS,v=aSў,vў(ако aОMС, то aОT и aОQ, а ако aПMС, то aОF и ШaОQ). Оттук, както знаем, следва и равенството jS,v=jSў,vў. Тъй като формулата j принадлежи на Q, а конфигурацията (Sў,vў) удовлетворява Q, това равенство показва, че и конфигурацията (S,v) удовлетворява j.

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

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

 

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

 Previous  Next  Contents