фиксираме структура S с носител D и интерпретации 0, 1, …;
0, 1, …; съответно на функционалните и на предикатните символи;
нека v е оценка на x е променлива и d D;
дефинираме оценка u по следния начин:
u (y) = d, ако y = x, u (y) = v (y) при y x;
оценката u наричаме модификация на v върху x чрез d;
модификацията бележим по следния начин: v[x : d];
нека v е произволна оценка; на всяка логическа формула F съпоставяме елемент от { 0, 1}, наречен стойност на F в S при оценката v; стойността на F в S при оценка v означаваме с F S, v;
дефинираме индуктивно стойност на формулата F при произволна оценка v;
База: ако F е атомарна формула, то при произволна оценка v
F S, v е вече дефинирано при семантика на атомарните формули;
ако F = true, то при произволна оценка v, F S, v = 1;
ако F = fail, то при произволна оценка v, F S, v = 0;
Предположение: нека F S, v, F1S, v, F2S, v, …, FnS, v са дефинирани за произволна оценка v;
Стъпка: тогава за произволна оценка v дефинираме:
not(F)S, v = 1 – F S, v;
(F1, F2, …, Fn)S, v = min { F1S, v, F2S, v, …, FnS, v},
(F1; F2; …; Fn)S, v = max { F1S, v, F2S, v, …, FnS, v},
for_all (x: F)S, v = min { F S, v[x : d] |d D},
for_some (x: F)S, v = max { F S, v[x : d] |d D};
казваме, че F е вярна в S при оценка v, ако F S, v = 1;
това записваме още по следния начин: S, v F;
нека F и G са логически формули; под импликация на F и G разбираме формулата (F) G; бележим импликацията с F G;
Твърдение: нека F и G са логически формули;
ако S, v F G и S, v F, то S, v G;
Доказателство: да допуснем, че G S, v = 0; тогава от F S, v = 1 получаваме F S, v = 0 (F) G S, v = 0, което е противоречие;
така S, v G;
ясно е, че S, v F G S, v F, S, v G;
Твърдение: нека е изпълнено, че ако S, v F, то S, v G;
тогава S, v F G;
Доказателство: да допуснем, че S, v F G; тогава
S, v F, S, v G, което е противоречие;
нека S е структура, F е формула; казваме, че F е тъждествено вярна в S, ако F е вярна в S при всяка оценка на променливите;
примери със структурата на семейство Вазови:
въвеждаме едноместни предикатни символи male, female;
1 (male) (A) = 1 A е мъж, A M;
1 (female) (A) = 1 A е жена, A M;
ясно е, че формулите male (X) female (X), (male (X) & female (X)),
parent (X, Y) distinct (X, Y) са тъждествено вярни в структурата;
нека S е структура с носител D;
да разгледаме формулата X p(X), където p е едноместен предикатен символ; нека v е произволна оценка на променливите;
тогава X p(X)S, v = min { p (X) S, v[X : d]|d D} = min { pS (d) |d D} и така верността на формулата X p(X) не зависи от оценката v;
ще докажем едно по-силно
Твърдение: нека S е структура с носител D; за произволна формула F, ако две оценки v и u съвпадат върху FVAR (F),
то F S, v = F S, u;
Доказателство: индукция по построението на F;
База: ако F е атомарна формула, то FVAR (F) = VAR (F) и твърдението е вярно (от съответното твърдение при семантика на атомарните формули); ако F = true, то F S, v = F S, u = 1;
ако F = fail, то F S, v = F S, u = 0;
Предположение: нека твърдението е изпълнено за формулите G,
F1, F2, …, Fn, n > 1 за произволни оценки v, u, съвпадащи върху върху съответните множества;
Стъпка:
нека v и u са произволни оценки, които съвпадат върху FVAR (F); ако F = G, то FVAR (F) = FVAR (G) v и u съвпадат върху
FVAR (G) GS, v = GS, u; така F S, v = 1 – GS, v = 1 – GS, u = F S, u;
ако F = F1 & F2 & … & Fn, то FVAR (Fi) FVAR (F)
FiS, v = FiS, v, i = 1, 2, …, n; така F S, v = min { F1S, v, F2S, v, …, FnS, v } =
= min { F1S, u, F2S, u, …, FnS, u } = F S, u;
ако F = F1 F2 … Fn, то FVAR (Fi) FVAR (F)
FiS, v = FiS, v, i = 1, 2, …, n; така F S, v = max { F1S, v, F2S, v, …, FnS, v } =
= max { F1S, u, F2S, u, …, FnS, u } = F S, u;
нека F = x G; v и u съвпадат върху FVAR (F) = FVAR (G)\{ x};
имаме F S, v = min { G S, v[x : d]|d D }, F S, u = min { G S, u[x : d]|d D };
за всяко d D имаме, че v[x : d], u[x : d] съвпадат върху FVAR (G);
действително, ако y VAR (G), y x, то y FVAR (F)
v[x : d] (y) = v (y) = u (y) = u[x : d] (y); ако y VAR (G), y = x, то
v[x : d] (y) = d = v[x : d]; така по индукционното предположение
GS, v[x : d] = GS, v[x : d] за всяко d D F S, v = F S, u;
Следствие: ако F е затворена формула, то за произволни оценки
u и v имаме F S, v = F S, u;
Доказателство: произволни оценки v и u съвпадат върху
FVAR (F) = ;
ако F е затворена формула, по дефиниция F S = FS, v за коя да е оценка v; ще казваме, че F е вярна в S, акоF S = 1;
означаваме S F; ще казваме, че F не е вярна в S, ако F S = 0;
Запазване на тъждествена вярност или изпълнимост при поставяне или премахване на съответните квантори
нека S е структура с носител D;
казваме, че формулата F е изпълнима в S, ако съществува
оценка v, такава че F S, v = 1;
пример със структурата на семейство Вазови: male (X) – например всяка оценка v, такава че v (x) = Иван Вазов;
ясно е, че ако F е затворена формула, то
F е тъждествено вярна в S F е вярна в S F е изпълнима в S;
нека S е структура с носител D, F е формула, x ;
Твърдение: F е тъждествено вярна в S x F е тъждествено вярна в S; F е изпълнима в S x F е изпълнима в S;
Доказателство:
нека F е тъждествено вярна в S; нека v е произволна оценка;
тогава x F S, v = min { F S, v[x : d]|d D}; тъй като F е тъждествено вярна в S, то F S, v[x : d] = 1 за всяко d D
min { F S, v[x : d]|d D} = 1 x F е тъждествено вярна в S;
нека x F е тъждествено вярна в S; тогава за всяко d D имаме
F S, v[x : d] = 1 при d = v (x) получаваме F S, v[x : v(x)] = F S, v = 1
F е тъждествено вярна в S;
нека F е изпълнима в S; нека v е оценка, такава че F S, v = 1;
тогава x F S, v = max { F S, v[x : d]|d D} = 1, тъй като
F S, v[x : v(x)] = F S, v = 1 x F е изпълнима в S;
нека x F е изпълнима в S; тогава съществува оценка v, такава че
x F S, v = 1 max { F S, v[x : d]|d D} = 1 съществува d D, така че F S, v[x : d] = 1 F е изпълнима в S;
Следствие: нека F е формула и FVAR (F) = { x1, x2, …, xn};
тогава F е тъждествено вярна в S x1x2…xn F е тъждествено вярна в S, т.е. x1x2…xn F е вярна в S, тъй като тя е затворена формула; формулата x1x2…xn F наричаме универсално затваряне на F, то е определено с точност до подредбата на кванторите;
Следствие: нека F е формула и FVAR (F) = { x1, x2, …, xn};
тогава F е изпълнима в S x1x2…xn F е изпълнима в S, т.е. x1x2…xn F е вярна в S, тъй като тя е затворена формула; формулата x1x2…xn F наричаме екзистенциално затваряне на F, то е определено с точност до подредбата на кванторите;
нека S е структура; F е произволна формула; в сила е:
F е тъждествено вярна в S F не е изпълнима в S;
F e изпълнима в S F не е тъждествено вярна в S;
казваме, че една формула F е тъждествено вярна, ако F е тъждествено вярна във всяка структура S;
казваме, че една формула F е изпълнима, ако F е изпълнима във някоя структура S;
например формулата p (X) p (X) е тъждествено вярна, формулата p (X) p (Y) е изпълнима;
ясно е, че F е тъждествено вярна F не е изпълнима;
също F е изпълнима F не е тъждествено вярна;
ще отбележим, че не съществува алгоритъм, който разпознава дали произволна формула е тъждествено вярна (Гьодел);
Сподели с приятели: |