Материал: discrete_mathematics

Будуємо дерево виведення для останньої отриманої секвенції:

Усі гілки дерева виведення замкнені, тому початкова формула є тавтологією. Це можна також перевірити за допомогою побудови семантичної таблиці:

3. Кон'юнкція антецедентів (засновків):

A → B →C ~ A B → C.

Дужки можна розставити таким чином:

(A → (B → C)) ~ ((A B) → C),

тому головною операцією є еквівалентність. Формуємо розміче-

Побудуємо дерево виведення окремо для двох зазначених секвенцій. Почнемо з першої секвенції:

××

Усі гілки дерева виведення замкнені, тобто секвенція виведена (це позначають A0 A → B → C* , 1B → C). Тепер будуємо дерево виведення для другої секвенції:

51

Зауваження. Імплікація є правоасоціативною операцією, тому A → B → C = A → (B → C); головною операцією є еквівалент-

ність, тобто дужки можна розставити таким чином: (A → (B →C)) ~ ((A → B) → C).

Для доведення істинності початкової формули треба довести (вивести) розмічену імплікацію:

0 A → (B → C) ~ (A → B) → C.

Головною операцією є еквівалентність. Тому застосовуємо

Оскільки повне виведення не вміщається по ширині сторінки, то розглянемо окремо виведення для двох секвенцій:

0 A → (B → C), 1(A → B) → C та 1 A → (B → C), 0(A → B) → C.

52

Проаналізуємо секвенцію 0 A → (B → C), 1(A → B) → C. Тут слід звернути увагу на формулу 0 A → (B → C). Правило 0 →

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

Дістали виведення

( →) 0 A → (B → C)*, 1(A → B) → C .

0 1 A, 0(B → C), 1(A → B) → C

Аналізуючи отриману секвенцію, бачимо, що найпростіше перетворення буде для формули 0 (B → C). Індексуємо цю фор-

мулу в секвенції знаком * і застосовуємо правило 0 → . Виведен-

Тепер єдиною формулою, до якої можна застосувати секвен-

Отримано дві нові секвенції. Друга секвенція є замкненою,

оскільки містить 0 С та 1 С, тобто секвенція вимагає, щоб С було одночасно істинним і хибним. Ці формули індексуємо знаком × . Дістали суперечність, тому на цій гілці доведення початкова секвенція не має спростування. Таку замкнену секвенцію позначаємо знаком ×.

×

53

Отримані секвенції є замкненими. Отже, усі випадки розглянуто, секвенцію 0 A → (B → C), 1(A → B) → C доведено.

Тепер почнемо будувати виведення секвенції

1 A → (B → C), 0(A → B) → C.

Її аналіз свідчить про те, що доцільно перетворювати формулу 0 (A → B) →C. Маємо

!!

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

Дійсно, обчислимо значення A → (B → C) ↔ (A → B) → C за значень A, B, C відповідно 0, 0, 0. Маємо:

0 → (0 → 0) ~ (0 → 0) → 0 = 0 → 1 ~ 1→ 0 = 1 → 0 = 0.

Такий само результат отримуємо за значень А, В, С, відповід-

но 0, 1, 0. Тепер будуємо дерево виведення для секвенції

1 B →C, 1 A → B, 0C.

Отримуємо за значень А, В, С, відповідно 0, 1, 0. Маємо

0 → (1 → 0) ~ (0 → 1) → 0 = 0 → 0 ~ 1 → 0 = 1 → 0 = 0.

Повернемось до побудови дерева виведення для секвенції

1 B →C, 1 A → B, 0C.

Отримуємо

54

×

Дерево доведення замкнене, тому наслідковість доведено. Зауваження щодо застосування правил до секвенцій. Дотепер

ми детально не описували процедуру застосування секвенційних правил до секвенцій. Вона складається із трьох пунктів:

1)вибір секвенційного правила, яке можна застосувати до заданої (об'єктної) секвенції;

2)побудова уніфікатора, тобто такого зв'язку змінних у засновках секвенційного правила з певними пропозиційними формулами (чи секвенціями), що при заміні цих змінних у засновках правила на формули з уніфікатора отримаємо об'єктну секвенцію;

55