ПРИЛАГАНЕ НА СУБСТИТУЦИЯ КЪМ ПРОИЗВОЛНА ФОРМУЛА

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

    Грубо казано, при прилагане на субституция към безкванторна формула, навсякъде във формулата променливите се заместват със съответните им при субституцията термове. За произволна формула обаче такъв начин на прилагане на субституциите не е уместен, защото при него може да се случи резултатът от прилагането изобщо да не бъде формула (ако заместим променливата на някой квантор с терм, който не е променлива), а дори и да бъде формула, в общия случай няма да се запазят добрите свойства от случая на прилагане към безкванторни формули. Да речем, ако бихме приели, че при прилагане на субституцията [U/X] към формулата  ∃X p(X,U)  (където p е двуместен предикатен символ) се получава формулата  ∃X p(X,X), то би се нарушило например запазването на тъждествената вярност при прилагане на субституция (лесно може да се посочи структура, в която първата от споменатите две формули е тъждествено вярна, а втората не е вярна). Причина за тази неприятност е обстоятелството, че подобно прилагане на субституцията предизвиква тъй наречената колизия на променливите. А именно, ролите на двете X в получената формула би трябвало да са различни, но това не се вижда от самата формула (по-общо, проблемът би възникнал при прилагане към същата формула на произволна субституция σ, за която  X∈VAR(σ(U)) ). Ето защо по-разумна би била дефиниция, при която за резултат от въпросното прилагане на субституцията [U/X] да може да се смята да речем формулата  ∃Y p(Y,X). За да дадем такава дефиниция, първо се уславяме за всяка субституция σ и всеки две променливи ξ и η да означаваме със σξ/η субституцията, която съвпада със σ за всяка променлива, различна от ξ, а на променливата ξ съпоставя η. След това за всяка формула φ и всяка субституция σ дефинираме множество σ<φ> (множество на допустимите резултати от прилагане на σ към φ) по следния индуктивен начин:

  1. Ако φ е атомарна формула или някоя от формулите true и fail, то σ<φ> = {φσ}.
  2. σ<¬φ> = { ¬ψ | ψ∈σ<φ> } за всяка формула φ.
  3. σ<φ1&…&φn> = { ψ1&…&ψn | ψ1∈σ<φ1>,…,ψn∈σ<φn> } при всеки избор на формулите φ1, …, φn.
  4. σ<φ1∨…∨φn> = { ψ1∨…∨ψn | ψ1∈σ<φ1>,…,ψn∈σ<φn> } при всеки избор на формулите φ1, …, φn.
  5. σ<∀ξφ> = { ∀ηψ | η∈Ξ \ ∪{ VAR(σ(ζ)) | ζ∈FVAR(φ)\{ξ} }, ψ∈σξ/η<φ> } за всяка формула φ и всяка променлива ξ.
  6. σ<∃ξφ> = { ∃ηψ | η∈Ξ \ ∪{ VAR(σ(ζ)) | ζ∈FVAR(φ)\{ξ} }, ψ∈σξ/η<φ> } за всяка формула φ и всяка променлива ξ.
    Пример 1. Формулата  ∃Y p(Y,X) принадлежи на множеството  [U/X]<∃X p(X,U)>,  защото
