Преименуване на свързани променливи

Привеждане на формули в пренексен вид

казваме, че една формула е в пренексен вид, ако тя е получена от безкванторна формула с добавяне на няколко (възможно 0) квантори по различни помежду си свободни променливи;

ще покажем, че всяка формула е еквивалентна на някоя формула в пренексен вид, която има същите свободни променливи;

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

x F  x F;

x F  x F;
Твърдение: нека F₁, F₂, …, F_n са произволни формули;

нека i  { 1, 2, …, n }, x  FVAR (F_j) за всяко j  i  { 1, 2, …, n };

тогава F₁ & … & F_i-1 & x F_i & F_i+1 & … & F_n  x (F₁ & F₂ & … & F_n);

Доказателство: нека S е структура с носител D, v е оценка на

променливите в S; имаме (F₁ & … & F_i-1 & x F_i & F_i+1 & … & F_n)^{S, v} =

= min { F₁^{S, v}, …, F_i-1^{S, v}, (x F_i)^{S, v}, F_i+1 ^{S, v}, …, F_n ^{S, v} } =

= min { F₁^{S, v}, …, F_i-1^{S, v}, min { F_i ^{S, v[x : d]}|d  D }, F_i+1 ^{S, v}, …, F_n ^{S, v} };

имаме (F₁ & … & F_i-1 & x F_i & F_i+1 & … & F_n)^{S, v} = 1 

F₁ ^{S, v} = 1, …, F_i-1 ^{S, v} = 1, min { F_i ^{S, v[x : d]}|d  D } = 1, F_i+1 ^{S, v} = 1, …,

F_n ^{S, v} = 1  F₁ ^{S, v} = 1, …, F_i-1 ^{S, v} = 1, F_i+1 ^{S, v} = 1, …, F_n ^{S, v} = 1

и за всяко d  D, F_i ^{S, v[x : d]} = 1;

от друга страна x (F₁ & F₂ & … & F_n) ^{S, v} =

= min { (F₁ & F₂ & … & F_n) ^{S, v[x : d]} |d  D } =

= min { min { F₁^{S, v[x : d]}, F₂^{S, v[x : d]}, …, F_n ^{S, v[x : d]} } |d  D };

имаме x (F₁ & F₂ & … & F_n) ^{S, v} = 1  за всяко d  D,

min { F₁^{S, v[x : d]}, F₂^{S, v[x : d]}, …, F_n ^{S, v[x : d]} } = 1  за всяко d  D,

F₁^{S, v[x : d]} = 1, F₂^{S, v[x : d]} = 1, …, F_n ^{S, v[x : d]} = 1  за всяко d  D,

F₁ ^{S, v} = 1, …, F_i-1 ^{S, v} = 1, F_i ^{S, v[x : d]} = 1, F_i+1 ^{S, v} = 1, …, F_n ^{S, v} = 1; използвали сме, че тъй като v и v[x : d] съвпадат върху FVAR (F_j), то F_j ^{S, v} = F_j ^{S, v[x : d]} за всяко j  i  { 1, 2, …, n }, d  D;

така (F₁ & … & F_i-1 & x F_i & F_i+1 & … & F_n)^{S, v} = 1 

x (F₁ & F₂ & … & F_n) ^{S, v} = 1;

нека i  { 1, 2, …, n }, x  FVAR (F_j) за всяко j  i  { 1, 2, …, n };

тогава F₁  …  F_i-1  x F_i  F_i+1  …  F_n  x (F₁  F₂  …  F_n);

Доказателство: нека S е структура с носител D, v е оценка на

променливите в S; имаме (F₁  …  F_i-1  x F_i  F_i+1  …  F_n)^{S, v} =

= max { F₁^{S, v}, …, F_i-1^{S, v}, (x F_i)^{S, v}, F_i+1 ^{S, v}, …, F_n ^{S, v} } =

= max { F₁^{S, v}, …, F_i-1^{S, v}, min { F_i ^{S, v[x : d]}|d  D }, F_i+1 ^{S, v}, …, F_n ^{S, v} };

имаме (F₁  …  F_i-1  x F_i  F_i+1  …  F_n)^{S, v} = 0 

F₁ ^{S, v} = 0, …, F_i-1 ^{S, v} = 0, min { F_i ^{S, v[x : d]}|d  D } = 0, F_i+1 ^{S, v} = 0, …,

