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

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

нека  е субституция от вида [x/T], където x  , T е терм;

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

в случай че  е приложима към F, който ще бележим с F;

База: ако F е атомарна формула, F = p (T₁, T₂, …, T_n), n  0,

T₁, T₂, …, T_n са термове, то  е приложима към F и резултатът от прилагането на  към F е F = p (T₁, T₂, …, T_n);

ако F = fail или F = true, то  е приложима към F и резултатът от прилагането на  към F е F = F;

Предположение: нека G, F₁, F₂, …, F_n, n > 1, са формули и за тях са дефинирани приложимост на  и резултат от прилагането на ,

в случай че  е приложима;

Стъпка: ако F = G, то  е приложима към F, ако  е приложима към G и в такъв случай F = (G) = (G);

ако F = F₁ & F₂ & … & F_n, то  е приложима към F, ако  е приложима към F₁, F₂, …, F_n и в такъв случай

F = (F₁ & F₂ & … & F_n) = F₁ & F₂ & … & F_n;

ако F = F₁  F₂  …  F_n, то  е приложима към F, ако  е приложима към F₁, F₂, …, F_n и в такъв случай

F = (F₁  F₂  …  F_n) = F₁  F₂  …  F_n;

нека F = y G; ако x  FVAR (F) = FVAR (y G),

то  е приложима към F и F = F;

ако x  FVAR (F) = FVAR (y G), то  е приложима към F, ако  е приложима към G и y  VAR (T); в такъв случай резултатът от прилагането на  към F е F = (y G) = y (G);

нека F = y G ; ако x  FVAR (F) = FVAR (y G),

то  е приложима към F и F = F;

ако x  FVAR (F) = FVAR (y G), то  е приложима към F, ако  е приложима към G и y  VAR (T); в такъв случай резултатът от прилагането на  към F е F = (y G) = y (G);

към F съвпада с по-горе дефинираното понятие;

[Y/X] не е приложима към формулата X p (X, Y), тъй като при заместване на Y с X получаваме X p (X, X) – свободната променлива Y става свързана в новата формула; това е недопустимо – например, възможно е първата формула да е тъждествено вярна в някаква структура, а втората да не е тъждествено вярна в същата структура;

Доказателство: индукция по дефиницията за приложимост;

База: ако F е атомарна формула, то  е приложима към F и

F = F, тъй като  = ; ако F = fail или F = true, то  е приложима към F и F = F (дори за произволна субституция );

Предположение: нека  е приложима към G, F₁, F₂, …, F_n, n > 1 и

G = G, F₁ = F₁, F₂ = F₂, …, F_n = F_n;

Стъпка: ако F = G, то  е приложима към F, тъй като  е приложима към G и F = (G) = (G) = G = F;

ако F = F₁ & F₂ & … & F_n, то  е приложима към F, тъй като  е приложима към F₁, F₂, …, F_n и

F = (F₁ & F₂ & … & F_n) = F₁ & F₂ & … & F_n =

= F₁ & F₂ & … & F_n = F;

съвсем аналогично разсъждаваме в случая F = F₁  F₂  …  F_n;

нека F = y G; ако x  FVAR (F), то  е приложима към F и F = F (дори за произволна субституция );

ако x  FVAR (F), то x  y, тъй като y  FVAR (F); така  е приложима към F, тъй като  е приложима към G и

y  VAR (T) = { x }; така F = (y G) = y (G) = y G = F;

съвсем аналогично разсъждаваме в случая F = y G;

База: ако F е атомарна формула, то BVAR (F) = ;

ако F = true или F = fail, дефинираме BVAR (F) = ;

Предположение: нека F, F₁, …, F_n (n > 1) са формули и BVAR (F),

BVAR (F₁), …, BVAR (F_n) са вече дефинирани;

Стъпка: дефинираме BVAR (F) = BVAR (F),

BVAR (F₁ & F₂ & … F_n) = BVAR (F₁)  BVAR (F₂)  … BVAR (F_n);

BVAR (F₁  F₂  …  F_n) = BVAR (F₁)  BVAR (F₂)  … BVAR (F_n);