∪{ VAR([U/X](ζ)) | ζ∈FVAR(p(X,U))\{X} } = {X},
Y ∈ Ξ \ {X},
[U/X]X/Y = [U/X,X/Y],
p(Y,X) ∈ [U/X,X/Y]<p(X,U)>.
Формулата  ∃X p(X,X) обаче не принадлежи на множеството  [U/X]<∃X p(X,U)>,  защото за разлика от Y променливата X не е от множеството  Ξ \ {X}.

    Чрез индукция, съобразена с дефиницията за безкванторна формула, се доказва, че  σ<φ> = { φσ }  за всяка безкванторна формула φ и всяка субституция σ. Използвайки пък индукция, съобразена с дефиницията за произволна формула, виждаме, че за всяка формула φ и всяка субституция σ множеството  σ<φ>  има поне един елемент (всъщност това множество има безбройно много елементи, когато формулата φ не е безкванторна). Друго свойство, лесно доказуемо чрез такава индукция, е следното: всяка формула φ принадлежи на съответното множество  ι<φ> , където ι е тъждествената субституция (в случаите от индуктивната стъпка, отнасящи се за формула с квантор в началото, използваме, че за всяка променлива ξ субституцията ιξ/ξ съвпада с ι и, която и да е формулата φ, променливата ξ не принадлежи на обединението на множествата VAR(ι(ζ)), където ζ∈FVAR(φ)\{ξ}).

    Индуктивно се дефинира понятие за брой на кванторите в една формула, като се приема, че атомарните формули и формулите true и fail са с нулев брой квантори, броят на кванторите в една конюнкция и в една дизюнкция е равен на сбора от броевете на кванторите в нейните членове, при образуване на отрицание броят на кванторите се запазва, а при поставяне на квантор този брой се увеличава с единица. Чрез индукция, съобразена с дефиницията за формула, се установяват следните свойства: а) нулев брой квантори имат точно онези формули, които са безкванторни, и б) за всяка формула φ и всяка субституция σ формулите от множеството  σ<φ>  са със същия брой квантори както формулата φ. Благодарение на свойството а) можем да разглеждаме свойството б) като обобщение на това, че при прилагане на субституция към безкванторна формула се получава безкванторна формула.

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

    Твърдение за свободните променливи на резултат от прилагане на субституция. За всяка формула φ, всяка субституция σ и всяка формула ψ от множеството σ<φ> имаме равенството

FVAR(ψ) = ∪{ VAR(σ(ζ)) | ζ∈FVAR(φ) }.
    Доказателство. Използваме индукция по построението на формулата φ. Ясно е, че твърдението е вярно в случаите, когато φ е безкванторна формула, и в частност то е вярно, когато φ е атомарна формула или някоя от формулите true и fail. Разсъжденията за случаите на отрицание, конюнкция и дизюнкция от индуктивната стъпка не се различават много от онези, които се правят в доказателството на аналогичното твърдение за прилагане на субституция към безкванторна формула. Затова ще разгледаме подробно само случая на поставяне на квантор. Ще се ограничим с разглеждането за квантор за общност, а за квантор за съществуване то е аналогично. Нека дадена формула φ е такава, че горното равенство е в сила за всяка субституция σ и всяка формула ψ от множеството σ<φ>. Ще покажем, че за всяка променлива ξ, всяка субституция σ и всяка формула ψ от множеството σ<∀ξφ> имаме равенството
FVAR(ψ) = ∪{ VAR(σ(ζ)) | ζ∈FVAR(∀ξφ) },
т.е. равенството
FVAR(ψ) = ∪{ VAR(σ(ζ)) | ζ∈FVAR(φ)\{ξ} },
Нека ξ е произволна променлива, σ е произволна субституция и ψ е някоя формула от множеството σ<∀ξφ>. Тогава ψ=∀ηψ, където η е някоя променлива, непринадлежаща на ∪{ VAR(σ(ζ)) | ζ∈FVAR(φ)\{ξ} }, а ψ е някоя формула от множеството σξ/η<φ>. Да положим  σ = σξ/η.  Предположението, което направихме за формулата φ, позволява да твърдим, че
FVAR(ψ) = ∪{ VAR(σ(ζ)) | ζ∈FVAR(φ) }.
Оттук получаваме, че
FVAR(ψ) = ∪{ VAR(σ(ζ)) | ζ∈FVAR(φ) } \ {η} = ∪{ VAR(σ(ζ))\{η} | ζ∈FVAR(φ) }.
Като вземем пред вид, че множеството VAR(σ(ζ))\{η} е празно при ζ=ξ и че субституциите σ и σ съвпадат за променливите, различни от ξ, виждаме, че
FVAR(ψ) = ∪{ VAR(σ(ζ))\{η} | ζ∈FVAR(φ)\{ξ} } = ∪{ VAR(σ(ζ))\{η} | ζ∈FVAR(φ)\{ξ} }.
При това положение е достатъчно само да забележим, че VAR(σ(ζ))\{η}=VAR(σ(ζ)) при ζ∈FVAR(φ)\{ξ}, понеже η не принадлежи на VAR(σ(ζ)) за никое такова ζ. □

    Твърдение за стойността на резултат от прилагане на субституция. Нека S е дадена структура. За всяка формула φ, всяка субституция σ, всяка формула ψ от множеството σ<φ> и всяка оценка v в S на променливите имаме равенството

