Като се използват твърденията 1, 2, 3 от текста „Субституции. Прилагане на субституция към терм“, лесно се получават следните аналогични твърдения за прилагането на субституция към атомарна формула.

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

      Доказателство. Равенството ιφ = φ е очевидно, когато φ е нулместен предикатен символ. Да предположим сега, че φ = π(τ₁,…,τ_n), където n е положително цяло число, π е n-местен предикатен символ и τ₁, …, τ_n са термове. Тогава

      Твърдение 2°. Нека σ и σ' са произволни субституции. Ако φ е произволна атомарна формула, то равенството σφ = σ'φ е изпълнено точно тогава, когато σ и σ' съвпадат върху множеството VAR(φ).

      Доказателство. Ако φ е нулместен предикатен символ, то твърдението е тривиално. Да предположим сега, че φ = π(τ₁,…,τ_n), където n е положително цяло число, π е n-местен функционален символ и τ₁, …, τ_n са термове. От равенствата

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

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

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

      Доказателство. Твърдението е вярно в случая, когато φ е нулместен предикатен символ, защото обединението на празно семейство от множества е празно. Да предположим сега, че φ = π(τ₁,…,τ_n), където n е положително цяло число, π е n-местен предикатен символ и τ₁, …, τ_n са термове. От равенството σφ = π(στ₁,…,στ_n) получаваме, че VAR(σφ) е обединение на множествата VAR(στ₁), …, VAR(στ_n) и следователно VAR(σφ) е обединение на множествата VAR(ση), където η принадлежи на обединението на множествата VAR(τ₁), …, VAR(τ_n). Последното обединение обаче е точно VAR(φ).  _□

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

      Дефиницията за резултат от прилагане на субституция към атомарна формула може без затруднение да се разпространи за случая на произволни безкванторни формули така, че да остане в съответствие със същата интуитивна представа за резултата и да се запазят свойствата, които доказахме. При формули, които имат свързани променливи, положението обаче е по-сложно. Нека например φ е формулата ∃x p(x,y), където p е двуместен предикатен символ. Ако се запитаме какво е разумно да разбираме под резултат от прилагане на дадена субституция σ към φ, веднага трябва да отхвърлим възможността да приемем за такъв резултат думата ∃θ p(θ,σy), където θ = σx. Преди всичко, тази дума няма да бъде формула, когато термът σx не е променлива. Но дори и σx да е променлива, споменатото приемане ще бъде поне в някои случаи неприемливо. Ако, да речем, σ е субституцията [x/y], то би се получила затворената формула ∃y p(y,y) и значи няма да е в сила аналогът на твърдение 3°, получаващ се чрез замяна на VAR(σφ) и VAR(φ) съответно с FVAR(σφ) и FVAR(φ) (ако той би бил в сила, променливата y би трябвало да се окаже свободна променлива на формулата ∃y p(y,y)). Понеже формулата φ във всяка конкретна структура изразява условие, отнасящо се до стойността на y, но не и до стойността на x, по-естествено би било да оставим променливата x така, както е, и под резултат от прилагане на σ към φ да разбираме формулата ∃x p(x,σy). Както ще видим, такова приемане наистина може да се смята за разумно, но при едно ограничение, а именно x не бива да е променлива на терма σy  –  в противен случай отново не би бил в сила споменатият преди малко аналог на твърдение 3° (ако той би бил в сила, променливата x, бидейки променлива на терма σy, би трябвало да се окаже свободна променлива на формулата ∃x p(x,σy), а това е невъзможно поради квантора ∃x в началото й).

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

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

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

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

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

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

      Пример 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).

      Когато за една субституция σ и една формула φ резултатът σφ е дефиниран, казва се, че σ e прилoжима към φ. В останалите случаи се казва, че при прилагането на σ към φ възниква колизия на променливи (това е свързано с обстоятелството, че при проверка посредством дефиницията дали споменатият резултат е дефиниран, заключение, че той не е дефиниран, се получава точно тогава, когато на някоя стъпка от проверката се използва точка 4_g или точка 4_e и се оказва нарушена частта от ограничителното изискване в нея след съюза „и“).

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

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

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

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

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

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

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

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

      Твърдение 2. Нека σ и σ' са субституции, като резултатът σ'φ е дефиниран за дадена формула φ. За да бъде дефиниран резултатът σφ и да имаме равенството σφ = σ'φ, необходимо и достатъчно е σ и σ' да съвпадат върху множеството VAR(φ)..

      Доказателство. Пак използваме индукция, съобразена с дефиницията за формула. Твърдението е в сила, когато φ е атомарна формула. Индуктивните стъпки, отнасящи се до отрицание, конюнкция и дизюнкция, са прости. Например нека φ и ψ са формули, които имат доказваното свойство, и нека резултатът σ'(φ&ψ) е дефиниран. Тогава са дефинирани резултатите σ'φ и σ'ψ и имаме равенството σ'(φ&ψ) = (σ'φ&σ'ψ). За да бъде дефиниран резултатът σ(φ&ψ) и да съвпада с резултата σ'(φ&ψ), необходимо и достатъчно е да бъдат дефинирани σφ и σψ и да съвпадат съответно с σ'φ и с σ'ψ. Благодарение на индуктивното предположение за формулите φ и ψ това е равносилно с изискването σ и σ' да съвпадат както върху множеството на свободните променливи на φ, така и върху множеството на свободните променливи на ψ, т.е. да съвпадат върху обединението на тези две множества. То обаче е точно множеството на свободните променливи на формулата (φ&ψ). От индуктивните стъпки, отнасящи се до генерализация и екзистенциализация, да разгледаме например първата. Нека φ е формула, която има доказваното свойство, ξ е променлива, σ и σ' са субституции и резултатът σ'∀ξφ е дефиниран. Тогава е дефиниран резултатът σ'_ξ/ξφ, ξ не е променлива на терма σ'η за никоя свободна променлива η на φ, различна от ξ, и имаме равенството σ'∀ξφ = ∀ξσ'_ξ/ξφ. За да бъде дефиниран резултатът σ∀ξφ и да съвпада с резултата σ'∀ξφ, необходимо и достатъчно е да е дефиниран резултатът σ_ξ/ξφ, ξ да не е променлива на терма ση за никоя свободна променлива η на φ, различна от ξ, и да имаме равенството σ_ξ/ξφ = σ'_ξ/ξφ. Благодарение на индуктивното предположение за формулата φ изискването да е дефиниран резултатът σ_ξ/ξφ и да съвпада с резултата σ'_ξ/ξφ е равносилно със съвпадане на σ_ξ/ξ и σ'_ξ/ξ върху множеството на свободните променливи на φ, а това е равносилно със съвпадане на σ и σ' върху множеството на свободните променливи на ∀ξφ. Когато такова съвпадане е налице, то осигурява, че ξ не е променлива на терма ση за никоя свободна променлива η на φ, различна от ξ, тъй че в крайна сметка нещата се свеждат до споменатото съвпадане.  _□

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

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

      Твърдение 3. Когато за една формула φ и една субституция σ резултатът σφ е дефиниран, множеството FVAR(σφ) е обединение на множествата VAR(ση), където η принадлежи на VAR(φ).

      Доказателство. Използваме индукция, съобразена с дефиницията за формула. Твърдението е вярно в случаите, когато φ е атомарна формула. Разсъжденията за случаите на отрицание, конюнкция и дизюнкция са лесни. Нека например резултатът σ(φ&ψ) е дефиниран за дадена субституция σ и дадени формули φ и ψ, които притежават доказваното свойство. Тогава σφ и σψ са дефинирани и е в сила равенството σ(φ&ψ) = (σφ&σψ). Оттук получаваме, че множеството на свободните променливи на формулата σ(φ&ψ) е обединение на множествата FVAR(σφ) и FVAR(σψ). Следователно то ще бъде обединение на всички множества VAR(ση), където η принадлежи на FVAR(φ), и всички множества VAR(ση), където η принадлежи на FVAR(ψ), тъй че в крайна сметка то ще бъде обединение на всички множества VAR(ση), където η принадлежи на множеството на свободните променливи на (φ&ψ). Да разгледаме сега случая на поставяне на квантор. Ще се ограничим с разглеждането за квантор за общност, а за квантор за съществуване то е аналогично. Нека резултатът σ∀ξφ е дефиниран за дадена субституция σ, дадена променлива ξ и дадена формула φ, притежаваща доказваното свойство. Ще покажем, че множеството FVAR(σ∀ξφ) е обединение на множествата VAR(ση), където η принадлежи на FVAR(∀ξφ), т.е. на множествата VAR(ση), където η принадлежи на FVAR(φ)\{ξ}. Това, че резултатът σ∀ξφ е дефиниран, дава, че е дефиниран резултатът σ_ξ/ξφ и ξ не е променлива на терма ση за никоя свободна променлива η на φ, различна от ξ, като при това имаме равенството σ∀ξφ = ∀ξσ_ξ/ξφ и следователно FVAR(σ∀ξφ) = FVAR(σ_ξ/ξφ)\{ξ}. От направеното индуктивно предположение за φ получаваме, че FVAR(σ_ξ/ξφ) е обединение на множествата VAR(σ_ξ/ξη), където η принадлежи на FVAR(φ). Въпросното обединение е всъщност обединението на множествата VAR(ση), където η принадлежи на FVAR(φ)\{ξ}, с евентуално добавена към него ξ. Тъй като ξ не принадлежи на никое от споменатите множества VAR(ση), оттук става ясно, че FVAR(σ∀ξφ) наистина съвпада с тяхното обединение.  _□

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

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

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