Previous | Next | Contents |
Сега ще докажем една теорема, която обхваща като частни случаи и двете споменати твърдения.
Обща теорема за компактност. Всяко локално изпълнимо множество от формули на предикатното смятане е изпълнимо.
Доказателство. Нека M е локално изпълнимо множество от формули на предикатното смятане. Нека s е субституция, която на свободните променливи на формулите от M съпоставя нулместни функционални символи, неучастващи в никоя формула от M, така, че на различни такива променливи да отговарят различни символи (такава субституция може да бъде дефинирана след евентуално разширяване на сигнатурата на езика). С Mў да означим множеството на формулите, които се получават като приложим s към всяка от формулите от M. Така построеното множество Mў се състои от затворени формули и знаем от допълнителната лема за равноизпълнимост, че ако то е изпълнимо, M също е изпълнимо. Засега, прилагайки същата лема към крайните подмножества на M, можем да забележим, че множеството Mў също е локално изпълнимо (използваме, че всяко крайно подмножество на Mў може да се получи от някое крайно подмножество на M чрез прилагане на s към формулите от това множество). На всяка формула от Mў да съпоставим еквивалентна на нея формула, която е в пренексен вид и не съдържа квантори с една и съща променлива. Нека MІ е множеството на така съпоставените формули. Очевидно MІ също е локално изпълнимо, а ако докажем, че е изпълнимо, ще можем да заключим, че и Mў е изпълнимо. Като заменим всяка формула от MІ с подходяща нейна Скулемова нормална форма (евентуално разширявайки сигнатурата на езика), получаваме такова множество M. от затворени универсални формули, за което основната лема за равноизпълнимост позволява да твърдим, че е локално изпълнимо и че ако е изпълнимо, то и MІ е изпълнимо. Като приложим към множеството M. теоремата за компактност за затворени универсални формули, получаваме, че това множество е изпълнимо, а оттук, връщайки се назад, заключаваме последователно, че и множествата MІ, Mў и M са изпълними.
Последно изменение: 26.07.1999 г.
Previous | Next | Contents |