| Previous | Next | Contents |
Теорема на Ербран. Ако съществува поне един нулместен функционален символ, то едно множество от затворени универсални формули е неизпълнимо точно тогава, когато е неизпълнимо някое крайно множество от техни конкретизации.
Доказателство. Нека съществува поне един нулместен функционален символ и нека M е дадено множество от затворени универсални формули. Вече знаем, че за да бъде M изпълнимо, необходимо и достатъчно е да бъде изпълнимо множеството K на всички конкретизации на формулите от M. Следователно M е неизпълнимо точно тогава, когато е неизпълнимо K. Разбира се, ако някое подмножество на K е неизпълнимо, толкова повече цялото К ще бъде неизпълнимо, тъй че при неизпълнимост на някое крайно множество от конкретизации на формули от M можем да бъдем сигурни, че M е неизпълнимо. Остава да докажем обратното - че при неизпълнимост на M някое крайно множество от конкретизации на формули от M е неизпълнимо. За да докажем това твърдение, да предположим, че M е неизпълнимо. Тогава и множеството K ще бъде неизпълнимо, а тъй като то се състои от безкванторни формули, теоремата за компактност за безкванторни формули дава, че K не е локално изпълнимо, т.е. някое крайно подмножество на K е неизпълнимо.
Пример 1. В пример 3 от предходния въпрос видяхме, че е неизпълнимо множеството от четирите универсални формули
Пример 2. Нека M е множеството, съставено от петте универсални формули
При доказателството на теоремата на Ербран ние си послужихме с теоремата за компактност за безкванторни формули. Като използваме теоремата на Ербран, ще получим един друг случай на общата теорема за компактност в предикатното смятане.
Теорема за компактност за затворени универсални формули. Всяко локално изпълнимо множество от затворени универсални формули е изпълнимо.
Доказателство. Нека M е локално изпълнимо множество от затворени универсални формули. Да допуснем, че M не е изпълнимо. Без ограничение на общността можем да приемем, че съществува поне един нулместен функционален символ. В такъв случай обаче теоремата на Ербран позволява да твърдим, че някое крайно множество от конкретизации на формули от M е неизпълнимо. Избирайки за всяка формула q от това крайно множество някоя формула от M, на която q е конкретизация, получаваме неизпълнимо крайно подмножество на M, а това противоречи на локалната изшълнимост на M.
В предходния въпрос видяхме, че при определени (твърде силни) ограничения съществува алгоритъм, чрез който за всяко крайно множество от затворени универсални формули можем да познаем дали е изпълнимо или не. В общия случай (когато не се поставят споменатите ограничения) такъв алгоритъм няма (доказано е, че не е възможен!). С помощта на теоремата на Ербран все пак се вижда, че в общия случай съществува алгоритъм, който за всяко неизпълнимо крайно множество от затворени универсални формули установява чрез краен брой действия неговата неизпълнимост, а за изпълнимо крайно множество установява неговата изпълнимост само в случай че при прилагане към множеството той завършва своята работа.Сега ще опишем (в общи линии) един такъв алгоритъм.
Както преди, и сега без ограничение на общността можем да считаме, че съществува поне един нулместен функционален символ. При това положение едно множество M от затворени универсални формули е неизпълнимо точно тогава, когато е неизпълнимо някое крайно множество от конкретизации на формули от M. Ние ще се ограничим със случая, когато M не е празно, тъй като празното множество е изпълнимо по тривиални причини. Нека освен това M е крайно. Тогава можем да приемем още, че функционалните символи са краен брой, а именно - функционалните символи, използвани при построяването на формулите от M, и евентуално някакъв допълнително добавен нулместен функционален символ (нужда от такова добавяне възниква тогава, когато при построяването на формулите от M не е използван никакъв нулместен функционален символ). В такъв случай всевъзможните затворени термове, които могат да се образуват, ще могат алгоритмично да бъдат подредени в редица - крайна или безкрайна. Същото ще важи и за всевъзможните конкретизации на формулите от M - и конкретизациите ще могат алгоритмично да бъдат подредени в една крайна или безкрайна редица q0, q1, q2, q3... Да положим сега
| 0. Полагаме n=0. |
| 1. Проверяваме дали множеството Kn е изпълнимо. Ако е изпълнимо, преминаваме към инструкция 2, а ако не е, прекратяваме работата и обявяваме, че M е неизпълнимо. |
| 2. Ако Kn е последен член на редицата K0, K1, K2, K3, ..., прекратяваме работата и обявяваме, че M е изпълнимо. В противен случай увеличаваме n с 1 и преминаваме отново към инструкция 1. |
Забележка. С малки изменения направените преди малко разглеждания са възможни и в случая на такова множество M от затворени универсални формули, което не е непременно крайно, но елементите му могат да бъдат алгоритмично подредени в редица (в този случай не е сигурно, че функционалните символи са краен брой, но можем да считаме, че те също допускат алгоритмично подреждане в редица).
От теоремата на Ербран може да се направи и още един извод с, тъй да се каже, мирогледно значение. Той е следният: ако M е неизпълнимо множество от затворени универсални формули, което е алгоритмично подредено в редица (крайна или безкрайна), неизпълнимостта на M може да бъде доказана по един твърде елементарен начин - чрез установяване на неизпълнимостта на подходящо крайно множество от безкванторни формули, които са конкретизации на формули от M (това, че M е алгоритмично подредено в редица, има значение, защото осигурява общ начин за установяване на принадлежност към M).
Последно изменение: 26.07.1999 г.
| Previous | Next | Contents |