Аксіоматичні формальні системи ЧВ. Система природного виведення. Теорема дедукції

3.3 1 Мета заняття

Засвоїти основні прийоми логічного виведення у ФС. Отримати практичні навички виведення теорем в аксіоматичних системах та системах природного виведення у ЧВ. Опрацювати використання основних правил виведення. Засвоїти застосування теореми дедукції шляхом вирішення конкретних завдань.

3.3.2 Методичні вказівки з організації самостійної роботи студентів

Необхідно ознайомитися з основними відомими аксіоматичними системами ЧВ. При вивченні матеріалу використовуйте конспект лекцій та наступні джерела: [4, с. 64-75; 7, с. 217-228; 8; 9, с. 170-180].

Зверніть увагу на такі основні теоретичні положення числення висловлень. У ЧВ в якості об'єктів дослідження використовуємо формули алгебри логіки. Однак, тут формули розглядаються не як спосіб подання функцій, а як складені висловлення, утворені з елементарних висловлень (змінних) за допомогою логічних операцій або, як кажуть у логіці, зв'язок v, &, Ø, →. При цьому увага приділяється тотожним висловленням, оскільки вони повинні входити в будь-яку теорію як загальнологічні закони. Їхнє породження і є основною задачею числення висловлень. Розглядають два основних типи ФС, що відповідають ЧВ: аксіоматичні системи ЧВ; системи природного виведення або виведення із припущень.

Нагадаємо, що ФС містить у собі алфавіт, систему аксіом, правила виведення. Визначається також, що будемо вважати теоремою або кінцевим результатом функціонування ФС. ЧВ визначається таким способом:

1) алфавіт ЧВ складається зі змінних висловлень (пропозиціональних букв): A, B, C,..., знаків логічних зв'язок Ú, &, Ø, → і дужок (,).

2) формули:

а) змінне висловлення є формула;

б) якщо А і В – формула, то (АÚB), (A&B), (A→B), ┐A – формули;

в) інших формул немає.

Зовнішні дужки у формул домовляються опускати.

3) аксіоми.

Розглянемо, як функціонує аксіоматична система ЧВ, призначена для виведення теорем – загальнозначущих формул. Виведення у такій ФС буде складатися з послідовності рядків (ППФ логіки висловлень), що позначають загальнозначущі формули. Останній рядок побудованої послідовності і є результат функціонування ФС.

Наведемо як приклад дві системи аксіом ЧВ. Перша з них безпосередньо використовує всі логічні зв'язки. Аксіоматичну систему з множиною аксіом I (10 аксіом) будемо називати численням висловлень в аксіоматичній формі з десятьма аксіомами.

Система аксіом I:

I1. A®(B®A);

I2. (A®B)®((A®(B®C))®(A®C));

I3. (AÙB)®A;

I4. (AÙB)®B;

I5. A®(B®(AÙB));

I6. A®(AÚB);

I7. B®(AÚB);

I8. (A®C)®((B®C)®((AÚB)®C));

