Previous  Next  Contents
 

 

ПРОМЕНЛИВИ НА ТЕРМ, СВОБОДНИ И СВЪРЗАНИ ПРОМЕНЛИВИ НА ФОРМУЛА

      Под термове и формули ще разбираме термове и формули при някоя дадена сигнатура Σ.

      За всеки терм T ще дефинираме индуктивно едно множество VAR(T), чиито елементи ще наричаме променливи на T. Дефиницията е следната: ако T е константа, то VAR(T) = ∅, ако T е променлива, то VAR(T) = {T}, а ако

T = φ(T1,…,Тn),
където n е положително цяло число, φ е n-местен функционален символ и T1, …, Тn са термове, то
VAR(T) = VAR(T1) ∪ … ∪ VAR(Тn).
      Така изказаната дефиниция определя еднозначно множеството VAR(T) за произволен терм T благодарение на еднозначното прочитане на термовете.

      Пример 1. Ако Σ е сигнатурата от пример 1 от въпроса "Сигнатури и структури", то имаме равенството VAR(a(s(b(X))))={X}, а множеството на променливите на терма b(s(a(a(e)))) е празно.

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

      Като си послужим с индукция, съобразена с дефиницията за терм, веднага се убеждаваме, че множеството на променливите на кой да е терм е крайно подмножество на множеството Ξ на всички променливи. Значението на това крайно подмножество от гледна точка на семантиката на термовете проличава от следното твърдение, показващо, че при дадена конфигурация (S,v) и даден терм T стойността TS,v не зависи от това как е дефинирана оценката v за променливите извън множеството VAR(T).

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

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

T = φ(T1,…,Тn),
където n е положително цяло число, φ е n-местен функционален символ и T1, …, Тn са термове, притежаващи доказваното свойство. Тогава и термът T ще има това свойство, защото ако две оценки v и v' в S на променливите съвпадат върху множеството VAR(T), то при i=1,…,n те ще съвпадат също върху подмножеството VAR(Ti) на VAR(T) и следователно ще имаме равенството TiS,v = TiS,v', а оттук получаваме, че
TS,v = φS(T1S,v,…,ТnS,v<) = φS(T1S,v',…,ТnS,v') = TS,v'. □

      За произволна формула F подобна роля играе едно множество FVAR(F), чиито елементи ще наричаме свободни променливи на F (английският термин е "free variables of F"). Дефиницията на това множество е също индуктивна и го определя еднозначно благодарение на еднозначното прочитане на формулите. Тя се състои от следните точки (отбелязваме, че последната от тях дава възможност една променлива, използвана при построяването на дадена формула, да не е свободна променлива на тази формула):

          0. Ако F е нулместен предикатен символ или е някоя от формулите true и fail, то FVAR(F) = ∅, а ако

F = π(T1,…,Тn),
където n е положително цяло число, π е n-местен предикатен символ и T1, …, Тn са термове, то
FVAR(F) = VAR(T1) ∪ … ∪ VAR(Тn).
          1. Ако F = ¬ F0 за някоя формула F0, то
FVAR(F) = FVAR(F0).
          2. Ако F = F1 & … & Fn или F = F1 ∨ … ∨ Fn, където n е цяло число, по-голямо от 1, и F1, …, Fn са формули, то
FVAR(F) = FVAR(F1) ∪ … ∪ FVAR(Fn).
          3. Ако F = ∀ξ F0 или F = ∃ξ F0 за някоя променлива ξ и някоя формула F0, то
FVAR(F) = FVAR(F0) \ {ξ}.

      Пример 2. Ако Σ е сигнатурата от пример 2 от въпроса "Сигнатури и структури", то имаме равенствата

FVAR((not(belongs(X,A));belongs(X,union(A,B)))) = {X,A,B},
FVAR((X,belongs(X,singleton(X)))) = ∅.

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

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

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

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

F0S,v[ξ→d] = F0S,v'[ξ→d].
Оттук, вземайки пред вид дефиницията за стойност на генерализация в дадена конфигурация, веднага получаваме желаното равенство FS,v=FS,v'. □

      С оглед на някои въпроси, които ще разглеждаме по-нататък, подходящо е да се дефинира за всяка формула F и едно друго множество BVAR(F), чиито елементи ще наричаме свързани променливи на F (английският термин е "bound variables of F"). Дефиницията е пак индуктивна и се състои от следните точки:

          0. Ако F е атомарна формула или е някоя от формулите true и fail, то

BVAR(F)=∅;
          1. Ако F = ¬ F0 за някоя формула F0, то
BVAR(F) = BVAR(F0);
          2. Ако F = F1 & … & Fn или F = F1 ∨ … ∨ Fn, където n е цяло число, по-голямо от 1, и F1, …, Fn са формули, то
BVAR(F) = BVAR(F1) ∪ … ∪ BVAR(Fn);
          3. Ако F = ∀ξ F0 или F = ∃ξ F0 за някоя променлива ξ и някоя формула F0, то
BVAR(F) = BVAR(F0) ∪ {ξ}.
Тази дефиниция еднозначно определя множеството BVAR(F) за всяка формула F и то винаги е крайно множество от променливи. Обединението на множествата FVAR(F) и BVAR(F) ще означаваме с VAR(F), а елементите му ще наричаме променливи на F. И множествата BVAR(F) и VAR(F) остават същите, когато разглеждаме една формула F при сигнатура Σ като формула при някоя друга сигнатура, съдържаща Σ.

      Забележка 1. Може да се случи една променлива да бъде едновременно свободна и свързана променлива на дадена формула. Например ако π е едноместен предикатен символ на сигнатурата Σ, а ξ е променлива, то ξ е както свободна, така и свързана променлива на формулата

π(ξ) & ∃ξ ¬ π(ξ).
Тази формула е вярна в дадена конфигурация (S,v) точно тогава, когато предикатът πS има стойност 1 за елемента v(ξ) на носителя на S, но има стойност 0 за някой друг елемент на въпросния носител. Не е трудно да се посочи формула със същото свойство, за която множеството на свободните променливи и множеството на свързаните променливи да имат празно сечение. Такава е например формулата
π(ξ) & ∃η ¬ π(η),
където π и ξ са както преди малко, а η е променлива различна от ξ. За да се избегнат евентуални технически усложнения, обикновено се предпочита да се работи с формули F, за които FVAR(F) ∩ BVAR(F) = ∅.

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

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

 

Последно изменение: 28.02.2005 г.
 
 Previous  Next  Contents