1. Булеви функции. Теорема на Пост-Яблонски за пълнота. Нека J2 = { 0, 1}. Всяка функция f : J2n  J

Доказателство: Провеждаме индукция по построението на 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, съвпадащи върху върху съответните множества.

Стъпка: Нека v и u са произволни оценки, които съвпадат върху FVAR (F). Случаите F = G, F = F₁ & F₂ & … & F_n и

F = F₁  F₂  …  F_n следват директно от индукционното предположение.

Нека 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). Така по индукционното предположение

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

Аналогично се разсъждава при F = x G.
Следствие: Ако F е затворена формула, то за произволни оценки

u и v имаме F ^{S, v} = F ^{S, u}.

Доказателство: Произволни оценки v и u се съгласуват по променливите от FVAR (F) = .

Означаваме S F. Ще казваме, че F не е вярна в S, ако F ^S = 0.

Означаваме S  F.
Нека S е структура с носител D.
Казваме, че формулата F е тъждествено вярна в S, ако F е вярна в S при всяка оценка на променливите.

Казваме, че формулата F е изпълнима в S, ако съществува

оценка v, такава че F ^{S, v} = 1.
Ясно е, че ако F е затворена формула, то

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. Нека v е произволна оценка. Тогава за всяко 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 е тъждествено вярна в 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.

F е изпълнима  F не е тъждествено вярна.

 (x)  x най-много за краен брой променливи.

Ако x₁, x₂, …, x_n са две по две различни променливи и u₁, u₂, …, u_n са термове, то със [x₁/u₁, x₂/u₂, …, x_n/u_n] означаваме субституцията , определена по следния начин:  (x_i) = u_i,

i = 1, 2, …, n,  (x) = x за x  { x₁, x₂, …, x_n}. Всяка субституция може да се зададе с краен израз по този начин. Тъждествената субституция бележим с ,  (x) = x за всяко x  ,  = [x/x ] за произволна променлива x.

База: Ако T  Ф₀, то T = T. Ако T  , T =  (T).

Предположение: Нека T = f (T₁, T₂, …, T_n) и T₁, T₂, …, T_n са дефинирани.

Стъпка: Тогава T = f (T₁, T₂, …, T_n).

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

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

субституция .

Доказателство: Нека  е произволна субституция. Тогава  и  съвпадат върху VAR (T) =   T = T = T.
Твърдение: Нека T е терм,  е субституция.

Тогава VAR (T) = .

Доказателство: Индукция по построението на T.
Нека F е безкванторна формула,  е субституция. Дефинираме индуктивно безкванторната формула F, която ще наричаме резултат от прилагането на  към F.

База: Ако F е атомарна формула, F = p (T₁, …, T_n) дефинираме

F = p (T₁, …, T_n), ако F  П₀, то F = F.

Ако F = true или F = fail, дефинираме F = F.

Предположение: Нека G, F₁, …, F_n (n > 1) са безкванторни формули и G, F₁, …, F_n са дефинирани.

Стъпка: Ако F = G, дефинираме F = (G).

Ако F = F₁ & F₂ & … & F_n, дефинираме F = F₁ & F₂ & …& F_n.

Ако F = F₁  F₂  …  F_n, дефинираме F = F₁  F₂  … F_n.

Доказателство: Индукция по построението на F, използваме и съответното твърдение за термове.

Доказателство: Тривиална индукция по F, използваме и съответното твърдение за термове.

VAR (F) = .

Доказателство: Индукция по построението на F, използваме и съответното твърдение за термове.
Нека S е структура,  е субституция. Дефинираме ^S – оператор за присвояване, съответен на  в S, който съпоставя на всяка оценка v на променливите в S друга оценка ^S (v) на променливите в S, така че (^S (v)) (x) =  (x) ^{S, v}.
Теорема: Нека S е структура,  е субституция, v е оценка на променливите в S. Ако E е терм или безкванторна формула, то

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

Доказателство: С отделни случаи, първо когато E е терм и след това когато E е безкванторна формула.
Нека F е произволна безкванторна формула. Частни случаи на формулата F наричаме всички формули от вида F, където  е произволна субституция.
Например, всяка безкванторна формула F е частен случай на себе си, тъй като F = F. Ако F е затворена безкванторна формула, то

F е единственият частен случай на F, тъй като F = F за всяка субституция . Напротив, ако F не е затворена, то е ясно, че F има и други частни случаи, дори безброй много.

В сила е:

1. 
   Ако F е тъждествено вярна в S, то всички частни случаи на F са тъждествено вярни в S.
   
2. 
   Ако някой частен случай на F е изпълним в S, то F е изпълнима в S.
   

Нека F е тъждествено вярна в S. Нека  е произволна субституция.

Тогава за произволна оценка v в S имаме: (F)^{S, v} = F ^{S, u}, където

u =  ^S (v). Имаме F ^{S, u} = 1  (F)^{S, v} = 1. Така F е тъждествено вярна в S, т.е. всеки частен случай на F е тъждествено верен в S.

Нека F е частен случай на F, който е изпълним в S ( е някаква субституция). Нека v е оценка, такава че (F)^{S, v} = 1. Имаме

1 = (F)^{S, v} = F ^{S, u}, където u =  ^S (v). Така F е изпълнима в S.
Обратното твърдение също е вярно, тъй като всяка формула F е частен случай на себе си.

Ясно е, че F е затворен частен случай на F 

 (x) е затворен терм за всяко x  VAR (F).
Следствие: Нека S е структура, F е безкванторна формула.

В сила е:

1. 
   Ако F е тъждествено вярна в S, то всички затворени частни случаи на F са вярни в S.
   
2. 
   Ако някой затворен частен случай на F е верен в S, то F е изпълнима в S.
   

