Съдържание 
 

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

      Знаем, че не винаги е дефиниран резултат от прилагане на дадена субституция към дадена формула без да се преименуват свързани променливи. Тук ще дефинираме едно общо понятие за резултат от прилагане на дадена субституция към дадена формула така, че той ще съществува винаги, но не винаги ще бъде единствен. Идеята на дефиницията ще поясним пак със задачата за прилагане на дадена субституция σ към формулата ∃x p(x,y), където p е двуместен предикатен символ. Когато x е променлива на терма σy, не е дефиниран резултат от прилагането на σ към тази формула без да се преименуват свързани променливи. Въпросната формула обаче е еквивалентна на всяка формула от вида ∃ζ p(ζ,y), където ζ е променлива, различна от y (вж. пример 3 от текста "Еквивалентни формули"). Понеже термът σy има само краен брой променливи, можем да изберем променливата ζ така, че не само да е различна от y, но и да не принадлежи на VAR(σy), и след това да разгледаме резултата σ∃ζ p(ζ,y). Той ще бъде ∃ζ p(ζ,σy), поради което ще зависи от избора на ζ. Пак според пример 3 от текста "Еквивалентни формули" обаче всеки две формули от вида ∃ζ p(ζ,σy), където ζ∉VAR(σy), са еквивалентни помежду си. Това навежда на мисълта да разглеждаме като резултат от прилагане на σ към формулата ∃x p(x,y) коя да е формула от вида ∃ζ p(ζ,σy), където ζ е променлива, непринадлежаща на VAR(σy) (всяка такава формула ще бъде, тъй да се каже, резултат от прилагане на σ към формулата ∃x p(x,y) с подходящо преименуване на свързаната променлива x). Например като резултат от прилагането на субституцията [y/x] към формулата ∃x p(x,y) бихме могли да разглеждаме формулата ∃z p(z,x), формулата ∃u p(u,x), формулата ∃v p(v,x) и даже формулата ∃y p(y,x) (макар че тя не е от вида [y/x]∃ζ p(ζ,y) за никоя променлива ζ, различна от y).

      С оглед на обобщение на използвания по-горе начин за прилагане на субституция нека отбележим, че за всяка променлива ζ имаме равенството p(ζ,σy) = σx/ζ p(x,y).

      Сега ще дадем общата дефиниция за резултат от прилагане на субституция към формула. За целта на всяка субституция σ и всяка формула φ ще съпоставим едно множество от формули, което ще означаваме със σ*φ и чиито елементи именно ще смятаме за резултати от прилагане на σ към φ. Съпоставянето ще извършим чрез следната индуктивна дефиниция:
        1. Ако φ е атомарна формула, то σ*φ = {σφ}.
        2. σ*¬φ = { ¬φ′ | φ′∈σ*φ } за всяка формула φ.
        3c. σ*(φ&ψ) = { (φ′&ψ′) | φ′∈σ*φ, ψ′∈σ*ψ} при всеки избор на формулите φ и ψ.
        3d. σ*(φ∨ψ) = { (φ′∨ψ′) | φ′∈σ*φ, ψ′∈σ*ψ} при всеки избор на формулите φ и ψ.
        4g. σ*∀ξφ = { ∀ζφ′ | ζ∈Ξ \ ∪{ VAR(ση) | η∈FVAR(φ)\{ξ} }, φ′∈σξ/ζ*φ } за всяка формула φ и всяка променлива ξ.
        4e. σ*∃ξφ = { ∃ζφ′ | ζ∈Ξ \ ∪{ VAR(ση) | η∈FVAR(φ)\{ξ} }, φ′∈σξ/ζ*φ } за всяка формула φ и всяка променлива ξ.

      Пример 1. Ако p е двуместен предикатен символ, а σ е произволна субституция, то множеството σ*∃x p(x,y) се състои от формулите от вида  ∃ζ p(ζ,σy), където ζ е променлива, непринадлежаща на VAR(σy). В частност, множеството [y/x]*∃x p(x,y) се състои от формулите от вида  ∃ζ p(ζ,x), където ζ е променлива, различна от x.

      Пример 2. Нека π е едноместен предикатен символ, а ξ е променлива. Тогава множеството ι*∀ξ π(ξ) се състои от всички формули от вида ∀ζ π(ζ), където ζ∈Ξ.

      Пример 3. Нека r е триместен предикатен символ, а f е двуместен функционален символ. Тогава

