Преди известно време дадохме дефиниция за резултат от прилагането на субституция към терм и към атомарна формула. Естествено би било да разширим дадената дефиниция и да кажем какво ще разбираме под резултат от прилагане на една субституция към произволна формула. Това обаче е свързано с известни трудности поради особената роля на свързаните променливи в онези формули, които имат такива променливи. Една разумна дефиниция на резултата от прилагането на една субституция към дадена формула, съдържаща свързани променливи, би трябвало преди всичко да се погрижи на кои места във формулата променливите да се заместят със съответните им термове и на кои да останат както са си били. Има обаче и по-съществена трудност. Дефиницията би трябвало да отчете също възможността на едно неприятно явление, наречено колизия на променливите. То се състои в следното: една свободна променлива на дадена формула да има такова свободно участие в нея, което е в областта на действие на квантор относно друга променлива, а тя пък да участва в терма, съответен на първата при разглежданата субституция. Например нека една формула има вида $Y p(X,Y), където p е двуместен предикатен символ, а X и Y са различни променливи, и нека [X/Y] е субституцията, която искаме да приложим. Формалното заместване на X с Y би дало формулата $Y p(Y,Y), но не би било разумно да приемем, че тя е резултатът от прилагането на разглежданата субституция към дадената формула (поне поради това, че формулата $Y p(Y,Y) е затворена, а би било естествено променливите на терма, с който заместваме една свободна променлива на дадена формула, да останат свободни и в резултата от заместването).

    Заради отбелязаните две трудности (преди всичко заради втората от тях) ние засега ще се въздържим от дефиниране на резултат от прилагането на субституция към произволна формула и ще дефинираме въпросния резултат само за безкванторни формули. В този случай не възникват никакви трудности и резултатът от прилагането Fs на една субституция s към една неатомарна безкванторна формула F е безкванторна формула, която се дефинира по следния индуктивен начин:
    1. Ако F е празна конюнкция или празна дизюнкция, полагаме Fs=F.
    2. При всеки избор на цяло число n, по-голямо от 1, и на безкванторни формули F₁, F₂, ..., F_n полагаме

    Твърденията, които доказахме по-рано за прилагането на субституция към терм и към атомарна формула (включително и твърдението за стойността на резултата от прилагането на субституция и твърденията, свързани с умножение на субституции), веднага се разпространяват и за прилагането на субституция към безкванторна формула (доказателствата им за този случай са чрез индукция, съобразена с горната дефиниция). А именно в сила е следното:

    Твърдение 1. Ако F е безкванторна формула, то резултатите от прилагането на две субституции s и sў към F съвпадат точно тогава, когато s и sў съвпадат върху множеството на променливите на F.

    Твърдение 2. За произволна безкванторна формула F е в сила равенството Fi=F.

    Следствие от твърдения 1 и 2 (доказва се и директно). Ако F е затворена безкванторна формула, то за всяка субституция s е в сила равенството Fs=F.

    Твърдение 3. Ако F е безкванторна формула, то за всяка субституция s е изпълнено равенството

    Следствие. Ако F е безкванторна формула, а s е субституция, то формулата Fs е затворена точно тогава, когато термът Xs е затворен за всяка променлива X от множеството VAR(F).

    Теорема за стойността на резултата от прилагане на субституция към безкванторна формула. Нека са дадени една субституция s,  една структура  S и една оценка v в S. Нека s_S(v)=vў и нека F е безкванторна формула. Тогава е в сила равенството (Fs)^S,v=F^S,vў.

    Прилагане на произведение на две субституции към безкванторни формули. Нека F е произволна безкванторна формула. Тогава за всеки две субституции s₁ и s₂ е в сила равенството

    Ако F е коя да е безкванторна формула, приемаме (аналогично на това, което направихме за термовете и атомарните формули), че

    Когато F е една безкванторна формула, формулите от вида Fs, отговарящи на всевъзможните субституции s, се наричат частни случаи на F. От отбелязаните по-горе свойства на прилагането на субституция към безкванторна формула се вижда, че всяка безкванторна формула е частен случай на себе си, при това единствен, когато тя е затворена, и че частните случаи на частните случаи на една безкванторна формула F винаги са частни случаи и на F.

    Следното свойство ще бъде използвано многократно в по-нататъшната ни работа.

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

    Доказателство. Нека F е една безкванторна формула, s е една субституция и S е една структура. Ако F е тъждествено вярна в S , то за произволна оценка v в S при vў=s_S(v) ще имаме (Fs)^S,v=F^S,vў=1. Ако пък Fs е изпълнима в S, можем да вземем оценка v в S, за която (Fs)^S,v=1, и, дефинирайки оценката vў както по-горе, получаваме, че F^S,vў=(Fs)^S,v=1.  _ї

    Следствие. Ако една безкванторна формула е тъждествено вярна, то всички частни случаи на формулата също са тъждествено верни, а ако някой частен случай на една безкванторна формула е изпълним, то и самата формула е изпълнима.
 

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

Previous  Next  Contents