Випереджені нормальні форми
У логіці висловлювань були введені дві нормальні форми: кон’юнктивна і диз’юнктивна. В аксіоматичній системі логік вводиться третя нормальна форма, яку називають випередженою нормальною формою.
Означення 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(х, у, и)).
Оскільки матриця А формули Ф не містить кванторів, то її можна подати у кон’юнктивній нормальній формі (КНФ). Формула Р знаходиться у кон’юнктивній нормальній формі, якщо вона має вигляд Р = 
… 
,
де 
= 
… 
, і кожне 
‒ це атомарна формула або її заперечення.