Заместване на променлива с терм в пренексна формула

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

Нека φ е дадена пренексна формула, ξ е дадена променлива, а τ е даден терм. При известни условия ще дефинираме резултат от заместването на ξ с τ във φ. Условията, при които ще направим това, са следните: а) ξ да е свободна променлива на φ и б) никоя променлива на τ да не е свързана променлива на φ. А именно, нека φ има вида Κ₁…Κ_nθ , където θ е безкванторна формула, n е неотрицателно цяло число и Κ₁, …, Κ_n са квантори по различни помежду си променливи на θ. Тогава, ако са изпълнени условията а) и б), то под резултат от заместването на ξ с τ във φ ще разбираме формулата Κ₁…Κ_nθ' , където θ' е резултатът от прилагането на субституцията [ξ/τ] към безкванторната формула θ. Разбира се, θ' също е безкванторна формула. Променливите, по които са кванторите Κ₁, …, Κ_n, са свободни променливи и на θ', защото благодарение на условието а) те са различни от променливата ξ. Поради това резултатът от заместването на ξ с τ във φ е пак пренексна формула. Ще я означаваме с φ[ξ/τ] (очевидно така дефинираният смисъл на означението не влиза в противоречие с досегашния негов смисъл в случая, когато φ е безкванторна формула).

Ясно е, че винаги, когато когато φ е пренексна формула, Κ е квантор по нейна свободна променлива, ξ е свободна променлива на пренексната формула Κφ , а τ е терм, никоя от променливите на който не е свързана променлива на Κφ , то е дефиниран резултат от заместването на ξ с τ във всяка от двете споменати пренексни формули и резултатът от това заместване в Κφ се получава, като се постави кванторът Κ пред резултата от същото заместване във φ. Това обстоятелство може да се използва за провеждане на индуктивни доказателства във връзка с разглежданото понятие, съобразени с индуктивната дефиниция на понятието пренексна формула. Например така може да се докаже, че винаги, когато φ е пренексна формула, ξ е променлива, τ е терм и са изпълнени условията а) и б) от дадената в началото дефиниция, в сила са следните две твърдения:

Твърдение 1. Множеството на свободните променливи на формулата φ[ξ/τ] се състои от свободните променливи на формулата φ, които са различни от ξ, и от всички променливи на терма τ.

Твърдение 2. За всяка конфигурация (S,v) е в сила равенството

(φ[ξ/τ])^S,v = φ^{S,v[ξ→τ^S,v]}.

И наистина, това, че твърденията 1 и 2 са в сила в случая, когато φ е безкванторна формула, се вижда, като приложим за субституцията [ξ/τ] подходящи твърдения от въпроса „Прилагане на субституция към безкванторна формула“, а именно твърдение 3 от споменатия въпрос и теоремата за стойността на резултата от прилагане на субституция към безкванторна формула (при прилагането на теоремата използваме и обстоятелството, че операторът за присвояване в S, съответен на субституцията [ξ/τ] преобразува оценката v в нейната модификация върху ξ чрез τ^S,v – то е известно от примера във въпроса „Оператори за присвояване, съответни на субституция“). Да предположим сега, че за дадена пренексна формула φ условията а) и б) гарантират верността на твърденията 1 и 2 и че тези условия, изменени по нужния начин, са в сила за дадена формула Κφ , където Κ е квантор по някоя свободна променлива η на φ, т.е. ξ е свободна променлива на формулата Κφ и никоя променлива на терма τ не е свързана променлива на тази формула. Тогава ξ е свободна променлива на формулата φ и е различна от променливата η, а променливите на терма τ също са различни от η и не са свързани променливи на φ. При това положение твърденията 1 и 2 ще бъдат в сила за формулата φ. Целта ни ще бъде да покажем, че, изменени по нужния начин, те са в сила и за формулата Κφ . За твърдението 1 постигаме това чрез веригата от равенства

FVAR((Κφ)[ξ/τ]) = FVAR(Κ(φ[ξ/τ])) = FVAR(φ[ξ/τ]) \ {η} = ((FVAR(φ) \ {ξ}) ∪ VAR(τ)) \ {η} = ((FVAR(φ) \ {ξ}) \ {η}) ∪ (VAR(τ) \ {η}) = (FVAR(Κφ) \ {ξ}) ∪ (VAR(τ) . За да постигнем това и за твърдението 2, ще трябва да разгледаме поотделно случая, когато Κ е квантор за общност, и случая, когато Κ е квантор за съществуване. В първия от тези два случая, означавайки с D носителя на S, имаме ((Κφ)[ξ/τ])^S,v = (Κ(φ[ξ/τ]))^S,v = min{(φ[ξ/τ])^S,v[η→d] | d∈D} = min{φ^{S,v[η→d][ξ→τ^S,v[η→d]]} | d∈D} = min{φ^{S,v[η→d][ξ→τ^S,v]} | d∈D} = min{φ^{S,v[ξ→τ^S,v][η→d]} | d∈D} = (Κφ)^{S,v[ξ→τ^S,v]} (освен семантиката на квантора за общност използваме и обстоятелството, че оценките v[η→d] и v съвпадат върху множеството на променливите на τ). Вторият от случаите се разглежда аналогично.

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