I9. (A®B)®((A®ØB)®ØA;

I10.ØØA®A.

Друга система аксіом використовує тільки дві зв'язки Ø і ®; при цьому скорочується алфавіт числення і, відповідно, визначення формули. Операції V, & розглядаються не як зв'язки ЧВ, а як скорочення (вживати які зручно, але не обов'язково) для деяких його формул: AÚB заміняє ØA®B, A&B заміняє Ø (A®ØB). У результаті система аксіом стає набагато компактніше.

Система аксіом II:

II1. A®(B®A);

II2. (A®(B®C))®((A®B) ®(A®C));

II3. (ØA®ØB)®((ØA®B)®A;

Наведені системи аксіом рівносильні в тому розумінні, що породжують одну й ту ж множину формул. Звичайно, таке твердження має потребу в доведенні, яке полягає в тому, що показується виводимість всіх аксіом системи II із аксіом системи I, і навпаки. Можливі й інші системи аксіом, рівносильні першим двом.

Яка із систем аксіом краще? Це залежить від точки зору. Система II компактніше та більш оглядна; відповідно, більш компактні й доведення різних її властивостей. З іншого боку, у більш багатій системі I виведення різних формул коротше.

Правила виведення:

1. Правило підстановки

Якщо U - вивідна формула (теорема), що містить букву А (позначається U (A)), то також вивідна і формула U (B), що виходить із U заміною всіх входжень А на довільну формулу (тобто U (B) - також теорема).

2. Правило відділення (відокремлення) (ModusPonens - MP)

Якщо U та U®B – вивідні формули, то B вивідна (також є теорема).

У цьому описі числення висловлень аксіоми є формулами числення (відповідним визначенню формули); формули ж, використані в правилах виведення (U, U®B і т.д.), це «метаформули», або схеми формул.

Схема формул, наприклад, U®B, позначає множину всіх тих формул числення, які отримуються, якщо її метазмінні замінити формулами числення. Наприклад зі схеми формул U®B можна одержати формулу A®A&B (заміною U на A, B на A&B).

Використання схем формул можна поширити й на аксіоми. Наприклад, якщо в системі II змінні A, B, C замінити змінними U,B,C, то отримаємо три схеми аксіом, що задають три нескінченних множини аксіом. В результаті виникає інший спосіб побудови UB: з нескінченною множиною аксіом (що задається кінцевим числом схем аксіом), але без правила підстановки, оскільки воно неявно міститься в тлумаченні схем аксіом. Перший спосіб більш послідовно конструктивний: всі його засоби, явно зафіксовані та скінчені. Другий спосіб більше відповідає математичній традиції тлумачення формул: наприклад, алгебраїчна тотожність (a+b)² = a² +2ab +b² або тотожності булевої алгебри розтлумачуються саме як схеми тотожностей, а не конкретні тотожності, справедливі лише для конкретних букв. Правило підстановки при цьому маємо на увазі. Очевидно, що перейти від одного способу побудови числень до іншого нескладно. Інші аксіоматизації ЧВ можна знайти в [6, 7]

Зауважимо, що для виведень у ЧВ не знайдено ефективного алгоритму, тому використання цієї системи в практичних застосуваннях не одержало достатнього поширення.

Більш практичною, ніж система виведення з аксіом, є система виведення з припущень, або система природного виведення. Так само, як і для аксіоматичних ФС числення висловлень, існує декілька варіантів (еквівалентних) систем природного виведення. Розглянемо систему, що одержала назву ЧС. Алфавіт ЧС збігається з алфавітом ЧВ. Множина аксіом складається з однієї тривіальної аксіоми A├ A; тобто з формули А виводиться формула А. Правила виведення діляться на основні й допоміжні. Цей поділ умовний, тому що в різних системах природного виведення різні множини правил включаються в основні. Однак існує мінімальний набір основних правил, з яких можна вивести в цій же системі всі додаткові правила. Чим більше правил використовується в системі, тим ефективніше можна виконати виведення.

В системі природного виведення працює правило підстановки у тому ж виді, що й у ЧВ. У явному виді це правило не включають в правила виведення, але мають на увазі та використовують при виведеннях.

Існує п’ятнадцять основних правил виведення в ЧС.

Нехай Г – список формул. Будь-яку доведену у численні вивідність вигляду Г ├ U, де Г – список формул, U – формула, можна розглядати як правило виведення , яке можна приєднати до тих, що вже є.

1. (введення Ù);

2. (видалення Ù);

3. (видалення Ù);

4. (введення Ú);

5. (введення Ú);

6. (видалення Ú);

7. (введення É);

8. (видалення É);

9. (введення Ø);

10. (зведення до протиріччя);

11. (видалення Ø);

12. (стоншення);

13. (розширення);

14. (перестановка);

15. (скорочення);

де А, В, С – похідна ППФ логіки висловлень, Г1, Г2, Г3, Г кінцеві послідовності формул, можливо, порожні.

У правилах виведення використані рядки, які називаються секвенціями: А1,..., Аn ├ B (позначає, що В вивідна з А1,..., Аn);

├ B позначає, що В вивідна;

А1,..., Аn ├ позначає, що множина А1,... Аn суперечлива, де А1,..., Аn, В - будь-які ППФ логіки висловлень, є секвенції. Правило виведення ,

де ∑₁, …, ∑_n, ∑ - секвенції, дає безпосередній висновок ∑ із ∑₁, …, ∑_n.

З погляду безпосереднього висновку розшифруємо деякі правила.

Правило 1: якщо секвенції Г₁ ├ А і Г₂ ├ В є рядками доведення, то секвенція Г₁,Г₂ ├ (A Ù B) - це безпосередній висновок зазначених секвенцій і може бути приєднаний до виведення.

Правило 6: якщо у виведенні є секвенції Г1 ├ А Ú B (з деякої послідовності формул Г1 виводиться диз'юнкція А Ú B), Г2,А├ C (з послідовності Г2 і формули А, що входить у диз'юнкцію, виводиться формула C), Г3, B├С (з Г3 і В, що входить у диз'юнкцію виводиться С), то до виведення можна приєднати секвенцію Г1, Г2, Г3 ├ С.

Правило 10: Якщо у виведенні є секвенції Г1 ├ А і Г2 ├ ØА, тобто виводиться формула А та її заперечення, то до виведення приєднується рядок Г1, Г2 ├ (множина Г1 і Г2 суперечлива).

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

Виведення в ЧС (системі природного виведення) – це кінцева послідовність секвенцій ∑₁, …, ∑_к така, що для кожного i (1 <= i <=k) ∑_i є або аксіома, або безпосередній висновок попередніх секвенцій за правилами підстановки 1-15 і додатковими правилами. Секвенція ∑ називається вивідною в ЧС, якщо існує виведення в ЧС, що закінчується ∑. Якщо результатом виведення в ЧС повинна бути формула А, тоді секвенція ∑ повинна мати вигляд ├ А.

Необхідно зрозуміти, як працює система виведення з припущень або система природного виведення. Виведення в ЧС починається з аксіоми. Щоб продовжити виведення від аксіоми, необхідно зробити припущення, специфічні для кожної формули, що виводиться. Робота механізму припущень і правил для виведення в ЧС показана нижче на прикладах, у яких використовуються прямі доведення із застосуванням припущень, що приводять до мети. Крім прямого виведення в системі природного виведення також використовується прийом непрямого доведення, де використовується заперечення того, що варто довести та зведення до протиріччя. При непрямому доведенні застосовується одне з додаткових правил, яке ми введемо під № 16:

16. .

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

Якщо в системі природного виведення ЧС вирази типу

А₁ É (А₂ É (…É (А_n-1 É А_n)...)

виводяться прямим методом (цей прийом називається умовним силогізмом), то в рядках виведення як допущення повинні з'явитися секвенції А₁├ А₁, …, А_n-1├ А_n-1, отримані підстановкою з аксіоми. При непрямому доведенні до цих рядків повинна додатися секвенція ØАn├ ØАn, при використанні правила видалення кон'юнкції, як допущення з'являється секвенція AÙB├ AÙB і т.д. Зазначимо, що використання правил природного виведення ближче до звичайних математичних доведень, ніж аксіоматична система.

Необхідно також знати та вміти користуватися теоремою дедукції. У ЧВ предметом дослідження є сама логіка, її закони (теореми), які формулюються за допомогою ППФ. Ці закони строго доводяться і є загальнозначущими функціями. Їх можна довести або в аксіоматичній системі, або в системі природного виведення, між якими існує глибокий внутрішній зв'язок. Справедлива наступна теорема дедукції:

якщо А ├ В, то ├ А ÉВ, а також

якщо А1,…, Аn-1, An ├ B, то А1,…, Аn-1 ├ An ÉВ.

Використовуючи систему аксіом, правила відділення та підстановки, теорему дедукції, можна довести у ЧВ всі формули, можуть бути виведені за допомогою кожного правила в ЧС. Інакше кажучи, у ЧВ можна довести допустимість кожного правила ЧС. Правила ЧС, застосовані до загальнозначущих формул, дають загальнозначущі формули. Оскільки виведення ЧС завжди починається введенням секвенції A├ A, то все, що в процесі виведення має вигляд ├ В, задає загальнозначущу формулу В. Оскільки в природному виведенні існує виведення з допущень, секвенція А1,..., Аn-1, An ├ B задає поняття вивідності - В може бути виведене з допущень А1,...,Аn-1,An. Секвенція ├А задає поняття доказовості - формула А може бути доведена.

Таким чином можна стверджувати, що аксіоматична система, наприклад, ЧВ, є основою для доведення всіх положень системи природного виведення (ЧС). Тому особливу роль і важливість набуває питання повноти, несуперечності та незалежності аксіом. Для системи числення висловлень доведено, що вона повна, несуперечлива та незалежна.

3.3.3 Контрольні запитання і завдання

1) За якою процедурою визначається числення висловлювань?

2) Наведіть приклад аксіоматичної системи ЧВ;

3) Які правила виведення використовуються в аксіоматичних системах ЧВ?

4) Що таке Modus Ponens?

5) Що таке «метаформула»? Наведіть приклади.