BVAR (x F) = BVAR (F)  { x}, BVAR (x F) = BVAR (F)  { x};
ясно е, че ако F е безкванторна формула, то BVAR (F) = ;
Твърдение: нека s = [x/T], F е формула;

ако VAR (T) Ç BVAR (F) = Æ, то s е приложима към F;

Доказателство: индукция по дефиницията за приложимост;

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

ако F = fail или F = true, то очевидно s е приложима към F;

Предположение: нека твърдението е изпълнено за

формулите G, F₁, F₂, …, F_n, n > 1;

Стъпка:

VAR (T) Ç BVAR (G) = Æ è s е приложима към G è

s е приложима към F;

нека F = F₁ & F₂ & … & F_n; имаме VAR (T) Ç BVAR (F) = Æ è

VAR (T) Ç BVAR (F₁) = Æ, VAR (T) Ç BVAR (F₂) = Æ, …,

VAR (T) Ç BVAR (F_n) = Æ è s е приложима към F₁, F₂, …, F_n è s е приложима към F;

аналогично разсъждаваме в случая F = F₁ Ú F₂ Ú … Ú F_n;

нека F = "y G; ако x Ï FVAR (F), то s е приложима към F по дефиниция; нека x Î FVAR (F); имаме VAR (T) Ç BVAR (F) = Æ, т.е.