ψS,v = φS,σS(v).
    Доказателство. Както при доказателството на предходното твърдение ще използваме индукция по построението на формулата φ. Ясно е, че твърдението е вярно в случаите, когато φ е безкванторна формула, и в частност то е вярно, когато φ е атомарна формула или някоя от формулите true и fail. Понеже разсъжденията за случаите на отрицание, конюнкция и дизюнкция от индуктивната стъпка не се различават много от онези, които се правят в доказателството на аналогичното твърдение за прилагане на субституция към безкванторна формула, ще разгледаме подробно само случая на поставяне на квантор. Ще се ограничим с разглеждането за квантор за общност, защото за квантор за съществуване то е аналогично. Нека дадена формула φ е такава, че горното равенство е в сила за всяка субституция σ, всяка формула ψ от множеството σ<φ> и всяка оценка v в S на променливите. Ще покажем, че за всяка променлива ξ, всяка субституция σ, всяка формула ψ от множеството σ<∀ξφ> и всяка оценка v в S на променливите имаме равенството
ψS,v = ∀ξφS,σS(v).,
т.е. равенството
ψS,v = min{ φS,σS(v)[ξ→d] | d∈D },
където D е носителят на S. Нека ξ е произволна променлива, σ е произволна субституция, ψ е някоя формула от множеството σ<∀ξφ> и v е някоя оценка на променливите в S. Тогава ψ=∀ηψ, където η е някоя променлива, непринадлежаща на ∪{ VAR(σ(ζ)) | ζ∈FVAR(φ)\{ξ} }, а ψ е някоя формула от множеството σξ/η<φ>. Имаме равенството
ψS,v = min{ ψS,v[η→d] | d∈D }.
Да положим  σ = σξ/η.  Предположението, което направихме за формулата φ, позволява да заключим от горното равенство, че
ψS,v = min{ φS,σS(v[η→d]) | d∈D }.
При това положение ще бъде достатъчно да покажем, че за всеки елемент d на D оценките σS(v[η→d]) и σS(v)[ξ→d] съвпадат върху множеството FVAR(φ), т.е. че за всяко ζ от FVAR(φ) имаме равенството σ(ζ)S,v[η→d]=σ(ζ)S,v, когато ζ е различно от ξ, и равенството σ(ζ)S,v[η→d]=d, ако ζ=ξ. Първото от тези две неща следва от обстоятелството, че при ζ∈FVAR(φ)\{ξ) термът σ(ζ) съвпада с терма σ(ζ), като двете оценки v[η→d] и v съвпадат върху множеството на неговите променливи (понеже η не принадлежи на това множество). Второто пък е очевидно поради равенството σ(ξ)=η. □

    Особено често използвани субституции са онези от вида [η/τ], където η е променлива, а τ е терм. Очевидно за произволна структура S и произволна оценка v в нея на променливите имаме равенството

