Випереджені нормальні форми

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

Означення 4.2.1.Формула Ф у логіці предикатів знаходиться у випередженій нормальній формі (ВНФ) тоді і тільки тоді, коли вона може бути зображена у вигляді ( )… ( ) (А), де ( ) є або ( х), або ( х) і всі різні для різних і = 1, …, п, а А – формула, що не містить квантора. Приставку ( ) називають префіксом, а А – матрицею формули Ф. Якщо формула А залежить від вільної змінної х, то це записується як А (х), якщо ні, то – А.

Теорема 4.2.1.Для будь-яких формул F, G, H теорії числення першого порядку справедливі такі еквівалентності:

а) х F(x) х ( F (x));

б) х F(x) х ( F(x));

в) х F(x) G х (F(x) G);

х F(x) G х (F(x) G);

г) х F(x) G х (F(x) G);

х F(x) G х (F(x) G);

д) х F(x) х Н (х) х (F(x) Н (х));

е) х F(x) х Н (х) х (F(x) Н (х));

є) х F(x) х Н (х) х у (F(x) Н (у));

ж) х F(x) х Н (х) х у (F(x) Н (у)).

Доведення . Виконаємо доведення еквівалентності.

а) х F(x) х ( F(x)). Нехай r – довільна інтер-претація на деякій області R. Якщо ( х F(x)) істинна в інтерпретації r, то х F(x) хибна в r. Це означає, що існує такий елемент k(x) R, для якого F ( k (x) ) хибна, або те саме, що F (k (x) ) істинна в r. Отже, х ( F(x)) істинна в r.

Якщо ( х F(x)) хибна в r, то х F(x) істинна в r. Це означає, що F(x) виконується на всіх послідовностях із R або що F(x) не виконується на жодній такій послідовності з R. Отже, х ( F(x)) хибна в r. Таким чином,

( х F(x)) х ( F(x)).

Доведення еквівалентності б) аналогічне доведенню еквівалентності а).

Доведемо еквівалентність в) х F(x) G

Û х (F(x) G). Нехай маємо хF(x) G ( хF(x))→ →G х ( F(x)) → G.

Отже,

1) х ( F(x)) → G – гіпотеза;

2) F(x) → х ( F(x)) – правило 7;

3) F(x) → G – транзитивність із 1) і 2) ;

4) x ( F(x) → G) x (F(x) G) – загальнозначність із 3).

І навпаки:

1) x (F(x) G) x ( F(x) → G) – гіпотеза ;

2) F(x) → G – правило 6 із 1;

3) ( F(x) → G) → ( G → F(x)) ‒ тавтологія ;

4) G → F(x) – МР із 2) і 3) ;

5) x ( G → F(x)) – узагальнення із 4 ;

6) х ( G → F(x)) → ( G → х F(x)) – схема аксіом АП5 ;

7) G → x F(x) – МР із 5 і 6 ;

8) ( G → xF(x)) → ( x F(x) → G) – тавтологія ;

9) x F(x) → G x F(x) G – МР із 7) і 8).

Доведемо спочатку першу еквівалентність г).

1) х F(x) G х ( F(x)) → G – гіпотеза ;

2) ( F(x)) → G – правило 6 ;

3) ( F(x)) → G) → х ( F(x) → G) – правило 7 ;

4) х ( F(x) G) х (F(x) G) – МР із 2) і 3).

І навпаки:

1) х ( F(x) → G) – гіпотеза;

2) х ( F(x) → G) → ( F(x) → G) – правило 7 ;

3) F(x) → G – МР із 1) і 2) ;

4) x ( F(x)) → F(x) – правило 6 ;

5) x ( F(x)) → G x ( F(x)) G х (F(x)) G – транзитивність із 3) і 4).

Доведення інших еквівалентностей із в) і г) тепер легко випливає із законів де Моргана.

x F(x) G ( x F(x) G)

Û (( х F(x)) G ( х ( F(x) G)

Û ( х (F(x) G) x (F(x)) G).

x F(x) G ( x F(x) G)

Û( х ( F(x)) G) ( х ( F(x) G) Û ( х (F(x) G) x (F(x) G).

Аналогічно доводяться й інші еквівалентності із г).

Доведення решти еквівалентностей пропонуються як вправи.

Теорема доведена.

Із теореми 4.2.1 випливає такий метод побудови ВНФ. Для зведення формули Ф до випередженої нормальної форми використовують такі дії:

а) вилучення логічних зв’язок “ →” і “ ” :

А В = (А → В) (В → А) ; А → В = А В ;

б) вилучення і перенесення знака “ ” всередину формул:

( x F(x)) = х ( F(x)); ( х F(x)) =

= x ( F(x)); F = F;

в) перенесення кванторів:

Q x Р(х) G = Q x (F(x) G);

Q x Р(х) G = Q x (F(x) G);

х F(x) х Н (х) = х (F(x) Н (х));

х F(x) х Н (х) = х (F(x) Н (х));

Q1 х F(x) х Н (х) = х у (F(x) Н (у));

Q1 х F(x) х Н (х) = х у (F(x) Н (у)).

Виходячи із методу побудови ВНФ, алгоритм отримання випередженої нормальної форми матиме такі кроки.

1. Вилучити логічні зв’язки еквіваленції “ ” та імплікації “ →” за допомогою правил а).

2. Перенести знак операції заперечення “ ” всередину формул, користуючись правилами: (F G) =

F G; (F G) = F G, і правилами б).

3. Виконати перейменування пов’язаних змінних, якщо є така необхідність.

4. Винести квантори на початок формули, використовуючи правила в).

Обґрунтуванням цього алгоритму є твердження, що безпосередньо випливає з теореми 4.2.1.

Теорема 4.2.2. Алгоритм випередженої нормальної форми перетворює будь-яку формулу А теорії числення предикатів першого порядку АП в таку формулу В, яка знаходиться у ВНФ, що ├ А В у ПL.

Приклад 4.2.1. Звести формулу х F(x) → х Н (х) до ВНФ.

Розв’язання. Користуючись кроками 1, 2, 4 алгоритму, отримаємо

х F(x) → х Н (х) = ( х F(x)) х Н (х) =

= х ( F(x)) х Н (х) = х ( F(x) Н (х)).

Приклад 4.2.2.Отримати ВНФ для формули

х у z (Р (х, у) Р(у, z)) → z R(x, y, z).

Розв’язання. Користуючись кроками 1, 2, 3, 4 алгоритму, отримаємо

х у z (Р (х, у) Р (у, z)) → z R(x, y, z) =

=( z y ( z (Р(х, у) Р(у, z)) z R(х, у, z) =

= x y z ( Р(х, у) Р(у, z)) u R(х, у, и) =

= x y z u ( Р(х, у) Р(у, z) R(х, у, и)).

Оскільки матриця А формули Ф не містить кванторів, то її можна подати у кон’юнктивній нормальній формі (КНФ). Формула Р знаходиться у кон’юнктивній нормальній формі, якщо вона має вигляд Р = … ,

де = … , і кожне ‒ це атомарна формула або її заперечення.