Съдържание 
 

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

      Дефиницията за резултат от прилагане на субституция към атомарна формула може без затруднение да се разпространи за случая на произволни безкванторни формули така, че да остане в съответствие със същата интуитивна представа за резултата и да се запазят свойствата, които доказахме. При формули, които имат свързани променливи, положението обаче е по-сложно. Нека например φ е формулата ∃x p(x,y), където p е двуместен предикатен символ. Ако се запитаме какво е разумно да разбираме под резултат от прилагане на дадена субституция σ към φ, веднага трябва да отхвърлим възможността да приемем за такъв резултат думата ∃σx p(σx,σy). Преди всичко, тази дума няма да бъде формула, когато термът σx не е променлива. Но дори и σx да е променлива, споменатото приемане ще бъде поне в някои случаи неприемливо от семантична гледна точка. Ако, да речем, σ е субституцията [x/y], то би се получила затворената формула ∃y p(y,y); има обаче структури, в които тя не е вярна, а φ е тъждествено вярна  -  следователно теоремата за стойността на резултат от прилагане на субституция не би останала в сила при такова приемане. Понеже формулата φ във всяка конкретна структура изразява условие, отнасящо се до стойността на y, но не и до стойността на x, по-естествено би било да оставим променливата x така, както е, и под резултат от прилагане на σ към φ да разбираме формулата ∃x p(x,σy). Както ще видим, такова приемане наистина може да се смята за разумно, но при едно ограничение, а именно x не бива да е променлива на терма σy. Нуждата от това ограничение може да бъде аргументирана така: нормално би било променливите на терма σy да бъдат свободни променливи на резултата от прилагането на σ към φ, но това би се нарушило за променливата x в случай че тя е променлива на σy и продължим под резултат от прилагане на σ към φ да разбираме формулата ∃x p(x,σy). Можем да си послужим и със следната семантична аргументация: ако S е структура с носител D, v е оценка в S и означим с v′ оценката σS(v), то
(∃x p(x,σy))S,v = max{p(x,σy)S,v[x→d] | d∈D} = max{pS(d,(σy)S,v[x→d]) | d∈D},
φS,v′ = max{p(x,y)S,v′[x→d] | d∈D} = max{pS(d,v′(y)) | d∈D} = max{pS(d,(σy)S,v) | d∈D}
и в общия случай поради различието на получените изрази за числата (∃x p(x,σy))S,v и φS,v′ няма гаранция, че тези числа са равни, докато в случаите, когато x не е променлива на σy, различието е несъществено.

      Формулата p(x,σy), за която стана дума преди малко, може да се получи от формулата p(x,y) чрез прилагане на субституция, преобразуваща x в x и съвпадаща със σ за всички други променливи. За произволна субституция σ, произволна променлива ξ и произволен терм θ ние ще означаваме със σξ/θ онази субституция, която преобразува променливата ξ в θ и съвпада със σ за всички други променливи (всъщност ще имаме повод да използваме това означение само в случаи, когато термът θ е променлива). При така въведеното означение казаното по-горе за формулите p(x,σy) и p(x,y) може да се запише посредством равенството

p(x,σy) = σx/xp(x,y).

      Сега ще дадем една индуктивна дефиниция за резултат σφ от прилагане на субституция σ към формула φ, който резултат ще бъде дефиниран еднозначно, но не винаги, а при известни ограничения, и, когато е дефиниран, ще бъде пак формула. За да различаваме въведеното чрез тази дефиниция понятие от едно по-общо друго, което ще въведем по-нататък, резултата, който ще въведем сега, ще го наричаме резултат от прилагане на σ към φ без да се преименуват свързани променливи (мотивите за избора на такъв термин ще станат ясни при въвеждането на по-общото понятие). Дефиницията се състои от следните точки:
        1. Резултатът от прилагане на σ към атомарна формула φ без да се преименуват свързани променливи е винаги дефиниран и съвпада с вече дефинирания резултат от прилагане на σ към φ.
        2. За всяка формула φ приемаме, че резултатът σ¬φ е дефиниран точно тогава, когато е дефиниран резултатът σφ, и че тогава σ¬φ = ¬σφ.
        3c. За всеки две формули φ и ψ приемаме, че резултатът σ(φ&ψ) е дефиниран точно тогава, когато са дефинирани резултатите σφ и σψ, и че тогава σ(φ&ψ) = (σφ&σψ).
        3d. За всеки две формули φ и ψ приемаме, че резултатът σ(φ∨ψ) е дефиниран точно тогава, когато са дефинирани резултатите σφ и σψ, и че тогава σ(φ∨ψ) = (σφ&σψ).
        4g. За всяка формула φ и всяка променлива ξ приемаме, че резултатът σ∀ξφ е дефиниран точно тогава, когато е дефиниран резултатът σξ/ξφ и ξ не е променлива на терма ση за никоя свободна променлива η на φ, различна от ξ; когато са изпълнени тези условия, приемаме, че σ∀ξφ = ∀ξσξ/ξφ.
        4e. За всяка формула φ и всяка променлива ξ приемаме, че резултатът σ∃ξφ е дефиниран точно тогава, когато е дефиниран резултатът σξ/ξφ и ξ не е променлива на терма ση за никоя свободна променлива η на φ, различна от ξ; когато са изпълнени тези условия, приемаме, че σ∃ξφ = ∃ξσξ/ξφ

      От горната дефиниция се вижда (чрез индукция, съобразена с дефиницията за безкванторна формула), че, която и да е субституцията σ, резултатът σφ е дефиниран за всяка безкванторна формула φ и е също безкванторна формула. Разбира се, при произволни формули не винаги е дефиниран резултат от прилагане на субституция без да се преименуват свързани променливи. Следният пример се получава, като приложим дефиницията към формулата ∃x p(x,y), с която илюстрирахме нещата в началото.

      Пример 1. При предположение, че p е двуместен предикатен символ, да означим със σ произволна субституция. Понеже (по точка 1 от дефиницията) резултатът σx/xp(x,y) е дефиниран и е равен на p(x,σy), точка 4e дава, че резултатът σ∃x p(x,y) е дефиниран точно тогава, когато x не е променлива на σy, и че тогава въпросният резултат е ∃x p(x,σy). В частност, [x/y]∃x p(x,y) = ∃x p(x,y).

      Ще разгледаме още два примера.

      Пример 2. Нека q е едноместен предикатен символ. Тогава