[η/τ]S(v)= v[η→τS,v].
Поради това съответният частен случай на твърдението за стойността на резултат от прилагане на субституция може да се изкаже така:

    Твърдение за стойността на резултат от заместване на променлива с терм. Нека S е дадена структура. За всяка формула φ, всяка променлива η, всеки терм τ, всяка формула ψ от множеството [η/τ]<φ> и всяка оценка v в S на променливите имаме равенството

ψS,v = φS,v[η→τS,v].

    Разбира се множеството [η/τ]<φ> се състои от безбройно много формули, когато формулата φ не е безкванторна. Ще дефинираме една точно определена формула φη[τ], за която при известно ограничение за φ, η и τ се показва, че принадлежи на въпросното множество (грубо казано, φη[τ] ще се получава чрез заместване на всички свободни участия на η във φ с τ без обаче да се вземат мерки срещу колизия на променливите). Дефиницията е чрез индукция по построението на φ и се състои от следните точки:

  1. Ако φ е атомарна формула или някоя от формулите true и fail, то φη[τ] = φ[η/τ].
  2. (¬φ)η[τ] = ¬φη[τ] за всяка формула φ.
  3. (φ1&…&φn)η[τ] = (φ1)η[τ]&…&(φn)η[τ] при всеки избор на формулите φ1, …, φn.
  4. (φ1∨…∨φn)η[τ] = (φ1)η[τ]∨…∨(φn)η[τ] при всеки избор на формулите φ1, …, φn.
  5. За всяка формула φ и всяка променлива ξ полагаме (∀ξφ)η[τ] = ∀ξφη[τ], ако променливата ξ е различна от η, и (∀ξφ)η[τ] = ∀ξφ в противен случай.
  6. За всяка формула φ и всяка променлива ξ полагаме (∃ξφ)η[τ] = ∃ξφη[τ], ако променливата ξ е различна от η, и (∃ξφ)η[τ] = ∃ξφ в противен случай.
    Чрез индукция по построението на φ се доказва следното твърдение: ако никоя свързана променлива на φ, различна от η, не принадлежи на множеството VAR(τ), то формулата φη[τ] принадлежи на множеството [η/τ]<φ>. Ето как изглежда например индуктивната стъпка за случая на поставяне на квантор за общност. Нека горното условно твърдение е вярно за дадена формула φ и нека за дадена променлива ξ никоя свързана променлива, различна от η, на формулата ∀ξφ не принадлежи на множеството VAR(τ). Понеже свързаните променливи на φ са свързани променливи и на ∀ξφ, тогава ножем да сме сигурни, че никоя свързана променлива на φ, различна от η, не принадлежи на VAR(τ) и следователно формулата φη[τ] принадлежи на множеството [η/τ]<φ>. Разбира се променливата ξ също няма да принадлежи на VAR(τ). Ако ξ е различна от η, това гарантира принадлежността на формулата (∀ξφ)η[τ] към множеството [η/τ]<∀ξφ>, тъй като тя тогава е ∀ξφη[τ], променливата ξ не принадлежи на множеството ∪{ VAR([η/τ](ζ)) | ζ∈FVAR(φ)\{ξ} } и е в сила равенството [η/τ]ξ,ξ = [η/τ]. Ако ли пък ξ съвпада с η, то отново формулата (∀ξφ)η[τ] принадлежи на множеството [η/τ]<∀ξφ>, понеже в този случай тя е ∀ξφ, променливата ξ отново не принадлежи на множеството ∪{ VAR([η/τ](ζ)) | ζ∈FVAR(φ)\{ξ} }, а формулата φ принадлежи на [η/τ]ξ,ξ<φ> (защото сега [η/τ] = [ξ/τ], [η/τ]ξ,ξ = ι).

    Пример 2. В условията на пример 1 имаме равенството (∃X p(X,U))U[X] = ∃X p(X,X). Поради това не може да се твърди, че винаги (без никакви предположения) формулата φη[τ] принадлежи на множеството [η/τ]<φ>.

 

Последно изменение във файла:  6 юни 2006 г.