Пълнота на метода на резолюцията

ПЪЛНОТА НА МЕТОДА НА РЕЗОЛЮЦИЯТА

И тук ще предполагаме, че е дадена една сигнатура Σ, и за всички дизюнкти, за които не е казано изрично нещо друго, ще смятаме, че са при сигнатура Σ.

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

Доказателство. Нека Δ е дадено множество от дизюнкти, което не притежава модел. Ще докажем, че празният дизюнкт е резолвентно изводим от Δ.

Ще разгледаме най-напред случая, когато в сигнатурата Σ има поне една константа. Нека Δ° е множеството на всички затворени частни случаи на дизюнктите от Δ. От свеждането на въпроса за съществуване на модел за множество от дизюнкти към същия въпрос за множество от затворени дизюнкти знаем, че щом в Σ има поне една константа и Δ няма модел, множеството Δ° е неизпълнимо. Оттук по лемата, която доказахме в текста „Пълнота на метода на резолюцията за множества от затворени дизюнкти“, получаваме, че празният дизюнкт е резолвентно изводим от Δ°. От друга страна обаче лесно е да се убедим, че всеки дизюнкт, резолвентно изводим от Δ°, е затворен частен случай на дизюнкт, резолвентно изводим от Δ. И наистина, за дизюнктите от самото множество Δ° това е ясно от дефиницията на това множество. От друга страна, ако два дизюнкта δ₁ и δ₂ са затворени частни случаи съответно на дизюнкти δ₁ и δ₂, резолвентно изводими от Δ, а трети дизюнкт е резолвента (разбира се непосредствена) на δ₁ и δ₂, той ще бъде резолвента на δ₁ и δ₂, следователно ще бъде резолвентно изводим от Δ и можем да използваме, че той е затворен частен случай на самия себе си. Като приложим доказаното към празния дизюнкт, получаваме, че той е затворен частен случай на някой дизюнкт, резолвентно изводим от множеството Δ, а въпросният дизюнкт не може да бъде друг освен празен. Значи празният дизюнкт е резолвентно изводим от Δ.

Преминаваме към случая, когато в сигнатурата Σ няма нито една константа. В този случай разглеждаме нова сигнатура Σ⁺, получена от Σ чрез добавяне на една константа α. Дизюнктите от множеството Δ могат да се разглеждат и като дизюнкти при сигнатура Σ⁺, като множеството Δ няма да има модел и сред структурите със сигнатура Σ⁺ (ако би имало такъв, от него щеше да може чрез обедняване да се получи и модел за Δ със сигнатура Σ). Нека Δ° е множеството на всички затворени частни случаи на дизюнктите от Δ при сигнатура Σ⁺, т.е. Δ° се състои от резултатите от замествания на променливите на дизюнктите от Δ със затворени термове при сигнатура Σ⁺. Множеството Δ° отново ще бъде неизпълнимо и лемата от текста „Пълнота на метода на резолюцията за множества от затворени дизюнкти“ позволява да твърдим, че от Δ° е резолвентно изводим при сигнатура Σ⁺ празният дизюнкт. Оттук ще успеем да заключим, че той е резолвентно изводим от Δ при сигнатура Σ (разбира се, от разглежданията, които направихме в първия случай, е ясно, че празният дизюнкт е изводим от Δ при сигнатура Σ⁺, но това твърдение е по-слабо от онова, което трябва да докажем). За целта избираме една променлива ξ и на всички затворени термове τ, затворени литерали λ и затворени дизюнкти δ при сигнатура Σ⁺ съпоставяме техни образи τ^ξ, λ^ξ и δ^ξ, които са съответно термове, литерали и дизюнкти при сигнатура Σ и са получени, грубо казано, чрез замяна на константата α с променливата ξ. Съпоставянето извършваме с помощта на следните равенства:

α^ξ = ξ;
ω(τ₁,…,τ_n)^ξ = ω(τ₁^ξ,…,τ_n^ξ) за всяко положително цяло число n, всеки n-местен функционален символ ω и всяка n-орка τ₁, …, τ_n от затворени термове при сигнатура Σ⁺;
π^ξ = π за всеки нулместен предикатен символ π;
π(τ₁,…,τ_n)^ξ = π(τ₁^ξ,…,τ_n^ξ) за всяко положително цяло число n, всеки n-местен предикатен символ π и всяка n-орка τ₁, …, τ_n от затворени термове при сигнатура Σ⁺;
(¬φ)^ξ = ¬φ^ξ за всяка затворена атомарна формула φ при сигнатура Σ⁺;
δ^ξ = {λ^ξ | λ∈δ} за всеки затворен дизюнкт δ при сигнатура Σ⁺.

