Семантика на атомарните формули

СЕМАНТИКА НА АТОМАРНИТЕ ФОРМУЛИ

Нека S=(Σ,D,I) е една структура. И тук атомарните формули в сигнатура Σ ще наричаме за краткост атомарни формули. Ако v е една оценка в S на променливите, то на всяка атомарна формула φ ще съпоставим число от множеството {0,1}, което число ще наричаме стойност на φ в S при оценката v и ще означаваме с φ^S,v. А именно, ако φ е нулместен предикатен символ, то под φ^S,v ще разбираме интерпретацията φ^S на въпросния предикатен символ, а ако φ е думата π(τ₁,…,τ_m), където m е положително цяло число, π e m-местен предикатен символ и τ₁, …, τ_m са термове, то полагаме φ^S,v=π^S(τ₁^S,v, …, τ_m^S,v). Ясно е, че във втория от тези два случая числото φ^S,v е 1 точно тогава, когато наредената m-орка (τ₁^S,v, …, τ_m^S,v) принадлежи на множеството на истинност на предиката π^S.

Пример 1. Ако S е структурата от примера в текста "Сигнатури и структури", а φ, ψ и θ са атомарните формули от пример 1 в текста "Атомарни формули", то за всяка оценка v в S имаме

φ^S,v = positive^S(x^S,v) = positive^S(v(x)),
ψ^S,v = positive^S(difference(difference(x,x),x))^S,v) = positive^S(−v(x)),
θ^S,v = positive^S(difference(x,y)^S,v) = positive^S(v(x)−v(y)). Значи равенствата φ^S,v=1, ψ^S,v=1 и θ^S,v=1 са равносилни съответно на неравенствата v(x)>0, v(x)<0, и v(x)>v(y),.

От лемата за базисна роля на променливите на един терм получаваме аналогично твърдение за атомарни формули:

Лема за базисна роля на променливите на една атомарна формула. Ако две оценки в S съвпадат върху множеството на променливите на дадена атомарна формула φ, то стойностите на φ в S при тези две оценки са равни. В частност, ако φ е затворена, то стойността на φ в S при всяка оценка в S е една и съща.

Доказателство. Нека φ е атомарна формула, а v и v′ са оценки в S, които съвпадат върху множеството VAR(φ). Ще покажем, че φ^S,v = φ^S,v′. Ако φ е нулместен предикатен символ, то равенството е налице, защото в този случай

φ^S,v = φ^S = φ^S,v′. Да предположим сега, че φ има вида π(τ₁,…,τ_m), където m е положително цяло число, π e m-местен предикатен символ и τ₁, …, τ_m са термове. За всяко k от множеството {1,…,m} оценките v и v′ ще съвпадат върху множеството VAR(τ_k), тъй като то се съдържа в VAR(φ), следователно (по лемата за базисна роля на променливите на един терм) ще имаме равенството τ_k^S,v = τ_k^S,v′. Оттук получаваме φ^S,v = π^S(τ₁^S,v, …, τ_m^S,v) = π^S(τ₁^S,v′, …, τ_m^S,v′) = φ^S,v′. _□

Ако φ е затворена атомарна формула, то независещото от избора на оценката v в S число φ^S,v ще наричаме стойност на φ в S. Когато φ е нулместен предикатен символ, тази стойност е интерпретацията φ^S на φ в S. Оттук нататък ще означаваме с φ^S стойността в S на всяка затворена атомарна формула φ. Очевидно е в сила следното твърдение: ако φ е атомарната формула π(τ₁,…,τ_m), където m е положително цяло число, π e m-местен предикатен символ и τ₁, …, τ_m са затворени термове, то φ^S = π^S(τ₁^S,…,τ_m^S).

Когато за дадена атомарна формула φ и дадена оценка v в S имаме равенството φ^S,v = 1, казваме, че φ е вярна в S при оценката v, и пишем S,v ⊨ φ, а за да изразим, че φ не е вярна в S при оценката v, пишем S,v ⊭ φ. В случай, че φ е затворена атомарна формула и имаме равенството φ^S = 1, казваме, че φ е вярна в S, и пишем S ⊨ φ, а за да изразим, че φ не е вярна в S, пишем S ⊭ φ.

Нека φ е атомарна формула. Ако ξ₁, …, ξ_n, където n>0, са две по две различни променливи и q е n-местен предикат в носителя D на S, ще казваме, че φ представя q от ξ₁, …, ξ_n в S, ако за всяка оценка v в S е изпълнено равенството φ^S,v = q(v(ξ₁), …, v(ξ_n)). Ако e е нулместен предикат (т.е. e е някое от числата 0 и 1), ще казваме, че φ представя e в S, ако за всяка оценка v в S е изпълнено равенството φ^S,v = e.

Пример 2. Нека q е едноместният предикат в множеството на целите числа, на който множеството на истинност се състои от отрицателните цели числа. Пример 1 показва, че разгледаната в него атомарна формула ψ представя q от x в структурата S.

Нека φ е атомарната формула π(τ₁,…,τ_m), където m е положително цяло число, π e m-местен предикатен символ, τ₁, …, τ_m са термове. Непосредствено се проверява, че ako ξ₁, …, ξ_n, където n>0, са две по две различни променливи, а g₁, …, g_m са такива n-местни функции в D, че τ_i представя g_i от ξ₁, …, ξ_n в S при i=1,…,m, то φ представя π^S(g₁,…,g_m) от ξ₁, …, ξ_n в S, а ако d₁, …, d_m са такива нулместни функции в D, че τ_i представя d_i в S при i=1,…,m, то φ представя π^S(d₁,…,d_m) в S.

Разбира се, ако пък φ е нулместен предикатен символ, то φ представя нулместния предикат φ^S в S.

Като използваме горните твърдения, убеждаваме се в истинността на следните две, отнасящи се до атомарна изразимост на предикати в S (припомняме, че атомарната изразимост на един предикат в S всъщност означава неговата атомарна изразимост чрез множеството от функции F^S и множеството от предикати P^S):

1. За произволна атомарна формула φ, ако всички нейни променливи са измежду две по две различните променливи ξ₁, …, ξ_n, където n>0, то съществува такъв n-местен предикат q в D, атомарно изразим в S, че φ представя q от ξ₁, …, ξ_n в S. Всяка затворена атомарна формула представя в S някой нулместен предикат, атомарно изразим в S.

2. Ако n е положително цяло число, q е n-местен предикат в D, който е атомарно изразим в S, и ξ₁, …, ξ_n са две по две различни променливи, то съществува такава атомарна формула φ, че всички променливи на φ са измежду променливите ξ₁, …, ξ_n и φ представя q от ξ₁, …, ξ_n в S. За всеки нулместен предикат, който е атомарно изразим в S, съществува затворен атомарна формула, която го представя в S.

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