Съдържание 
 

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

    Нека φ е дадена пренексна формула, ξ е дадена променлива, а τ е даден терм. При известни условия ще дефинираме резултат от заместването на ξ с τ във φ. Условията, при които ще направим това, са следните: а) ξ да е свободна променлива на φ и б)  никоя променлива на τ да не е свързана променлива на φ. А именно, нека φ има вида
Κ1Κnθ ,
където θ е безкванторна формула, n е неотрицателно цяло число и Κ1, , Κn са квантори по различни помежду си променливи на θ. Тогава, ако са изпълнени условията а) и б), то под резултат от заместването на ξ с τ във φ ще разбираме формулата
Κ1Κnθ' ,
където θ' е резултатът от прилагането на субституцията [ξ/τ] към безкванторната формула θ. Разбира се, θ' също е безкванторна формула. Променливите, по които са кванторите Κ1, , Κ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,vd] | dD} = min{φS,vd][ξτS,vd]] | dD} = min{φS,vd][ξτS,v] | dD} = min{φS,vτS,v][ηd] | dD} = (Κφ)S,vτS,v]
(освен семантиката на квантора за общност използваме и обстоятелството, че оценките  vd и v съвпадат върху множеството на променливите на τ). Вторият от случаите се разглежда аналогично.

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