| Съдържание |
Във въпроса „Субституции“ дадохме дефиниция за резултат от прилагането на субституция към атомарна формула, а по-късно – и към отрицателен литерал. Естествено би било да разширим дадената дефиниция и да кажем какво ще разбираме под резултат от прилагане на една субституция към произволна формула. Това обаче е свързано с известни трудности поради особената роля на променливите в кванторите. Една разумна дефиниция на резултата от прилагането на една субституция към дадена формула, съдържаща квантори, би трябвало преди всичко да се погрижи на кои места във формулата променливите да се заместят със съответните им термове и на кои да останат както са си били (казано накратко, променливата на всеки квантор трябва да остане както си е била и в квантора, и в областта на неговото действие). Има обаче и по-съществена трудност. Дефиницията би трябвало да отчете също възможността на едно неприятно явление, наречено колизия на променливите. Ще го илюстрираме с пример. Нека една формула има вида ∃Y p(X,Y), където p е двуместен предикатен символ, и нека искаме да приложим към нея субституцията [X/Y]. Формалното заместване на X с Y би дало формулата ∃Y p(Y,Y), но не би било разумно да приемем, че тя е резултатът от прилагането на разглежданата субституция към дадената формула (поне поради това, че така получената формула е затворена, а би било естествено променливите на терма, с който заместваме една свободна променлива на дадена формула, да останат свободни и в резултата от заместването).
Заради отбелязаните две трудности (преди всичко заради втората от тях) ние засега ще се въздържим от дефиниране на резултат от прилагането на субституция към произволна формула и ще дефинираме въпросния резултат само за безкванторни формули. Нека σ е дадена субституция. Като използваме еднозначното прочитане на безкванторните формули, ще дефинираме индуктивно за всяка безкванторна формула φ една безкванторна формула φσ, която ще наричаме резултат от прилагането на σ към φ. В случай, че φ е атомарна формула, този резултат е вече дефиниран, а за останалите безкванторни формули дефиницията е чрез следните равенства, където φ и ψ могат да бъдат произволни безкванторни формули (очевидно първото от тях е в съгласие с вече дадената дефиниция за резултат от прилагането на субституция към отрицателен литерал):
| (¬φ)σ | = | ¬(φσ), |
| (φ & ψ)σ | = | (φσ) & (ψσ), |
| (φ ∨ ψ)σ | = | (φσ) ∨ (ψσ). |
Основните свойства на прилагането на субституции към към атомарни формули са налице и за прилагането на субституции към безкванторни формули, като доказателството за това е чрез индукция, съобразена с дефиницията за безкванторна формула (предоставяме го на читателя).
Твърдение 1. Ако φ е произволна безкванторна формула, то резултатите от прилагането на две субституции σ и σ' към φ съвпадат точно тогава, когато σ и σ' съвпадат върху множеството на променливите на φ.
Твърдение 2. За всяка безкванторна формула φ е в сила равенството φι = φ.
Твърдение 3. Ако φ е произволна безкванторна формула, то за всяка субституция σ множеството на променливите на формулата φσ е обединение на множествата VAR(ξσ), където ξ пробягва множеството на променливите на φ.
Теорема за стойността на резултата от прилагане на субституция към безкванторна формула. Нека са дадени една субституция σ, една структура S и една оценка v в S. Нека σS(v) = v' и нека φ е произволна безкванторна формула. Тогава е в сила равенството (φσ)S,v = φS,v'.
От горните свойства следва, че ако φ е затворена безкванторна формула, то φσ = φ за всяка субституция σ, а ако φ е произволна безкванторна формула, то формулата φσ е затворена точно за онези субституции σ, които съпоставят затворени термове на всички променливи на φ. Следва също, че когато една безкванторна формула е тъждествено вярна в дадена структура, всички частни случаи на тази формула също са тъждествено вярна във въпросната структура, а когато някой частен случай на една безкванторна формула е изпълним в дадена структура, то и самата формула е изпълнима в тази структура.
Последно изменение: 25.08.2008 г.