КРИТЕРИЙ ЗА НЕИЗПЪЛНИМОСТ НА МНОЖЕСТВО ОТ ЕЛЕМЕНТАРНИ СЕКВЕНЦИИ

    Теорема за противоречивост на неизпълнимите множества от елементарни секвенции. Всяко неизпълнимо множество от елементарни секвенции е ec-противоречиво.

    Доказателство. Тъй като всяка елементарна секвенция е еквивалентна на някоя безкванторна формула, теоремата за компактност за безкванторни формули гарантира, че всяко неизпълнимо множество от елементарни секвенции има неизпълнимо крайно подмножество. Поради това ще бъде достатъчно да докажем, че всяко неизпълнимо крайно множество от елементарни секвенции е ec-противоречиво (използваме разбира се и обстоятелството, че всяко множество от секвенции, което има ec-противоречиво подмножество, също е ec-противоречиво). Ограничавайки се с разглеждането на крайни множества от елементарни секвенции, придобиваме възможността да си послужим с индукция относно броя на формулите в обединението на всички предпоставки и всички заключения на секвенции от множеството. За краткост да наречем въпросния брой сложност на множеството. Ако едно неизпълнимо множество от елементарни секвенции е със сложност 0, то всички секвенции от това множество са празни, а от друга страна поради неизпълнимостта си то самото не е празно, следователно празната секвенция със сигурност принадлежи на множеството и значи то наистина е ec-противоречиво. Да направим сега индуктивното предположение, че n е дадено естествено число и всяко неизпълнимо множество от елементарни секвенции, имащо сложност, не по-голяма от n, е ec-противоречиво. Ще докажем, че в такъв случай и всяко неизпълнимо множество от елементарни секвенции, което е със сложност n+1, също е ec-противоречиво. Нека M е произволно неизпълнимо множество от елементарни секвенции, имащо сложност n+1. Да означим с a някоя формула от обединението на всички предпоставки и всички заключения на формули от M (това обединение има n+1 елемента и значи не е празно). С M₁ да означим множеството на онези секвенции от M, на които заключението не съдържа формулата a като елемент, а с M₂ - множеството на онези, на които предпоставката не я съдържа. Ще се стремим да докажем, че от M₁ е ec-изводима секвенцията a-: или празната секвенция, а от M₂ - секвенцията -:a или празната секвенция. Ако успеем да сторим това, задачата ни ще бъде фактически решена, защото тогава разбира се ще може да се твърди, че от M са ec-изводими двете секвенции a-: и -:a или е ec-изводима празната секвенция, и тъй като празната секвенция е съществено сечение на секвенциите a-: и -:a, с това ec-противоречивостта на M ще бъде установена. Ще докажем само твърдението, което се отнася до ec-изводимост от M₁, а твърдението, което се отнася до ec-изводимост от M₂, се доказва аналогично.

    Нека M₁ў е множеството на всички секвенции от вида G\{a}-:D, където G-:D е секвенция от M₁. Очевидно M₁ў е множество от елементарни секвенции, на което сложността не надминава n. Да допуснем, че то е изпълнимо, и да разгледаме някоя конфигурация (S,v), в която са верни всички секвенции от него. С U да означим обединението на всички предпоставки и всички заключения на секвенции от M₁ў, след това да означим с F множеството на онези формули от U, които са неверни в конфигурацията (S,v), а с T - множеството, състоящо се от формулите от U, верни в тази конфигурация, и още от формулата a. Тъй като a не принадлежи на U, множествата T и F нямат общи елементи, и, понеже тези множества са съставени от атомарни формули, това позволява да приложим основната лема за осъществимост и да заключим, че има конфигурация (Sў,vў), в която всички формули от T са верни, а всички формули от F са неверни. В конфигурацията (Sў,vў) всички формули от U имат същите стойности както в конфигурацията (S,v) и това гарантира, че всички секвенции от множеството M₁ў са верни и в (Sў,vў). Разбира се в (Sў,vў) е вярна и формулата a. От друга страна всяка секвенция от M съдържа a като елемент на своето заключение или е разширение на секвенция от M₁ў. Оттук се получава, че в (Sў,vў) са верни и всички секвенции от множеството M, нещо, което противоречи на неизпълнимостта на M. И така, допускането ни, че M₁ў е изпълнимо, е погрешно. При това положение въз основа на индуктивното предположение можем да твърдим, че M₁ў е ec-противоречиво, т.е. от M₁ў е ec-изводима празната секвенция. Сега ще покажем, че за всяка секвенция G-:D, ec-изводима от M₁ў, формулата a не принадлежи на GИD, а някоя от двете секвенции GИ{a}-:D и G-:D е ec-изводима от множеството M₁ (в случая, когато G-:D е празната секвенция, това ще даде желаното заключение, че секвенцията a-: или празната секвенция е ec-изводима от M₁). В случая, когато G-:D е секвенция от M₁ў, доказваното свойство е налице благодарение на дефиницията на множеството M₁ў. При това положение ще бъде достатъчно да покажем, че въпросното свойство се запазва при образуване на съюествено сечение. Нека Gў-:Dў и GІ-:DІ са секвенции, имащи доказваното свойство, т.е. a не принадлежи нито на GўИDў, нито на GІИDІ, някоя от секвенциите GўИ{a}-:Dў и Gў-:Dў е ec-изводима от M₁ и някоя от секвенциите GІИ{a}-:DІ и GІ-:DІ също е ec-изводима от M₁. Нека секвенцията G-:D е съществено сечение на Gў-:Dў и GІ-:DІ. Ще покажем, че и тази секвенция има доказваното свойство. Понеже G и D се съдържат съответно в GўИGІ и в DўИDІ, ясно е, че a не принадлежи на GИD. Ако и двете секвенции Gў-:Dў и GІ-:DІ са ec-изводими от M₁, то разбира се и секвенцията G-:D ще бъде такава. Остава да разгледаме останалите три възможни случая. Това ще направим, като покажем, че секвенцията GИ{a}-:D е съществено сечение на всяка от трите двойки секвенции GўИ{a}-:Dў и GІ-:DІ, Gў-:Dў и GІИ{a}-:DІ, GўИ{a}-:Dў и GІИ{a}-:DІ. За тази цел отбелязваме, че според дефиницията за съществено сечение имаме равенствата

    Теоремата за противоречивост на неизпълнимите множества от елементарни секвенции може да се използва за доказване на изпълнимост на множество от елементарни секвенции. А именно, ако за дадено множество от елементарни секвенции се установи, че не е ec-противоречиво, теоремата позволява да се заключи, че то е изпълнимо.

    Пример. Нека искаме да проверим дали е изпълнимо множеството от двете затворени универсални формули

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

    Като вземем пред вид доказаната теорема и разглежданията от предходния въпрос, виждаме, че е в сила още такова твърдение:

    Критерий за неизпълнимост на множество от елементарни секвенции. За произволно множество M от елементарни секвенции следните три условия са равносилни: а) M е неизпълнимо; б) M е c-противоречиво; в) M е ec-противоречиво.

    Оттук нататък в случаите, когато M е множество от елементарни секвенции, двете равносилни условия - M да бъде c-противоречиво и M да бъде ec-противоречиво - ще изказваме по-кратко, като ще изпускаме "c-" и "ec-".

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