След това доказваме следното твърдение: винаги, когато един затворен дизюнкт δ е резолвентно изводим при сигнатура Σ⁺ от множеството Δ°, съответният дизюнкт δ^ξ е частен случай на дизюнкт, резолвентно изводим при сигнатура Σ от множеството Δ. Прилагайки това твърдение в случая, когато δ е празният дизюнкт, получаваме нужното ни заключение за неговата изводимост от Δ при сигнатура Σ. Що се касае до доказателството на въпросното твърдение, основните моменти са два:
1. За дизюнктите от множеството Δ° верността на твърдението се установява, като се докаже, че е в сила равенството δ[ξ₁/θ₁,…,ξ_m/θ_m]^ξ = δ[ξ₁/θ₁^ξ,…,ξ_m/θ_m^ξ] винаги, когато ξ₁, …, ξ_m са различни помежду си променливи, δ е дизюнкт при сигнатура Σ, нямащ променливи, различни от ξ₁, …, ξ_m, а θ₁, …, θ_m са затворени термове при сигнатура Σ⁺ (равенството се доказва, като най-напред последователно се докажат аналогични равенства за термове и за литерали при сигнатура Σ).
2. За да покажем, че верността на твърдението се запазва при образуване на непосредствена резолвента на два затворени дизюнкта при сигнатура Σ⁺, използваме, че (δ \ {λ})^ξ = δ^ξ \ {λ^ξ} за всеки затворен дизюнкт δ при сигнатура Σ⁺ и всеки литерал λ, който му принадлежи (верността на това твърдение следва от обстоятелството, че литералите λ^ξ, съответстващи на различни затворени литерали λ при сигнатура Σ⁺, са различни помежду си, а че това обстоятелство е налице, може да се види, като последователно се докаже, че за всеки затворен терм τ при сигнатура Σ⁺ е в сила равенството τ^ξ[ξ/α] = τ и за всеки затворен литерал λ при сигнатура Σ⁺ е в сила равенството λ^ξ[ξ/α] = λ). _□

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

Забележка 2. Пълнотата на метода на резолюцията заедно с методите, които изучихме преди това, показва наличието на алгоритъм, с помощта на който чрез извършване на краен брой действия да можем да установяваме тъждествената вярност на една затворена формула на предикатното смятане винаги, когато такава тъждествена вярност е налице (ограничаването със затворени формули очевидно не е съществено). А именно, тъждествената вярност на формулата е равносилна с неизпълнимост на нейното отрицание. Чрез привеждане на това отрицание в пренексен вид и скулемизация можем да намерим такава безкванторна формула, че неизпълнимостта му да е равносилна с несъществуването на модел за тази формула. В случай че такъв модел не съществува, това обаче може да се установи чрез метода на резолюцията.

Забележка 3. Описаният по-горе алгоритъм не дава резултат в случаите, когато дадената формула не е тъждествено вярна, а прилагането на метода на резолюцията поражда безбройно много нови дизюнкти. Една теорема, доказана от Алонзо Чърч (Alonzo Church), показва, че при подходяща сигнатура с краен брой функционални и предикатни символи общ алгоритмичен начин за разпознаване на тъждествената вярност на формулите на предикатното смятане е по принцип невъзможен. За съжаление нямаме възможност да се занимаем по-подробно с този резултат. Ще отбележим само една равносилна негова формулировка, дадена от Алън Тюринг (Alan Mathison Turing). Тя, ако си служим със съвременната терминология, би могла да се изкаже например така: при подходяща сигнатура с краен брой функционални и предикатни символи не съществува машина на Тюринг, която при всяко стартиране върху лента със записана на нея формула на предикатното смятане да завършва работата си така, че наблюдаваната клетка от лентата при завършването на работата да бъде празна точно тогава, когато дадената формула е тъждествено вярна.

Забележка 4. Нека една математическа теория е аксиоматизирана така, че нейните аксиоми могат да се представят чрез затворени формули на предикатното смятане от първи ред, и нека за едно твърдение, което също е представимо чрез такава формула, се интересуваме дали е теорема на въпросната теория. Отговорът на този въпрос е положителен точно тогава, когато не съществува модел за множеството, състоящо се от формулите, представящи аксиомите на теорията, и отрицанието на формулата, представяща разглежданото твърдение. Значи при направените предположения споменатият въпрос попада в полето на действие на изучените от нас методи. Това показва, че за широк кръг аксиоматични математически теории са възможни формални методи за доказване на техните теореми. Това е било установено строго за пръв път през 1929 г. от Курт Гьодел (Kurt Gödel) чрез неговата теорема за пълнота на предикатното смятане (тя се отнася за методи, основани на формално извеждане от аксиоми).

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