F_n ^{S, v} = 0  F₁ ^{S, v} = 0, …, F_i-1 ^{S, v} = 0, F_i+1 ^{S, v} = 0, …, F_n ^{S, v} = 0

и съществува d  D, такова че F_i ^{S, v[x : d]} = 0;

от друга страна x (F₁  F₂  …  F_n) ^{S, v} =

= min { (F₁  F₂  …  F_n) ^{S, v[x : d]} |d  D } =

= min { max { F₁^{S, v[x : d]}, F₂^{S, v[x : d]}, …, F_n ^{S, v[x : d]} } |d  D };

имаме x (F₁  F₂  …  F_n) ^{S, v} = 0  съществува d  D, такова че

max { F₁^{S, v[x : d]}, F₂^{S, v[x : d]}, …, F_n ^{S, v[x : d]} } = 0  съществува d  D, такова че F₁^{S, v[x : d]} = 0, F₂^{S, v[x : d]} = 0, …, F_n ^{S, v[x : d]} = 0  съществува d  D, такова че F₁ ^{S, v} = 0, …, F_i-1 ^{S, v} = 0, F_i ^{S, v[x : d]} = 0, F_i+1 ^{S, v} = 0, …, F_n ^{S, v} = 0; използвали сме, че тъй като v и v[x : d] съвпадат върху FVAR (F_j), то F_j ^{S, v} = F_j ^{S, v[x : d]} за всяко j  i  { 1, 2, …, n }, d  D;

така (F₁  …  F_i-1  x F_i  F_i+1  …  F_n)^{S, v} = 1 

x (F₁  F₂  …  F_n) ^{S, v} = 1;

F₁ & … & F_i-1 & x F_i & F_i+1 & … & F_n  x (F₁ & F₂ & … & F_n)

F₁  …  F_i-1  x F_i  F_i+1  …  F_n  x (F₁  F₂  …  F_n)

при условие, че x  FVAR (F_j) за всяко j  i  { 1, 2, …, n };

База: ако F е атомарна формула, F = true или F = fail, броят на кванторите на F е 0;

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

Стъпка: ако F = G, броят на кванторите на F е броят на кванторите на G;

ако F = F₁ & F₂ & … & F_n или F = F₁  F₂  …  F_n, броят на кванторите на F е сума от броя на кванторите на F₁, броя на кванторите на F₂, …, броя на кванторите на F_n;

ако F = "y G или F = y G, броят на кванторите на F е с едно

по-голям от броя на кванторите на G;
съвсем лесно се показва, че F е безкванторна формула  броят на кванторите на F е 0;

Лема: нека F е формула с n+1 квантора, n  0; тогава съществува формула F с n квантора, такава че F е еквивалентна на някоя от формулите "x F или x F, x  ;

