За една субституция σ ще казваме, че удовлетворява дадена атомарна формула ψ в дадена структура S, ако формулата ψσ е тъждествено вярна в S.

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

    Пример 2. Заключението, което направихме в предходния пример, остава в сила и в по-общия случай, когато носителят на S е произволно непразно множество D, двуместният функционален символ f се интерпретира като някоя функция в D, подчиняваща се на асоциативния закон, и за всеки елемент d на носителя на S е в сила равенството p^S(d,d) = 1.

    За една субституция σ ще казваме, че удовлетворява дадено множество Γ от атомарни формули в дадена структура S, ако σ удовлетворява в S всеки атом от Γ.

    Пример 3. Нека S е произволна структура с двуместен функционален символ f и с двуместен предикатен символ p, такава, че за всеки елемент d на носителя на S е в сила равенството p^S(d,d) = 1. Тогава субституцията [X/Z, Y/Z] удовлетворява множеството на всички атомарни формули от вида

    Забележка 1. Точка Б на следствие 2 от въпроса „Оператори за присвояване, съответни на субституция“ показва, че за да бъде едно множество Γ от атомарни формули изпълнимо в дадена структура S, достатъчно е да съществува субституция, която удовлетворява Γ в S. Следващият пример показва, че това достатъчно условие не винаги е необходимо.

    Пример 4. Нека S е онази от двете структури, разгледани в пример 1, за която f^S е функцията събиране. Атомът p(f(X,X),X) е изпълним в S, но не съществува субституция, която да го удовлетворява в S. Последното произтича от обстоятелството, че всеки терм в сигнатурата на S има поне една променлива и стойността му в S е различна от 0 при всяка оценка в S, която съпоставя на някоя негова променлива число, различно от 0 (положението би било друго, ако структурата S притежаваше константа o, чиято стойност в S да е 0  –  тогава субституцията [X/o] би удовлетворявала атома p(f(X,X),X) в S).

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

    Забележка 2. Свойството, формулирано в забележка 1 от въпроса „Семантика на термовете и атомарните формули“, има аналог, отнасящ се до удовлетворяване чрез субституция и също играещ съществена роля за обосноваването на метода, по който в Пролог се изпълняват логически програми. Този аналог е следният: ако една формула φ следва в дадена структура S от дадено множество Γ от атомарни формули, а Δ е произволно множество от атомарни формули, то всяка субституция, която удовлетворява в S обединението на множествата Γ и Δ, удовлетворява в S също и множеството {φ}∪Δ. Това свойство се доказва, като се използва точка А на следствие 2 от въпроса „Оператори за присвояване, съответни на субституция“ заедно с обстоятелството, че за всяка субституция σ имаме равенствата  (Γ∪Δ)σ = Γσ ∪ Δσ  и  ({φ}∪Δ)σ = {φσ} ∪ Δσ.

    Ще формулираме и докажем две твърдения относно условия, при които произведението на две субституции удовлетворява дадено множество от атомарни формули.

    Твърдение 1. Ако Γ е множество от атомарни формули, а σ₁ и σ₂ са субституции, то субституцията σ₁σ₂ удовлетворява множеството Γ в дадена структура точно тогава, когато субституцията σ₂ удовлетворява множеството Γσ₁ в тази структура.

    Доказателство. От верността на равенството (2) за произволна атомарна формула τ е ясно, че за всяко множество Γ от атомарни формули и всеки две субституции σ₁ и σ₂ е в сила равенството Γ(σ₁σ₂) = (Γσ₁)σ₂.  _□

    Твърдение 2. Ако Γ е множество от атомарни формули, а σ₁ и σ₂ са субституции, като σ₁ удовлетворява Γ в дадена структура S, то σ₁σ₂ също удовлетворява Γ в S.

    Доказателство. Ако σ₁ удовлетворява Γ в структурата S, то всички атомарни формули от множеството Γσ₁ са тъждествено верни в S, откъдето по точка А на следствие 1 от текста „Оператори за присвояване, съответни на субституция“ получаваме, че и всички атомарни формули от множеството (Γσ₁)σ₂ са тъждествено верни в S, т.е. σ₂ удовлетворява Γσ₁ в S. По предходното твърдение от настоящия текст това гарантира, че σ₁σ₂ удовлетворява Γ в S.  _□

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