Под субституция при дадена сигнатура Σ ще разбираме такова изображение σ на множеството Ξ на всички променливи в множеството на термовете при сигнатура Σ, че равенството σ(ξ)=ξ да е нарушено най-много за краен брой променливи ξ. По-нататък ще предполагаме, че сигнатурата Σ е фиксирана и няма да я споменаваме, като ще наричаме субституциите, термовете и атомарните формули при сигнатура Σ просто субституции, термове и атомарни формули. Ако ξ₁, …, ξ_m (m>0) са различни помежду си променливи, а θ₁, …, θ_m са термове, то ще означаваме със знака [ξ₁/θ₁,…,ξ_m/θ_m] субституцията σ, определена по следния начин: σ(ξ_i)=θ_i при i=1,…,m и σ(ξ)=ξ за всяка променлива ξ, различна от ξ₁, …,ξ _m; тази субституция ще наричаме заместване на ξ₁, …, ξ_m съответно с θ₁, …, θ_m. Субституцията, която изобразява всяка променлива в самата нея, ще наричаме тъждествена субституция и ще я означаваме с ι (тя разбира се съвпада със субституцията [ξ₀/ξ₀] при произволно избрана променлива ξ₀).

    Нека σ е дадена субституция. Като използваме еднозначното прочитане на термовете, ще дефинираме индуктивно за всеки терм τ един терм τσ, който ще наричаме резултат от прилагането на σ към τ. Дефиницията е следната:
        а) ξσ = σ(ξ) за всяка променлива ξ;
        б) ασ = α за всяка константа α;
        в) ω(τ₁,…,τ_n)σ = ω(τ₁σ,…,τ_nσ) всеки път, когато n>0, ω е n-местен функционален символ и τ₁, …, τ_n са термове.

    След като дефинирахме какво разбираме под резултат от прилагане на дадена субституция σ към произволен терм, лесно се дефинира и резултат от прилагане на σ към произволна атомарна формула, като този резултат е пак атомарна формула. Дефиницията е следната: когато π е нулместен предикатен символ, приемаме, че резултатът от прилагането на σ към π е π, а когато n е положително цяло число, π е n-местен предикатен символ и τ₁, …, τ_n са термове, за резултат от прилагането на σ към π(τ₁,…,τ_n) считаме атомарната формула π(τ₁σ,…,τ_nσ). Разбира се резултата от прилагането на субституцията σ към една атомарна формула φ ще означаваме с φσ. Като използваме така въведеното означение, можем да запишем, че πσ=π за всеки нулместен предикатен символ π и имаме равенството

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

    Твърдение 1. Ако τ е терм или атомарна формула, то резултатите от прилагането на две субституции σ и σ′ към τ съвпадат точно тогава, когато σ и σ′ съвпадат върху множеството на променливите на τ.

    Доказателство. В случая, когато τ е терм, разсъждаваме по следния начин. Ако τ е променлива или константа, то верността на твърдението е непосредствено ясна от точки а) и б) на дефиницията за резултат от прилагане на субституция към терм. Да предположим сега, че τ е терм от вида ω(τ₁,…,τ_n), където n>0, ω e n-местен функционален символ и τ₁, …, τ_n са такива термове, че при i=1,…,n равенството τ_iσ = τ_iσ′ да е равносилно със съвпадането на σ и σ′ върху множеството VAR(τ_i). От точка в) на дефиницията се вижда, че равенството τσ = τσ′ е изпълнено точно тогава, когато са изпълнени равенствата τ_iσ = τ_iσ′, i=1,…,n. Значи резултатите от прилагането на σ и σ′ към τ съвпадат точно тогава, когато σ и σ′ съвпадат върху всяко от множествата VAR(τ_i), i=1,…,n, т.е. когато σ и σ′ съвпадат върху обединението на тези множества. Въпросното обединение обаче е точно множеството на променливите на τ.  _□

    Твърдение 2. Ако τ е терм или атомарна формула, то е в сила равенството τι = τ.

    Доказателство. Ако τ е променлива или константа, то верността на твърдението е непосредствено ясна от точки а) и б) на дефиницията за резултат от прилагане на субституция към терм. Ако пък τ е терм от вида ω(τ₁,…,τ_n), където n>0, ω е n-местен функционален символ и термовете τ₁, …, τ_n са такива, че при i=1,…,n е в сила равенството τ_iι = τ_i, то точка в) на дефиницията дава

    Следствие от твърдения 1 и 2. Ако τ е затворен терм или затворена атомарна формула, то за всяка субституция σ е в сила равенството τσ = τ.

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

    Твърдение 3. Ако τ е терм или атомарна формула, то за всяка субституция σ е изпълнено равенството

    Доказателство. Разсъжденията за случая, когато τ е терм, са следните. Ако τ е променлива, то VAR(τ)={τ}, тъй че дясната страна на доказваното равенство се равнява на VAR(τσ), което е и лявата страна. Ако τ е константа, равенството пак е вярно, защото двете му страни са празни. Нека сега τ=ω(τ₁,…,τ_n), където n>0, ω е n-местен функционален символ и τ₁, …, τ_n са такива термове, че при i=1,…,n е в сила равенството

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

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