Материал: discrete_mathematics

перетворилась на нову секвенцію

0 A, 0 B, 0 ← A ← B.

В останній секвенції є лише одна складена (неатомарна) формула

0 ← A ← B,

яка свідчить, що формула ← A ← B має бути хибною.

Кон'юнкція набуває значення хиби у трьох випадках (див.

табл. 1.2):

1)коли перший і другий аргументи кон'юнкції є хибними;

2)коли перший аргумент є хибою, а другий – істиною;

3)коли перший аргумент є істиною, а другий – хибою. Ці три випадки можна замінити двома спрощеними випадками:

1)перший аргумент кон'юнкції є хибою;

2)другий аргумент кон'юнкції є хибою.

Тому далі для кон'юнкції (як і для диз'юнкції) розглядатимемо лише по два випадки.

Отже, формула ← A ← B будехибною тоді й тільки тоді, коли:

1)← A – хибне або

2)←B – хибне.

Це означає, що секвенція

0 A, 0 B, 0 ← A ← B

перетворилась на дві секвенції:

0 A, 0 B, 0 ← A та 0 A, 0 B, 0 ← B.

У першій із них неатомарною є формула 0 ←A, яку заміняємо на 1 A. Отримано секвенцію

0 A, 0 B, 1 A.

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

Тепер проаналізуємо другу секвенцію

0 A, 0 B, 0 ← B.

Перетворюючи 0 ← B на 1 В, отримуємо секвенцію

0A, 0 B, 1 В.

Уцій секвенції суперечність виникає для формули B . Отже, і ця

секвенція не може спростувати початкове наслідкове твердження.

46

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

Ми розглянули всі можливі випадки та продемонстрували, що наслідкове твердження не може буди спростовано, тому воно є істинним. Це дає змогу зробити загальні висновки:

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

впошуку суперечності для множин індексованих формул, отриманих у процесі доведення;

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

3)секвенційне доведення (секвенційне виведення) може бути подане у вигляді дерева, його корінь – початкова розмічена секвенція, а переходи задаються секвенційними правилами.

Як сформулювати секвенційні правила? Бачимо, що для кожної логічної операції є два правила: перше задає перетворення формули, яка розмічена 1, друге – формули, яка розмічена 0. Наприклад, для операції диз'юнкції можна записати два такі правила (засновки пишемо над рискою, висновки – під рискою):

Ці правила сформульовані для однієї формули, але секвенція може мати також інші формули. Позначимо їх множину як Σ . Загальне правило матиме такий вигляд (ліворуч пишемо назву правила):

Аналогічно можна побудувати правила для інших логічних операцій. Отримаємо таку сукупність секвенційних правил:

При виконанні завдань виведення доцільно записувати у зворотному порядку – тобто висновки писати над рискою, а засновки

– під рискою. Іншими словами, складніші формули пишемо над рискою, а простіші – під рискою. Отже, надалі записуватимемо секвенційні правила в такому вигляді:

Зауваження. Прямий і зворотний записи правил можна трактувати як пряме та зворотне доведення. Тому для зворотного доведення можемо в правилі засновки писати над рискою, а ви-

сновки – під рискою. Прохання звертати на це увагу при побудові доведень.

48

Нижче наведено запис секвенційного виведення розглянутого наслідкового твердження: ←(A B) |= ¬A ¬B:

A → B → A. Нагадуємо, що дужки у цій формулі розставляють таким чином: (A → (B → A)), тобто головною операцією є пер-

ша імплікація. Подаємо формулу як розмічену секвенцію:

0 A → B → A. Застосовуємо правило 0→. Назву правила пишемо ліворучвід риски. Отримуємо

( →) 0 A → B → A.

0 1 A, 0 B → A

Аналізуємо отриману секвенцію 1 A, 0 B → A. Тут є лише одна складна формула 0 B → A. Індексуємо її знаком * і застосову-

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

×

Побудувавши таблицю істинності, переконуємось, що початкова формула є тавтологією:

49

2. Комутативність антецедентів (засновків):

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

Формуєморозмічену секвенцію:

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

Головною її операцією є еквівалентність ~, тому застосовуємо правило 0 ~.

Отримано дві нові секвенції. Розглянемо першу

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

Доцільно застосувати правило 0 → до першої формули, яку індексуємо знаком *. Це саме правило застосовуємо також для другої секвенції:

Залишилось розглянути секвенцію

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

Двічі застосовуємо правило 0 → до позначених формул:

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

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

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

50