6) Чим відрізняється система виведення з припущень від аксіоматичної ФС числення висловлень?

7) Як будується система виведення з припущень?

8) Які аксіоми використовуються у ФС природного виведення?

9) Поясніть, як працює механізм логічного виведення у формальній системі природного виведення;

10) Що таке секвенція? Наведіть приклади;

11) Скільки правил виведення існує у системі природного виведення? Наведіть їх;

12) Як працює правило видалення імплікації?

13) Які правила виведення у системі природного виведення є основними, а які - допоміжними? Наведіть приклади;

14) Сформулюйте теорему дедукції, поясніть її смисл.

3.3.4 Приклади аудиторних і домашніх задач

Приклад1: показати що формула A®A вивідна у ЧВ.

Розв’язання: виведення представимо у вигляді такої послідовності формул

(1) (А В) ((А (В С)) (А С)) аксіома 2;

(2) (А (В А)) ((А (В А) А)) (А А))

З (1) заміною В на В А, С на А;

(3) (A (B A)) аксіома 1;

(4) (A ((B A) A)) (A A) з 3,2 і MP;

(5) (A ((B A) A)) з 3 заміною B на B A;

(6) A A з 5,4 і MP.

Приклад 2: показати що формула (AÙB) (BÙA) вивідна у ЧВ.

