Теорема на Дейвис и Пътнам. Нека Δ е дадено множество от затворени дизюнкти, а φ е дадена затворена атомарна формула. Да означим с Δ₀ множеството на онези дизюнкти от Δ, сред елементите на които не фигурират нито φ, нито ¬φ, с Δ₁  –  множеството на онези дизюнкти от Δ, на които принадлежи φ, но не принадлежи ¬φ, и с Δ₂  –  множеството на онези дизюнкти от Δ, на които принадлежи ¬φ, но не принадлежи φ. Нека Δ′ е обединението на Δ₀ с множеството на всички дизюнкти от вида (δ₁\{φ})∪(δ₂\{¬φ}), където δ₁ принадлежи на Δ₁, а δ₂  –  на Δ₂. За да бъде множеството Δ изпълнимо, необходимо и достатъчно е да е изпълнимо множеството Δ′.

    Доказателство. От дефиницията на множеството Δ′ е ясно, че всеки елемент на това множество е елемент на Δ или е непосредствена резолвента на някои два елемента на Δ. Поради това всеки модел за Δ е модел и за Δ′. Значи ако Δ е изпълнимо, то и Δ′ е изпълнимо. За да докажем обратното твърдение на това, да предположим, че множеството Δ′ е изпълнимо. Нека S е някой модел за Δ′. С допускане на противното се показва, че за всеки дизюнкт δ₁ от Δ₁ дизюнктът δ₁\{φ} е верен в S или за всеки дизюнкт δ₂ от Δ₂ дизюнктът δ₂\{¬φ} е верен в S. И наистина, ако допуснем противното, получаваме, че в S не е верен някой дизюнкт от вида (δ₁\{φ})∪(δ₂\{¬φ}), където δ₁ принадлежи на Δ₁, а δ₂  –  на Δ₂, но това противоречи на предположението, че S е модел за Δ′.

    Случай 1. Нека за всеки дизюнкт δ₁ от Δ₁ дизюнктът δ₁\{φ} е верен в S. Да означим с S° такава структура, че в нея сред затворените атомарни формули са верни точно онези, които са различни от φ и са верни в S. Структура S°, удовлетворяваща това изискване, съществува (вж. текста „Съществуване на структура с отнапред дадено множество на верните затворени атомарни формули“). Ще покажем, че S° е модел за множеството Δ. За целта да разгледаме произволен дизюнкт δ от Δ. Ако на този дизюнкт принадлежи литералът ¬φ, дизюнктът ще бъде верен в S°, тъй като литералът ¬φ е верен в S°. Да предположим сега, че ¬φ не принадлежи на δ. Ако на δ принадлежи φ, то δ е от множеството Δ₁, следователно дизюнктът δ\{φ} е верен в S, т.е. някой литерал от него е верен в S, а значи и в S° (понеже стойността на този литерал в S° е същата както в S)  –  значи дизюнктът δ пак е верен в S°. Ако пък на δ не принадлежи и литералът φ, то δ е от множеството Δ₀, а значи и от множеството Δ′, следователно някой литерал от δ е верен в S, а значи и в S° (тъй като стойността на този литерал в S° отново е същата както в S)  –  отново дизюнктът δ се оказва верен в S°.

    Случай 2. Нека за всеки дизюнкт δ₂ от Δ₂ дизюнктът δ₂\{¬φ} е верен в S. Да означим с S° такава структура, че множеството на верните в нея затворени атомарни формули се състои от от φ и всички затворени атомарни формули, верни в S (и такава структура разбира се съществува). Ще покажем, че S° е модел за множеството Δ. Нека δ е произволен дизюнкт от Δ. Ако на този дизюнкт принадлежи атомарната формула φ, дизюнктът ще бъде верен в S°, тъй като φ е вярна в S°. Да предположим сега, че φ не принадлежи на δ. Ако на δ принадлежи ¬φ, то δ е от множеството Δ₂, следователно дизюнктът δ\{¬φ} е верен в S, т.е. някой литерал от него е верен в S, а значи и в S° (тъй като стойността на този литерал в S° е същата както в S)  –  значи дизюнктът δ пак е верен в S°. Ако пък на δ не принадлежи и литералът ¬φ, то δ е от множеството Δ₀ и можем да разсъждаваме по същия начин както в случая 1.  _□

    При условията и означенията на доказаната теорема обединението на дизюнктите от множеството Δ′ очевидно се съдържа в обединението на дизюнктите от множеството Δ. Ако поне един от двата противоположни литерала φ и ¬φ принадлежи на някой дизюнкт от Δ, то въпросното включване е строго, понеже нито φ, нито ¬φ може да принадлежи на дизюнкт от Δ′. В този случай казваме, че Δ′ е получен от Δ чрез елиминация на φ.

    Когато от дадено множество от дизюнкти отстраним всички тавтологични дизюнкти, които му принадлежат, и евентуално някои дизюнкти, имащи и същински подмножества, принадлежащи на даденото множество, за полученото по този начин множество от дизюнкти ще казваме, че е получено от даденото чрез прочистване. Лесно е да се види, че споменатите две множества от дизюнкти имат едни и същи модели.

    Методът на Дейвис и Пътнам може да бъде описан по следния начин. Дадено е едно крайно множество от затворени дизюнкти, за което трябва да се провери дали е изпълнимо. Ако празният дизюнкт принадлежи на това множество, то е неизпълнимо, а ако самото множество е празно, то е изпълнимо. Ако не е налице никой от тези два случая, извършваме прочистване на множеството и елиминация на атомарни формули, докато стигнем до някой от двата случая. Последното със сигурност ще се случи, защото след прочистване на множеството и елиминация на атомарна формула обединението на дизюнктите от множеството намалява строго, а това обединение в началния момент на работата е крайно и то е празно само в случаите, когато множеството от самите дизюнкти е празно или има за единствен елемент празния дизюнкт.

    Забележка. Когато се извърши прочистване на дадено множество от затворени дизюнкти, за елиминацията на атомарна формула от полученото по този начин негово подмножество теоремата на Дейвис и Пътнам може да се използва с опростена дефиниция на множествата Δ₁ и Δ₂  –  тъй като в това подмножество няма тавтологични дизюнкти, в дефинициите на Δ₁ и Δ₂ стават излишни изискванията за непринадлежност съответно на ¬φ и на φ към разглежданите дизюнкти.

    Пример 1. Нека φ, ψ и θ са три различни затворени атомарни формули, а Δ е множеството, състоящо се от следните шест дизюнкта:

    Пример 2. Нека пак φ, ψ и θ са три различни затворени атомарни формули, но Δ да е множеството, състоящо се от следните четири дизюнкта:

    Пример 3. Ще изследваме с помощта на метода на Дейвис и Пътнам дали има модел множеството, разгледано в пример 2 от текста „Свеждане на въпроса за съществуване на модел за множество от дизюнкти към същия въпрос за множество от затворени дизюнкти“. Това беше множеството от следните два дизюнкта, където p е двуместен предикатен символ, a и b са константи и разглежданата сигнатура няма други функционални символи освен тези две константи:

    Пример 4. В предходния пример успяхме да приложим метода на Дейвис и Пътнам без да прибегнем нито веднъж до образуване на резолвента. При друга последователност на елиминиране на атомарните формули можеше и да не е така. Нека например ги елиминраме в следния ред:  p(a,a),  p(b,b),  p(a,b),  p(b,a). Тогава при първите две елиминации ще се извърши и резолюция. Последователно получаваните множества ще бъдат

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