Частни случаи и варианти на безкванторна формула

Частни случаи и варианти на безкванторна формула

нека F е произволна безкванторна формула; частни случаи на формулата F наричаме всички формули от вида F, където  е произволна субституция;

F е единственият частен случай на F, тъй като F = F за всяка субституция ; напротив, ако F не е затворена, то е ясно, че F има и други частни случаи, дори безброй много;

действително по условие G = F₁, H = G₂  H = (F₁)₂ = F (₁₂), т.е. H е частен случай на F;

в сила е:

1. 
   ако F е тъждествено вярна в S, то всички частни случаи на F са тъждествено вярни в S;
   
2. 
   ако някой частен случай на F е изпълним в S, то F е изпълнима в S;
   

нека F е тъждествено вярна в S; нека  е произволна субституция;

тогава за произволна оценка v в S имаме: (F)^{S, v} = F ^{S, u}, където

u =  ^S (v); имаме F ^{S, u} = 1  (F)^{S, v} = 1; така F е тъждествено вярна в S, т.е. всеки частен случай на F е тъждествено верен в S;

нека F е частен случай на F, който е изпълним в S ( е някаква субституция); нека v е оценка, такава че (F)^{S, v} = 1; имаме

1 = (F)^{S, v} = F ^{S, u}, където u =  ^S (v); така F е изпълнима в S;
обратното твърдение също е вярно, тъй като всяка формула F е частен случай на себе си;

ясно е, че F е затворен частен случай на F 

 (x) е затворен терм за всяко x  VAR (F);
Следствие: нека S е структура, F е безкванторна формула;

в сила е:

1. 
   ако F е тъждествено вярна в S, то всички затворени частни случаи на F са вярни в S;
   
2. 
   ако някой затворен частен случай на F е изпълним в S, то F е изпълнима в S;
   

един затворен частен случай F е верен в S  F е изпълним в S  F е тъждествено верен в S;

например ако S e структурата на семейство Вазови без функционалните символи next и prev, то всички затворени частни случаи на формулата parent (X, Y)  male (Y) са вярни, тъй като от всички деца функционален символ има само Иван Вазов; тази формула, обаче, не е тъждествено вярна, тъй като Иван Вазов е имал и сестри;

формулата parent (X, Y) & female (Y) няма изпълними затворени частни случаи по същата причина като по-горе, въпреки че тя е изпълнима – например, ако v е оценка, такава че

v (X) = Минчо Вазов, v (Y) е някоя от сестрите на Вазов, то

(parent (X, Y) & female (Y))^{S, v} = 1;

например структурата S на семейство Вазови с функционалните символи next и prev има термално породен носител;

нека F е безкванторна формула; в сила е:

1. 
   ако всички затворени частни случаи на F са вярни в S, то F е тъждествено вярна в S;
   
2. 
   ако F е изпълнима в S, то съществува затворен частен случай на F, който е верен в S;
   

нека всеки затворен частен случай на F е верен в S;

нека v е произволна оценка; ще покажем, че F ^{S, v} = 1;

ако F е затворена формула, то тя е затворен частен случай на себе си  F е вярна в S, т.е. F е тъждествено вярна в S;

нека VAR (F) = { x₁, x₂, …, x_n}, n  1; за i = 1, 2, …, n

v (x_i) е елемент на носителя на S, така че съществува затворен

терм T_i, такъв че T_i^S = v (x_i); разглеждаме следната субституция

 = [x₁/T₁, x₂/T₂, …, x_n/T_n]; ясно е, че F е затворен частен случай на F, тъй като  (x) е затворен терм за всяко x  VAR (F);

така (F)^S = 1  (F)^{S, v} = 1  F ^{S, u} = 1, където

тъй като  (x) = x; така F ^{S, v} = F ^{S, u} = 1;

нека F е изпълнима в S; нека v е оценка в S, такава че

F ^{S, v} = 1;

ако F е затворена формула, то тя е затворен частен случай на себе си и тя е търсения верен затворен частен случай;

