Проблема розв’язності логіки предикатів
1)Постановка проблеми:
Чи існує алгоритм, який дозволяв би за видом формули логіки предикатів судити про те, який її характер (наприклад, тавтологія це чи формула лише здійсненна).
Як підтверджено (1936 р., Черч), проблема має негативний відповідь, тобто. логіка предикатів нерозв'язна.
2) Причина нерозв'язності полягає в наявності нескінченних предметних областей і, взагалі кажучи, різна поведінка формули на нескінченній і кінцевій множині. Так, наприклад, існує формула, здійсненна на нескінченній множині, але не здійсненна на жодній кінцевій множині.
3) Проте за певних «судженнях» логіки предикатів, ми отримуємо розв'язання зазначеної проблеми. Приміром, якщо розглядати лише кінцеві предметні області М=< a1, a2,…. am >, то в цьому випадку логіка предикатів буде розв'язаною. Це випливає із наступної теореми.
Теорема.Для будь-якого предикату Р(х) мають місце рівносильності: (xР(х))ó(P(a1)/\P(a2)/\./\P(am)) (1 )
( хР(х))ó(Р(a1) \/P(a2) \/. \/P(am)) (2)
Сенс твердження у цьому, що кванторні операції на кінцевих множинах є заможними, а виражаються через логічні зв'язки /\, \/.
Доказ.Доведемо (1), (2) - аналогічно.
а) Р(х) – тотожно правдивий на М. І тут обидві частини (1) приймають значення істини.
б) Інакше, будь-якого Р(х) є хибне висловлювання, а й у правій частині (1) у складі кон'юнкції є «хибний компонент», тобто. кон'юнкція є брехня.
В обох можливих випадках набули висловлювання однакового значення істинності, чим і довели рівносильність (1). Тепер будь-яка формула на кінцевій множині, відповідно до теореми (1), може бути«звільнено» від кванторних операцій. Але в цьому випадку кожен компонент, що входить у формулу, на елементах кінцевої множини може реалізуватися тільки як істина або брехня, а, значить, механізм таблиці істинності у випадку кінцевого М виявляється застосовним, тим самим визначається характер формул, а, значить, позитивно вирішена зазначена проблема.
4) Виявляється, як і логіка одномісних предикатів теж можна розв'язати, т.к. обмежившись лише одномісними предикатами, ми можемо проблему звести випадку кінцевих множин (без докази).
5) Отже, логіка предикатів не суперечлива тому, що неспроможна формула бути тавтологією і спростованою (суперечністю і здійсненної). Логіка предикатів повна теорія, тобто. кожна формула або є тавтологія, або спростовується. Нарешті, вона нерозв'язна, тобто. немає єдиного відповідного алгоритму. Однак це не означає, що для конкретної формули не можна знайти прийому для визначення її характеру: просто цей прийом буде застосовний до неї безпосередньо або до цілого класу формул, але не до всієї логіки загалом.
Поняття обчислення предикатів (ІП).
1) Синтаксис теорії той самий, як і синтаксис логіки предикатів.
Синтаксис - алфавіт та поняття формули:
Предметна змінна, предикатна змінна 0 місцева, n – місцева, логічні зв'язки, ┐,→ та символи , .
Формула – це предикатна змінна, а так само якщо P і Q – формули, то P→Q, xP, xQ – формули, де в останніх двох випадках x має вільно входити до формул P та Q.
2) Аксіоми теорії, які приймаються як формули, що виводяться спочатку:
б) а також аксіоми (xP(x))→P(t) і P(t)→(xP(x)).
3) Правило висновки інших формул:
Б) Ще два правила:
-Якщо B→P(x) виводиться, то B→( xP(x))виведено.
- Якщо B→P(x) виводиться, то ( xP(x))→B виводиться.
Виведення формули в ЛП перетворюється на властивості її тавтологічності. Зокрема, аксіоми ІП, які застосовуються як виведені формули, в ЛП як легко перевірити, виявляються тавтологіями.
Правила виведення в ІП перетворюються на ЛП на правила побудови нових тавтологій.
5)Метатеорія.
а) ІП не суперечлива;
б) ІП повна, у тому сенсі, що кожна формула ІП або виведена, або не має цієї властивості.
в) ІП нерозв'язна теорія (інакше всі її семантики були нерозв'язні, а це неправильно через нерозв'язність ЛП).