VAR (T) Ç BVAR ("y G) = Æ è y Ï VAR (T), VAR (T) Ç BVAR (G) = Æ è

s е приложима към G, y Ï VAR (T) è s е приложима към F;

аналогично разсъждаваме в случая F = $y G;
Твърдение: нека F е формула, T е терм; ако x Ï FVAR (F), то

s = [x/T] е приложима към F и Fs = F;

Доказателство:

индукция по дефиницията за приложимост;

База: ако F е атомарна формула, то s е приложима към F и

Fs = F, тъй като s и i съвпадат върху FVAR (F) = VAR (F);

ако F = fail или F = true, то s е приложима към F и Fs = F (дори за произволна субституция s);

Предположение: нека твърдението е изпълнено за

формулите G, F₁, F₂, …, F_n, n > 1;

Стъпка:

s е приложима към G и Gs = G è s е приложима към F и

Fs = (ØG)s = Ø(Gs) = ØG = F;

нека F = F₁ & F₂ & … & F_n; тъй като x Ï FVAR (F), то x Ï FVAR (F₁),

F₁s = F₁, F₂s = F₂, …, F_ns = F_n è s е приложима към F₁, F₂, …, F_n и

Fs = (F₁ & F₂ & … & F_n)s = F₁s & F₂s & … & F_ns =

= F₁ & F₂ & … & F_n = F;

съвсем аналогично разсъждаваме в случая F = F₁ Ú F₂ Ú … Ú F_n;

нека F = "y G; тъй като x Ï FVAR (F), то s е приложима към F и

Fs = F (дори за произволна субституция s);

съвсем аналогично разсъждаваме в случая F = $y G;

Доказателство: индукция по построението;

База: ако F е атомарна формула, то

FVAR (Fs) = VAR (Fs) = = от съответното твърдение за безкванторни формули;

ако F = true или F = fail, то FVAR (Fs) = FVAR (F) = Æ и твърдението очевидно е изпълнено;

Предположение: нека твърдението е изпълнено за формулите

G, F₁, F₂, …, F_n, n > 1;

Стъпка:

= FVAR (Gs) = = , тъй като

FVAR (F) = FVAR (ØG) = FVAR (G);

ако F = F₁ & F₂ & … & F_n, то FVAR (Fs) =

= FVAR (F₁s & F₂s & … & F_ns) = FVAR (F₁s) È FVAR (F₂s) È … È

È FVAR (F_ns) = È È … È

È = = =;

съвсем аналогично се разсъждава, ако F = F₁ Ú F₂ Ú … Ú F_n;

нека F = "y G; ако x Ï FVAR (F), то Fs = F è FVAR (Fs) = FVAR (F); от друга страна = , тъй като s (z) = z

за всяко z ¹ x è = FVAR (F) = FVAR (Fs);

нека x Î FVAR (F); тъй като s е приложима към F, то y Ï VAR (T) и s е приложима към G; също, тъй като y Ï FVAR (F), то x ¹ y;

имаме FVAR (Fs) = FVAR (("y G)s) = FVAR ("y (Gs)) =

= FVAR (Gs) \ { y } = \ { y } ;

от друга страна = =

= \ VAR (s (y)) = \ { y }, тъй като

y ¹ x è s (y) = y; така FVAR (Fs) = ;

съвсем аналогично разсъждаваме в случая F = $y G;

Доказателство: индукция по построението на F за произволна субституция от вида s = [x/T];

База: ако F е атомарна формула, то (Fs)^{S, v} = F ^{S, u} от съответното твърдение за безкванторни формули; ако F = true или F = fail,

то Fs = F и F ^{S, v} = F ^{S, u}, тъй като верността на F не зависи от оценките;

Предположение: нека твърдението е изпълнено за формулите

G, F₁, F₂, …, F_n, n > 1;

Стъпка: ако F = ØG, то (Fs)^{S, v} = ((ØG)s)^{S, v} = (Ø(Gs))^{S, v} = 1 - (Gs)^{S, v} =

= 1 - G ^{S, u} = (ØG)^{S, u} = F ^{S, u};

ако F = F₁ & F₂ & … & F_n, то (Fs)^{S, v} = ((F₁ & F₂ & … & F_n)s)^{S, v} =

= (F₁s & F₂s & … & F_ns)^{S, v} = min { (F₁s)^{S, v}, (F₂s)^{S, v}, …,(F_ns)^{S, v}} =

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

съвсем аналогично се разсъждава, ако F = F₁ Ú F₂ Ú … Ú F_n;

нека F = "y G; ако x Ï FVAR (F), то Fs = F è (Fs)^{S, v} = F ^{S, v}; от друга страна v и u съвпадат върху FVAR (F), тъй като x Ï FVAR (F) è

F ^{S, v} = F ^{S, u}; така (Fs)^{S, v} = F ^{S, u}; нека x Î FVAR (F); тъй като s е приложима към F, то y Ï VAR (T) и s е приложима към G;

имаме (Fs)^{S, v} = (("y G)s) ^{S, v} = ("y (Gs)) ^{S, v} = min { (Gs)^{S, v[y : d]}|d Î D } = min { |d Î D } = min { |d Î D }, тъй като

y Ï VAR (T) è v[y : d] и v съвпадат върху VAR (T) è T ^{S, v[y :d]} = T ^{S, v};

от друга страна F ^{S, u} = ("y G) ^{S, u} = min { G^{S, u[y : d]}|d Î D } =

= min { |d Î D }; имаме x Î FVAR (F) è x ¹ y è

v[y : d][x : T ^{S, v}] = v[x : T ^{S, v}][y : d]; така (Fs)^{S, v} = F ^{S, u};
като следствие получаваме, че ако F е формула, която е тъждествено вярна в структура S и s е субституция, приложима към F, то Fs също е тъждествено вярна в S;
нека F и G са формули; казваме, че от F следва G,

ако от F ^{S, v} = 1 (S – структура, v – оценка на променливите в S) следва G ^{S, v} = 1; бележим F G;

ясно е, че F G ó F à G е тъждествено вярна ó F ^{S, v} £ G^{S, v} за всяка структура S и оценка v на променливите в S; в частност е рефлексивна и транзитивна релация в множеството от всички формули; при това F G и G F ó F º G;
Твърдение: нека s = [x/T], s е приложима към F;

тогава "x F Fs $x F;

Доказателство: нека S е структура с носител D, v е оценка на променливите в S; имаме ("x F)^{S, v} = min { F ^{S, v[x : d]}|d Î D },

(Fs)^{S, v} = , ($x F)^{S, v} = max { F ^{S, v[x : d]}|d Î D }; така

("x F)^{S, v} £ (Fs)^{S, v} £ ($x F)^{S, v} è "x F Fs $x F;