(b) «Wx=Wy «. (Указівка. Зведіть до цієї проблеми проблему «функція фx тотальна».)
(c) «фx(х)=0».
(d) «фx(y)=0».
(e) «х Î Еу «.
(f) «функція фx тотальна і постійна».
(g) «Wx=Æ».
(h) «множина Еx нескінченна».
(i) «фх=g», де g є будь-яка фіксована обчислювана функція.
2. Покажіть, що не існує тотальної обчислюваної функції f (x, у), що володіє наступними властивістями: якщо програма Рх(у) зупиняється, те це відбувається за f (x, у) чи менше кроків (Указівка. Покажіть, що якби така функція існувала, те проблема зупинки булаб розв'язна.)
Можливість розв'язання і нерозв'язання в інших областях математики. У багатьох областях математики виникають проблеми загального характеру, для яких має сенс неформальне поняття можливості розв'язання. Звичайно такі проблеми стосуються кінцевих об'єктів деякої конкретної області. У цьому випадку поняттю можливості розв'язання тієї чи іншої властивості, що стосується цих об'єктів, можна надати точний зміст, використовуючи придатне кодування натуральними числами.
Виявленню розв'язних і нерозв'язних проблем у самих різних математичних ситуаціях присвячено багато досліджень.
1. Логіка висловлень (пропозиційна логіка) [1] – одна з базових теорій математичної логіки, на якій базуються більш складні формальні логіки.
Алфавіт логіки висловлень (ЛВ) складається зі зчисленної множини елементарних висловлень, які позначуються літерами (можливо, з індексами) і 5 логічних операцій: заперечення (^), кон’юнкції (/\, або &), диз’юнкції (\/), імплікації (->) і тотожності, еквівалетності (<->), які задаються скінченими таблицями істинності.
Як відомо, кожне висловлення може мати значення істинно (позначається Т, 1), або хибно (позначається F, 0).
Алфавіт висловлень дає змогу будувати складні висловлення (формулу) із простіших за допомогою логічних операцій [1] по наступній рекурсивній схемі, а саме, формулами ЛВ є тільки наступні конструкції:
– кожне висловлення є формулою;
– якщо А і В є формули, то ^A, (A/\B), (A\/B), (A -> B) i (Aя2=я0B) – є формулами.
Формули задають синтаксис мови ЛВ. А який сенс, семантика цієї мови?
Вона задається за допомогою інтерпретацій. Інтерпретація – це відображення I, що зпівставляє кожному елементарному висловленню р деяке значення істинності. Інтерпретацію I, що задана на множині елементарних висловлень, природнім чином можна продовжити на множину формул за допомогою таблиць істинності. Інтерпретація, при якій істиносне значення формули А є істинно, називається моделлю цієї формули.
Літера, або літерал – це елементарне висловлення р або його заперечення ^p. Літери р і ^р є протилежні.
Формула ЛВ називається виконуваною, якщо вона допускає деяку модель, тобто її можна інтерпретувати із значенням Т.
Формула ЛВ А називається суперечністю (не виконуваною), якщо А = F для всіх моделей А (наприклад, (р/\^p).
Формула ЛВ називається тавтологією, якщо вона істина при всіх інтерпретаціях (на всіх моделях). Відмітимо, що заперечення тавтології є суперечність.
2. Нехай, Е – множина формул ЛВ. Формула А є наслідком (логічним) з Е (позначення, Е (= А), якщо на всіх моделях, на яких істині всі формули з Е, істина також формула А. Ясно, що тавтологія є наслідком із пустої множини формул ЛВ.
Легко довести [1], що мають місце:
Твердження 1. Нехай, Е = {H1, H2,… Hn} є множиною формул ЛВ.
Формула А є наслідком (логічним) з Е (E (= A) тоді і тільки тоді, коли імплікація:
(H1/\H2/\…/\Hn) -> A
є тавтологією. Прямим наслідком із твердження 1 є
Твердження 2. Нехай, Е = {H1, H2..Hn} є множиною формул ЛВ.
Формула А є наслідком (логічним) з Е тоді і тільки тоді, коли формула
(H1/\H2/\…/\Hn/\^A)
є суперечністю.
Диз’юнктом називається диз’юнкція скінченного числа літералів, тобто формула виду
(L1\/L2\/..\/Lm).
Її часто записують у «скороченому» вигляді як послідовність літералів: {L1., Lm}.Пустий диз’юнкт – єдиний диз’юнкт, що не виконується, і його позначають через Л.
Кон’юктивною нормальною формою (КНФ) називається кон’юнкція скінченої кількості диз’юнктів.
Теорема 1. Довільна формула ЛВ має логічно еквівалентну їй КНФ.
Наступний алгоритм нормалізації формул ЛВ дає доведення теореми 1.
Етап 1. Спочатку замінюємо (А<->В) на ((А->B)/\(B->A)), а потім заміняємо (U->V) на (^U\/V). Це робиться для виключення операцій <-> і ->.
Етап 2. Необхідну кількість раз застосовуються перетворення на основі законів де Моргана:
^(X/\Y) ==> (^X\/^Y), ^(X\/Y) ==> (^X/\^Y).
Символ ==> означає «замінити на». В цій заміні подвійні заперечення елімінуються, тобто
^^X ==> X.
На цій стадії операція заперечення залишається тілки безпосередньо перед висловленнями.
Етап 3. необхідну кількість разів застосовуються правила перетворень, що виведені із законів дистрибутивності:
X \/ (Y /\ Z) ==> (X \/ Y) /\ (X \/ Z)
(X /\ Y) \/ Z ==> (X \/ Z) /\ (Y \/ Z).
Етап 4. Диз’юнкти, що містять протилежні літерали (тобто висловлення і його заперечення), є тавтологіями і можуть бути еліміновані. Також елімінуються повторення літералів у межах одного ж і того диз’юнкта.
Формула, що отримується в кінці четвертого етапу, і є КНФ, яка еквівалентна вихідній формулі ЛВ.
Відмітимо, що диз’юнкт є тавтологією тоді і тільки тоді, коли він містить пару протилежних літералів. КНФ є тавтологією тоді і тільки тоді, коли всі її диз’юнкти – тавтології.
Єдиним не виконуваним диз’юнктом є пустий диз’юнкт Л.
3. Не існує загального ефективного критерію для перевірки виконуваності КНФ. Але існує зручний метод для виявлення не виконуваності множини диз’юнктів. Дійсно, множина диз’юнктів є не виконувані тоді і тілки тоді, коли пустий диз’юнкт Л є логічним наслідком із неї. Таким чином, не виконуваність множини S можна перевірити, породжуючи логічні наслідки з S, поки не отримаємо пустий диз’юнкт. Для цього використовується наступна схема міркувань.
Припустимо, що дві формули (A \/ X) i (B \/ ^X) – істині. Якщо Х також істина, то звідси випливає, що B істина. Навпаки, якщо Х хибна, то А істина, тобто отримується правило
{(A \/ X), (B \/ ^X)} [= A \/ B,
яке можна записати у вигляді
{^X -> A, X -> B} [= A \/ B. Зокрема, якщо Х – висловлення, а A i B – диз’юнкти, то правило називається правилом резолюції.
Твердження 3. Нехай s1 i s2 – диз’юнкти КНФ S. Якщо літерал р входить у s1 і ^p – у s2, то диз’юнкт
r = (s1\{p}) \/ (s2\{^p})
є логічним наслідком КНФ S.
Тут через si\{L} позначається диз’юнкт, що отримується з si вилученням літералу L. Диз’юнкт r називається резольвентою диз’юнктів s1 i s2.
Твердження 4. Нормальні форми S i (S /\ r) еквівалентні.
Доведення невиконувансті формул дуже важливо для роботи із знаннями. Воно широко використовується в логічному програмуванні. З твердження 3 і 4 випливає наступний алгоритм – метод резолюцій для доведення того, що КНФ S є суперечністю.
Метод резолюцій
Крок 1. Якщо Л належить S, то КНФ S є суперечністю, і алгоритм зупиняється.
Крок 2. Вибираються довільні L, s1, s2 такі, що літерал L входить в диз’юнкт s1, а ^L входить у s2.
Крок 3. Обчислюється резольвента r.
Крок 4. КНФ S замінюється на КНФ S' = S /\ r, і повертаються на крок 1. Вибираються довільні L, s1, s2 такі, що літерал L входить в диз’юнкт s1, а ^L входить у s2.
Твердження 5. Якщо нормальна форма S є невикнуваною формулою, тобто суперечністю, то цей факт завжди можна виявити за допомогою метода резолюцій.
1. Необхідно побудувати кон’юктивну нормальну форму для формули А логіки висловлень, де
A = (p -> (q -> r)) -> ((p /\ s) -> r).
Використаємо алгоритм із розділу 1.2. Кожна з нижченаведених формул еквівалентна А.
Етап 1 (виключення імплікацій).
(p -> (q -> r)) -> ((p /\ s) -> r),
^ (p -> (q -> r)) \/ ((p /\ s) -> r),
^ (^p \/ (q -> r)) \/ (^(p /\ s) \/ r),
^ (^p \/ (^q \/r)) \/ (^(p /\ s) \/ r),
Етап 2.
(^ ^p /\ ^ (^q \/r)) \/ ((^p \/ ^s) \/ r),
(^ ^p /\ (^ ^q /\ ^r)) \/ ((^p \/ ^s) \/ r),
(p /\ (q /\ ^r)) \/ ((^p \/ ^s) \/ r).
Етап 3.
a) (p \/ ((^p \/ ^s) \/ r)) /\ ((q /\ ^r) \/ \/ ((^p \/ ^s)
\/ r))
b) (p \/ (^p \/ ^s) \/ r)) /\ /\ (q \/ (^p \/ ^s) \/ r) /\
(^r \/ (^p \/ ^s) \/r);
c) (p \/ ^p \/ ^s \/ r) /\ /\ (q \/ ^p \/ ^s \/ r) /\ (^r
\/ ^p \/ ^s \/ r);
d) T /\ (q \/ ^p \/ ^s \/ r) /\ T;
e) (q \/ ^p \/ ^s \/ r).
Ми отримали, що КНФ В = (q \/ ^p \/ ^s \/ r) формули А складається з одного диз’юнкта.
Приклад
2. Необхідно перевірити за допомогою метода резолюцій, чи є КНФ S суперечністю, де
S = {p \/q, p /\ r, ^q \/ ^r, ^p}.
Диз’юнкти зручно перенумерувати. Отримаємо список:
1. p \/q
2. p \/ r
3. ^q \/ ^r
4. ^p
Далі обчислюються резольвенти і додаються до S. У нижченаведеному списку кожний диз’юнкт – резольвента деяких попередніх диз’юнктів. Номера їх наводяться з права від відповідної резольвенти
5. p \/ ^r 1,3
6. q 1,4
7. p \/ ^q 2,3
8. r 2,4
9. p 2,5
10. ^r 3,6
11. ^q 3,8
12. ^r 4,5
13. ^q 4,7
14. Л 4,9
Отримали, що із КНФ S виводиться пустий диз’юнкт Л, тобто S є суперечністю (не виконуваною формулою).
(Теорема про нерозв'язність числення предикатів)
Найпростішою логічною системою, у якій знаходять висвітлення деякі аспекти математичного мислення, є числення висловлень. У цьому численні складні твердження будуються з деяких основних висловлень за допомогою символів, що позначають логічні зв'язки «не», «і», «чи» і «волоче». Досить легко переконатися в тому, що якщо числення висловлень визначене досить акуратно, то воно розв'язне. Це означає, що існує ефективна процедура рішення питання про те, чи є те чи інше твердження цього числення (тотожно) істинним, тобто справедливим у всіх можливих ситуаціях. Алгоритм цього дається методом істиннісних таблиць, добре знайомим багатьом читачам.
Більш широкими можливостями, ніж числення висловлень, володіє логічна система, що називається численням предикатів (першого порядку). мовою цього числення можна формалізувати значну частину всієї математики. Основні твердження в ньому формуються із символів, що представляють індивідуальні об'єкти (чи елементи), і предикатів і функцій на них. Складні твердження будуються з основних з використанням логічних символів числення висловлень, а також символів " і $.