Материал: discrete_mathematics
(0 →) |
|
|
|
|
|
|
|
1 A → B →C, 0 A B →C* |
|
|
|
|
|
|
. |
||||||||||||
(1 ) |
|
|
|
|
|
1 A → B →C, 1 A B*, 0C |
|
||||||||||||||||||||
|
|
|
|
|
|
|
|
|
|
|
|
|
|
||||||||||||||
|
|
(1→) |
|
|
|
|
1 A → B →C*, 1 A, 1B, 0C |
|
|||||||||||||||||||
|
|
|
|
|
|
|
|
||||||||||||||||||||
|
|
|
|
|
|
A, 1 |
A, 1B, 0C |
|
|
|
|
|
|
1 B →C*, |
1 A, 1B, 0C |
|
|||||||||||
|
|
|
|
|
0 |
(1 |
→) |
|
|
||||||||||||||||||
|
|
|
|
|
|
|
|
× |
|
|
|
|
A, 1B, 0C 1C, 1 A, 1B, 0C |
||||||||||||||
|
|
|
|
|
|
|
|
|
|
|
|
|
0 B, 1 |
||||||||||||||
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
× |
|
|
|
|
|
× |
|
|
|
|
|
Усі гілки замкнені, тому A → B → C ~ A B → C є тавтологією. |
|||||||||||||||||||||||||||
Це можна також перевірити побудовою семантичної таблиці: |
|||||||||||||||||||||||||||
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
||||||
|
A B C |
B → C |
A B |
A → (B → C) |
(A B) → C |
|
|
A → (B → C) ~ |
|
||||||||||||||||||
|
|
|
~ (A B) → C |
|
|
||||||||||||||||||||||
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|||||||
|
0 0 0 |
|
1 |
|
|
0 |
|
1 |
|
|
|
|
|
1 |
|
|
|
|
1 |
|
|
|
|
|
|||
|
0 0 1 |
|
1 |
|
|
0 |
|
1 |
|
|
|
|
|
1 |
|
|
|
|
1 |
|
|
|
|
|
|||
|
0 1 0 |
|
0 |
|
|
0 |
|
1 |
|
|
|
|
|
1 |
|
|
|
|
1 |
|
|
|
|
|
|||
|
0 1 1 |
|
1 |
|
|
0 |
|
1 |
|
|
|
|
|
1 |
|
|
|
|
1 |
|
|
|
|
|
|||
|
1 0 0 |
|
1 |
|
|
0 |
|
1 |
|
|
|
|
|
1 |
|
|
|
|
1 |
|
|
|
|
|
|||
|
1 0 1 |
|
1 |
|
|
0 |
|
1 |
|
|
|
|
|
1 |
|
|
|
|
1 |
|
|
|
|
|
|||
|
1 1 0 |
|
0 |
|
|
1 |
|
0 |
|
|
|
|
|
0 |
|
|
|
|
1 |
|
|
|
|
|
|||
|
1 1 1 |
|
1 |
|
|
1 |
|
1 |
|
|
|
|
|
1 |
|
|
|
|
1 |
|
|
|
|
|
|||
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
: перевірити |
|
|
еквівалентність |
|
|
|||||||
|
A → B → C ~ (A → B) → C . |
|
|
|
|
|
|
||||||||||||||||||||
|
4. Неасоціативність імплікації |
|
|
|
|
|
|
|
|
|
|
|
|
|
|||||||||||||
Зауваження. Імплікація є правоасоціативною операцією, тому A → B → C = A → (B → C); головною операцією є еквівалент-
ність, тобто дужки можна розставити таким чином: (A → (B →C)) ~ ((A → B) → C).
Для доведення істинності початкової формули треба довести (вивести) розмічену імплікацію:
0 A → (B → C) ~ (A → B) → C.
Головною операцією є еквівалентність. Тому застосовуємо
правило 0~. Отримуємо виведення |
|
|
||
0 ~ |
|
0 A → (B → C) ~ (A → B) → C |
|
. |
|
A → (B → C), 1(A → B) → C 1 A → (B → C), 0 |
(A → B) → C |
||
0 |
|
|||
Оскільки повне виведення не вміщається по ширині сторінки, то розглянемо окремо виведення для двох секвенцій:
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 →) |
0 A → (B → C)*, 1(A → B) → C |
. |
|
|
|||
|
(0 →) |
1 A, 0(B → C)*, 1(A → B) → C |
|
1 A, 1B, 0C, 1(A → B) → C |
|
||
|
|
|
|
Тепер єдиною формулою, до якої можна застосувати секвен-
ційне правило, є формула |
1 (A → B) → C. Одержуємо |
|
|
||||
(0 →) |
|
|
0 A →(B →C)*, 1(A → B) →C |
|
. |
||
|
|
|
1 A, |
0(B →C)*, 1(A → B) →C |
|
||
(0 |
→) |
|
|
|
|||
(1→) |
1 A, 1B, 0C, 1( A → B) →C * |
|
|
||||
|
|
|
|
|
|||
|
|
|
1 A, 1B, 0C, 0 A → B 1 A, 1B, 0C, 1С |
|
|
||
|
|
|
|
|
|
||
Отримано дві нові секвенції. Друга секвенція є замкненою,
оскільки містить 0 С та 1 С, тобто секвенція вимагає, щоб С було одночасно істинним і хибним. Ці формули індексуємо знаком × . Дістали суперечність, тому на цій гілці доведення початкова секвенція не має спростування. Таку замкнену секвенцію позначаємо знаком ×.
Перетворюємо першу секвенцію, застосовуючи правило 0→: |
|||||||||
(0 →) |
|
|
0 A →(B →C)*, 1(A → B) →C |
|
. |
||||
(0 →) |
|
1 A, |
0(B →C)*, 1(A → B) →C |
|
|||||
|
|
|
|
||||||
|
(1→) |
|
|
1 A, 1B, 0C, 1(A → B) →C* |
|
|
|||
|
|
|
|
|
|
||||
|
|
|
|
|
1 A, 1B, 0C×, 1С× |
|
|
||
|
|
|
(0 →) |
1 A, 1B, 0C, 0 A → B* |
|
|
|
||
|
|
1 A, 1B×, 0C, 1 A, 0 B× |
× |
|
|
||||
|
|
|
|
|
|
||||
×
53
Отримані секвенції є замкненими. Отже, усі випадки розглянуто, секвенцію 0 A → (B → C), 1(A → B) → C доведено.
Тепер почнемо будувати виведення секвенції
1 A → (B → C), 0(A → B) → C.
Її аналіз свідчить про те, що доцільно перетворювати формулу 0 (A → B) →C. Маємо
|
|
|
(0 →) |
1 A → (B → C), 0(A → B) → C * |
. |
|
|
|
||||||
|
|
|
|
|||||||||||
|
|
|
|
|
|
|
1 A → (B → C), 1 A → B, 0C |
|
|
|
||||
Розкриваючи першу формулу отриманої секвенції, маємо: |
||||||||||||||
|
(0 →) |
|
|
|
|
1 A → (B → C), |
0(A → B) → C * |
|
. |
|
||||
|
|
|
1 |
A → (B → C)*, 1 A → B, 0C |
|
|
||||||||
|
|
|
(1→) |
|
|
|
|
|||||||
|
|
|
|
|
A, 1 A → B, 0C 1 B → C, 1 A → B, 0C |
|||||||||
0 |
|
|||||||||||||
Дістали дві секвенції: 0 A, 1 A → B, 0C та 1 B →C, 1 A → B, 0C. |
||||||||||||||
До першої застосовуємо правило 0→. Отримуємо |
|
|
|
|||||||||||
(0 →) |
|
|
|
|
|
1 A → (B → C), |
0(A → B) → C * |
|
|
. |
||||
|
1 |
A → (B → C) *, 1 A → B, 0C |
|
|||||||||||
|
(1→) |
|
|
|
|
|
|
|
||||||
|
|
|
0 A, |
1 A → B *, |
0C |
1 B → C, |
1 A → B, 0C |
|||||||
|
|
(1→) |
|
|
|
|||||||||
|
|
0 A, 0 A, 0C 0 A, |
1B, 0C |
|||||||||||
|
|
|
|
|
|
|
|
|
||||||
!!
Цей |
випадок дає дві незамкнені секвенції: 0 A, 0 A, 0C та |
0 A, 1B, |
0C, які позначаємо знаком ! Незамкнена секвенція на- |
дає контрприклад, тобто вказує значення пропозиційних змінних, які спростовують формулу.
Дійсно, обчислимо значення 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→) |
|
|
|
|
|
|
|
|
|
|
1 B →C*, 1A →B, 0C |
|
|
|
|
|
|
|
|
|
. |
|
||||||||||
(1→) |
|
|
0 B, 1A |
→B*, 0C |
(1→) |
|
0 C*, 1 A → B, |
0C |
|
|
||||||||||||||||||||||
|
|
|
|
|
|
|
|
|
|
|||||||||||||||||||||||
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
||||
|
|
|
|
|
|
0 B, 0 A, 0C 0 B×, 1B×, 0C |
|
0 C, 0 A, 0C 0 C, 1B, 0C |
|
|
|
|
||||||||||||||||||||
|
|
|
|
|
|
|
! |
|
|
|
|
× |
|
|
|
|
|
|
|
! |
|
|
|
|
! |
|
|
|
|
|||
Незамкненими є секвенції |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
||||||||||||||||||
|
|
|
|
|
|
|
0 B, 0 A, 0C; 0 C, 0 A, 0C; 0 C, 1B, 0C. |
|
|
|
|
|
||||||||||||||||||||
Вони всі надають контрприклади для початкової секвенції. |
|
|
|
|
||||||||||||||||||||||||||||
|
Побудуємо для неї таблицю істинності: |
|
|
|
|
|
|
|
|
|
|
|
|
|||||||||||||||||||
|
A B C |
B → C |
A → B |
A → (B → C) |
(A → B) → C |
|
A → (B → C) ~ |
|
|
|
|
|||||||||||||||||||||
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
~ (A → B) → C |
|
|
|
|
|||
|
0 0 0 |
|
1 |
|
1 |
|
|
1 |
|
|
|
|
|
0 |
|
|
|
|
|
0 |
|
|
|
|
|
|||||||
|
0 0 1 |
|
1 |
|
1 |
|
|
1 |
|
|
|
|
|
1 |
|
|
|
|
|
1 |
|
|
|
|
|
|||||||
|
0 1 0 |
|
0 |
|
1 |
|
|
1 |
|
|
|
|
|
0 |
|
|
|
|
|
0 |
|
|
|
|
|
|||||||
|
0 1 1 |
|
1 |
|
1 |
|
|
1 |
|
|
|
|
|
1 |
|
|
|
|
|
1 |
|
|
|
|
|
|||||||
|
1 0 0 |
|
1 |
|
0 |
|
|
1 |
|
|
|
|
|
1 |
|
|
|
|
|
1 |
|
|
|
|
|
|||||||
|
1 0 1 |
|
1 |
|
0 |
|
|
1 |
|
|
|
|
|
1 |
|
|
|
|
|
1 |
|
|
|
|
|
|||||||
|
1 1 0 |
|
0 |
|
1 |
|
|
0 |
|
|
|
|
|
0 |
|
|
|
|
|
0 |
|
|
|
|
|
|||||||
|
1 1 1 |
|
1 |
|
1 |
|
|
1 |
|
|
|
|
|
1 |
|
|
|
|
|
0 |
◄ |
|
|
|
|
|||||||
|
5. Довестинаслідковість a b, ¬ a c Bb c. |
|
|
|
|
|
||||||||||||||||||||||||||
|
Формуємо розмічену секвенцію: |
1 a b, 1¬a c, 0b c. Будує- |
||||||||||||||||||||||||||||||
мо її секвенційне виведення: |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
||||||||||||||||||
(0 ) |
|
|
|
|
|
|
|
|
|
|
|
1a b, 1¬a c, 0b c * |
|
|
|
|
|
|
|
. |
||||||||||||
(1 ) |
|
|
|
|
|
|
|
|
1 a b*, 1¬a c, 0b, 0c |
|
|
|
|
|
||||||||||||||||||
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|||||||||||||||
|
|
(1 ) |
|
|
1 a , 1¬a c*, 0b, |
0c |
|
|
|
|
1b×,1 ¬a c,0 b×,0 c |
|||||||||||||||||||||
|
|
|
|
|
|
|
|
|
|
|
||||||||||||||||||||||
|
|
|
|
|
( ) |
1 a, 1¬a*, 0b, 0c |
|
1 a, 1c×, 0b, 0c× |
|
|
|
× |
|
|
|
|
|
|||||||||||||||
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
||||||||||||||||||
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
||||||||||||||||
|
|
|
|
|
|
|
1 |
|
1 a×, |
0 a×, 0b, 0c |
× |
|
|
|
|
|
|
|
|
|
|
|
|
|
||||||||
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
×
Дерево доведення замкнене, тому наслідковість доведено. Зауваження щодо застосування правил до секвенцій. Дотепер
ми детально не описували процедуру застосування секвенційних правил до секвенцій. Вона складається із трьох пунктів:
1)вибір секвенційного правила, яке можна застосувати до заданої (об'єктної) секвенції;
2)побудова уніфікатора, тобто такого зв'язку змінних у засновках секвенційного правила з певними пропозиційними формулами (чи секвенціями), що при заміні цих змінних у засновках правила на формули з уніфікатора отримаємо об'єктну секвенцію;
55
3) застосування побудованого уніфікатора до висновків секвенційного правила, що дає висновок для об'єктної секвенції.
Наприклад, маємо об'єктну секвенцію
1 A → (B → C), 0(A → B) → C.
Проаналізувавши її, застосуємо правило 0→ до другої формули секвенції. Правило запишемо у вигляді
0→ |
0 |
A → B, ∑ |
. |
|
1 A, 0 B, ∑ |
||||
|
|
|||
Тепер побудуємо уніфікатор. У засновках правила прописано змінні (краще навіть називати їх метазмінними, оскільки їх значен-
нями будутьпропозиційнізмінні чиформули) A, B, Σ.
Тут A та B – пропозиційні метазмінні (оскільки вони будуть
замінюватися на пропозиційні формули), Σ – секвенційна метазмінна (оскільки замінюватиметься на секвенцію). Виокремлю-
ємо формулу
0 (A → B) → C,
яку перетворюватимемо. Другу формулу 1 A → (B → C) наразі
не перетворюватимемо. Тому секвенційній метазмінній Σ відповідатиме формула 1 A → (B → C) (записуємо у вигляді
∑ |
→ (В → С)), |
|
1 А |
||
|
а формулі 0 A → B із засновків правила відповідатиме формула
0 (A → B) → C
з об'єктної секвенції. В об'єктній формулі головною операцією є друга імплікація, тому при уніфікації метазмінній A з правила відповідає формула A → B (записуємо у вигляді A/ A → B), а
метазмінній В – формула С (записуємо у вигляді В/С). Це означає, про побудовано уніфікатор
|
∑ |
→ (В → С), |
1 А |
→ В, |
В |
|
|
|
|
|
. |
||
1 А |
А |
|
||||
|
|
|
С |
|||
|
|
|
|
|
|
|
Тепер застосовуємо отриманийуніфікатор до висновківправила
1 A, 0 B, ∑,
56