​

ЛОГІКА ПРЕДИКАТІВ

Крім логічних зв’язок в математичних міркуваннях часто зустрічаються квантори “для всякого (∀)” і “існує (∃)”. Наприклад, визначення неперервності починається словами “для всякого ε>0 існує δ>0 таке, ...”.

Можна формулювати різні твердження, що включають квантори. Ми будемо запи-сувати такі твердження з допомогою формул і дамо визначення істинності формул при даній інтерпретації вхідних символів.

​

Формули і інтерпретації

Почнемо з прикладу. Нехай М – деяка непуста множина, а R – бінарне відношення на ній. Розглянемо формулу

∀x∃yR(x,y).

Ця формула виражає деяку властивість відношення R (а саме, для всякого елемента x∈M існує елемент y∈M такий, що R(x,y)) і може бути істинною або фальшивою в за-лежності від області М.

Питання про істинність чи фальшивість формули

∀x∃yR(x,y)

для даних множини М і бінарного відношен-ня R на ній не має змісту, поки не уточнена область М. Наприклад, якщо М = N і R(x,y) є x>y, то формула є фальшивою. Якщо R(x,y) є x<y, то формула є істинною.

Перейдемо до формальних визначень.

​

Нехай М – непорожня множина.

Df. Назвемо k-місною функцією довільне відображення M^k в М визначене на всьому M^k.

Df. Назвемо k-місним предикатом на мно-жині М довільне відображення M^k в множи-ну {0,1}.

Зафіксуємо деякий набір символів, які будемо називати змінними. Як правило, це латинські букви x, y, z, u, … або ті ж букви з індексами.

​

Символи f, g, h, … будемо називати функціональними.

Символи P, Q, R, … будемо називати предикатними.

Всякий функціональний або предикатний символи, як було зазначено, мають визначе-ну кількість аргументів.

Функціональний символ без аргументів будемо ототожнювати з елементами множи-ни М.

​

​

Визначимо поняття терма.

Df. Термом називається послідовність змінних, ком, дужок і функціональних сим-волів, яку можна побудувати за наступними правилами:

1. Змінна є терм.

2. Константа є терм (функ. символ без аргументів).

3. Якщо t₁, …, t_k – терми, а f – функціо-нальний символ розмірності k>0, то f(t₁, …, t_k) є термом.

​

Df. Якщо А – предикатний символ розмірності k, а t₁, …, t_k – терми, то вираз

А(t₁, …, t_k) є атомарною формулою.

Формули логіки предикатів будуються за такими правилами:

1. Атомарна формула – формула.

2. Якщо α - формула, то ¬α - формула.

3. Якщо α і β - формули, то вирази (α∧β),

(α∨β), (α→β) – формули.

Якщо α є формулою, а ξ - змінна, то вирази ∀ξα і ∃ξα - формули.

​

​

Отже, поняття формули повністю визна-чене. Такі формули іноді називають форму-лами першого порядку або формулами мови першого порядку.

Наступний крок – це визначення інтер-претації. Щоб задати інтерпретацію необхід-но:

1. Задати не порожню множину М (носій інтерпретації).

2. Для кожного предикатного символа вказати предикат, визначений на множині М.

​

3. Для кожного функціонального символу вказати функцію з аргументами і значеннями в множині М.

Для кожної інтерпретації формула може приймати значення 1 або 0 згідно з наступ-ними правилами:

1. Якщо задані значення формул α і β, то значення формул ¬α, (α∧β), (α∨β), (α→β) можна одержати з відповідних таблиць.

2. Значення формули (∀x)α рівне 1 ⇔ ко-ли α приймає значення 1 для кожного x∈M.

​

3. Значення формули (∃x)α рівне 1 ⇔ ко-ли α приймає значення 1 хоча б для одного x∈M.

Df. Параметрами (вільними змінними)

- терма є всі змінні, що в нього входять;

- атомарної формули є параметри всіх термів, що в неї входять;

- формули ¬α є параметри формули α;

- формул (α∧β), (α∨β), (α→β) є всі пара-метри формул α і β;

​

- формул (∀x)α і (∃x)α є всі параметри формули α, крім змінної x.

Зазначимо, що формула може мати змін-ну, яка вільно і зв’язано входить в формулу.

Приклад. Розглянемо формули

(∀x) P(x) і (∃x)¬P(x).

Нехай задана інтерпретація:

