Структури с термално породен носител

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

Ако S е структура, термално представими в S ще наричаме онези елементи на носителя на S, които са стойности в S на затворени термове (разбира се такива елементи има тогава и само тогава, когато съществуват затворени термове). Ще казваме, че една структура S е с термално породен носител, ако всеки елемент на нейния носител е термално представим в S. Важен пример за структури с термално породен носител са ербрановите структури – в такава структура всеки елемент на нейния носител е затворен терм и, както знаем, той е стойност в тази структура на самия себе си.

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

Лема за термално представимите стойности на променливите. Нека S е структура, v е оценка в S на променливите, φ е формула, ξ е променлива и τ е затворен терм, чиято стойност в S е равна на v(ξ). При тези предположения е в сила равенството

φ^S,v = φ[ξ/τ]^S,v.
Доказателство. Имаме равенството φ[ξ/τ]^S,v = φ^S,v', където v' = v[ξ→τ^S,v] = v[ξ→v(ξ)] = v. _□

В структурите с термално породен носител заместването на променливи със затворени термове играе по-съществена семантична роля отколкото в произволни структури. А именно с помощта на горната лема ще докажем следното твърдение.

Семантична достатъчност на заместването със затворени термове в структура с термално породен носител. Нека S е структура с термално породен носител, φ е формула и ξ е променлива. В такъв случай:
а) ако за всеки затворен терм τ формулата φ[ξ/τ] е тъждествено вярна в S, то и формулата φ е тъждествено вярна в S;
б) ако формулата φ е изпълнима в S, то за някой затворен терм τ формулата φ[ξ/τ] също е изпълнима в S.

Доказателство. Да означим с C носителя на структурата S. По предположение всеки елемент на C може да се представи във вида τ^S, където τ е затворен терм. Ако за всеки затворен терм τ формулата φ[ξ/τ] е тъждествено вярна в S, то за коя да е оценка v в S на променливите ще имаме равенствата

φ^S,v=φ[ξ/τ]^S,v=1, когато τ е затворен терм, удовлетворяващ условието τ^S=v(ξ), следователно φ е тъждествено вярна в S. Ако пък формулата φ е изпълнима, то ще имаме равенството φ[ξ/τ]^S,v=1, стига v да е оценка в S на променливите, за която φ^S,v=1, а τ да е затворен терм, за който τ^S=v(ξ). _□

Забележка 1. От свойствата на заместването на променлива с терм е ясно, че при направените по-горе предположенията за φ, ξ и τ свободни променливи на формулата φ[ξ/τ] са точно свободните променливи на φ, различни от ξ. Значи ако свободните променливи на φ са n на брой и са ξ₁, …, ξ_n, а τ₁, …, τ_n са затворени термове, то формулата φ[ξ₁/τ₁]…[ξ_n/τ_n] е затворена.

Следствие 1. Нека S е структура с термално породен носител, а φ е формула, на която свободните променливи са n на брой и са ξ₁, …, ξ_n. Тогава:
а) ако при всеки избор на затворени термове τ₁, …, τ_n формулата φ[ξ₁/τ₁]…[ξ_n/τ_n] е вярна в S, то формулата φ е тъждествено вярна в S;
б) ако формулата φ е изпълнима в S, то при някой избор на затворени термове τ₁, …, τ_n формулата φ[ξ₁/τ₁]…[ξ_n/τ_n] е вярна в S.

Доказателство. При предположението от а) доказваме чрез индукция, при която k се мени от n до 0, че формулата φ[ξ₁/τ₁]…[ξ_k/τ_k] е тъждествено вярна в S при всеки избор на затворени термове τ₁, …, τ_k. При предположението от б) доказваме, че споменатата формула е изпълнима в S при някой избор на затворени термове τ₁, …, τ_k – за целта използваме индукция, при която k се мени от 0 до n. _□

Следствие 2. Нека S е структура с термално породен носител. Тогава:
а) ако всички затворени частни случаи на една формула са верни в S, то тази формула е тъждествено вярна в S;
б) ако една формула е изпълнима в S, то някой затворен частен случай на тази формула е верен в S.

Доказателство. Използваме следствие 1 и обстоятелството, че при предположенията в него за ξ₁, …, ξ_n и φ всички формули от вида φ[ξ₁/τ₁]…[ξ_n/τ_n], където τ₁, …, τ_n са затворени термове, представляват затворени частни случаи на φ. _□

Забележка 2. Следствие 1 и следствие 2 могат да се разглеждат като несъществено различни помежду си, защото при предположенията от следствие 1 всеки затворен частен случай на φ може да се представи във вида φ[ξ₁/τ₁]…[ξ_n/τ_n], където τ₁, …, τ_n са затворени термове. По-долу ще докажем това при допълнителното предположение, че формулата φ е безкванторна (твърдението обаче е вярно и без такова предположение). Нека отбележим, че за произволните (не непременно затворени) частни случаи на една формула положението е доста по-сложно. Например ако буквата p е двуместен предикатен символ, а буквите x, y и z са променливи, то имаме равенството

