Оператори за присвояване, съответни на субституции

Оператори за присвояване, съответни на субституции

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

например, ако  = [x₁/T₁, x₂/T₂, …, x_n/T_n], то (^S (v)) (x_i) = T_i ^{S, v},

ако  = [x₀/T₀] и v е оценка, то ^S (v) = v[x₀: T₀ ^{S, v}];

действително, (^S (v)) (x₀) = T₀ ^{S, v}, (^S (v)) (x) = v (x) за всяко x  x₀;
Теорема: нека S е структура,  е субституция, v е оценка на променливите в S; ако E е терм или безкванторна формула, то

(E)^{S, v} = E ^{S, u}, където u = ^S (v);

Доказателство: първо да разгледаме случая когато E е терм;

провеждаме индукция по постронието на E;

База: ако E е константа, то Е = Е  (Е)^{S, v} = E ^{S, v} = E ^{S, u};

ако E  , то E =  (E) и (E)^{S, v} =  (E)^{S, v}; от друга страна

E ^{S, u} = u (E) =  (E)^{S, v} по дефиницията на оператора за присвояване; така (E)^{S, v} = E ^{S, u};

Предположение: нека E = f (T₁, T₂, …, T_n) и твърдението е изпълнено за термовете T₁, T₂, …, T_n;

Стъпка: имаме E = f (T₁, T₂, …, T_n) 

(E)^{S, v} = f (T₁, T₂, …, T_n)^{S, v} = f ^S ( (T₁)^{S, v}, (T₂)^{S, v}, …, (T_n)^{S, v});

от индукционното предположение за термовете T₁, T₂, …, T_n и получаваме, че (T₁)^{S, v} = T₁^{S, u}, (T₂)^{S, v} = T₂^{S, u}, …, (T_n)^{S, v} = T_n^{S, u} 

(E)^{S, v} = f ^S (T₁^{S, u}, T₂ ^{S, u}, …, T_n^{S, u}) = E ^{S, u};

сега да разгледаме случая когато E е безкванторна формула;

провеждаме индукция по построението на E;

База: нека E = p (T₁, T₂, …, T_n); тогава E = p (T₁, T₂, …, T_n) 

(E)^{S, v} = p (T₁, T₂, …, T_n)^{S, v} = p ^S ( (T₁)^{S, v}, (T₂)^{S, v}, …, (T_n)^{S, v});

тъй като T₁, T₂, …, T_n са термове, от по-горе получаваме:

(T₁)^{S, v} = T₁^{S, u}, (T₂)^{S, v} = T₂^{S, u}, …, (T_n)^{S, v} = T_n^{S, u} 

(E)^{S, v} = p ^S (T₁^{S, u}, T₂ ^{S, u}, …, T_n^{S, u}) = E ^{S, u};

ако E  П₀, то E = E  (E)^{S, v} = E ^{S, v} = E ^S = E ^{S, u};

ако E = true, то E = E  (E)^{S, v} = E ^{S, v} = 1 = E ^{S, u};

ако E = fail, то E = E  (E)^{S, v} = E ^{S, v} = 0 = E ^{S, u};

Предположение: нека твърдението е изпълнено за безкванторните формули G, F₁, F₂, …, F_n (n > 2);

Стъпка:

от индукционното предположение (G)^{S, v} = G^{S, u};

така (E)^{S, v} = 1 – G^{S, u} = (G)^{S, u} = E ^{S, u};

ако E = F₁ & F₂ & … & F_n, то E = F₁ & F₂ & … & F_n 

(E)^{S, v} = (F₁ & F₂ & … & F_n)^{S, v} = min { (F₁)^{S, v}, (F₂)^{S, v}, …,(F_n)^{S, v}};

от индукционното предположение (F₁)^{S, v} = F₁^{S, u},

(F₂)^{S, v} = F₂^{S, u}, …, (F_n)^{S, v} = F_n^{S, u}; така (E)^{S, v} =

= min { F₁^{S, u}, F₂^{S, u}, …,F_n^{S, u}} = (F₁ & F₂ & … & F_n)^{S, u} = E ^{S, u};

ако E = F₁  F₂  …  F_n, то E = F₁  F₂  …  F_n 

(E)^{S, v} = (F₁  F₂  …  F_n)^{S, v} = max { (F₁)^{S, v}, (F₂)^{S, v}, …,(F_n)^{S, v}};

от индукционното предположение (F₁)^{S, v} = F₁^{S, u},

(F₂)^{S, v} = F₂^{S, u}, …, (F_n)^{S, v} = F_n^{S, u}; така (E)^{S, v} =

= max { F₁^{S, u}, F₂^{S, u}, …,F_n^{S, u}} = (F₁  F₂  …  F_n)^{S, u} = E ^{S, u};