Материал: discrete_mathematics

Секвенції такого вигляду, тобто ті, що містять формулу, індексовану як 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

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

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

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

A → B →C ~ A B → C.

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

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

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

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

××

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

51