Да предположим, че са дадени една субституция σ и една структура S. Ще дефинираме едно преобразование σ^S, което преобразува всяка оценка в S на променливите пак в такава оценка. Дефиницията на това преобразование е следната: ако v е произволна оценка в S на променливите, то σ^S(v) = v′, където оценката v′ се дефинира с условието, че

     Пример. Нека субституцията σ има вида [ξ₀/τ₀], където ξ₀ и τ₀ са съответно дадена променлива и даден терм. Ако приложим преобразованието σ^S към дадена оценка v в S на променливите, ще получим нова оценка v′, такава, че v′(ξ₀) = τ₀^S,v и v′(ξ) = v(ξ) за всяка променлива ξ, различна от ξ₀, т.е. ще получим модификацията на v върху ξ₀ чрез τ₀^S,v. Това показва, че ако в някой език за програмиране могат да се пишат програми с променливи, приемащи стойности в S, и в този език е допустим операторът за присвояване ξ₀ := θ₀, то преобразованието σ^S действа върху оценките на променливите по същия начин както въпросният оператор.

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

     Теорема за стойността на резултата от прилагане на субституция към терм или атомарна формула. Нека са дадени една субституция σ,  една структура  S и една оценка v в S. Нека σ^S(v) = v′ и нека τ е терм или атомарна формула. Тогава е в сила равенството (τσ)^S,v=τ^S,v′.

     Доказателство. За да докажем твърдението за случая, когато τ е терм, ще използваме индукция, съобразена с дефиницията на понятието терм. Първо проверяваме верността на равенството в случая, когато τ е променлива или константа. Ако τ е някоя променлива ξ, то равенството, което имаме да докажем, добива вида (ξσ)^S,v = v′(ξ) и е вярно благодарение на равенството σ^S(v) = v′ и дефиницията на преобразованието σ^S. Ако τ е някоя константа, то доказваното равенство пак е вярно, защото и двете му страни са равни на интерпретиращия тази константа елемент на носителя на S. Нека сега да имаме τ = ω(τ₁,…,τ_n), където n>0, ω е n-местен функционален символ, τ₁, …, τ_n са термове и са изпълнени равенствата (τ_iσ)^S,v = τ_i^S,v′, i=1,…,n. Тогава ще имаме веригата от равенства

    Следствие 1. Нека са дадени една структура S, една атомарна формула φ и една субституция σ. Тогава:
    А. Ако атомарната формула φ е тъждествено вярна в S, то и атомарната формула φσ е тъждествено вярна в S.
    Б. Ако атомарната формула φσ е изпълнима в S, то и φ е изпълнима в S.

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

    Забележка 1. Може да се изкаже едно мнемонично правило, което улеснява запомнянето на заключението на доказаната теорема. Ще изкажем въпросното правило за случая, когато са изпълнени предположенията на тази теорема и τ е терм (аналогично е изказването, когато τ е атомарна формула). Да наречем термовете τ и τσ съответно „стария терм“ и „новия терм“, а оценките v и v′  –  съответно „старата оценка“ и „новата оценка“. Тогава, не споменавайки структурата S, която е една и съща в двете страни на равенството (τσ)^S,v=τ^S,v′, можем да прочетем това равенство по следния начин: „стойността на новия терм при старата оценка е равна на стойността на стария терм при новата оценка“.

    Забележка 2. Когато субституцията σ има вида от разгледания преди теоремата пример, изказаното в теоремата твърдение за стойността на резултата от прилагане на σ към атомарна формула може да се разглежда като възможна формулировка на едно известно твърдение на Антъни Хоар (Charles Antony Richard Hoare). Въпросното твърдение е полезно при доказване на коректност на програми, съдържащи оператори за присвояване. Според него, за да бъде удовлетворено дадено условие след изпълнението на оператора за присвояване ξ₀ := θ₀, необходимо и достатъчно е преди изпълнението на този оператор да е удовлетворено същото условие с ξ₀, заместено с θ₀.

    Ако Γ е някое множество от атомарни формули, а σ е субституция, то множеството на атомарните формули от вида ψσ, където ψ∈Γ, ше наричаме резултат от прилагане на σ към Γ и ще означаваме с Γσ. Твърдението, което сега ще формулираме, в известен смисъл обобщава следствие 1 (пред вид на това, че тъждествената вярност на една атомарна формула в дадена структура S е равносилна със следване на тази атомарна формула в S от празното множество, а изпълнимостта й в S е равносилна с изпълнимост в S на множеството, имащо нея като свой единствен елемент).

    Следствие 2. Нека са дадени една структура S, едно множество Γ от атомарни формули и една субституция σ. Тогава:
    А. Ако една атомарна формула φ следва в S от множеството Γ, то атомарната формула φσ следва в S от множеството Γσ.
    Б. Ако множеството Γσ е изпълнимо в S, то и множеството Γ е изпълнимо в S.

     Доказателство. От теоремата, която доказахме, следва веднага, че в структурата S една оценка v удовлетворява множеството Γσ точно тогава, когато оценката σ^S(v) удовлетворява множеството Γ. Оттук разбира се е ясно, че е в сила изказаното в точка Б. За да се убедим и в изказаното в точка А, да предположим, че дадена атомарна формула φ следва в S от Γ. Тогава за произволна оценка v в S, удовлетворяваща множеството Γσ, оценката σ^S(v) ще удовлетворява Γ, а следователно и φ, откъдето пак с помощта на теоремата заключаваме, че оценката v ще удовлетворява φσ. _□

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