Обратното твърдение на следствието не е вярно в общия случай.

Нека S е структура. Казваме, че S има термално породен носител, ако всеки елемент на носителя на S е стойност в S на някой затворен терм.
Твърдение: Нека S е структура с термално породен носител.

Нека F е безкванторна формула. В сила е:

1. 
   Ако всички затворени частни случаи на F са вярни в S, то F е тъждествено вярна в S.
   
2. 
   Ако F е изпълнима в S, то съществува затворен частен случай на F, който е верен в S.
   

Нека всеки затворен частен случай на F е верен в S.

Нека v е произволна оценка. Ще покажем, че F ^{S, v} = 1.

Ако F е затворена формула, то тя е затворен частен случай на себе си  F е вярна в S, т.е. F е тъждествено вярна в S.

Нека VAR (F) = { x₁, x₂, …, x_n}, n  1. За i = 1, 2, …, n

v (x_i) е елемент на носителя на S, така че съществува затворен

терм T_i, такъв че T_i^S = v (x_i). Разглеждаме следната субституция

 = [x₁/T₁, x₂/T₂, …, x_n/T_n]. Ясно е, че F е затворен частен случай на F, тъй като  (x) е затворен терм за всяко x  VAR (F).

Така (F)^S = 1  (F)^{S, v} = 1  F ^{S, u} = 1, където

Нека F е изпълнима в S. Нека v е оценка в S, такава че

F ^{S, v} = 1. Ако F е затворена формула, то тя е затворен частен случай на себе си и тя е търсения верен затворен частен случай.

Нека VAR (F) = { x₁, x₂, …, x_n}, n  1. v (x_i) е елемент на носителя

на S, така че съществува затворен терм T_i, така че v (x_i) = T_i^S,

i = 1, 2, …, n. Нека  = [x₁/T₁, x₂/T₂, …, x_n/T_n]. Тъй като T₁, T₂, …, T_n са затворени термове, то F е затворен частен случай на F.

Ще покажем, че (F)^{S, v} = 1. Имаме (F)^{S, v} = F ^{S, u}, където u =  ^S (v). Както по-горе u = v. Така (F)^S = (F)^{S, v} = F ^{S, u} = F ^{S, v} = 1 и F е търсеният верен затворен частен случай на F.
Оттук нататък предполагаме допълнително изискване Ф₀  .

Множеството от всички затворени термове наричаме ербранов универсум – бележим го с H. При направеното изискване, H  , така че H може да е носител на структура.

Казваме, че една структура S е ербранова, ако е изпълнено:

1. 
   Носителят на S е H.
   
2. 
   Ако c  Ф₀, то c^S = c.
   
3. 
   Ако f  Ф_n, n > 0, то f ^S (T₁, T₂, …, T_n) = f (T₁, T₂, …, T_n) са всяка наредена n-торка T₁, T₂, …, T_n от елементи на H.
   

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

Доказателство: Действително, всеки затворен терм от H е стойност на същия затворен терм в S.

Доказателство: Ще построим ербрановата структура S. Тя има носител H и функционалните символи са интерпретирани по дефиницията за ербранова структура. Нека p е n-местен предикатен символ.

Ако n > 0 определяме p^S (T₁, T₂, …, T_n) = 1  p (T₁, T₂, …, T_n)  M за всяка наредена n-торка T₁, T₂, …, T_n от елементи на H.

При n = 0 определяме p^S = 1  p  M.

Ще покажем, че описаното свойство е в сила.

Нека A е затворена атомарна формула.

Ако A = p (T₁, T₂, …, T_n), то

A^S = p^S (T₁^S, T₂^S, …, T_n^S) = p^S (T₁, T₂, …, T_n) = 1 

p (T₁, T₂, …, T_n)  M, т.е. A^S = 1  A  M.

Ако A = p  П₀, то A^S = p^S = 1  p  M, т.е. A^S = 1  A  M.

Очевидно е, че ербрановата структура с описаното свойство е единствена.
По този начин една ербранова структура се определя еднозначно, ако се зададат атомарните формули, които са вярни в нея.
Нека M е множество от формули. Модел на M наричаме всяка структура S, в която всички формули от M са тъждествено вярни.
Едно множество M от формули се нарича изпълнимо, ако съществува структура S и оценка v, такива че всяка формула от M вярна в S при оценката v.
Едно множество М от формули се нарича силно изпълнимо, ако съществува структура S, която е модел на M.
Ясно е, че за множества от затворени формули понятията изпълнимост и силна изпълнимост са еквивалентни.
Твърдение: Нека M е множество от безкванторни формули.

Нека M е множеството на всички затворени частни случаи на формулите от М. Тогава следните условия са еквивалентни:

1. 
   M е силно изпълнимо.
   
2. 
   M e изпълнимо.
   
3. 
   Съществува ербранова структура, която е модел на M.
   

1  2  3  1.

Съществува ербранова структура S₀, в която вярните атомарни формули са точно формулите от M₀. С индукция по построението се показва, че F ^S = за всяка безкванторна формула F.

В частност, тъй като F ^S = 1 за всяка F  M  = 1 за всяка

F  M. С други думи, всички затворени частни случаи на формулите от M са вярни в S₀ и тъй като S₀ е с термално породен носител, всяка формула от M е тъждествено вярна в S₀, т.е. S₀ е ербранова структура, която е модел на M.

Доказателство: Да разгледаме множеството M от безкванторните части на формулите от даденото множество. Очевидно моделите на M и на даденото множество са едни и същи. Тогава M е силно изпълнимо и от твърдението съществува ербранова структура, която е модел за M. Тази ербранова структура е модел и за първоначалното множество.