[x/y](q(x)∨∀x¬q(x)) = ([x/y]q(x)∨[x/y]∀x¬q(x)) = (q(y)∨∀xι¬q(x)) = (q(y)∨∀x¬ιq(x)) = (q(y)∨∀x¬q(x)).

      Пример 3. Нека r е триместен предикатен символ. Тогава [z/x]∀x∃y r(x,y,z) и [z/y]∀x∃y r(x,y,z) не са дефинирани, а [x/y,y/x,z/u,u/z]∀z r(x,y,z) = ∀z r(y,x,z).

      Когато за една субституция σ и една формула φ резултатът σφ не е дефиниран, казва се, че при прилагането на σ към φ възниква колизия на променливи. Тази терминология е свързана с обстоятелството, че при проверка посредством дефиницията дали споменатият резултат е дефиниран, заключение, че той не е дефиниран, се получава точно тогава, когато на някоя стъпка от проверката се използва точка 4g или точка 4e и се оказва нарушена частта от ограничителното изискване в нея след съюза "и".

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

      Достатъчно условие за съществуване на резултат от прилагане на дадена субституция към дадена формула без да се преименуват свързани променливи. Нека φ е формула, а σ е такава субституция, че за никоя свободна променлива η на φ множеството VAR(ση) да не съдържа свързани променливи на φ, различни от η. В такъв случай съществува резултат от прилагане на σ към φ без да се преименуват свързани променливи.

      Доказателство. Ще използваме индукция, съобразена с дефиницията на понятието формула. Ако φ е атомарна формула, то резултатът σφ е дефиниран за всяка субституция σ. Индуктивните стъпки за случаите на отрицание, конюнкция и дизюнкция са прости. Например нека φ и ψ са формули, които имат доказваното свойство, и нека σ е такава субституция, че за никоя свободна променлива η на конюнкцията (φ&ψ) множеството VAR(ση) да не съдържа свързани променливи на (φ&ψ), различни от η. Понеже свободните и свързаните променливи на всеки от членовете на конюнкцията са съответно свободни и свързани променливи и на самата конюнкция, не е възможно за някоя свободна променлива η на φ множеството VAR(ση) да съдържа свързани променливи на φ, различни от η, нито е възможно за някоя свободна променлива η на ψ въпросното множество да съдържа свързани променливи на ψ, различни от η. Поради това резултатите σφ и σψ са дефинирани, следователно дефиниран е и резултатът σ(φ&ψ). Малко повече труд изискват индуктивните стъпки за случаите на генерализация и екзистенциализация. Ще разгледаме първия от тях, а вторият е напълно аналогичен. Нека φ е формула, която има доказваното свойство, нека ξ e променлива и нека σ е такава субституция, че за никоя свободна променлива η на формулата ∀ξφ множеството VAR(ση) да не съдържа свързани променливи на ∀ξφ, различни от η. Понеже всяка свободна променлива на формулата φ е свободна променлива на ∀ξφ или е ξ, а всяка свързана променлива на φ е свързана променлива и на ∀ξφ, не е възможно за някоя свободна променлива на φ множеството VAR(σξ/ξη) да съдържа свързани променливи на φ, различни от η. Поради това резултатът σξ/ξφ е дефиниран. За да покажем, че резултатът σ∀ξφ е дефиниран, остава да отбележим, че ако η е коя да е свободна променлива на φ, различна от ξ, то ξ не принадлежи на VAR(ση), понеже тогава η е свободна променлива на формулата ∀ξφ, а ξ е нейна свързана променлива, различна от η.  □

      Следствие. Ако σ е субституция от вида [ξ1/θ1,…,ξk/θk], където θ1, …, θk са затворени термове, то резултатът σφ е дефиниран за всяка формула φ.

      Достатъчното условие от доказаното твърдение е изпълнено например за безкванторните формули, тъй като те изобщо нямат свързани променливи. Изпълнено е и в случаите от разгледаните примери, когато съществува резултат от прилагане без да се преименуват променливи. Условието обаче не е необходимо. Например то не е изпълнено за формулата (q(y)∨∀x¬q(x)) и субституцията [y/x], но въпреки това резултатът [y/x](q(y)∨∀x¬ιq(x)) = (q(y)∨∀x¬q(x)) е дефиниран (той е (q(x)∨∀x¬q(x))).

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

      Твърдение 1. За всяка формула φ е дефиниран резултатът ιφ и е в сила равенството ιφ=φ.

      Доказателство. Използваме индукция, съобразена с дефиницията за формула. Знаем, че заключението на твърдението е в сила, когато φ е атомарна формула. Индуктивните стъпки, отнасящи се до отрицание, конюнкция и дизюнкция, са съвсем прости, а при индуктивните стъпки за случаите на генерализация и екзистенциализация използваме обстоятелството, че ιξ/ξ=ι за всяка променлива ξ.  □

      Твърдение 2. Нека σ и σ′ са субституции, които съвпадат върху множеството на свободните променливи на дадена формула φ. Ако резултатът σφ е дефиниран, то резултатът σ′φ също е дефиниран и е изпълнено равенството σφ=σ′φ.

      Доказателство. Пак използваме индукция, съобразена с дефиницията за формула. Твърдението е в сила, когато φ е атомарна формула. Индуктивните стъпки, отнасящи се до отрицание, конюнкция и дизюнкция, са прости. Например нека φ и ψ са формули, които имат доказваното свойство, и нека σ и σ′ са субституции, които съвпадат върху множеството на свободните променливи на дизюнкцията (φ∨ψ), като освен това резултатът σ(φ∨ψ) е дефиниран. Тогава, разбира се, σ и σ′ съвпадат както върху множеството на свободните променливи на φ, така и върху множеството на свободните променливи на ψ, като са дефинирани също резултатите σφ и σψ. Оттук получаваме, че и резултатите σ′φ и σ′ψ са дефинирани и са в сила равенствата σφ=σ′φ, σψ=σ′ψ. Това показва, че е дефиниран и резултатът σ′(φ∨ψ), като имаме