p(y,x) = p(x,y)[x/z][y/x][z/y] и значи формулата p(y,x) е частен случай на формулата p(x,y), не съществуват обаче термове σ и τ, за които да е в сила равенството p(y,x) = p(x,y)[x/σ][y/τ].

По дефиницията за частен случай на формула, ако една формула ψ е частен случай на дадена формула φ, то ψ има вида φ[η₁/σ₁]…[η_m/σ_m] за някое естествено число m, някои променливи η₁, …, η_m и някои термове σ₁, …, σ_m. С индукция относно m ще покажем, че когато ψ има този вид, а ξ е свободна променлива наφ, всички променливи на терма ξ[η₁/σ₁]…[η_m/σ_m] са свободни променливи на ψ. При m=0 имаме равенствата ψ=φ и ξ[η₁/σ₁]…[η_m/σ_m]=ξ, тъй че твърдението в този случай е тривиално. Да предположим сега, че за дадено естествено число m твърдението е вярно, и да разгледаме формула ψ' от вида φ[η₁/σ₁]…[η_m/σ_m][η_m+1/σ_m+1], където η₁, …, η_m, η_m+1 са някои променливи, а σ₁, …, σ_m, σ_m+1 са някои термове. Тогава ψ'=ψ[η_m+1/σ_m+1], където ψ=φ[η₁/σ₁]…[η_m/σ_m]. Да разгледаме и терм τ' от вида ξ[η₁/σ₁]…[η_m/σ_m][η_m+1/σ_m+1], където ξ е свободна променлива на φ. Имаме равенството τ'=τ[η_m+1/σ_m+1], където τ=ξ[η₁/σ₁]…[η_m/σ_m], а индуктивното предположение позволява да заключим, че всички променливи на терма τ са свободни променливи на формулата ψ. За коя да е променлива η на терма τ' има две възможности: η е променлива на терма σ_m+1, като същевременно η_m+1 е променлива на τ, или η е променлива на τ, различна от η_m+1. Значи е налице някой от следните два случая: η е променлива на терма σ_m+1, като същевременно η_m+1 е свободна променлива на формулата ψ, или η е променлива на ψ, различна от η_m+1. И в двата случая η е свободна променлива на формулата ψ'.

Да предположим сега, че ψ е затворен частен случай на дадена формула φ. Тогава пак ще имаме

ψ=φ[η₁/σ₁]…[η_m/σ_m] за някое естествено число m, някои променливи η₁, …, η_m и някои термове σ₁, …, σ_m, но току-що установеното свойство показва, че за всяка свободна променлива ξ на формулата φ съответният терм ξ[η₁/σ₁]…[η_m/σ_m] е затворен. Нека свободните променливи на φ са n на брой и са ξ₁, …, ξ_n. Да дефинираме затворени термове τ₁, …, τ_n, като положим τ_k = ξ_k[η₁/σ₁]…[η_m/σ_m] при k=1,…,n. Може да се покаже, че при такъв избор на термовете τ₁, …, τ_n е в сила равенството ψ = φ[ξ₁/τ₁]…[ξ_n/τ_n]. За да си спестим някои грижи, ще опишем само как се разглежда случаят, когато формулата φ е безкванторна. Разглеждането му има подготвителна част, в която чрез индукция, съответна на дефиницията за терм, се доказва, че за всеки терм γ, ако променливите му са измежду ξ₁, …, ξ_n, то е в сила равенството γ[η₁/σ₁]…[η_m/σ_m] = γ[ξ₁/τ₁]…[ξ_n/τ_n]. При индуктивната стъпка се използва лесно доказуемият факт, че при всеки избор на r-местен функционален символ f, където r>0, и на термове γ₁, …, γ_r са в сила равенствата f(γ₁,…,γ_r)[η₁/σ₁]…[η_m/σ_m] = f(γ₁[η₁/σ₁]…[η_m/σ_m],…,γ_r[η₁/σ₁]…[η_m/σ_m]),
f(γ₁,…,γ_r)[ξ₁/τ₁]…[ξ_n/τ_n] = f(γ₁[ξ₁/τ₁]…[ξ_n/τ_n],…,γ_r[ξ₁/τ₁]…[ξ_n/τ_n]). Основната част на разглеждането пък използва индукция, съответна на дефиницията за безкванторна формула, и представлява доказателство на твърдението, че ако променливите на една безкванторна формула θ са измежду ξ₁, …, ξ_n, то е в сила равенството θ[η₁/σ₁]…[η_m/σ_m] = θ[ξ₁/τ₁]…[ξ_n/τ_n] (използват се равенства, аналогични на двете, написани във връзка с индуктивната стъпка в подготвителната част). Накрая прилагаме доказаното, като вземем φ в качеството на θ.

Последно изменение във файла: 7 ноември 2005 г.