М = {1,2}, P(1) = 1, P(2) = 0.

Легко бачити, що значення формули (∀x) P(x) є 0 так, як P(2) = 0. Значення формули (∃x)¬P(x) є 1 так, як ¬P(2) = 1 в цій інтерпр.

​

Приклад. Розглянемо формулу

(∀x) (∃y) P(x,y).

Задамо наступну інтерпретацію:

М={1,2}, P(1,1)=1, P(1,2)=0, P(2,1)=0, P(2,2)=1.

Якщо x=1, то існує y (y=1) таке, P(1,y)= 1. Якщо x=2, то існує y (y=2) таке, P(1,y) = 1. Отже, при заданій інтерпретації для кожного x із М існує y таке, що P(x,y) = 1, тобто формула (∀x) (∃y) P(x,y) є істинною в цій інтерпретації.

​

Приклад. Розглянемо формулу

(∀x) (P(x) →Q(f(x),a)).

В цій формулі маємо константу а, одно-місний функціональний символ f, одноміс-ний предикатний символ P і один двохмісний предикатний символ Q.

Нехай маємо наступну інтерпретацію:

М={1,2}, a=1, f(1)=2, f(2)=1, P(1)=0, P(2)=1, Q(1,1)=1, Q(1,2)=1, Q(2,1)=0, Q(2,2)=1.

​

Якщо x=1, то

P(x) →Q(f(x),a) = P(1) → Q(f(1),a) = P(1)→Q(2,1) = 0→0 = 1.

Якщо x=2, то

P(x) →Q(f(x),a) = P(2) → Q(f(2),a) = P(2)→Q(1,1) = 1→1 = 1.

Так як P(x) →Q(f(x),a) істинна для всіх x∈M, то формула (∀x) (P(x) →Q(f(x),a)) істинна в заданій інтерпретації.

​

​

Приклад. В формулі (∀x) P(x,y) парамет-ром (вільною змінною) є змінна y.

В формулі (∀x) P(x,y) ∧ (∀y) Q(y) змінна y є одночасно і вільною і зв’язаною.

В формулі (∀x) P(x,y) змінна x є зв’яза-ною.

Df. Формула називається замкнутою, якщо вона не має параметрів.

Приклад. Формула

(∀x) (∃y) P(x,y)

є замкнутою формулою.

​

Як і у випадку алгебри (логіки) вислов-лювань, можна ввести наступні визначення:

Df. Говорять, що формула G істинна при деякій інтерпретації I, якщо її значення є істиною при цій інтерпретації. При цьому говорять, що I є моделлю формули G.

Df. Говорять, що формула загальнозначи-ма (тавтологія), якщо вона істинна при всіх можливих інтерпретаціях.

​

​

Df. Формула незагальнозначима, якщо вона не є загальнозначимою.

Df. Говорять, що формула суперечлива, якщо вона фальшива при всіх можливих інтерпретаціях.

Df. Формула несуперечлива (виконувана), якщо вона не є суперечливою.

Df. Говорять, що G є логічним наслідком формул F₁, F₂, ..., F_n, якщо для всякої інтер-претації I в якій F₁ ∧ F₂ ∧ … ∧ F_n істинна, G також істинна.

​

Так як в логіці предикатів існує нескін-ченна кількість областей, то відповідно існує

і нескінченна кількість інтерпретацій. Отже, на відміну від алгебри висловлювань, не можна довести загальнозначимість чи супе-речливість формули її оцінкою при всіх можливих інтерпретаціях.

В випадку логіки предикатів потрібна інша процедура або інший метод перевірки загальнозначимості формули.

​

В алгебрі висловлювань ми вводили дві нормальні форми – кон’юнктивну і диз’юнк-тивну. В логіці предикатів теж є нормальні форми. Мета їх введення – спрощення проце-дури доведення загальнозначимості. Одна з них – так звана попередня нормальна форма.

Df. Формула F логіки предикатів знахо-диться в попередній нормальній формі тоді і тільки тоді, коли формула F має вигляд

(Q₁x₁) … (Q_nx_n) (M),

де (Q_ix_i), i=1,…n, є або (∀x_i) або (∃x_i), М -

​

формула, яка не містить кванторів.

(Q₁x₁) … (Q_nx_n) є префіксом , а М – матрицею формули F.

Приклад. Формули

(∀x)(∀y)(P(x,y)∧Q(y)),