при това FVAR (F) = FVAR ("x F) (= FVAR (x F));

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

База: тъй като F има поне един квантор, то F не е атомарна формула, F  true, F  fail; така твърдението в този случай е изпълнено по тривиални причини;

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

G, F₁, F₂, …, F_m, m > 1;

Стъпка: нека F = G; тъй като F има n+1 квантора, то G има n+1 квантора; по индукционното предположение

G  "x G или G  x G, където G е формула с n квантора;

при това FVAR (G) = FVAR ("x G); при това положение,

ако G  "x G, то G  "x G  x G; така F = G  x G и

FVAR (F) = FVAR (G) = FVAR ("x G) = FVAR (G)\{ x } =

= FVAR (G)\{ x } = FVAR (x G);

ако G  x G, разсъжденията са аналогични с използване на еквивалентността x F  x F;

нека F = F₁ & F₂ & … & F_m; тъй като F съдържа n+1 квантора, то съществува j  { 1, 2, …, m }, такова че F_j съдържа

k+1 квантора, k  0; по индукционното предположение

F_j  "x F_j или F_j  x F_j, където F_j е формула с k квантора;

при това FVAR (F_j) = FVAR ("x F_j);

нека F_j  "x F_j; при това положение F = F₁ & F₂ & … & F_m  F₁ & … & F_j-1 & "x F_j & F_j+1 & … & F_m; нека y  ,

 FVAR (F_m); такова y съществува, тъй като ограничението е свързано с крайно обединение на крайни множества, което е крайно множество, а  е безкрайно множество; при това положение субституцията [x/y] е приложима към F_j,

тъй като VAR (y) = { y}  BVAR (F_j) = ; тъй като y  FVAR (F_j) от едно твърдение по-горе получаваме, че "x F_j º "y (F_j [x/y]);

при това y  FVAR (F_i) за i  j  { 1, 2, …, m } 

F  F₁ & … & F_j-1 & "x F_j & F_j+1 & …& F_m 

 F₁ & … & F_j-1 & "y (F_j [x/y]) & F_j+1 & … & F_m 

 "y (F₁ & … & F_j-1 & F_j [x/y] & F_j+1 & … & F_m);

нека F = F₁ & … & F_j-1 & F_j [x/y] & F_j+1 & … & F_m;

имаме F  "y F; съвсем лесно с индукция по построението се показва, че формулата F_j [x/y] има същия брой квантори като формулата F_j, т.е. k; при това положение е ясно, че формулата F има n квантора; ще покажем, че FVAR ("x F_j) = FVAR ("y (F_j [x/y]));

имаме FVAR ("y (F_j [x/y])) = FVAR (F_j [x/y])\{ y } = = \ { y }; ако x  FVAR (F_j), то

 VAR (x [x/y]) \ { y } = FVAR (F_j)\ { x } = FVAR ("x F_j);

ако x  FVAR (F_j), то  \ { y } = FVAR (F_j) \ { y } =

= FVAR (F_j) = FVAR (F_j) \ { x } = FVAR ("x F_j), тъй като

FVAR (F) = FVAR (F₁)  FVAR (F₂)  …  FVAR (F_m) =

= FVAR (F₁)  … FVAR (F_j-1)  FVAR ("x F_j) 

 FVAR (F_j+1)  … FVAR (F_m) = FVAR (F₁)  … FVAR (F_j-1) 

 FVAR ("y (F_j [x/y]))  FVAR (F_j+1)  … FVAR (F_m) =

= FVAR (F₁)  … FVAR (F_j-1)  FVAR (F_j [x/y])  FVAR (F_j+1)  …

 FVAR (F_m) \ { y } = FVAR (F)\ { y } = FVAR ("y F);

случаят F_j  x F_j се разглежда по аналогичен начин с използване на съответните еквивалентности от по-горе;

разсъжденията в случая F = F₁  F₂  …  F_m, m > 1, са аналогични на случая F = F₁ & F₂ & … & F_m;

нека F = "y G; тогава очевидно F  "y G, G има n квантора и

FVAR (F) = FVAR ("y G);

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

F е в пренексен вид, F  F и FVAR (F) = FVAR (F);

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

База: нека F има брой на кванторите 0; тогава F е безкванторна формула и очевидно F = F е такава,

че F  F и FVAR (F) = FVAR (F);

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

Стъпка: нека F има n+1 квантора; от горната лема F  "x G или

F  x G, където G има n квантора и FVAR (F) = FVAR ("x G);

нека например F  "x G; по индукционното предположение съществува формула G в пренексен вид, такава че G  G и

FVAR (G) = FVAR (G); имаме F  "x G  "x G;

ако x  FVAR (G), то "x G е в пренексен вид, F  "x G и

FVAR (F) = FVAR ("x G) = FVAR (G)\ { x } = FVAR (G)\ { x } =

= FVAR ("x G);

ако x  FVAR (G), то G е в пренексен вид, F  "x G  G и

FVAR (F) = FVAR ("x G) = FVAR (G)\ { x } = FVAR (G)\ { x } =

= FVAR (G), тъй като x  FVAR (G);

изнасяме кванторите YZ отпред – това е позволено, тъй като

Y, Z  FVAR (YZ p (Y, Z));

така F  XYZ(p (Y, Z)  YZ  p (Y, Z)); за да изнесем кванторите YZ е необходимо да преименуваме свързаните променливи Y и Z, тъй като Y, Z  FVAR (p (Y, Z)); така получаваме:

F  XYZ(p (Y, Z)  YZ p (Y, Z)) 

 XYZ(p (Y, Z)  TV p (T, V)) 

 XYZTV(p (Y, Z)  p (T, V))  YZTV(p (Y, Z)  p (T, V)),

тъй като X  FVAR (YZTV(p (Y, Z)  p (T, V)));

така YZTV(p (Y, Z)  p (T, V)) е формула в пренексен вид, която е еквивалентна на F и е затворена;