Субституция наричаме изображение  на множеството на променливите 

 (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.

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

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

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

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

Доказателство: Индукция по построението на T.
Следствие: Нека T е терм,  е субституция. Тогава термът T е затворен  термът  (x) е затворен терм за всяко x  VAR (T).

Доказателство: Директно от твърдението.

База: Ако 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.
Следствие: Нека F е безкванторна формула,  е субституция. Тогава формулата F е затворена  термът  (x) е затворен терм за всяко x  VAR (T).

Доказателство: Директно от твърдението.

Доказателство: Ще разгледаме само случая когато E е терм. За безкванторните формули разсъжденията са абсолютно аналогични.

Провеждаме индукция по постронието на E.

База: Нека  и  са такива субституции, че E = E.

Ако E е константа, то очевидно  и  съвпадат върху

VAR (E) = . Ако E  , то E =  (E), E =  (E)   (E) =  (E) 

 и  съвпадат върху VAR (E) = { E}.

Предположение: Нека E = f (T₁, T₂, …, T_n) и твърдението е изпълнено за термовете T₁, T₂, …, T_n.

Стъпка: Нека  и  са субституции, такива че E = E.

Имаме E = f (T₁, T₂, …, T_n), E = f (T₁, T₂, …, T_n). От еднозначния синтактичен анализ на термовете получаваме

T₁ = T₁, T₂ = T₂, …, T_n = T_n. Използваме индукционното предположение за термовете T₁, T₂, …, T_n и получаваме, че

 и  съвпадат върху VAR (T₁), VAR (T₂), …, VAR (T_n). Тогава

 и  съвпадат върху VAR (T₁)  VAR (T₂)  …  VAR (T_n) = VAR (E).
Нека ₁ и ₂ са субституции. Дефинираме функция  (x) от множеството  на променливите в множеството от всички термове по следния начин:  (x) = (x₁)₂ за всяко x  .

Ще покажем, че  (x) е субституция, т.е.  (x)  x най-много за краен брой променливи x. За целта ще покажем, че за всяко x   ако  (x)  x, то ₁ (x)  x или ₂ (x)  x. Да допуснем противното –

 (x)  x и ₁ (x) = x, ₂ (x) = x за някоя променлива x  . Тогава

 (x) = (x₁)₂ = x₂ = x, което е противоречие. Ясно е, че

₁ (x)  x или ₂ (x)  x е изпълнено само за краен брой

променливи x, тъй като ₁ и ₂ са субституции. Така  (x)  x само за краен брой променливи x, т.е.  (x) е субституция. Тази субституция наричаме произведение на субституциите ₁ и ₂, означаваме  = ₁₂. Така по дефиниция x(₁₂) = (x₁)₂.

Действително, за всяко x   имаме x() = (x) = x (от съответното твърдение за термове)   = . Също, за всяко x   имаме x() = (x) = x   = .

Ясно е, че умножението на субституции не е комутативно.
Твърдение: Ако E е терм или безкванторна формула и ₁, ₂ са субституции, то E(₁₂) = (E₁)₂.

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

Доказателство: Нека x  .

Тогава x ((₁₂)₃) = (x(₁₂))₃ = ((x₁)₂)₃.

Също x (₁(₂₃)) = (x₁)(₂₃) = ((x₁)₂)₃. Тук използваме горното твърдение за терма (x₁).

Така x ((₁₂)₃) = x (₁(₂₃)) за всяко x    (₁₂)₃ = ₁(₂₃).
Нека F е произволна безкванторна формула. Частни случаи на формулата F наричаме всички формули от вида F, където  е произволна субституция.

Например, всяка безкванторна формула F е частен случай на себе си, тъй като F = F. Ако F е затворена безкванторна формула, то

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

Релацията “е частен случай на” е транзитивна: Ако G е частен случай на F и H е частен случай на G, то H е частен случай на F.

Действително по условие G = F₁, H = G₂  H = (F₁)₂ = F (₁₂), т.е. H е частен случай на F.
Нека F е безкванторна формула. Вариант на F наричаме такъв частен случай G на F, такъв че F е частен случай на G.

С други думи, релацията “е вариант на” е симетричното затваряне на релацията “е частен случай на”. В такъв случай е очевидно, че

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

Напротив, ако F е безкванторна формула, която не е затворена, то тя има безброй много варианти, както се вижда от следното

Нека VAR (F) = { x₁, x₂, …, x_n}, n  1, x_i  x_j при i  j  { 1, 2, …, n}.

Нека y₁, y₂, …, y_n са две по две различни променливи.

Ако  = [x₁/y₁, x₂/y₂, …, x_n/y_n], то G = F е вариант на F.

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

Очевидно G е частен случай на F. Ще покажем, че F е частен случай на G. Да разгледаме субституцията

 = [y₁/x₁, y₂/x₂, …, y_n/x_n] – тя е коректно зададена, тъй като

y_i  y_j при i  j  { 1, 2, …, n}. Ще покажем, че F = G.

Имаме G = (F) = F ().

За i = 1, 2, …, n имаме: x_i () = (x_i) = y_i = x_i.

Така  и  съвпадат върху VAR (F)  F () = F = F.

Така G = F и G е вариант на F.
Тъй като множеството  е безкрайно, по посочения начин можем да построим безброй много варианти на F. Дори можем да построим вариант на F, който не съдържа променливи от дадено крайно подмножество на .
Твърдение: Нека F е безкванторна формула, която не е затворена. Нека VAR (F) = { x₁, x₂, …, x_n}, n  1, x_i  x_j при i  j  { 1, 2, …, n}.

Нека G е произволен вариант на F. Тогава

G = F[x₁/y₁, x₂/y₂, …, x_n/y_n], за някои променливи y₁, y₂, …, y_n, които са две по две различни помежду си.

Доказателство: Тъй като G е вариант на F, то G = F, F = G за някои субституции  и . Тогава F = G = (F) = F () 

 и  съвпадат върху VAR (F), т.е. x_i () = x_i, i = 1, 2, …, n.

Да допуснем, че x_i е съставен терм. Тогава x_i () = (x_i) също е съставен терм, тъй като след прилагането на субституцията ,

(x_i) отново ще съдържа функционални символи. Така

x_i = (x_i) е съставен терм, което е противоречие тъй като съставните термове са различни от променливите.

Да допуснем, че x_i е константа. Тогава x_i = (x_i) = x_i, което е противоречие, тъй като множествата Ф₀ и  не се пресичат.

Така x_i е променлива, нека x_i = y_i  . Тогава

 и [x₁/y₁, x₂/y₂, …, x_n/y_n] съвпадат върху VAR (F) 

G = F = F [x₁/y₁, x₂/y₂, …, x_n/y_n]. Ако допуснем, че за някои

i  j  { 1, 2, …, n} имаме y_i = y_j  x_i = x_j 

(x_i) = (x_j)  x_i = x_j, което е противоречие. Така y₁, y₂, …, y_n са две по две различни помежду си.
Нека A и B са произволни атомарни формули. Въпросът, който ще разглеждаме е съществува ли атомарна формула, която е частен случай както на A, така и на B, т.е. съществуват ли субституции

, , такива че A = B.

субституция , такава че A = B. Ако A и B притежават унификатор, казваме че A и B са унифицируеми.

VAR (A)  VAR (B) = . Ако съществува атомарна формула, която е частен случай на A и на B, то A и B са унифицируеми.

Доказателство: По условие съществуват субституции ,  такива че

A = B. Разглеждаме изображението  от  в множеството на всички термове,  (x) =  (x), ако x  VAR (A),  (x) =  (x), ако

най-много за променливите от VAR (A)  VAR (B), които са краен брой. Тъй като  и  съвпадат върху VAR (A), то A = A.

Също, тъй като VAR (A)  VAR (B) =   VAR (B)  \VAR (A) 

 и  съвпадат върху VAR (B)  B = B.

Така  е унификатор на A и B.
Нека A и B са произволни атомарни формули. Както знаем, съществува вариант B на B, такъв че VAR (A)  VAR (B) = .

Ясно е, че B и B имат едни и същи частни случаи. Тогава една атомарна формула е частен случай на A и на B  тя е частен случай на A и на B. От горното твърдение, тъй като

VAR (A)  VAR (B) = , то съществува атомарна формула, която е частен случай на А и на B  A и B са унифицируеми.

От доказателството на твърдението заключаваме, че общият вид на атомарните формули, които са частни случаи на A и на B

е A, където  е унификатор на A и на B.
Нека A и B са атомарни формули.

Ако A и B имат различни предикатни символи или предикатни символи с различен брой аргументи, то очевидно A и B не са унифицируеми.

от вида T = U, където T и U са термове. Решение на това уравнение наричаме субституция , такава че T = U.

T₁ = U₁, T₂ = U₂, …, T_n = U_n.

Празното множество от уравнения също е система и нейните решения са всички субституции.
Твърдение: Нека A = p (T₁, T₂, …, T_n) и B = p (U₁, U₂, …, U_n) са атомарни формули с един и същ предикатен символ с един и същ брой аргументи. Една субституция  е унификатор на A и B 

 е решение на системата T₁ = U₁, T₂ = U₂, …, T_n = U_n.

Доказателство: Нека  е произволна субституция.

Имаме A = p (T₁, T₂, …, T_n), B = p (U₁, U₂, …, U_n).

От еднозначния синтактичен анализ имаме:

A = B  T₁ = U₁, T₂ = U₂, …, T_n = U_n, т.е.  е унификатор на A и B   е решение на системата T₁ = U₁, T₂ = U₂, …, T_n = U_n.

Ясно е, че релацията “е частен случай на” върху субституциите е рефлексивна и транзитивна.

₂ е частен случай на ₁, такъв че ₁ е частен случай на ₂.

С други думи, както при безкванторни формули, релацията

“е вариант на” е симетрично затваряне на релацията “е частен случай на” за субституции. Естествено, в такъв случай релацията “е вариант на” за субституциите е релация на еквивалентност.

От тази дефиниция, по тривиални съображения, празната система е в решен вид.

Тъй като x₁, x₂, …, x_n са две по две различни помежду си можем да построим субституцията ₀ = [x₁/U₁, x₂/U₂, …, x_n/U_n]

(₀ =  при n = 0).

Доказателство: За i = 1, 2, …, n имаме x_i₀ = U_i, U_i₀ = U_i = U_i, тъй като ₀ и  съвпадат върху VAR (U_i). Така x_i₀ = U_i = U_i₀,

i = 1, 2, …, n  ₀ е решение на системата.

Нека  е произволно решение на системата, т.е. x_i = U_i,

i = 1, 2, …, n. Тогава x_i(₀) = (x_i₀) = U_i = x_i, i = 1, 2, …, n.

Също за всяко x  \{ x₁, x₂, …, x_n}, x(₀) = (x₀) = x. Така  = ₀.

 е решение на системата.

на . В случая когато системата е в решен вид, т.е. има вида

(₀ =  при n = 0) е най-общо решение на тази система, така че решенията на тази система се изчерпват със ₀, където  е произволна субституция.

U  x и x  VAR (U).

Доказателство: С индукция по построението ще покажем следното свойство: За всеки терм W, ако x  VAR (W) и x  W, то за всяка субституция , |W| > |x|.

База: Ако W е константа, свойството е тривиално изпълнено, тъй като една от предпоставките (x  VAR (W)) не е удоволетворена.

Ако W е променлива, свойството отново е тривиално изпълнено, тъй като двете препоставки (x  VAR (W), W  x) не могат да са изпълнени едновременно.

Предположение: Нека W = f (W₁, W₂, …, W_k) и свойството е изпълнено за термовете W₁, W₂, …, W_k.

Стъпка: Нека  е произволна субституция. Имаме

W = f (W₁, W₂, …, W_k). Ясно е, че |W| > |W_i| за всяко

i = 1, 2, …, n. Тъй като x  VAR (W), то x  VAR (W_i)

за някое i  { 1, 2, …, k }. Ако W_i  x, то по индукционното предположение|W_i| > |x|  |W| > |W_i| > |x|.

Ако W_i = x, то |W| > |W_i| = |x|.

Така и в двата случая |W| > |x|.

Сега, ако допуснем, че  е решение на системата x = U ще получим, че |x|= |U|, което е противоречие.

Ще посочим четири еквивалентни преобразувания на системи, т.е. преобразувания чрез които една система преминава в еквивалентна на нея система.

Нека T₁ = U₁, T₂ = U₂, …, T_n = U_n е система от уравнения между термове.

1. Премахване на тъждество – ако за някое i  { 1, 2, …, n} имаме T_i = U_i премахваме това уравнение от системата. Системата очевидно преминава в еквивалентна на нея, тъй като премахнатото уравнение се удоволетворява от всяка субституция.

2. Разпадане – ако за някое i  { 1, 2, …, n} имаме

T_i = f (V₁, V₂, …, V_m), U_i = f (W₁, W₂, …, W_m), m > 0 и T_i  U_i, заменяме уравнението T_i = U_i с уравненията V₁ = W₁, V₂ = W₂, …, V_m = W_m. Системата преминава в еквивалентна на нея, тъй като  е решение на T_i = U_i, т.е. T_i = U_i 

 f (V₁, V₂, …, V_m) = f (W₁, W₂, …, W_m)  (от еднозначния синтактичен анализ) V₁ = W₁, V₂ = W₂, …, V_m = U_m.

Изисква се T_i  U_i, тъй като при T_i = U_i е удачно да се извърши премахване на тъждество.

3. Обръщане – ако за някое i  { 1, 2, …, n} имаме T_i  , U_i  ,

то заменяме уравнението T_i = U_i с U_i = T_i. Очевидно системата преминава в еквивалентна на нея.

4. Заместване – ако за някое i  { 1, 2, …, n} имаме T_i  ,

T_i  VAR (U_i) и T_i  VAR (U_j)  VAR (T_j) за някое j = 1, 2, …, n, то заменяме системата със следната:

T₁[T_i/U_i] = U₁[T_i/U_i], …, T_i-1[T_i/U_i] = U_i-1[T_i/U_i],

T_i = U_i, T_i+1[T_i/U_i] = U_i+1[T_i/U_i], …, T_n[T_i/U_i] = U_n[T_i/U_i].

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

Да означим ₀ = [T_i/U_i]. Нека  е произволно решение на изходната система. Тъй като  е решение на уравнението T_i = U_i, T_i   и

T_i  VAR (U_i), то от по-предното твърдение,  = ₀.

За j  i  { 1, 2, …, n} T_j = T_j(₀) = (T_j₀) и U_j = U_j(₀) = (U_j₀)  (T_j₀) = (U_j₀). Така  е решение и на преобразуваната система.

Нека  е произволно решение на преобразуваната система. Отново  е решение на уравнението T_i = U_i, така че  = ₀.

За j  i  { 1, 2, …, n} T_j = T_j(₀) = (T_j₀) и

U_j = U_j(₀) = (U_j₀)  T_j = U_j, т.е.  е решение на изходната система.