(∀x)(∀y)(¬P(x,y)→Q(y)),

(∀x)(∀y)(∃z)(Q(x,y)→R(z))

знаходяться в попередній нормальній формі.

Як перетворити формулу до попередньої нормальної форми?

​

Df. Формули F і G еквівалентні (запису-ється F=G) тоді і тільки тоді, коли істинносні значення цих формул одні і ті ж при будь-яких інтерпретаціях.

Основні пари еквівалентних формул ал-гебри висловлювань будуть, зрозуміло, екві-валентними і логіці предикатів. Крім них існують еквівалентності, що містять кванто-ри. Розглянемо такі еквівалентності.

​

Нехай F є формулою, що містить вільну змінну x. Щоб підкреслити, що вільна змінна x входить в F, будемо записувати F в вигляді F[x]. Нехай G є формулою, яка не містить змінної x. Тоді будемо мати наступні пари еквівалентних формул (де Q є ∀ або ∃):

1. (Qx)F[x]∨G = (Qx)(F[x]∨G),

2. (Qx)F[x]∧G = (Qx)(F[x]∧G),

3. ¬((∀x)F[x]) = (∃x)(¬F[x]),

4. ¬((∃x)F[x]) = (∀x)(¬F[x]).

​

Еквівалентності 1 і 2 істинні, так як G не містить x, а, отже, може бути внесена в область дії квантора Q.

Еквівалентності 3 і 4 можна довести без-посередньо. Нехай I – довільна інтерпретація з областю М. Якщо ¬((∀x)F[x]) істинна в I, то (∀x)F[x] фальшива в I. Це означає, що існує такий елемент e в М, що F[e] фальшива, тобто ¬F[e] істинна в I. Отже, (∃x)(¬F[x]) істинна в I.

​

З іншого боку, якщо ¬((∀x)F[x]) фальши-ва в I, то (∀x)F[x] істинна в I. Це означає, що F[x] істинна для кожного елемента x в М, тобто ¬F[x] фальшива для кожного елемента x в М. Отже, (∃x)(¬F[x]) фальшива в I. Так як ¬((∀x)F[x]) і (∃x)(¬F[x]) завжди приймають одне і те ж істиносне значення для довільної інтерпретації I, то за визначенням

¬((∀x)F[x])=(∃x)(¬F[x]).

Аналогічно доводиться 4.

​

Нехай F[x] і H[x] – формули з вільною змінною x. Тоді справедливі наступні тотожності:

​

5. (∀x)F[x]∧ (∀x)H[x]=(∀x)(F[x]∧H[x]),

6. (∃x)F[x]∨ (∃x)H[x]=(∃x)(F[x]∨H[x]),

​

тобто квантор загальності ∀ і квантор існу-вання ∃ можна розподіляти по ∧ і ∨ відповід-но.

​

В загальному випадку справедливі нас-тупні тотожності:

​

7.(Q₁x)F[x]∨(Q₂x)H[x]=(Q₁x)(Q₂z)(F[x]∨H[z]),

8.(Q₃x)F[x]∧(Q₄x)H[x]=(Q₃x)(Q₄z)(F[x]∧H[z]),

​

де Q₁, Q₂, Q₃, Q₄ є ∀ або ∃, а z не входить в F[x].

Використовуючи тотожності алгебри вис-ловлювань та логіки предикатів можна пере-творити формулу ЛП до нормальної форми.

​

Алгоритм перетворення формул ЛП до попередньої нормальної форми

1. Використовуючи правила

F↔G=(F→G)∧(G→F),

F→G=¬F∨G,

виключити логічні операції ↔, →.

2. Використовуючи правило

¬(¬F)=F,

закони де Моргана і закони

¬((∀x)F[x])=(∃x)(¬F[x]), ¬((∃x)F[x])=(∀x)(¬F[x]),

​

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

3. Перейменовуємо зв’язані змінні, якщо це потрібно.

4. Використовуємо тотожності ЛП 1-6 з тим, щоб винести квантори на початок фор-мули.

Приклад. Привести формулу

(∀x)P(x)→(∃x)Q(x)

до попередньої нормальної форми.

​

​

(∀x)P(x)→(∃x)Q(x) = ¬(∀x)P(x)∨(∃x)Q(x) =

= (∃x)(¬P(x))∨(∃x)Q(x)=

= (∃x)(¬P(x)∨Q(x)).

