Материал: discrete_mathematics
1)що відбуватиметься за відсутності вільних предметних змінних у множині формул ∑ { xA(x)};
2)чи буде правило правильним, якщо в процесі виведення з'являться нові вільні змінні?
У першому випадку, якщо вільних змінних немає, то беремо
довільну нову змінну, наприклад z1. У другому випадку ситуація складніша, оскільки на значеннях нових змінних формула А(х) також має бути хибною. Щоб урахувати цей момент, у правилі
залишаємо формулу 0 А(х), яка при розгортанні зможе врахувати значення нових змінних. Таким чином, виправлене правило матиме вигляд
0 |
0 xA(x), ∑ |
, |
0 A(z1),..., 0 A(zm ), ∑, 0 xA(x) |
де {z1,…, zт} – усі вільні змінні ∑ { xA(x)}; якщо вільних
змінних немає, то беремо довільну нову змінну z1.
Зазначимо, що в цьому правилі спрощення не відбувається, але з'являються нові простіші формули, які, можливо, зроблять секвенцію замкненою.
Дуально будують секвенційні правила для універсального квантора.
Зауваження. Обговоримо питання про введення нових змінних у правилах 1 та 0 розкриття кванторів. Ці нові змінні можна тлумачити як константи в тому сенсі, що їх значення вже не будуть змінюватись. Тому для таких змінних можна використовувати позначення, які застосовуються для предметних констант: a, b, c, d, e, … . Іншими словами, нові змінні мають подвійну природу: з одного боку, це змінні, а з іншого – їх можна тлумачити як константи. Тому правило 1 можна записати у вигляді
1 |
1 xA(x), ∑ |
|
1 A(a), ∑ |
||
|
за умови, що нова змінна (константа) a не входить до ∑ { xA(x)} , і казати, що константа a підтверджує істинність
предиката A.
Аналогічно правило 0 також можна подати формулою
76
0 |
0 xA(x), ∑ |
, |
0 A(z1),..., 0 A(zm ), ∑, 0 xA(x) |
де {z1,…, zт} – усі вільні змінні ∑ { xA(x)} ; якщо вільних
змінних немає, то беремо довільну нову змінну (константу) z1. Проте такі константи в секвенційних правилах трактуються як
змінні, а в інтерпретаціях їх можна розуміти як константи (зауваження зроблено з метою додаткового роз'яснення правил).
У секвенційних правилах (формах) для логіки предикатів висновки пишемо над рискою, засновки – під рискою:
1← |
|
1← A, ∑ |
|
|
|
|
|
0← |
0 ← A, ∑ |
|
||||||||||
0 |
A, ∑ |
|
|
|
|
|
|
|
1 A, ∑ |
|||||||||||
|
|
|
|
|
|
|
|
|
|
|||||||||||
1 |
|
|
|
|
1 A B, |
∑ |
|
0 |
|
0 A B, ∑ |
|
|||||||||
1 A, ∑ |
1B, ∑ |
|
0 |
A, 0 B, ∑ |
||||||||||||||||
|
|
|
||||||||||||||||||
1 |
1 A B, ∑ |
|
|
|
|
0 |
|
|
|
|
0 A B, ∑ |
|
||||||||
|
1 A,1 B, ∑ |
|
|
|
|
|
0 |
A, Σ 0 B, ∑ |
||||||||||||
|
|
|
|
|
|
|
|
|||||||||||||
1→ |
|
|
|
|
1 A → B, ∑ |
|
0→ |
|
|
0 A → B, ∑ |
|
|||||||||
0 |
A, ∑ |
|
1B, ∑ |
|
|
|
1 A, 0 B, ∑ |
|||||||||||||
|
|
|
|
|
|
|
||||||||||||||
1↔ |
|
1 A ↔ B, ∑ |
0↔ |
|
0 A ↔ B, ∑ |
|||||||||||||||
0 A, 0 B, ∑ |
|
1A,1 B, ∑ |
0 A, 1 B, ∑ 1A,0 B, ∑ |
|||||||||||||||||
1 |
1 xA(x), ∑ |
|
|
1 A( y), ∑ |
|
|
|
|
|
|
|
заумови, що нова змінна у не входить до ∑ { xA(x)}. |
|||
|
0 |
0 xA(x), ∑ |
, |
|
0 A(z1),..., 0 A(zm ), ∑, 0 xA(x) |
||
де {z1,…, zт} – усі вільні змінні ∑ { xA(x)}; якщо вільних змінних немає, то береться довільна нова змінна z1.
1 1 xA(x), ∑ ,
1 A(z1),..., 1A(zm ), ∑, 1 xA(x)
77
де {z1,…, zт} – усі вільні змінні ∑ { xA(x)}; якщо вільних |
|||
змінних немає, то беремо довільну нову змінну z1. |
|||
0 |
0 xA(x), ∑ |
|
|
0 A( y), ∑ |
|||
|
|||
заумови, що нова змінна у не входить до ∑ { xA(x)}.
Припускатимемо, що в атомарних формулах відображені всі змінні, кількість яких дорівнює арності предиката. Однак у формулах правил вільні змінні не вказуватимемо, тобто записи A та
A(x) не міститимуть список усіх вільних змінних (те саме сто-
сується формул B і множини формул ∑).
Приклад 1.27.
1. Довести формулу x(A(x) → B(x)) → ( xA(x) → xB(x)).
► Формулюємо розмічену секвенцію:
0 x(A(x) → B(x)) → ( xA(x) → xB(x)).
Головною операцією є друга імплікація, тому застосовуємо
правило 0→:
( →) 0 x(A(x) → B(x)) → ( xA(x) → xB(x)) .
0 1 x(A(x) → B(x)), 0 xA(x) → xB(x)
Отримано нову секвенцію із двох формул. До другої формули доцільно застосувати правило 0→:
( →) 0 x(A(x) → B(x)) → (xA(x) → xB(x)) . 0 (0 →) 1 x(A(x) → B(x)), 0 xA(x) → xB(x)*
1 x(A(x) → B(x)), 1 xA(x), 0 xB(x)
У новій секвенції доцільно застосувати правило 1 до другої формули 1 xA(x). Це правило вимагає виявити всі вільні змінні
в секвенції. У даному випадку вільних змінних немає, тому беремо довільну нову змінну y, яку підставляємо до формули А(х) замість x. Маємо:
(0 →) |
0 |
x(A(x) → B(x)) → (xA(x) → xB(x)) |
|
. |
|||
(0 →) |
|
|
1 x(A(x) → B(x)), 0 xA(x) → xB(x)* |
|
|||
|
|
|
|
|
|||
|
(1) |
|
1 x(A(x) → B(x)), 1 xA(x)* , 0 xB(x) |
|
|
||
|
|
|
|
|
|||
|
|
|
x(A(x) → B(x)), 1 A( y), 1 xA(x), 0 xB(x) |
|
|
||
|
|
|
1 |
|
|
||
Далі до першої формули можна застосувати правило 1, однак тепер маємо вільну змінну y. Отримуємо:
78
(0 →) |
|
0 x(A(x) → B(x)) → (xA(x) → xB(x)) |
|
||||
(0 →) |
1 |
x(A(x) → B(x)), 0 xA(x) → xB(x)* |
|
||||
|
|
||||||
|
(1) |
|
|
1 x(A(x) → B(x)), |
1 xA(x)*, 0 xB(x) |
|
|
|
|
|
|
|
|||
|
|
( ) |
1 x(A(x) → B(x))* , 1 A( y), 1 xA(x), 0 xB(x) |
|
|||
|
|
|
|
||||
|
|
|
|
||||
|
|
1 |
|
1 A( y) → B( y),1 |
x(A(x) → B(x)), |
|
|
|
|
|
|
|
|
||
1 A( y), 1 xA(x), 0 xB(x) (остання секвенція розміщена на двох рядках).
До останньої формули секвенції застосуємо правило 0, ура-
ховуючи, що в секвенції єдиною вільною змінною є y: |
|
||
(0 →) |
0 |
x(A(x) → B(x)) → (xA(x) → xB(x)) |
. |
|
1 x(A(x) → B(x)), 0 xA(x) → xB(x)* |
||
(0 →) |
|
|
|
||
|
1 x(A(x) → B(x)), 1 xA(x)* , 0 xB(x) |
|
|||
|
(1 ) |
|
|
|
|
|
( ) 1 |
x(A(x) → B(x))* , 1 A( y), 1 xA(x), 0 xB(x) |
|
||
|
|
|
|||
1 |
|
1 A( y) → B( y),1 x(A(x) → B(x)), |
|
||
|
|
|
|||
( ) 1 A( y), 1 xA(x), 0 xB(x)*
0 1 A( y) → B( y),1 x(A(x) → B(x)), 1 A( y), 1 xA(x), B( y), 0 xB(x)
Тепер до першої формули застосуємо правило 1 → . Оскільки
отримані секвенції доволі великі, то запишемо їх у кілька рядків:
(0 →) |
|
|
0 x(A(x) → B(x)) → ( xA(x) → xB(x)) |
|
|
|
. |
|||||||||
(0 →) |
1 |
x( A(x) |
→ B(x)), 0 xA(x) |
→ xB(x)* |
|
|||||||||||
|
|
|
|
|
||||||||||||
|
(1 ) |
|
|
|
1 x(A(x) → B(x)), 1 xA(x)* , 0 xB(x) |
|
|
|
|
|||||||
|
|
|
|
|
|
|
|
|
||||||||
|
|
|
1 x( A(x) → B(x))* , 1 A( y), 1 xA(x), 0 xB(x) |
|
|
|
|
|||||||||
|
|
|
(1 ) |
|
|
|
|
|
||||||||
|
|
|
|
|
1 |
A( y) → B( y),1 |
x( A(x) → B(x)), |
|
|
|
|
|||||
|
|
|
|
|
|
|
|
|
|
|||||||
|
|
|
|
(0 ) |
|
1 A( y), 1 xA(x), |
0 xB(x)* |
|
|
|
|
|||||
|
|
|
|
|
|
|
1 A( y) → B( y),1 x(A(x) → B(x)), |
|
|
|
|
|||||
|
|
|
|
|
|
|
|
|
|
|
|
|
||||
|
|
|
|
|
|
|
(1 →) |
|
1 A( y), 1 xA(x), |
0 B( y), 0 xB(x) |
|
|
|
|
||
|
|
|
|
|
|
|
|
|
|
|
1 B( y)×,1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
0 A( y)×, |
|
|
|
|
|
|
||
|
|
|
|
|
|
|
|
1 x( A(x) → B(x)), |
|
x( A(x) → B(x)), |
|
|
|
|
||
|
|
|
|
|
|
|
|
1 A( y)×, |
|
|
1 A( y), |
|
|
|
|
|
|
|
|
|
|
|
|
|
1 xA(x), |
|
|
1 xA(x), |
|
|
|
|
|
|
|
|
|
|
|
|
|
0 B( y), 0 xB(x) |
|
|
0 B( y)×, 0 xB(x) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Усі отримані секвенції замкнені, тому початкова формула є всюди істинною. ◄
79
2. Чи є всюди істинною формула?
( xA(x) → xB(x)) → x(A(x) → B(x)).
► У цьому й подальших прикладах не вказуватимемо назву застосованого правила, оскільки воно легко визначається за головною операцією формули, індексованої знаком *. Формулюємо розмічену секвенцію та починаємо будувати дерево виведення:
0 |
( xA(x) → xB(x)) → x(A(x) → B(x)) |
. |
|
1 xA(x) → xB(x)*, 0 x(A(x) → B(x)) |
|
|
|
0 xA(x)*, 0 x(A(x) → B(x)) 1 xB(x)*, 0 x(A(x) → B(x))
Отримано дві секвенції, які не мають вільних змінних. Застосування правила 0 до першої формули першої секвенції вводить нову змінну y; при застосуванні правила 1 до першої формули другої секвенції можна взяти ту саму нову (для другої сек-
венції) змінну y. Дістанемо: |
|
|
|
|
||
|
|
0 (xA(x) → xB(x)) → x(A(x) → B(x)) |
|
. |
||
|
|
1 xA(x) → xB(x)*, 0 x(A(x) → B(x)) |
|
|||
|
|
|
|
|||
|
|
0 xA(x)*, 0 x(A(x) → B(x)) |
|
1 xB(x)*, 0 x(A(x) → B(x)) |
|
|
|
|
0 A( y), 0 x(A(x) → B(x)) |
|
1 B( y), 0 x(A(x) → B(x)) |
|
|
До обох нових секвенцій входить формула
1 B( y), 0 x(A(x) → B(x)),
яку розкриваємо за правилом 0 із використанням нової вільної змінної z. Далі застосовуємо правило 0 → . Маємо:
|
|
|
|
0(xA(x) → xB(x)) → x( A(x) → B(x)) |
|
. |
|||||||||||
|
|
|
|
1 xA(x) → xB(x)*, |
0 x( A(x) → B(x)) |
|
|||||||||||
|
|
|
|
|
|
||||||||||||
|
0 xA(x)*, 0 x( A(x) → B(x)) |
1 xB(x)*, 0 x( A(x) → B(x)) |
|
|
|||||||||||||
|
|
0 A( y), 0 x( A(x) → B(x)) |
|
|
1B( y), 0 x( A(x) → B(x)) |
|
|
||||||||||
|
|
|
0 A( y), 0 A(z) → B(z) |
|
|
|
|
1B( y), 0 A(z) → B(z) |
|
|
|
||||||
|
|
|
|
0 A( y), 1A(z), 0B(z) |
|
|
|
|
|
|
1B( y), 1A(z), 0B(z) |
|
|
|
|
||
|
|
|
|
! |
|
|
|
|
|
|
|
! |
|
|
|
|
|
Отримані секвенції 0 A( y), 1 A(z), 0 B(z) та 1 B( y), 1 A(z), 0 B(z) містять лише атомарні формули, але не є замкненими. Це означає,
що можна побудувати контрприклади, які спростовують початкову формулу. Кожна із секвенцій має дві вільні змінні y та z. Тому оберемо модель із двох констант a та b, вважаючи їх відповідно зна-
80