∀u∃y r(u,y,x)∈[z/x]*∀x∃y r(x,y,z),  ∀x∃u r(x,u,y)∈[z/y]*∀x∃y r(x,y,z),  ∀u∃v r(u,v,f(x,y))∈[z/f(x,y)]*∀x∃y r(x,y,z),  ∀u r(y,z,u)∈[x/y,y/z]*∀z r(x,y,z).

      Чрез индукция, съобразена с дефиницията за безкванторна формула, се доказва, че  σ*φ = { σφ }  за всяка безкванторна формула φ и всяка субституция σ. Използвайки пък индукция, съобразена с дефиницията за произволна формула, виждаме, че за всяка формула φ и всяка субституция σ множеството σ*φ има поне един елемент и че винаги, когато е дефиниран резултат от прилагане на σ към φ без преименуване на свързани променливи, той принадлежи на σ*φ. Виждаме също, че σ*φ има безбройно много елементи, когато формулата φ не е безкванторна.

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

      Твърдение 1. Всяка формула φ принадлежи на съответното множество ι*φ.

      Доказателство. Нека φ е произволна формула. Според твърдение 1 от текста "Прилагане на субституция към атомарна формула" φ е резултат от прилагане на субституцията ι към φ без преименуване на свързани променливи и следователно принадлежи на множеството ι*φ.  □

      Твърдение 2. Когато σ и σ′ са субституции и една формула χ принадлежи на множеството σ*φ за дадена формула φ, за да принадлежи χ и на множеството σ′*φ, необходимо и достатъчно е σ и σ′ да съвпадат върху множеството FVAR(φ).

      Доказателство. Отново прибягваме към индукция, съобразена с дефиницията за формула. За атомарна φ твърдението е вярно и индуктивните стъпки за случаите на отрицание, конюнкция и дизюнкция са прости. От останалите два случая ще разгледаме случая на генерализация, а другият е аналогичен. Нека дадена формула χ принадлежи на σ*∀ξφ за дадена субституция σ, дадена променлива ξ и дадена формула φ, притежаваща доказваното свойство. Ще покажем, че χ принадлежи на σ′*∀ξφ точно за онези субституции σ′, които съвпадат със σ върху множеството FVAR(∀ξφ). Това, че χ принадлежи на σ*∀ξφ, означава, че χ=∀ζφ′ за някоя променлива ζ и някоя формула φ′ от множеството σξ/ζ*φ, като ζ не принадлежи на VAR(ση) за никоя свободна променлива η на φ, различна от ξ. При това положение принадлежност на χ към σ′*∀ξφ ще бъде налице точно тогава, когато φ′ принадлежи на σ′ξ/ζ*φ и ζ не принадлежи на VAR(σ′η) за никоя свободна променлива η на φ, различна от ξ. Направеното индуктивно предположение за формулата φ позволява да заключим, че принадлежността на φ′ към σ′ξ/ζ*φ е равносилна със съвпадане на σξ/ζ*φ и σ′ξ/ζ*φ върху множеството на свободните променливи на φ, а това пък е равносилно със съвпадане на σ и σ′ върху множеството FVAR(∀ξφ). Тъй като при такова съвпадане ще имаме ση=σ′η за всяка свободна променлива η на φ, различна от ξ, с това случаят фактически е разгледан.  □

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

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

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

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

    Теорема за стойността на резултат от прилагане на субституция. Нека S е дадена структура. За всяка формула φ, всяка субституция σ, всяка формула χ от множеството σ*φ и всяка оценка v в S на променливите имаме равенството

χS,v = φS,σS(v).
    Доказателство. Както при доказателствата на предходните твърдения ще използваме индукция по построението на формулата φ. Твърдението е вярно в случаите, когато φ е атомарна формула, и разсъжденията за случаите на отрицание, конюнкция и дизюнкция от индуктивната стъпка са прости. Ще разгледаме подробно само случая на поставяне на квантор. Ще се ограничим с разглеждането за квантор за общност, защото за квантор за съществуване то е аналогично. Нека χ принадлежи на σ*∀ξφ за дадена субституция σ, дадена променлива ξ и дадена формула φ, притежаваща доказваното свойство, и нека v е оценка в S. Да означим с v′ оценката σS(v). Ще покажем, че χS,v = (∀ξφ)S,v′, т.е. че χS,v е най-малката от стойностите на φS,v′[ξ→d] при изменението на d в носителя на S. Това, че χ принадлежи на σ*∀ξφ, означава, че χ=∀ζφ′ за някоя променлива ζ и някоя формула φ′ от множеството σξ/ζ*φ, като ζ не принадлежи на VAR(ση) за никоя свободна променлива η на φ, различна от ξ. При това положение χS,v е най-малката от стойностите на φ′S,v[ζ→d] при изменението на d в носителя на S. От направеното индуктивно предположение за φ получаваме, че φ′S,v[ζ→d] = φS,σS(v[ζ→d]), където σ = σξ/ζ. Нашата цел ще бъде постигната, ако се убедим, че за всяко d от носителя на S оценките σS(v[ζ→d]) и v′[ξ→d] съвпадат в множеството FVAR(φ). Нека d е произволен елемент на носителя на S. Двете оценки съвпадат за променливата ξ, защото стойността на първата от оценките за ξ е (σξ)S,v[ζ→d] = d, колкото е и стойността на втората. Ако пък η е произволна свободна променлива на φ, различна от ξ, то стойността на първата от оценките за η е (ση)S,v[ζ→d] = (ση)S,v[ζ→d], докато стойността на втората за η е v′(η) = (ση)S,v. Имаме обаче равенството (ση)S,v[ζ→d] = (ση)S,v, понеже оценките v[ζ→d] и v съвпадат върху множеството VAR(ση).  □
 

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