| Съдържание |
Ще се запознаем с един метод за свеждане на въпроси за съществуване на модел за какви да е формули към аналогични въпроси за безкванторни формули. Вече знаем, че бихме могли да се ограничим с разглеждането на формули в пренексен вид. Споменатият метод, известен под името „скулемизация“ – по името на автора му Торалф Скулем (Albert Thoralf Skolem), позволява да премахнем в коя да е такава формула всички налични квантори за съществуване, като за сметка на това по подходящ начин въведем във формулата нови функционални символи. Кванторите за общност, които евентуално биха останали след това, могат пък да се пропуснат без да се повлияе на съществуването или несъществуването на модел.
Методът, за който става дума, може да бъде основан на две леми за отстраняване на квантор за съществуване в началото на пренексна формула.
Лема за отстраняване на квантор за съществуване в началото на затворена пренексна формула. Нека φ е пренексна формула в сигнатура Σ = (Φ,Π,ρ), а η е единствената свободна променлива на φ. Нека сигнатурата Σ′ е получена от Σ чрез добавяне на една нова константа α, т.е. Σ′ = (Φ∪{α},Π,ρ′), където α не принадлежи на Φ, ρ′ е продължение на ρ и ρ′(α) = 0. Тогава:
1. Ако S е структура със сигнатура Σ, то формулата ∃η φ е вярна в S точно тогава, когато съществува такава структура S ′ със сигнатура Σ′, че S ′ е обогатяване на S и в S ′ е вярна формулата φ[η/α].
2. За да съществува структура, която е със сигнатура Σ и е модел за формулата ∃η φ, необходимо и достатъчно е да съществува структура, която е със сигнатура Σ′ и е модел за формулата φ[η/α].
Доказателство. Преди да пристъпим към разсъждения, доказващи заключението на лемата, отбелязваме изрично, че заместването на η с α във φ е възможно, защото α е константа. Понеже φ няма свободни променливи, различни от η, ясно е още, че формулите ∃η φ и φ[η/α] са затворени. За да докажем точка 1 от заключението, разглеждаме произволна структура S = (Σ,D,I) със сигнатура Σ. Да предположим най-напред, че формулата ∃η φ е вярна в S. Нека v е някоя оценка на променливите в S. Понеже формулата ∃η φ е вярна в S при оценката v, съществува такъв елемент d на D, че формулата φ е вярна в S при оценката v[η→d]. Избираме елемент d на D с това свойство и полагаме S ′ = (Σ′,D,I ′), където I ′ съвпада с I върху Φ∪Π и I ′(α) = d. Тогава
Лема за отстраняване на квантор за съществуване в началото на незатворена пренексна формула. Нека φ е пренексна формула в сигнатура Σ = (Φ,Π,ρ), и φ има точно n+1 свободни променливи ξ1, …, ξn, η (n>0). Нека сигнатурата Σ′ е получена от Σ чрез добавяне на един нов n-местен функционален символ ω, т.е. Σ′ = (Φ∪{ω},Π,ρ′), където ω не принадлежи на Φ, ρ′ е продължение на ρ и ρ′(ω) = n. Тогава:
1. Ако S е структура със сигнатура Σ, то формулата ∃η φ е тъждествено вярна в S точно тогава, когато съществува такава структура S ′ със сигнатура Σ′, че S ′ е обогатяване на S и в S ′ е тъждествено вярна формулата φ[η/ω(ξ1,…,ξn)].
2. За да съществува структура, която е със сигнатура Σ и е модел за формулата ∃η φ, необходимо и достатъчно е да съществува структура, която е със сигнатура Σ′ и е модел за формулата φ[η/ω(ξ1,…,ξn)].
Доказателство. Заместването на η с ω(ξ1,…,ξn) във φ е възможно, защото никоя от променливите ξ1, …, ξn не е свързана променлива на φ. Ясно е още, че свободните променливи на всяка от формулите ∃η φ и φ[η/ω(ξ1,…,ξn)] са точно ξ1, …, ξn. За да докажем точка 1 от заключението, разглеждаме произволна структура S = (Σ,D,I) със сигнатура Σ. Да предположим най-напред, че формулата ∃η φ е тъждествено вярна в S. При произволни d1, …, dn от D да означим с vd1,…,dn онази оценка в S на променливите, която съпоставя на променливите ξ1, …, ξn съответно елементите d1, …, dn , а на всички останали променливи да речем елемента d1. Понеже при всеки избор на d1, …, dn в D формулата ∃η φ е вярна в S при оценката vd1,…,dn , съществува такава n-местна функция f в D, че формулата φ е вярна в S при оценката vd1,…,dn[η→f(d1,…,dn)], както и да избираме d1, …, dn в D (т.е. f(d1,…,dn) е някой от онези елементи d на D, за които φ има стойност 1 в S при оценката vd1,…,dn[η→d]). Избираме такава функция f и полагаме S ′ = (Σ′,D,I ′), където I ′ съвпада с I върху Φ∪Π и I ′(φ) = f. Ще докажем, че формулата φ[η/ω(ξ1,…,ξn)] е тъждествено вярна в така дефинираната структура S ′. За тази цел да разгледаме произволна оценка v в нея на променливите и да положим d1 = v(ξ1), …, dn = v(ξn). Имаме равенствата
Забележка 1. Твърдението за съществуване на функция f със свойството, нужно за гореизложеното доказателство, фактически се основава на тъй наречената аксиома за избора. Тя дълго време е била една от най-оспорваните аксиоми на теорията на множествата, обаче се използва и в многобройни други математически доказателства – например при доказателството за еквивалентност на двете най-често прилагани дефиниции за непрекъснатост на функция в множеството на реалните числа.
Ще разгледаме някои примери за прилагане на доказаните леми.
Пример 1. Задачата за бръснаря, която разглеждахме по-рано, би могла да се формулира и като въпрос дали съществува модел със сигнатура без функционални символи и с един двуместен предикатен символ s за формулата
Пример 2. В същата сигнатура без функционални символи както в предходния пример да разгледаме формулата
Пример 3. В сигнатура без функционални символи и с един триместен предикатен символ p да разгледаме формулата
Няколкократно последователно прилагане на лемите както в горните примери позволява по всяка дадена формула в пренексен вид да намерим такава безкванторна формула в сигнатура с някакъв брой допълнителни функционални символи, че съществуването на модел за дадената формула да е равносилно със съществуването на модел за намерената. За простота да предположим, че дадената формула е затворена (ако не е, можем да я направим затворена чрез поставяне на известен брой квантори за общност в началото й). Тя може да се представи във вида
Пример 4. Пренексните формули (срещащи се в предходните примери)
Скулемизацията може да се използва и за изследване дали съществува модел за дадено множество от пренексни формули. За целта е достатъчно да извършим скулемизация във всички формули от множеството, като обаче за различните формули добавяме към сигнатурата различни функционални символи, и след това да изследваме дали за множеството от получените чрез скулемизацията формули съществува модел, чиято сигнатура е разширението на дадената чрез всички така добавени функционални символи. Коректността на такъв начин на процедиране може лесно да се обоснове чрез използване на първите точки от двете леми.
Пример 5. В сигнатурата от пример 1 да разгледаме множеството от двете формули ∀X ∃Y s(X,Y) и ∀X ∃Y ¬ s(X,Y) . Работейки така, както беше казано по-горе, можем да изследваме дали съществува модел за това множество, като добавим към сигнатурата едноместни функционални символи f и g и изследваме дали съществува модел с така разширената сигнатура за множеството от формулите s(X,f(X)) и ¬ s(X,g(X)) . Очевидно такъв модел съществува, следователно съществува модел с първоначалната сигнатура и за даденото множество от формули (до това заключение разбира се можеше да стигнем лесно и чрез явно построяване на въпросния модел). Добре е да отбележим обаче, че нямаше да получим правилно заключение, ако вместо двата различни функционални символи f и g бяхме използвали един и същ.
Забележка 2. Методите, които изучихме, дават алгоритъм, с помощта на който чрез извършване на краен брой действия да можем да установяваме тъждествената вярност на една формула на предикатното смятане винаги, когато такава тъждествена вярност е налице. А именно, тъждествената вярност на една формула е равносилна с неизпълнимост на нейното отрицание. Чрез привеждане на това отрицание в пренексен вид и скулемизация можем да намерим такава безкванторна формула, че неизпълнимостта му да е равносилна с несъществуването на модел за тази формула. В случай че такъв модел не съществува, това обаче може да се установи чрез метода на резолюцията.
Забележка 3. Описаният по-горе алгоритъм не дава резултат в случаите, когато дадената формула не е тъждествено вярна, а прилагането на метода на резолюцията поражда безбройно много нови дизюнкти. Една теорема, доказана от Алонзо Чърч (Alonzo Church), показва, че при подходяща сигнатура с краен брой функционални и предикатни символи общ алгоритмичен начин за разпознаване на тъждествената вярност на формулите на предикатното смятане е по принцип невъзможен. За съжаление нямаме възможност да се занимаем по-подробно с този резултат. Ще отбележим само една равносилна негова формулировка, дадена от Алън Тюринг (Alan Mathison Turing). Тя, ако си служим със съвременната терминология, би могла да се изкаже например така: при подходяща сигнатура с краен брой функционални и предикатни символи не съществува машина на Тюринг, която при всяко стартиране върху лента със записана на нея формула на предикатното смятане да завършва работата си така, че наблюдаваната клетка от лентата при завършването на работата да бъде празна точно тогава, когато дадената формула е тъждествено вярна.
Забележка 4. Нека една математическа теория е аксиоматизирана така, че нейните аксиоми могат да се представят чрез формули на предикатното смятане от първи ред, и нека за едно твърдение, което също е представимо чрез такава формула, се интересуваме дали е теорема на въпросната теория. Отговорът на този въпрос е положителен точно тогава, когато не съществува модел за множеството, състощо се от формулите, представящи аксиомите на теорията, и отрицанието на формулата, представяща разглежданото твърдение. Значи при направените предположения споменатият въпрос попада в полето на действие на изучените от нас методи. Това показва, че за широк кръг аксиоматични математически теории са възможни формални методи за доказване на техните теореми.
Последно изменение: 9.01.2009 г.