нека VAR (F) = { x₁, x₂, …, x_n}, n  1; v (x_i) е елемент на носителя

на S, така че съществува затворен терм T_i, така че v (x_i) = T_i^S,

i = 1, 2, …, n; нека  = [x₁/T₁, x₂/T₂, …, x_n/T_n]; тъй като T₁, T₂, …, T_n са затворени термове, то F е затворен частен случай на F;

ще покажем, че (F)^{S, v} = 1; имаме (F)^{S, v} = F ^{S, u}, където u =  ^S (v); ще покажем, че u = v; за i = 1, 2, …, n имаме

u (x_i) = (x_i)^{S, v} = T_i^{S, v} = T_i^S = v (x_i); за x  x_i, u (x) = v (x),

тъй като  (x) = x; така (F)^S = (F)^{S, v} = F ^{S, u} = F ^{S, v} = 1 и F е търсеният изпълним затворен частен случай на F;

пример: F = p (X, Y), G = p (U, V); ясно е, че G = F[X/U, Y/V],

F = G[U/X, V/Y];
релацията “е вариант на” в множеството от всички безкванторни формули е релация на еквивалентност:

рефлексивност: всяка формула F е вариант на себе си: F = F

симетричност: ако G е вариант на F, то F е вариант на G;

транзитивност: ако G е вариант на F и H е вариант на G, то H е вариант на F - това следва от транзитивността на релацията “е частен случай на”;

напротив, ако F е безкванторна формула, която не е затворена, то тя има безброй много варианти, както се вижда от следното

нека VAR (F) = { x₁, x₂, …, x_n}, n  1, x_i  x_j при i  j  { 1, 2, …, n};

нека y₁, y₂, …, y_n са две по две различни променливи;

ако  = [x₁/y₁, x₂/y₂, …, x_n/y_n], то G = F е вариант на F;

Доказателство:
очевидно F е частен случай на G; ще покажем, че G е частен случай на F; да разгледаме субституцията

 = [y₁/x₁, y₂/x₂, …, y_n/x_n] – тя е коректно зададена, тъй като

имаме G = (F) = F ();

за i = 1, 2, …, n имаме: x_i () = (x_i) = y_i = x_i;

така  и  съвпадат върху VAR (F)  F () = F = F;

така G = F и G е вариант на F;
тъй като множеството  е безкрайно, по посочения начин можем да построим безброй много варианти на F; дори можем да построим вариант на F, който не съдържа променливи от дадено крайно подмножество на ;
Твърдение: нека F е безкванторна формула, която не е затворена; нека VAR (F) = { x₁, x₂, …, x_n}, n  1, x_i  x_j при i  j  { 1, 2, …, n};

нека G е произволен вариант на F; тогава

G = F[x₁/y₁, x₂/y₂, …, x_n/y_n], за някои променливи y₁, y₂, …, y_n, които са две по две различни помежду си;

Доказателство: тъй като G е вариант на F, то G = F, F = G за някои субституции  и ; тогава F = G = (F) = F () 

 и  съвпадат върху VAR (F), т.е. x_i () = x_i, i = 1, 2, …, n;

да допуснем, че x_i е съставен терм; тогава x_i () = (x_i) също е съставен терм, тъй като след прилагането на субституцията ,

(x_i) отново ще съдържа функционални символи; така

x_i = (x_i) е съставен терм, което е противоречие – например с факта, че x_i не съдържа леви и десни ограничители;

да допуснем, че x_i е константа; тогава x_i = (x_i) = x_i, което е противоречие, тъй като множествата Ф₀ и  не се пресичат;

така x_i е променлива, нека x_i = y_i  ; тогава

 и [x₁/y₁, x₂/y₂, …, x_n/y_n] съвпадат върху VAR (F) 

G = F = F [x₁/y₁, x₂/y₂, …, x_n/y_n]; ако допуснем, че за някои

i  j  { 1, 2, …, n} имаме y_i = y_j  x_i = x_j 

(x_i) = (x_j)  x_i = x_j, което е противоречие; така y₁, y₂, …, y_n са две по две различни помежду си;