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

      Лема за отстраняване на квантор за съществуване в началото на затворена формула. Нека G е формула в сигнатура  Σ = (Φ,Π,ρ),  η е променлива и формулата  ∃η G  е затворена. Нека сигнатурата  Σ′  е получена от Σ чрез добавяне на една нова константа α, т.е.  Σ′ = (Φ∪{α},Π,ρ′),  където α не принадлежи на Φ,  ρ′ е продължение на ρ  и  ρ′(α) = 0.  Тогава:
        1. Ако S е структура със сигнатура Σ, то формулата  ∃η G  е вярна в S точно тогава, когато съществува такава структура S ′ със сигнатура Σ′, че S ′ е обогатяване на S и в S ′ е вярна формулата  G_η[α].
        2. За да съществува структура, която е със сигнатура Σ и е модел за формулата  ∃η G,  необходимо и достатъчно е да съществува структура, която е със сигнатура Σ′ и е модел за формулата  G_η[α].

      Доказателство. Преди да пристъпим към разсъждения, доказващи заключението на лемата, отбелязваме изрично, че заместването на η с α в G е възможно, защото α е константа. Понеже освен това G няма свободни променливи, различни от η, ясно е още, че формулата  G_η[α] е затворена. За да докажем точка 1 от заключението, разглеждаме произволна структура  S = (Σ,D,I)  със сигнатура Σ. Да предположим най-напред, че формулата  ∃η G  е вярна в S. Нека v е някоя оценка на променливите в S. Понеже формулата  ∃η G  е вярна в S при оценката v, съществува такъв елемент d на D, че формулата G е вярна в S при оценката v[η→d]. Избираме елемент d на D с това свойство и полагаме  S ′ = (Σ′,D,I ′),  където I ′ съвпада с I върху  Φ∪Π  и  I ′(α) = d.  Тогава

      Лема за отстраняване на квантор за съществуване в началото на незатворена формула. Нека G е формула в сигнатура  Σ = (Φ,Π,ρ),  η е променлива и формулата  ∃η G  има точно n свободни променливи  ξ₁, …, ξ_n (n>0), като никоя от тях не е свързана променлива на G. Нека сигнатурата  Σ′  е получена от Σ чрез добавяне на един нов n-местен функционален символ φ, т.е.  Σ′ = (Φ∪{φ},Π,ρ′),  където φ не принадлежи на Φ,  ρ′ е продължение на ρ  и  ρ′(φ) = n.  Тогава:
        1. Ако S е структура със сигнатура Σ, то формулата  ∃η G  е тъждествено вярна в S точно тогава, когато съществува такава структура S ′ със сигнатура Σ′, че S ′ е обогатяване на S и в S ′ е тъждествено вярна формулата  G_η[φ(ξ₁,…,ξ_n)].
        2. За да съществува структура, която е със сигнатура Σ и е модел за формулата  ∃η G,  необходимо и достатъчно е да съществува структура, която е със сигнатура Σ′ и е модел за формулата  G_η[φ(ξ₁,…,ξ_n)].

      Доказателство. За да докажем точка 1 от заключението, разглеждаме произволна структура  S = (Σ,D,I)  със сигнатура Σ. Да предположим най-напред, че формулата  ∃η G  е тъждествено вярна в S. При произволни  d₁, …, d_n  от D да означим с  v_d1,…,dn  онази оценка в S на променливите, която съпоставя на променливите  ξ₁, …, ξ_n  съответно елементите  d₁, …, d_n ,  а на всички останали променливи да речем елемента  d₁.  Понеже при всеки избор на  d₁, …, d_n  в D  формулата  ∃η G  е вярна в S при оценката  v_d1,…,dn ,  съществува такава n-местна функция f в D,  че формулата G е вярна в S при оценката  v_d1,…,dn[η→f(d₁,…,d_n)],  както и да избираме   d₁, …, d_n  в D  (т.е.  f(d₁,…,d_n)  е някой от онези елементи d на D, за които S,v_d1,…,dn[η→d] ⊨ G ). Избираме такава функция f и полагаме  S ′ = (Σ′,D,I ′),  където I ′ съвпада с I върху  Φ∪Π  и  I ′(φ) = f.  Ще докажем, че формулата  G_η[φ(ξ₁,…,ξ_n)]  е тъждествено вярна в така дефинираната структура  S ′.  За тази цел да разгледаме произволна оценка v в нея на променливите и да положим  d₁ = v(ξ₁), …, d_n = v(ξ_n). Имаме равенствата

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

      Забележка 2. Предположението, че никоя от променливите  ξ₁, …, ξ_n  не е свързана променлива на формулата G, беше направено, за да осигури възможността да заместим в тази формула променливата η с терма  φ(ξ₁,…,ξ_n).  То със сигурност е изпълнено в случаите, когато формулата G е в пренексен вид, а в останалите случаи не ограничава съществено общността, защото чрез подходящи преименувания на свързани променливи G винаги може да бъде заменена с еквивалентна на нея формула със същите свободни променливи и със същия брой квантори, на която никоя от променливите  ξ₁, …, ξ_n  не е свързана променлива.

      Ще разгледаме някои примери за прилагане на доказаните леми.

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

      Пример 2. В същата сигнатура без функционални символи както в предходния пример да разгледаме формулата

      Пример 2'. След като в предходния пример стигнахме до формулата

      Пример 3. В сигнатура без функционални символи и с един триместен предикатен символ p да разгледаме формулата

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

      Пример 4. Формулите (срещащи се в примери 1 и 3)

      Пример 5. Формулата

      Скулемизацията може да се използва и за изследване дали съществува модел за дадено множество от формули. За целта е достатъчно да извършим скулемизация във всички формули от множеството, като обаче за различните формули добавяме към сигнатурата различни функционални символи, и след това да изследваме дали за множеството от получените чрез скулемизацията формули съществува модел, чиято сигнатура е разширението на дадената чрез всички така добавени функционални символи. Коректността на такъв начин на процедиране може лесно да се обоснове чрез използване на първите точки от двете леми.

      Пример 6. В сигнатурата от пример 1 да разгледаме множеството от двете формули  ∀X ∃Y s(X,Y)  и  ∀X ∃Y ¬ s(X,Y) .  Работейки така, както беше казано по-горе, можем да изследваме дали съществува модел за това множество, като добавим към сигнатурата едноместни функционални символи f и g и изследваме дали съществува модел с така разширената сигнатура за множеството от формулите  s(X,f(X))  и  ¬ s(X,g(X)) .  Очевидно такъв модел съществува, следователно съществува модел с първоначалната сигнатура и за даденото множество от формули (до това заключение разбира се можеше да стигнем лесно и чрез явно построяване на въпросния модел). Добре е да отбележим обаче, че нямаше да получим правилно заключение, ако вместо двата различни функционални символи f и g бяхме използвали един и същ.

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

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

      Забележка 5. В полето на действие на методите, за които става дума, попада и въпросът дали дадена формула следва от дадено непразно крайно множество от формули. Това е така, защото този въпрос е равносилен с въпроса дали е тъждествено вярна импликацията, имаща за предпоставка конюнкцията на формулите от споменатото множество и за заключение дадената формула. С други думи, имаме алгоритъм, позволяващ с краен брой действия да установим следването на формулата от множеството, ако въпросното следване е налице. Това показва, че за широк кръг аксиоматични математически теории са възможни формални методи за доказване на техните теореми, ако под теореми на теорията разбираме твърдения, верни във всяка структура, в която са верни аксиомите на тази теория.

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

Previous  Next  Contents