1.3. Рівносильні формули. Нормальні форми

Дві формули А і В називаються рівносильними , якщо кожна з них є логічним наслідком іншої.

Можна довести, що тоді і тільки тоді, коли ⊨ .

В логіці предикатів рівносильними будуть формули, отримані з рівносильних формул алгебри висловлень підстановкою замість пропозиційних змінних довільних формул логіки предикатів (окремі випадки). Наприклад, рівносильними будуть формули

, бо вони отримані з рівносильностей і за допомогою різних підстановок.

Крім окремих випадків у логіці предикатів є рівносильності, пов’язані з операцією навішування кванторів. Деякі рівносильності можна записати із тавтологій, що містять головну операцію , доведення яких здійснено у попередньому пункті. Варто пам’ятати рівносильності, що часто використовуються при рівносильних перетвореннях формул та при зведенні їх до нормальних форм :

1. -закони перейменування змінних;

2. -закони де Моргана для кванторів;

3. -дистрибутивні закони (і тільки такі два!);

4. -закони перенесення кванторів через кон’юнкцію, тут і далі Qне містить вільного x;

5. -закони пронесення кванторів через диз’юнкцію;

6. 

-закони пронесення кванторів через імплікацію.

Зведеною формою для формули логіки предикатів називається така рівносильна їй формула, яка або елементарна, або містить лише операції , причому заперечення стосується лише елементарних підформул.

Випередженою нормальною формою для формули логіки предикатів називається така її зведена форма, яка або не має кванторних операцій, або всі вони виконуються останніми.

Випереджена нормальна форма (ВНФ) довільної формули А логіки предикатів має вигляд , де -довільна сукупність кванторів (префікс формули А), а В- формула, яка не містить кванторів (матриця формули А).

Теорема. Для кожної формули логіки предикатів існує зведена та випереджена нормальна форми.

Щоб отримати зведену форму, потрібно скористатися законами, що дозволяють виразити через, , та законами де Моргана. Після застосування дистрибутивних законів та законів пронесення кванторів через логічні операції (винесення кванторів за дужки) отримують випереджену форму. Тут буває необхідно перейменовувати змінні у області дії кванторів, але робити це треба так, щоб не трапилось «колізії». Для перейменовування краще використовувати імена змінних, які у формулі не зустрічаються. Потрібно пам’ятати, що вільні змінні не перейменовуються, а одна і та ж змінна у областях дії різних кванторів може перейменовуватись на різні змінні. Наприклад, -зведена форма даної формули. Квантор загальності та існування не можна винести за дужки (пронести через диз’юнкцію), бо змінна х входить в усі доданки. Перейменуємо в області дії першого квантора хнау, а в області другого на z. Далі по черзі пронесемо квантори через диз’юнкцію: -випереджена нормальна форма, яка рівносильна даній формулі.

При аналізі формул логіки предикатів на виконуваність зручно мати формулу, яка не містить кванторів існування, а її матриця представлена у кон’юнктивній нормальній формі (кнф). Вилучення кванторів існування із префікса ВНФ проводять за допомогою введення сколемівських сталих та сколемівських функцій за правилом:

1.Знайти перший зліва на право квантор існування. Якщо він знаходиться у префіксі на першому місці, то замість змінної, яка зв’язана цим квантором, скрізь у матриці поставити деяку сколемівську сталу, яка у формулі ще не зустрічалась, а квантор існування видалити.

2.Якщо квантор існування не на першому місці префікса, наприклад то замість змінної х_і скрізь у матриці поставити деяку сколемівську функцію f(х₁х₂,...х_п), яка у формулі ще не зустрічалась, а квантор існування видалити.

3.Перейти до пункту 1, аж поки не видалиться останній квантор існування. У результаті таких перетворень отримується нова формула : , яка називається сколемівською стандартною формулою (ССФ).

Наприклад, розглянемо крок за кроком сколемізацію формули ;

1. Замість х вводимо сталу а : ;

2. Комбінація кванторів читається «для довільних у та z існує і може трактуватись, як означення деякої функції.  Після підстановки цієї функції у матрицю отримаємо нову формулу: ;

3.Комбінація кванторів рівносильна існуванню функції f=g(y,z,w). Вилучаємо останній квантор існування і маємо ССФ для А: .

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

Теорема. Формула А є суперечністю тоді і тільки тоді, коли її сколемівська стандартна форма є суперечністю.