Свободни променливи на формула

СВОБОДНИ ПРОМЕНЛИВИ НА ФОРМУЛА

Под формули ще разбираме формули при някоя дадена сигнатура Σ. На всяка формула φ ще съпоставим едно множество от променливи FVAR(φ), чиито елементи ще наричаме свободни променливи на φ (английският термин е „free variables of φ“). Ще направим това, като приемем, че FVAR(φ) = VAR(φ) за всяка атомарна формула φ и при всеки избор на формули φ и ψ и на променлива ξ са в сила равенствата FVAR(¬φ) = FVAR(φ),
FVAR(φ & ψ) = FVAR(φ ∨ ψ) = FVAR(φ) ∪ FVAR(ψ),
FVAR(∀ξφ) = FVAR(∃ξφ) = FVAR(φ) \ {ξ} Тазииндуктивна дефиниция е коректна благодарение на еднозначния прочит на формулите. Тя дава възможност една променлива да не е свободна променлива на дадена формула, въпреки че е използвана при нейното построяване.

Пример. Да разгледаме формулите

∃Z m(Y,Z,X) ,
¬ m(X,X,X) & ∀Y ∀Z( ¬ m(Y,Z,X) ∨ (m(Y,Y,Y) ∨ m(Z,Z,Z))) , където m е триместен предикатен символ. При първата от тях множеството на свободните променливи се състои от променливите X и Y, а при втората то има като единствен свой елемент променливата X. И при двете формули има променливи, които са използвани при построяването на формулата, но не са нейни свободни променливи (при първата това е променливата Z, а при втората такива са Y и Z).

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

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

Лема за базисна роля на свободните променливи на една формула. Нека S е дадена структура. Тогава за произволна формула φ имаме, че ако две оценки v и v' в S на променливите съвпадат върху множеството FVAR(φ), то е в сила равенството φ^S^,v = φ^S^,v'.

Доказателство. Използваме индукция, съобразена с дефиницията за формула. Ако φ е атомарна формула, то тя притежава доказваното свойство по лемата за базисна роля на променливите на една атомарна формула. Доказателството, че това свойство се запазва при образуване на отрицание, конюнкция или дизюнкция се свежда до лесна проверка. Малко повече грижи изискват случаите на генерализация и на екзистенциализация. Ще извършим индуктивната стъпка за първия от тях, а за втория разсъжденията са аналогични. Нека φ е формула, която има доказваното свойство, а ξ е произволна променлива. Ще покажем, че и формулата ∀ξφ го притежава. За целта да предположим, че две оценки v и v' в S на променливите съвпадат върху множеството FVAR(∀ξφ). Тогава при всеки избор на елемент d на носителя на S двете модифицирани оценки v[ξ→d] и v'[ξ→d] ще съвпадат върху множеството FVAR(φ). Това е така, защото те очевидно съвпадат върху променливата ξ, а пък всяка свободна променлива на φ, различна от ξ, е свободна променлива и на ∀ξφ, като за нея имаме съвпадане на двете модифицирани оценки съответно с v и с v'. Следователно за всеки елемент d на носителя на S имаме равенството

φ^S,v[ξ→d] = φ^S,v'[ξ→d]. Оттук, вземайки пред вид дефиницията за стойност на генерализация в дадена конфигурация, веднага получаваме желаното равенство (∀ξφ)^S^,v = (∀ξφ)^S^,v'. _□

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

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