σ(φ∨ψ) = (σφ∨σψ) = (σ′φ∨σ′ψ) = σ′(φ∨ψ).
От индуктивните стъпки, отнасящи се до генерализация и екзистенциализация, да разгледаме например първата. Нека φ е формула, която има доказваното свойство, и нека σ и σ′ са субституции, които съвпадат върху множеството на свободните променливи на формулата ∀ξφ, където ξ е дадена променлива, като освен това резултатът σ∀ξφ е дефиниран. Тогава субституциите σξ/ξ и σ′ξ/ξ ще съвпадат върху множеството на свободните променливи на φ, ще бъде дефиниран резултатът σξ/ξφ и ξ няма да бъде променлива на терма ση за никоя свободна променлива η на φ, различна от ξ. Това гарантира, че ще бъде дефиниран и резултатът σ′ξ/ξφ, ще имаме равенството σξ/ξφ=σ′ξ/ξφ и ξ няма да бъде променлива на терма σ′η за никоя свободна променлива η на φ, различна от ξ. Оттук получаваме, че е дефиниран и резултатът σ′∀ξφ, като имаме
σ∀ξφ = ∀ξσξ/ξφ = ∀ξσ′ξ/ξφ = σ′∀ξφ.  □

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

      Доказателство. Прилагаме твърдение 2 при σ′=ι.  □

      Като се използват дефинициите за конюнкции и дизюнкции с произволен ненулев краен брой членове, както и за импликация и еквиваленция, лесно се установява, че за всяка субституция σ е в сила следното:
.        (a) ako θ е конюнкция или дизюнкция на дадена непразна крайна редица φ1,…,φn от формули, то резултатът σθ е дефиниран точно тогава, когато са дефинирани резултатите σφ1, …, σφn, и тогава σθ е съответно конюнкция или дизюнкция на редицата σφ1,…,σφn;
.        (б) ako θ е импликация от φ към ψ или еквиваленция на φ и ψ, резултатът σθ е дефиниран точно тогава, когато са дефинирани резултатите σφ и σψ, и тогава σθ е съответно импликация от σφ към σψ или еквиваленция на σφ и σψ.
 

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