Скулемизация. Скулемова нормална форма

СКУЛЕМИЗАЦИЯ. СКУЛЕМОВА НОРМАЛНА ФОРМА

Под модел за дадена формула се разбира модел за множеството, имащо за единствен елемент тази формула, т.е. модели за една формула са структурите, в които тя е тъждествено вярна. Ще се запознаем с един метод за свеждане на въпроси за съществуване на модел за какви да е формули към аналогични въпроси за безкванторни формули. Вече знаем, че бихме могли да се ограничим с разглеждането на формули в пренексен вид. Споменатият метод, известен под името „скулемизация“ – по името на автора му Торалф Скулем (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. Тогава

([η/ω]φ)^S ′ = ([η/ω]φ)^S ′,v = φ^{S ′,v[η→ω^S ′,v]} = φ^S,v[η→d] = 1, т.е. формулата [η/ω]φ е вярна в структурата S ′. Обратно, да предположим, че формулата [η/ω]φ е вярна в някоя структура S ′, която е със сигнатура Σ′ и е обогатяване на S. Тъй като от формулата [η/ω]φ следва формулата ∃ηφ (вж. твърдението „Закони за универсална и за екзистенциална конкретизация“ в текста „Основни следствия от теоремата за стойността на резултат от прилагане на субституция към формула“), оттук получаваме, че и формулата ∃ηφ е вярна в структурата S ′. Понеже ∃ηφ е формула при сигнатурата на структурата S, а S ′ е обогатяване на S, заключаваме, че формулата ∃ηφ е вярна и в структурата S. С това точка 1 е доказана. Точка 2 се получава веднага от нея и от очевидното обстоятелство, че всяка структура със сигнатура Σ′ е обогатяване на някоя структура със сигнатура Σ. _□

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

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

[η/ω(ξ₁,…,ξ_n)]φ^S ′,v = φ^{S ′,v[η→ω(ξ₁,…,ξ_n)^S ′,v]} = φ^{S,v[η→f(d₁,…,d_n)]} = 1 (последното от тях е в сила благодарение на това, че оценката v[η→f(d₁,…,d_n)] съвпада с оценката v_{d₁,…,d_n}[η→f(d₁,…,d_n)] за свободните променливи на формулата φ). Значи наистина [η/ω(ξ₁,…,ξ_n)]φ е тъждествено вярна в S ′. Обратно, да предположим, че формулата [η/ω(ξ₁,…,ξ_n)]φ е тъждествено вярна в някоя структура S ′, която е със сигнатура Σ′ и е обогатяване на S. Тъй като от формулата [η/ω(ξ₁,…,ξ_n)]φ следва формулата ∃ηφ, тя също е тъждествено вярна в S ′, а следователно и в S. С това точка 1 е доказана, а точка 2 се получава от нея и от обстоятелството, че всяка структура със сигнатура Σ′ е обогатяване на някоя структура със сигнатура Σ _□

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

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

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

∃u∀x(p(u,x)↔¬p(x,x) ) (чрез тази формула би могло да се запише условието на задачата за бръснаря, а именно някой човек от дадена група мъже да бръсне точно онези от тях, които не се бръснат сами). Според точка 2 от първата лема, за да съществува такъв модел, необходимо и достатъчно е да съществува модел със сигнатура, получена от гореспоменатата чрез добавяне на константата a, за формулата ∀x(p(a,x)↔¬p(x,x) ). Разбира се, съществуването на модел с тази сигнатура за горната формула е равносилно със съществуването на модел със същата сигнатура за безкванторната формула p(a,x)↔¬p(x,x). Такъв обаче не съществува, защото ако би съществувал, то в него би трябвало да е верен частният случай p(a,a)↔¬p(a,a) на въпросната безкванторна формула, а това е невъзможно.

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

∀ξ_1,1…∀ξ_1,k₁∃η₁∀ξ_2,1…∀ξ_2,k₂∃η₂ … ∀ξ_m,1…∀ξ_{m,k_m}∃η_m∀ξ_m+1,1…∀ξ_{m+1,k_m+1}θ , където m и k₁, k₂, … k_m са някои естествени числа, променливите ξ_i,j и η_i са две по две различни помежду си и θ е безкванторна формула, чиито променливи са точно споменатите. За прилагането на доказаните леми се налага последователно да добавим към сигнатурата на дадената формула m нови функционални символи ω₁, …, ω_m, където ω_i е k₁+k₂+…+k_i-местен при i = 1, …, m. В резултат на прилагането на лемите се получава, че за дадената формула съществува модел с нейната сигнатура точно тогава, когато съществува модел с току-що описаната разширена сигнатура за безкванторната формула [η_m/τ_m]…[η₁/τ₁]θ, където τ_i = ω_i при k₁+k₂+…+k_i = 0 и τ_i = ω_i(ξ_1,1,…,ξ_1,k₁,ξ_2,1,…,ξ_2,k₂,…,ξ_i,1,…,ξ_{i,k_i}) в противен случай (получава се също, че една структура със сигнатурата на дадената формула е неин модел точно тогава, когато някое обогатяване на тази структура до структура с описаната разширена сигнатура е модел за горната безкванторна формула). Разбира се, една структура е модел за тази безкванторна формула точно тогава. когато е модел за затворената формула ∀ξ_1,1…∀ξ_1,k₁∀ξ_2,1…∀ξ_2,k₂… ∀ξ_m,1…∀ξ_{m,k_m}∀ξ_m+1,1…∀ξ_{m+1,k_m+1}[η_m/τ_m]…[η₁/τ₁]θ . Току-що написаната затворена формула се нарича скулемова нормална форма (със скулемови функционални символи ω₁, …, ω_m) за дадената формула.

Пример 2. При същата сигнатура както в пример 1 пренексната формула

∃u∀v∃w∀x∃y∀z(p(u,v)∨ ¬p(v,w)∨ p(w,x)∨ ¬p(x,y)∨ p(y,z)∨ ¬p(z,u)) има скулемова нормална форма ∀v∀x∀z(p(a,v)∨ ¬p(v,f(v))∨ p(f(v),x)∨ ¬p(x,g(v,x))∨ p(g(v,x),z)∨ ¬p(z,a))

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

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

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