Променливи на терм и на атомарна формула

ПРОМЕНЛИВИ НА ТЕРМ И НА АТОМАРНА ФОРМУЛА

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

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

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

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

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

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

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

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

τ = ω(τ₁,…,τ_n), където n е положително цяло число, ω е n-местен функционален символ и τ₁, …, τ_n са термове, притежаващи доказваното свойство. Тогава и термът τ ще има това свойство, защото ако две оценки v и v' в S на променливите съвпадат върху множеството VAR(τ), то при i=1,…,n те ще съвпадат също върху подмножеството VAR(τ_i) на VAR(τ) и следователно ще имаме равенството τ_i^S^,v = τ_i^S^,v', а оттук получаваме, че τ^S^,v = ω^S(τ₁^S,v,…,T_n^S^,v<) = ω^S(τ₁^S,v',…,T_n^S^,v') = τ^S^,v'. _□

И за произволна атомарна формула φ ще дефинираме множество VAR(φ), чиито елементи ще наричаме променливи на φ. А именно, ако φ е нулместен предикатен символ, то полагаме VAR(φ) = ∅, а ако

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

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

VAR((belongs(X,union(A,B))) = {X,A,B}.

Отбелязаните по-горе свойства на множеството на променливите на един терм се пренасят веднага и за множеството на променливите на една атомарна формула. Ако Σ′ е коя да е сигнатура, съдържаща Σ, то за всяка атомарна формула φ при сигнатура Σ множеството на променливите на φ ще остане същото и тогава, когато разглеждаме φ като формула при сигнатура Σ′. Множеството на променливите на коя да е атомарна формула е крайно подмножество на множеството Ξ на всички променливи и е в сила следното твърдение.

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

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