Под субституция ще разбираме такава функция 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 е терм или атомарна формула, то резултатите от прилагането на две субституции s и sў към E съвпадат точно тогава, когато s и sў съвпадат върху множеството на променливите на E.

    Доказателство. В случая, когато E е терм, разсъждаваме по следния начин. Ако E е променлива или константа, то верността на твърдението е непосредствено ясна от точки а) и б) на дефиницията за резултат от прилагане на субституция към терм. Да предположим сега, че E е терм от вида f(E₁,E₂...,E_n), където n>0, fОF_n и E₁, E₂, ..., E_n са такива термове, че при i=1,2,...,n равенството E_is=E_isў да е равносилно със съвпадането на s и sў върху множеството VAR(E_i). От точка в) на дефиницията се вижда, че равенството Es=Esў е изпълнено точно тогава, когато са изпълнени равенствата E_is=E_isў, i=1,2,...,n. Значи резултатите от прилагането на s и sў към E съвпадат точно тогава, когато s и sў съвпадат върху всяко от множествата VAR(E_i), i=1,2,...,n, т.е. когато s и sў съвпадат върху обединението на тези множества. Въпросното обединение обаче е точно множеството на променливите на E.  _ї

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

    Доказателство. Ако E е променлива или константа, то верността на твърдението е непосредствено ясна от точки а) и б) на дефиницията за резултат от прилагане на субституция към терм. Ако пък E е терм от вида f(E₁,E₂...,E_n), където n>0, fОF_n и термоветеE₁, E₂, ..., E_n са такива, че при i=1,2,...,n е в сила равенството E_ii=E_i, то точка в) на дефиницията дава

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

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

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

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

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

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

Previous  Next  Contents