Материал: discrete_mathematics
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
ченнями y та z. Перша секвенція 0 A( y), 1 A(z), 0 B(z) визначає значення базових предикатів A та B: A(a) = 0, A(b) = 1, B(b) = 0. Значення В(а) секвенція не визначає, тому воно можу бутидовільним
(позначаємо знаком *). Будуємо таблицю, що |
x |
A(x) |
B(x) |
задає модель (інтерпретацію предикатних |
a |
0 |
* |
символів): |
b |
1 |
0 |
Обчислимо значення формули |
|
|
|
(xA(x) → xB(x)) → x(A(x) → B(x)) |
|
|
|
у цій моделі. Оскільки вільних змінних немає, то початковий стан змінних задається порожньою множиною. У наведеній формулі головною операцією є імплікація, тому обчислюємо значення: антецедента – xA(x) → xB(x); консеквентна – x(A(x) → B(x))
на початковому стані. Антецедент сформовано за допомогою імплікації, тому обчислюємо xA(x) та xB(x).
Бачимо, що в нашій моделі xA(x) набуває значення 0, відповідно xA(x) → xB(x) отримує значення 0 (тут значення кон-
секвента не є важливим), отже, значення
( xA(x) → xB(x)) → x(A(x) → B(x)) = 0,
тобто формула спростовна.
Аналогічно будують модель для незамкненої секвенції 1 B( y), 1 A(z), 0 B(z). Ця модель також задає контрприклад. ◄
3. Чиєвсюдиістинноюформула x(A(x) →B(x)) →(A(x) →xB(x))?
► Зауважимо, що у формулі є вільна змінна x. Будуємо секвенційне виведення цієї формули (коментарі для правил виведення пишемо у фігурних дужках):
|
|
0 x(A(x) → B(x)) → (A(x) → xB(x)) |
|
|
. |
|||||
|
|
1 x(A(x) → B(x)), |
0(A(x) → xB(x))* |
|
||||||
|
|
|
|
|
||||||
|
|
1 x(A(x) → B(x))*, |
|
1 A(x), 0 xB(x) |
|
|
|
|||
|
|
1 A(y) → B(y))*, |
1 A(x), 0 xB(x)) |
|
|
|
||||
|
|
0 A(y), 1 A(x), 0 xB(x)* |
|
|
|
1 B(y), 1 A(x), 0 xB(x)* |
|
|
|
|
|
|
{тут вільні x, y} |
|
|
|
{тут вільні x, y} |
|
|
|
|
|
|
0 A( y), 1 A(x), 0 B(x), 0 B(y), |
|
|
1 B(y), 1 A(x), 0 xB(x)* |
|
|
|
||
|
|
0 xB(x) |
|
|
|
|
1 B(y)×, 1 A(x), 0 B( y) ×, |
|
|
|
|
|
{тут вільні x, y, z} |
|
|
|
|
0 B(x), 0 xB(x) |
|
|
|
|
|
|
|
|
|
× |
|
|
|
|
|
|
! |
|
|
|
|
||||
|
|
|
81 |
|
|
|
|
|
||