Семантика на логическите формули

Семантика на логическите формули

фиксираме структура S с носител D и интерпретации ₀, ₁, …;

₀, ₁, …; съответно на функционалните и на предикатните символи;
нека v е оценка на x е променлива и d  D;

дефинираме оценка u по следния начин:

оценката 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}, F₁^{S, v}, F₂^{S, v}, …, F_n^{S, v} са дефинирани за произволна оценка v;

Стъпка: тогава за произволна оценка v дефинираме:

not(F)^{S, v} = 1 – F ^{S, v};

(F₁, F₂, …, F_n)^{S, v} = min { F₁^{S, v}, F₂^{S, v}, …, F_n^{S, v}},

(F₁; F₂; …; F_n)^{S, v} = max { F₁^{S, v}, F₂^{S, v}, …, F_n^{S, 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;

ако 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  G; тогава

S, v F, S, v G, което е противоречие;
нека S е структура, F е формула; казваме, че F е тъждествено вярна в S, ако F е вярна в S при всяка оценка на променливите;
примери със структурата на семейство Вазови:

въвеждаме едноместни предикатни символи male, female;

₁ (male) (A) = 1  A е мъж, A  M;

₁ (female) (A) = 1  A е жена, A  M;

ясно е, че формулите male (X)  female (X), (male (X) & female (X)),

parent (X, Y)  distinct (X, Y) са тъждествено вярни в структурата;

да разгледаме формулата X p(X), където p е едноместен предикатен символ; нека v е произволна оценка на променливите;

тогава X p(X)^{S, v} = min { p (X) ^{S, v[X : d]}|d  D} = min { p^S (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,

F₁, F₂, …, F_n, n > 1 за произволни оценки v, u, съвпадащи върху върху съответните множества;

Стъпка:

FVAR (G)  G^{S, v} = G^{S, u}; така F ^{S, v} = 1 – G^{S, v} = 1 – G^{S, u} = F ^{S, u};

ако F = F₁ & F₂ & … & F_n, то FVAR (F_i)  FVAR (F) 

F_i^{S, v} = F_i^{S, v}, i = 1, 2, …, n; така F ^{S, v} = min { F₁^{S, v}, F₂^{S, v}, …, F_n^{S, v} } =

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

ако F = F₁  F₂  …  F_n, то FVAR (F_i)  FVAR (F) 

F_i^{S, v} = F_i^{S, v}, i = 1, 2, …, n; така F ^{S, v} = max { F₁^{S, v}, F₂^{S, v}, …, F_n^{S, v} } =

= max { F₁^{S, u}, F₂^{S, u}, …, F_n^{S, 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) 

G^{S, v[x : d]} = G^{S, v[x : d]} за всяко d  D  F ^{S, v} = F ^{S, u};

Доказателство: произволни оценки v и u съвпадат върху

FVAR (F) = ;
ако F е затворена формула, по дефиниция F ^S = F^{S, v} за коя да е оценка v; ще казваме, че F е вярна в S, акоF ^S = 1;

означаваме S F; ще казваме, че F не е вярна в S, ако F ^S = 0;

оценка v, такава че F ^{S, v} = 1;

F е тъждествено вярна в S  F е вярна в S  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) = { x₁, x₂, …, x_n};

тогава F е тъждествено вярна в S  x₁x₂…x_n F е тъждествено вярна в S, т.е. x₁x₂…x_n F е вярна в S, тъй като тя е затворена формула; формулата x₁x₂…x_n F наричаме универсално затваряне на F, то е определено с точност до подредбата на кванторите;

тогава F е изпълнима в S  x₁x₂…x_n F е изпълнима в S, т.е. x₁x₂…x_n F е вярна в S, тъй като тя е затворена формула; формулата x₁x₂…x_n F наричаме екзистенциално затваряне на 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 не е тъждествено вярна;