Page 38 - 6109

істинність виразу (G)(а 1,…,а n).
Поняття логічного наслідку пов’язано з поняттям не виконуваності. Так,
формула G(x 1,…,x n) називається логічним наслідком формул F 1(x 1,…,x n), …,
F k(x 1,…,x n) тоді і тільки тоді, токи множина формул {F 1(x 1,…,x n), …, F k(x 1,…,x n),
~ G(x 1,…,x n)} не виконувана.

4.3 Приведення формул до нормальних форм

Як зазначалося раніше, логічна формула, записана за допомогою
імплікацій і тотожностей, може бути переписана в термінах кон'юнкцій,
диз'юнкцій і заперечень. Розглянемо, як твердження числення предикатів
перетворюється на спеціальну уніфіковану фразову форму.
Дамо неформальний опис такого переведення, що має шість основних дій.
Дія 1. Вилучення імплікацій і тотожностей.
Вилучення імплікацій “” і тотожностей “” можна провести на основі
формул:
а  b дорівнює ( ~ а)  b,
а  b дорівнює (а  b)  (~ а  ~ b),

а  b дорівнює (а  b)  (b  а).
Так, формула x(P(x)F(x)) перетвориться на формулу x(~P(x)  F(x)).
Дія 2. Втягнення заперечення всередину.
Ця дія застосовується для випадків, коли “~” вживана у формулі, що не є
частковою. Тоді робиться така заміна на основі правил:
~ (а  b) дорівнює (~ a)  (~ b),
~ u, r дорівнює u, ~r,
~ u, r дорівнює u, ~ r.
Наприклад, ~(P(x)& F(x)) переводиться у ~ P(x)  ~F(x).

Після другої дії у наших формулах запишаться лише заперечення,
прив'язані до конкретних формул. Часткові твердження з або без "~" попереду
ми називаємо точними. У наступних кількох діях ми будемо поводитися з
точними твердженнями як з простими одиницями.
Дія 3. Заміна змінних.
Наступна дія включає вилучення існуючих кванторів. Це робиться
шляхом вставлення нових константних символів на місце, де були змінні, що
являють собою існуючі квантори. Тобто, замість того, щоб говорити, що існує
об'єкт з певним набором характеристик, можна створити ім'я для такого об'єкта
і просто сказати, що в нього є характеристики. В цьому і полягає основна суть
введення сколемівських констант. Ця дія є не повністю еквівалентною, але вона
має одну важливу властивість. Існує інтерпретація символів формули, яка
справджує формулу тільки тоді, коли існує інтерпретація для сколемівської
версії формули. Для наших потреб цієї форми відповідності достатньо.
Тому, x(P(x)  F(x,y)) перетворюється за допомогою сколемізації на P(c 1)
F(c 1, у),
де c 1, – деяка нова константа, що ніде раніше не використовувалась. Тут
важливим є застосування символу, який раніше ніде не вживався, оскільки

38