Под субституция ще разбираме такава функция s с дефиниционна област множеството X на всички променливи и със стойности в множеството на термовете, че равенството s(X)=X да е нарушено най-много за краен брой променливи X. Ако X₁,..., X_m (m>0) са различни помежду си променливи, а U₁, ..., U_m са термове, то ще означаваме със знака [X₁/U₁,...,X_m/U_m] субституцията s, определена по следния начин: s(X_i)=U_i при i=1,...,m и s(X)=X за всяка променлива X, различна от X₁, ...,X_m; тази субституция ще наричаме заместване на X₁, ..., X_m съответно с U₁, ..., U_m. Субституцията, която изобразява всяка променлива в самата нея, ще наричаме тъждествена субституция и ще я означаваме с i (тя разбира се съвпада със субституцията [X₀/X₀] при произволно избрана променлива X₀).

    Нека s е дадена субституция. Като използваме еднозначното прочитане на термовете, дефинираме индуктивно за всеки терм T един терм Ts, който ще наричаме резултат от прилагането на s към T. Дефиницията е следната:
        а) Xs=s(X) за всяка променлива X;
        б) cs=c за всяка константа c;
        в) f(T₁,T₂...,T_n)s = f(T₁s,T₂s...,T_ns) всеки път, когато n>0, fОF_n и T₁, T₂, ..., T_n са термове.

    След като дефинирахме какво разбираме под резултат от прилагане на дадена субституция s към произволен терм, лесно се дефинира и резултат от прилагане на s към произволна атомарна формула, като този резултат е пак атомарна формула. Дефиницията е следната: когато pОP₀, приемаме, че резултатът от прилагането на s към p е p, а когато n е положително цяло число, pОP_n и T₁, Т₂, ..., Т_n са термове, за резултат от прилагането на s към p(T₁,Т₂...,Т_n) считаме атомарната формула p(T₁s,T₂s...,T_ns). Разбира се резултата от прилагането на субституцията s към една атомарна формула A ще означаваме с As. Като използваме така въведеното означение, можем да запишем, че ps=p за всеки нулместен предикатен символ p и имаме равенството

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

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

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

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

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

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

    Следствие. Ако E е терм или атомарна формула, а s е субституция, то резултатът Es е затворен точно тогава, когато термът Xs е затворен за всяка променлива X на E.

    Ще изложим само доказателството на твърдение 3 за случая на термове. Ако E е дадена променлива X₀, то VAR(E)={X₀}, тъй че дясната страна на доказваното равенство се равнява на VAR(X₀s), което е и лявата страна. Ако EОF₀, равенството пак е вярно, защото двете му страни са празни. Нека сега E е терм от вида f(T₁,E₂...,E_n), където n>0, fОF_n и E₁, E₂, ..., E_n са такива термове, че са верни равенствата

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

Previous  Next  Contents