7.6. Аксіоми числення предикатів. Формальне виведення

Числення предикатів є аксіоматичною системою. Тому в численні предикатів, як і в численні висловлювань, формалізується не лише запис предикатів (у вигляді формул, а й задаються аксіоми й правила перетворення формул для виділення вивідних формул з множини всіх формул. Аксіомами числення предикатів є аксіоми числення висловлювань (певного його різновиду), а правилами виведення — відповідні правила числення висловлювань. Проте оскільки числення предикатів порівняно з численням висловлювань має свою специфіку (в ньому використовують квантори загальності й існування), то вводяться ще дві аксіоми, пов’язані з ними (в аксіомах не виключається, що в формули входять, крім зв’язаної змінної х і вільної змінної y, інші вільні змінні):

: ;

: ,

де — будь-яка предикатна формула, яка містить вільну змінну х.

Якщо серед правил виведення є правило висновку (modus popens), то воно формулюється так само, як і в численні висловлювань, але набір формул, до яких його застосовують, значно ширший. Також в численні предикатів вводять правила введення квантора загальності й вилучення квантора існування:

;

,

де формула містить вільну змінну х, а формула F не містить.

У численні предикатів, як і в численні висловлювань, поряд з раніше доведеними формулами, для спрощення доведень можуть використовуватися й інші, допоміжні, правила виведення. Наприклад, правило узагальнення: , де формула F не містить вільної змінної х; правило перейменування вільних змінних: якщо у формулі предметна змінна х є вільною і жодне її входження не міститься в області дії квантора за змінною y, то з вивідності формули випливає вивідність формули , де одержуємо, замінюючи в усі вільні входження х на y; правило перейменування зв’язаних змінних: якщо формула не містить вільних входжень предметної змінної у і містить вільні входження предметної змінної х, жодне з яких не входить в область дії квантора за змінною у, то з вивідності формули випливає вивідність формули (де — будь-який з кванторів чи , а одержуємо, замінюючи в усі вільні входження х на y). Правила перейменування вільних і зв’язаних змінних можна подати формулами: , , .

Приклад 7.17. Доведемо, що формула є теоремою числення предикатів. При цьому, крім правил, введених при розгляді числення предикатів, скористаємося також правилами, які ми розглядали в численні висловлювань:

1) у схему аксіом К2 замість предиката F підставимо предикат Р з відповідними змінними і застосуємо правило контрапозиції (див. приклад 6.46). Одержимо:

;

2) до результату пункту 1 застосуємо правило введення квантора загальності , матимемо:

;

3) до висновку пункту 2 застосуємо правило перейменування зв’язаних змінних:

;

4) до результатів пунктів 2 і 3 застосуємо правило силогізму (див. п. 6.5, наслідок 3 з теореми дедукції). Одержимо:

,

що й треба було довести.

Приклад 7.18. Нехай засновками є твердження “Усі, хто має властивість Р, має й властивість Q”, а також “y має властивість Р”. Треба довести, що висновком буде твердження “y має властивість Q”. Предикатний запис задачі має вигляд:

.

При доведенні використаємо аксіому К1 і правило modus popens:

1) — засновок I;

2) — засновок II;

3) у схему аксіом К1 замість підставимо :

;

4) за правилом modus popens , беручи замість формули результат пункту 3, а замість атомарної формули Р засновок I, матимемо:

;

5) за правилом modus popens, беручи замість формули результат пункту 4, а замість атомарної формули Р засновок II, одержимо , що й треба було довести.

Приклад 7.19. Нехай предикатні формули F і G не містять вільної змінної х. Доведемо, що :

1) F — засновок I;

2) — засновок II;

3) до засновку I застосуємо правило узагальнення і матимемо ;

4) за правилом modus popens , беручи замість формули засновок II, а замість атомарної формули Р результат пункту 3, матимемо G;

5) до результату пункту 4 застосуємо правило узагальнення і одержимо .

Теорема 7.1 (Геделя³ про повноту числення предикатів). Будь-яка теорема числення предикатів є тавтологією і будь-яка тавтологія вивідна в численні предикатів.

Основною проблемою будь-якого формального числення є знаходження ефективного алгоритму розв’язання задачі, чи є вивідною дана формула в заданій аксіоматичній формальній системі. Якщо такий алгоритм існує, то формальну систему називають розв’язною. Числення висловлювань є розв’язною системою, оскільки для перевірки тавтологічності будь-якої його формули можна застосувати метод таблиць істинності (систему обчислень; див. п. 6.3) чи еквівалентні перетворення (див. п. 6.4). Для встановлення тотожної істинності формули числення предикатів треба перевірити її істинність на всіх інтерпретаціях в області визначення, яка може містити й нескінченну кількість елементів. Таким чином, в теорії предикатів єдиним методом дослідження істинності формул є застосування формального виведення. Числення предикатів називають нерозв’язним, оскільки не існує загального алгоритму доведення істинності формул, який для довільної формули G і довільної множини формул розв’язував би задачу вивідності формули G із формул , , …, за законами логіки предикатів.

Незважаючи на нерозв’язність числення предикатів, його застосовують при розв’язуванні практичних задач. Так, якщо відомо, що формула G вивідна із формул , , …, , то існують алгоритми, які це підтверджують. Якщо ж із формул , , …, формула G не виводиться, то ті самі алгоритми не завжди це можуть встановити. Але й сама можливість доведення теореми теж є досить важливою.