Розв’язання:

(1) (А В) ((А С) (А (BÙС))) аксіома 5;

(2) ((АÙВ) B) (((А ÙВ) А) ((АÙB) (B ÙА)) з (1) заміною A на АÙB, С на А;

(3) (AÙB) B аксіома 4;

(4) ((AÙB) A) ((AÙB) (BÙA)) з 3,2 і MP;

(5) (AÙB) A аксіома 3;

(6) (AÙB) (BÙA) з 5,4 і MP.

Приклад 3: показати, що формула (AÙB)É(BÙA) може бути виведена в системі природного виведення в ЧС.

Розв’язання: основне припущення: необхідно з А Ù B вивести окремо А і окремо B, потім виконати їхню перестановку з використанням правила введення Ù. Реалізуємо ці припущення наступним виведенням:

(1) A├ A; - аксіома

(2) AÙB ├ AÙB – з (1) підстановкою AÙB замість А;

(3) AÙB ├ A – з (2) і правила 2;

(4) AÙB ├ B – з (2) і правила 3;

(5) AÙB, AÙB ├ BÙA – з (4), (3) і правила 1 з заміною А на В та В на А;

(6) AÙB ├ BÙА – з (5) і правила 15.

(7) ├ (AÙB) É (BÙA) з (6) і правила 7.

Коментарі до рядків (кроків) виведення:

Рядок (3): до секвенції AÙB ├ AÙB рядка (2) уважає ліву частину формулою Г. Тоді Г├ AÙB задовольняє умові правила 2. Отже до виведення можна приєднати рядок Г├ A. Після розшифровки Г маємо рядок (3).

Рядок (5): рядки (3) і (4) формують умови для застосування правила 1. При цьому Г1 = AÙB ліва частина секвенції в рядку (3), Г2 = AÙB - ліва частина секвенції в рядку (4). Отже, можна застосувати правило 1, що дає рядок (5).

Рядок (6): у рядку (5) сформовані умови для застосування правила 15, де Г1, Г2 - порожні ланцюжки.

Рядок (7): це заключний рядок виведення, отримий з рядка (6), де сформовані умови введення імплікації, у яких Г - порожній ланцюжок.

Приклад 4: показати, що формула (АÚ(BÙC))É((AÚB) Ù(AÚC)) може бути виведена в системі природного виведення ЧС.

Розв’язання: Оосновне припущення полягає в тому, щоб спробувати вивести праву частину імплікацій з лівої застосуванням правила виключення диз'юнкцій у формулі АÚ(BÙC). Але для цього необхідно задовольнити наступним умовам: сама Ú повинна бути правою частиною якоїсь секвенції, що перебуває у виведенні; з першого числа Ú і послідовності формул виводиться права частина É, тобто формула (AÚB)Ù(AÚC); з послідовності формул і другого члена Ú виводиться права частина É. Все виведення побудоване на цих припущеннях.

(1) A├ A; - аксіома

(2) BÙC ├ BÙC – з (1) підстановкою BÙC замість А;

(3) BÙC ├ B – з (2) і правила 2;

(4) BÙC ├ C – з (2) і правила 3;

(5) BÙC ├ AÚB – з (3) і правила 5;

(6) BÙC ├ AÙC – з (4) і правила 5 з заміною B на С;

(7) BÙC, BÙC ├ (AÚB) Ù(AÚC) з (5), (6) і правила 1 з заміною в правилі А на AÚB, В на AÚС;

(8) BÙC ├ (AÚB) Ù(AÚC) – з (7) і правила 15;

(9) A├AÚB – з (1) і правила 4;

(10) A├AÚС – з (1) і правила 4 з заміною В на С;

(11) A,A├(AÚB) Ù(AÚC) – з (9) і (10) та правила 1;

(12) A├(AÚB) Ù(AÚC) – з (11) і правила 15.

(13) AÚ(BÙC)├ AÚ(BÙC) – із (1) з заміною А на AÚ(BÙC);

(14) AÚ(BÙC)├ (AÚB) Ù(AÚС) з (13), (12), (8) і правила 6.

(15) ├(AÚ(BÙC))É((AÚB)Ù(AÚС)) з (14) і правила 7.

У наведеному виведенні: рядки (1)-(8) показують як вивести праву частину імплікації з другого члена Ú, тобто отримано секвенцію (BÙC) ├ ((AÚB) Ù(AÚC))

Рядки (9) - (12) дають виведення правої частини імплікації з першого члена Ú, тобто формули А, а рядок (13) дає секвенцію для диз'юнкції.

Таким чином у рядках (13), (12) і (8) сформульовані умови, що дозволяють застосувати правило виключення Ú. При цьому послідовності формул Г1, Г2, Г3 із правила 6 такі: Г2, Г3 - порожні ланцюжки, Г1 = AÚ(BÙC).

Рядок (14) отриманий застосуванням правила 6.

Приклад 5: показати, що (AÉB) É(ØAÚB) може бути виведена в системі природного виведення ЧС.

Розв’язання: дана формула збігається з умовним твердженням «якщо АÉВ, то ØAÚB». При непрямому доведенні за допущення приймаємо заперечення формули, яку потрібно довести, тобто Ø(ØAÚB). Це міркування на змістовному рівні.

Формально основне допущення:

Формули АÉВ і Ø(ØAÚB) становлять суперечливу множину, тобто АÉВ, Ø(ØAÚB)├

(1) A├ A – аксіома;

(2) АÉB ├ AÉB – з (1) підстановкою AÉB замість А;

(3) АÉB,A ├ B – з (1),(2) і правила 8;

(4) B├ B – з (1) заміною А на В;

(5) B├ (ØAÚB) – з (4) і правила 5 з заміною А на ØА;

(6) Ø(ØAÙB), B├ (ØAÙB) – з (5) і правил 14, 13;

(7) Ø(ØAÙB)├ (ØAÙB) з (1) заміною А на Ø(ØAÙB), B├ (ØAÙB);

(8) Ø(ØAÙB), B├ (ØAÙB) – з (7) і правила 13;

(9) Ø(ØAÙB), B├ – з (6), (8) і правила 10;

(10) Ø(ØAÚB)├ ØВ – з (9) і правила 9;

(11) AÉB,A,Ø(ØAÚB) ├ – з (3) і (10) та правила 10;

(12) ØA├ ØA – з (1) заміною А на ØA;

(13) ØA├ ØAÚB – з (12) і правила 4 з заміною А на ØA;

(14) Ø(ØAÚB), ØА├ ØAÚB – з (13) і правила 13,14;

(15) Ø(ØAÚB),ØА├ Ø(ØAÚB) з (7) і правила 13 з заміною B на ØA.

(16) Ø(ØAÚB),ØА├ з (14), (15) і правила 10;

(17) Ø(ØAÚB)├ A – з (16) і правила 11;

(18) A, AÉB, Ø(ØAÚB) ├ з (11) і правила 14;

(19) AÉB, Ø(ØAÚB) ├ з (17), (18) і правил 16, 14, 15;

(20) AÉB├ ØAÚB – з (19) і правила 11;

(21) ├(AÉB)É(ØAÚB) з (20) і правила 7.

Наведемо пояснення до виведення. Доведення секвенцій AÉB, Ø(ØAÚB) ├ проведемо в кілька етапів. Спочатку в (1) - (3) доводимо АÉB,A ├ B, потім в (4)-(10) Ø(ØAÚB)├ ØВ, тобто з однієї множини формул виводиться формула В, а з іншої - її заперечення, що дає можливість виразити протиріччя (рядок (11)).

Однак у ліву частину секвенцій крім формул AÉB, Ø(ØAÚB), що цікавлять нас, входить формула А. Для її усунення можна використовувати правило 16, якщо буде доведено, що А виходить з AÉB або з Ø(ØAÚB) (випливання А з інших формул у цьому випадку не влаштовує, тому що в лівій частині секвенції повинна бути тільки назва формули).

Рядки (12) - (17) доводять Ø(ØAÚB)├A. Послідовність (18) - (21) усуває А з лівої частини секвенції та виводить початкову формулу. Відзначимо застосування у виведенні правил введення та видалення заперечення розширення. Так, для одержання (10) використовували Ø(ØAÙB), B├ (9) і правило 9, у якому одержуємо Г = Ø(ØAÙB), А = В. Щоб перейти від (16) до (17) застосовуємо правило 11, припускаючи Г = Ø(ØAÙB). Одержуючи рядок (6) з (5) за допомогою правила 13, що дозволяє додавати в ліву частину секвенції будь-яку формулу, припускаємо в ньому Г = В, А = ØAÙB, формула, що додається: В = Ø(ØAÙB). Для скорочення запису виведеня вживаємо неявні підстановки та послідовне застосування декількох правил виведення, наприклад рядки (6), (19).