Прилагане на субституция към атомарна формула

ПРИЛАГАНЕ НА СУБСТИТУЦИЯ КЪМ АТОМАРНА ФОРМУЛА

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

Като се използват твърденията 1, 2, 3 от текста "Субституции. Прилагане на субституция към терм", лесно се получават следните аналогични твърдения за прилагането на субституция към атомарна формула.

Твърдение 1. За всяка атомарна формула φ е в сила равенството ιφ=φ.

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

ιφ = π(ιτ₁,…,ιτ_n) = π(τ₁,…,τ_n) = φ. _□

Твърдение 2. Нека σ и σ′ са произволни субституции. Ако φ е произволна атомарна формула, то равенството σφ=σ′φ е изпълнено точно тогава, когато σ и σ′ съвпадат върху множеството VAR(φ).

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

σφ = π(στ₁,…,στ_n), σ′φ = π(σ′τ₁,…,σ′τ_n) е ясно, че равенството σφ=σ′φ е изпълнено точно тогава, когато са изпълнени равенствата στ_i=σ′τ_i, i=1,…,n. Следователно равенството σφ=σ′φ е равносилно със съвпадането на σ и σ′ върху всяко от множествата VAR(τ_i), i=1,…,n, т.е. със съвпадането на σ и σ′ върху обединението на въпросните n множества, което пък е VAR(φ). _□

Следствие. Нека σ е произволна субституция. Ако φ е произволна атомарна формула, то равенството σφ=φ е изпълнено точно тогава, когато σξ=ξ за всяка променлива ξ от множеството VAR(φ). В частност σφ=φ за всяка затворена формула φ.

Доказателство. Прилагаме твърдение 2 при σ′=ι. _□

Твърдение 3. Нека σ е произволна субституция. Тогава за всяка атомарна формула φ множеството VAR(σφ) е обединение на множествата VAR(σξ), където ξ∈VAR(φ).

Доказателство. Твърдението е вярно в случая, когато φ е нулместен предикатен символ, защото обединението на празно семейство от множества е празно. Да предположим сега, че φ=π(τ₁,…,τ_n), където n е положително цяло число, π е n-местен предикатен символ и τ₁, …, τ_n са термове. От равенството σφ = π(στ₁,…,στ_n) получаваме, че VAR(σφ) е обединение на множествата VAR(στ₁), …, VAR(στ_n) и следователно VAR(σφ) е обединение на множествата VAR(σξ), където ξ принадлежи на обединението на множествата VAR(τ₁), …, VAR(τ_n). Последното обединение обаче е точно VAR(φ). _□

Следствие. Ако σ е субституция и φ е атомарна формула, то атомарната формула σφ е затворена точно тогава, когато за всяка променлива ξ на φ съответният терм σξ е затворен.

С помощта на теоремата за стойността на резултат от прилагане на субституция към терм пък се получава нейният аналог за прилагане на субституция към атомарна формула:

Теорема за стойността на резултат от прилагане на субституция към атомарна формула. Ako S е структура със сигнатура Σ, то за всяка субституция σ и всяка атомарна формула φ в тази сигнатура е в сила равенството

(σφ)^S,v=φ^{S,σ^S(v)}.

Доказателство. Нека са дадени структура S, оценка v в нея и субституция σ. Да означим с v′ оценката σ^S(v). Имаме да докажем, че за всяка атомарна формула φ е в сила равенството (σφ)^S,v=φ^S,v′. Ако φ е нулместен предикатен символ, то равенството е тривиално. Да предположим сега, че φ=π(τ₁,…,τ_n), където n е положително цяло число, π е n-местен предикатен символ и τ₁, …, τ_n са термове. Тогава

(σφ)^S,v=π(στ₁,…,στ_n)^S,v=π^S((στ₁)^S,v,…,(στ_n)^S,v)=π^S(τ₁^S,v′,…,τ_n^S,v′)=φ^S,v′. _□

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

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