​

Отже, попередня нормальна форма формули

​

(∀x)P(x)→(∃x)Q(x) є (∃x)(¬P(x)∨Q(x)).

​

Приклад. Привести формулу

(∀x) (∀y)((∃z)P(x,z)∧P(y,z))→(∃u)Q(x,y,u)).

до попередньої нормальної форми.

​

(∀x) (∀y)((∃z)P(x,z)∧P(y,z))→(∃u)Q(x,y,u)) =

​

(∀x)(∀y)(¬((∃z)P(x,z)∧P(y,z)))∨(∃u)Q(x,y,u))=

(∀x)(∀y)((∀z)(¬P(x,z)∨¬P(y,z))∨(∃u)Q(x,y,u))

​

=(∀x)(∀y)(∀z)(∃u)(¬P(x,z)∨¬P(y,z)∨Q(x,y,u).

​

Теорема Ербрана

Як показав Чьорч, не існує ніякої загаль-ної процедури, ніякого алгоритму для пере-вірки загальнозначимості формули логіки предикатів.

Разом з тим, існують алгоритми, які мо-жуть підтвердити, що формула логіки преди-катів є тавтологією, якщо це дійсно так.

В їх основі лежить метод Ербрана, який є основою більшості сучасних алгоритмів пошуку доведень.

​

За визначенням тавтологія – це формула істинна при всіх інтерпретаціях. Ербран роз-робив алгоритм знаходження інтерпретації, яка спростовує дану формулу. Однак, якщо формула справді є тавтологією, то ніякої інтерпретації не існує і алгоритм завершує роботу за скінченну кількість кроків.

Метод Ербрана є основою більшості сучасних алгоритмів пошуку доведень.

​

Скулемівські стандартні форми

​

Подальші процедури пошуку доведень насправді є процедурами спростування, тобто замість доведення загальнозначимості формули доводиться, що її заперечення суперечливе. Це тільки питання зручності.

Крім цього ці процедури використовують так звану “стандартну форму” логічної формули.

​

Використовувались наступні ідеї:

1. Формула логіки предикатів може бути зведена до попередньої нормальної форми (ПНФ).

2. Оскільки матриця не містить кванторів, вона може бути зведена до КНФ.

3. Зберігаючи суперечливість формули, в ній можна елімінувати квантори існування шляхом використання скулемівських функ-цій.

​

Ми вже обговорювали, як звести формулу до попередньої нормальної форми. Ми, та-кож, можемо зводити матрицю до КНФ. Зараз ми поговоримо про те, як елімінувати квантори існування.

Нехай формула F знаходиться в ПНФ

(Q₁x₁) … (Q_nx_n) (M), де М є КНФ і Q_r є квантор існування в префіксі (Q₁x₁) … (Q_nx_n),

1≤r≤n.

​

1. Якщо ніякий квантор загальності не стоїть в префіксі лівіше Q_r , то вибираємо нову константу с, відмінну від інших конс-тант, які входять в М, замінюємо всі x_r, що зустрічаються в М, на с і викреслюємо (Q_rx_r) з префікса.

2. Якщо , …, - список всіх кванторів загальності, що знаходяться лівіше Q_r , 1≤s₁< …< s_m< r, то вибираємо новий функціональ-ний символ f, відмінний від інших, всі x_r в М міняємо на f( , …, ), елімінуємо (Q_rx_r).

​

3. Повторюємо пункти 1 або 2 для всіх кванторів існування в префіксі. Остання з одержаних формул є скулемівською стан-дартною формою (або просто стандартною формою) формули F.

Константи і функції, що використовують-ся для заміни змінних квантора існування, називаються скулемівськими функціями.

​

​

Приклад. Одержати стандартну форму для формули

(∃x)(∀y)(∀z)(∃u)(∀v)(∃w) P(x,y,z,u,v,w).

В цій формулі лівіше (∃x) нема ніяких кванторів загальності, лівіше (∃u) стоять (∀y) і (∀z), лівіше (∃w) стоять (∀y) і (∀z) і (∀v). Отже, замінюємо змінну x на константу а, змінну u – на двомісну функцію f(y,z), змінну w – на тримісну функцію g(y,z,v). Таким чином одержимо стандартну форму

(∀y)(∀z)(∀v) P(а,y,z, f(y,z),v, g(y,z,v)).

​

Приклад. Одержати стандартну форму для формули

(∀x)(∃y)(∃z) ((¬P(x,y) ∧ Q(x,z)) ∨ R(x,y,z)).

​

Спочатку зведемо матрицю до КНФ:

(∀x)(∃y)(∃z)((¬P(x,y)∨R(x,y,z))∧(Q(x,z)∨ R(x,y,z))).

Змінні y, z замінюємо одномісними функці-ями f(x), g(x) відповідно. Одержимо СФ

(∀x)((¬P(x,f(x))∨R(x,f(x),g(x)))∧(Q(x,g(x))∨ R(x,f(x),g(x)))).

​

Df. Диз’юнкт є диз’юнкція літер.

Іноді будемо розглядати множину літер, як синонім диз’юнкту. Наприклад, P∨Q∨¬R = {P, Q, ¬R}.

Df. Диз’юнкт, що містить r літер, назива-ється r-літерним диз’юнктом. Диз’юнкт, що не містить літер, називається пустим диз’юнктом і позначається .

Диз’юнкції ¬P(x,f(x))∨R(x,f(x),g(x)) і Q(x,g(x))∨ R(x,f(x),g(x)) в стандартній формі з останнього прикладу суть диз’юнкти.

​

Будемо вважати, що множина диз’юнктів S є кон’юнкцією всіх диз’юнктів із S, де кожна змінна вважається керованою кванто-ром загальності. При такій домовленості стандартна форма може задаватись множи-ною диз’юнктів. Наприклад, стандартна форма з останнього прикладу може бути задана множиною:

{¬P(x,f(x))∨R(x,f(x),g(x)), Q(x,g(x))∨ R(x,f(x), g(x))}.

​

Теорема. Нехай S – множина диз’юнктів, які задають стандартну форму формули F. Тоді F суперечлива тоді і тільки тоді коли S суперечлива.

Доведення. Будемо вважати, що F знахо-диться в ПНФ, тобто F = (Q₁x₁) … (Q_nx_n) M[x₁, … , x_n] (M[x₁, … , x_n] означає, що матриця М містить змінні x₁, … , x_n). Нехай Q_r – перший квантор існування і

F₁ = (∀x₁)…(∀x_r-1) (Q_r+1x_r+1) … (Q_nx_n) M[x₁, …, x_r-1, f(x₁, …, x_r-1), x_r+1, … x_n],

​

де f – скулемівська функція для x_r, 1≤r≤n. Ми хочемо показати, що F суперечлива тоді і тільки тоді, коли F₁ суперечлива.

Нехай F суперечлива. Якщо F₁ несупереч-лива, то існує інтерпретація I така, що F₁ істинна в I. Тобто, формула (Q_r+1x_r+1) … (Q_nx_n) M[x₁, …, x_r-1, f(x₁, …, x_r-1), x_r+1, … x_n] буде істинною в I для всіх x₁, …, x_r-1. Отже, для всіх x₁, …, x_r-1 буде існувати x_r (= f(x₁, …, x_r-1)) для якого (Q_r+1x_r+1) … (Q_nx_n)M[x₁, …,x_r-1, x_r, x_r+1, … x_n] істинна.

​

Таким чином, F суперечлива. Отже, F₁ повинна бути суперечливою.

З іншого боку, припустимо, що F₁ супе-речлива. Якщо F несуперечлива, то існує інтерпретація I така, що для всіх x₁, …, x_r-1 буде існувати x_r для якого (Q_r+1x_r+1) … (Q_nx_n) M[x₁, …,x_r-1, x_r, x_r+1, … x_n] істинна в I. Розши-римо I, включаючи функцію f, яка відобра-жає x₁, …,x_r-1 в x_r . Позначимо це розширення через I′.

​

Зрозуміло, що для всіх x₁, …, x_r-1 формула (Q_r+1x_r+1) … (Q_nx_n) M[x₁, …,x_r-1, f(x₁, …, x_r-1), x_r+1, … x_n] буде істинною в I′, тобто F₁ істин-на в I′, що суперечить припущенню про те, що F₁ суперечлива. Отже, F повинна бути суперечливою.

Аналогічно у випадку декількох кван-торів існування.

​

Якщо F суперечлива, то за попередньою теоремою F=S. Якщо F несуперечлива, то взагалі кажучи, F≠S. Наприклад, якщо

F = (∃x)P(x), то стандартна форма цієї формули є S=P(a). Але в інтерпретації I з носієм М={1,2}, значеннями для предиката Р(1) = 0, Р(2)=1, значенням для константи а=1формула F буде істинною в I, а S – фальшивою. Таким чином F≠S.

​

Зауваження. Якщо F=F₁∧ …∧ F_n, то ми можемо побудувати множини S_i диз’юнктів, де кожна S_i є стандартною формою F_i.

Якщо S = S₁∪ … ∪S_n, то можна показати (за аналогією з попередньою теоремою), що F суперечлива тоді і тільки тоді, коли S суперечлива.

​

​

Приклад. Як довести наступне тверд-ження: якщо xx=e для всіх х в групі G, то G комутативна, де e – одиниця групи.

Формалізуємо це твердження мовою ло-гіки предикатів разом з деякими основними аксіомами теорії груп, а потім подамо запе-речення цього твердження множиною диз’юнктів.

Група задовольняє наступним аксіомам:

​

А₁. Якщо x,y ∈G, то xy∈G (властивість замкнутості)

А₂. Якщо x,y,z ∈G, то x(yz)=(xy)z (асоціативність).

А₃. Існує e∈G таке, що xe=ex=x для всіх x∈G (існування одиниці).

А₄. Для кожного x∈G існує елемент

х^-1∈ G такий, що х х^-1= х^-1х=e (існування оберненого елемента).

​

Нехай P(x,y,z) позначає предикат xy=z, а i(x) позначає х^-1. Тоді аксіоми А₁-А₄ можна переписати у вигляді формул ЛП:

А₁. (∀х)(∀y)(∃z) P(x,y,z)

A₂. (∀x)(∀y)(∀z)(∀u)(∀v)(∀w)(P(x,y,u)∧

P(y,z,v)∧P(u,z,w)→P(x,v,w)) ∧

(∀x)(∀y)(∀z)(∀u)(∀v)(∀w)(P(x,y,u)∧

P(y,z,v)∧P(x,v,w)→P(u,z,w))

A₃. (∀x)P(x,e,x)∧(∀x)P(e,x,x)

A₄. (∀x)P(x,i(x),e)∧(∀x)P(i(x),x,e)

​

Саме твердження може бути представле-не наступною формулою ЛП:

В. (∀x)P(x,x,e)→((∀u)(∀v)(∀w)(P(u,v,w)

→ P(v,u,w)))

Тепер наше твердження може бути пред-ставлене формулою F = A₁∧ … ∧ A₄ → B. Отже, ¬F = A₁∧ … ∧ A₄∧ ¬B.

Для того, щоб одержати множину диз’юнктів S для ¬F, одержимо множини диз’юнктів S_i для кожної з аксіом A₁-A₄ та твердження В відповідно.

Будемо мати

S₁. {P(x,y,f(x,y))};

​

S₂. {¬P(x,y,u)∨¬P(y,z,v)∨¬P(u,z,w)∨

P(x,v,w), ¬P(x,y,u)∨¬P(y,z,v)∨

¬P(x,v,w)∨ P(u,z,w)};

​

S₃. {P(x,e,x), P(e,x,x)};

​

S₄. {P(x,i(x),e), P(i(x),x,e).

​

Так як

¬В = ¬((∀x)P(x,x,e)→((∀u)(∀v)

(∀w) (P(u,v,w)→ P(v,u,w)))) =

¬(¬(∀x)P(x,x,e)∨ ((∀u)(∀v)(∀w)

(¬P(u,v,w)∨ P(v,u,w)))) = (∀x)P(x,x,e)∧

¬((∀u)(∀v)(∀w) (¬P(u,v,w)∨ P(v,u,w))) =

(∀x)P(x,x,e)∧ (∃u)(∃v)(∃w)(P(u,v,w) ∧

¬P(v,u,w)), то множина диз’юнктів для

¬В є наступною:

T. {P(x,x,e), P(a,b,c), ¬P(b,a,c)}.

​

​

Таким чином, множина S = S₁∪ … ∪S₄∪T є множиною з десяти диз’юнктів:

1. P(x,y,f(x,y)),

2. ¬P(x,y,u)∨¬P(y,z,v)∨¬P(u,z,w)∨

P(x,v,w),

3. ¬P(x,y,u)∨¬P(y,z,v)∨ ¬P(x,v,w) ∨

P(u,z,w),

4. P(x,e,x),

5. P(e,x,x),

​

6. P(x,i(x),e),

7. P(i(x),x,e),

8. P(x,x,e),

9. P(a,b,c),

10. ¬P(b,a,c).

​

В цьому прикладі ми показали, як одер-жати множину диз’юнктів S для формули ¬F. Крім того, формула F тавтологія тоді і тільки тоді, коли S суперечлива.

​

Ербранівський універсум множини диз’юнктів

За визначенням множина диз’юнктів суперечлива тоді і тільки тоді, коли вона фальшива при всіх інтерпретаціях на всіх областях. Так як неможливо розглянути всі інтерпретації на всіх областях, було б дуже зручно зафіксувати одну область H таку, що S суперечлива тоді і тільки тоді, коли S фальшива при всіх інтерпретаціях на цій області.

​

На щастя така область існує і називається ербранівським універсумом множини S.

Df. Нехай H₀ – множина констант, які зустрічаються в S. Якщо ніяка константа не зустрічається в S, то покладають H₀ = {a}. Для i=0, 1, 2, … нехай H_i+1 є об’єднання H_i і множини всіх термів fⁿ(t₁, ... ,t_n), що зустрі-чаються в S, де t_j належать H_i.

Кожне H_i називається множиною кон-стант i-го рівня для S, а H_∞ називається ербранівським універсумом S.

​

Приклад. Нехай S = {P(a), ¬P(x)∨P(f(x))}.

​

Тоді

H₀ = {a},

H₁ = {a, f(a)},

H₂ = {a, f(a), f(f(a))},

. . . . . . . . . . . . . . . . .

H_∞ = {a, f(a), f(f(a)), f(f(f(a))), … }

​

Приклад. Нехай S = {P(f(x), a, g(y), b}.

Тоді

H₀ = {a, b},

H₁ = {a, b, f(a), f(b), g(a), g(b)},

H₂ = {a, b, f(a), f(b), g(a), g(b), f(f(a)),

f(f(b)), g(f(a)), g(f(b)), g(g(a)), g(g(b))},

. . . . . . . . . . . . . . . . .

H_∞ = . . . . . . . .

​

Df. Множина атомів виду P(t₁, ... ,t_n) для всіх предикатів, що зустрічаються в S, нази-вається ербранівським базисом S, де t_i – елементи ербранівського універсума.

Df. Основним прикладом диз’юнкта C множини S є диз’юнкт, одержаний заміною змінних в С на елементи ербранівського універсуму.

Приклад. Якщо S = {P(x), Q(f(y))∨R(y)}, то P(a), P(f(f(a))) основні приклади диз’юнкту C=P(x).

​

Нехай S – множина диз’юнктів, H – ер-бранівський універсум S і I – інтерпретація S над Н.

Df. Говорять, що I є H-інтерпретація множини S, якщо вона задовольняє наступ-ним умовам:

1. I відображає константи в самих себе.

2. Якщо f – n-місний функціональний символ і h₁, …, h_n – елементи H, то в I через f позначається функція, яка відображає h₁, …, h_n в f(h₁, …, h_n).

​

При цьому не виникає ніяких обмежень при інтерпретації предикатних символів з S.

Якщо А = {A₁, A₂, …, A_n, …} – ербранів- ський базис множини S, то H-інтерпретацію I зручно подавати у вигляді

I = {m₁, m₂, …, m_n, … },

де m_j є або А_j або ¬А_j для j=1,2, … При цьому, якщо m_j є А_j, то значення атома А_j дорівнює 0, в іншому випадку – 1.

​

Приклад. Розглянемо множину S = {P(x) ∨ Q(x), R(f(y))}.

Ербранівський універсум H для S є H = {a, f(a), f(f(a)), …}.

В S входять три предикатні символи: P, Q, R. Отже, ербранівський базис S є A = {P(a), Q(a), R(a), P(f(a)), Q(f(a)), R(f(a)), …}.

H-інтерпретаціями множини S можуть бути:

I₁={P(a), Q(a), R(a), P(f(a)), Q(f(a)),R(f(a)),…},

I₂={P(a), Q(a), ¬R(a), P(f(a)), Q(f(a)), ¬R(f(a)), …}.

​

Інтерпретацію множини диз’юнктів S не обов’язково задавати над ербранівським універсумом – інтерпретація може не бути H-інтерпретацією. Наприклад, якщо S = {P(x), Q(y,f(y,a))}, то можлива наступна інтерпре-тація над областю D={1,2}: a=2, f(1,1)=1, f(1,2)=2, f(2,1)=2, f(2,2)=1, P(1) = 1, P(2) = 0, Q(1,2)=1, Q(2,1)=0, Q(2,2)=1.

Для такої інтерпретації можна визначити H-інтерпретацію I*, що відповідає I.

​

Наприклад, ербранівський базис поперед-ньої множини диз’юнктів S є:

A={P(a), Q(a,a), P(f(a,a)), Q(a,f(a,a)), Q(f(a,a),a), Q(f(a,a),f(a,a)), …}.

Оцінюємо кожний член А, використовую-чи попередню інтерпретацію:

P(a) = P(2) = 0, Q(a,a)=Q(2,2)=1,

P(f(a,a))=P(f(2,2))=P(1)=1,

Q(a,f(a,a))=Q(2,f(2,2))=Q(2,1)=0,

Q(f(a,a),a)=Q(f(2,2),2)=Q(1,2)=1,

Q(f(a,a),f(a,a))=Q(f(2,2),f(2,2))=Q(1,1)=0.

​

Отже, H-інтерпретація I*, що відповідає I є I*={¬P(a), Q(a,a), P(f(a,a)), ¬Q(a, f(a,a)),

Q(f(a,a),a), ¬Q(f(a,a),f(a,a)), …}.

Якщо в S відсутні константи, то елемент а, який використовується для побудови ер-бранівського універсуму, може бути відобра-жений в довільний елемент області D. В цьо-му випадку, якщо D більш як одноелементна, то існує більше однієї H-інтерпретації, що відповідає I.

​

Df. H-інтерпретацією I*, що відповідає I, є інтерпретація, яка задовольняє наступним умовам: нехай h₁, …, h_n – елементи ербра-нівського універсуму H, які відображаються в елементи d_i з D. Якщо P(d₁, …, d_n) має значення 1(0) в інтерпретації I, то P(h₁, …, h_n) теж має значення 1(0) в I*.

Твердження. Якщо інтерпретація I на області D задовольняє множині дизюнктів S, то довільна H-інтерпретація I*, що відповідає I,теж задовольняє S.

​

Теорема. Множина диз’юнктів S супе-речлива тоді і тільки тоді, коли S фальшива при всіх H-інтерпретаціях в S.

Доведення. (⇒). Доведення в цю сторону очевидне, так як за визначенням S супереч-лива тоді і тільки тоді, коли S фальшива при всіх інтерпретаціях на будь-якій області.

(⇐). Припустимо, що S фальшива при всіх H-інтерпретаціях в S. Якщо S не супе-речлива, то існує інтерпретація I на деякій області D така, що S істинна при I.

​

За попереднім твердженням S істинна при інтерпретації I*, що відповідає I. А це супе-речить тому, що S фальшива при всіх H-інтерпретаціях. Отже, S повинна бути суперечливою.

Таким чином, для перевівки суперечли-вості множини диз’юнктів, необхідно роз-глядати тільки H-інтерпретації.

Далі, говорячи про інтерпретацію, будемо мати на увазі H-інтерпретацію.

​

Твердження. Множина диз’юнктів супе-речлива тоді і тільки тоді, коли для кожної інтерпретації I існує по крайній мірі один основний приклад С′ деякого диз’юнкта C з S, фальшивий в інтерпретацї I.

Приклад (a). Розглянемо диз’юнкт

C = ¬P(x) ∨Q(f(x)).

Нехай маємо інтерпретації:

I₁={¬P(a), ¬Q(a), ¬P(f(a)), ¬Q(f(a)), ¬P(f(f(a))), ¬Q(f(f(a))), …};

​

I₂={P(a), Q(a), P(f(a)), Q(f(a)), P(f(f(a))), Q(f(f(a))), …};

I₃={P(a), ¬Q(a), P(f(a)), ¬Q(f(a)), P(f(f(a))), ¬Q(f(f(a))), …};

Диз’юнкт С істинний в інтерпретаціях I₁ та I₂ і фальшивий в інтерпретації I₃.

(b) Нехай S={P(x), ¬P(a)}. Існують дві H-інтерпретації :

I₁ = {P(a)} і I₂ = {¬P(a)}.

На підставі останнього твердження S – суперечлива.