§7. Нормальные формы формул логики предикатов.
В логике предикатов, как и в логике высказываний, формулы могут иметь нормальную форму, т. е. существуют эквивалентные нормальные формы представления любых предикатных формул. При этом, используя равносильности алгебры высказываний и логики предикатов, каждую формулу логики предикатов можно привести к нормальной форме. В логике предикатов различают два вида нормальных форм: приведенную и предваренную.
Определение.
Говорят, что формула логики предикатов имеет приведенную нормальную форму, если она содержит только операции конъюнкции, дизъюнкции и кванторные операции, а операция отрицания отнесена к элементарным формулам.
Пример 1.
.
Получили приведенную нормальную форму исходной формулы.
Среди нормальных форм формул логики предикатов выделяют так называемую предваренную (префиксную, пренексную) нормальную форму (ПНФ). В ней кванторные операции либо полностью отсутствуют, либо они используются после всех операций алгебры логики, т. е. ПНФ формулы логике предикатов имеет вид
,
где под символом 
понимается один из кванторов 
или 
, а формула А кванторов не содержит.
Процедура получения (приведения) ПНФ. Состоит в следующем:
1. Используя формулы 18, 19 (отнесенные к предикатам), заменить операции 
и ~ на 
.
2. Используя форм, а также форм, 17, представить предикатную формулу таким образом, чтобы символы отрицания относились непосредственно к символам предикатов (и, таким образом, мы приводим исходную формулу к приведенной форме).
3. Для формул, содержащих подформулы вида 
, вести новые переменные, позволяющие использовать соотношения 46, 47, 49, 50 или 53, 54.
4. С помощью формул 35 – 38, 46, 47, 49, 50, 53, 54 получить формулу в виде ПНФ.
Пример 2.
обозначим в предикате Q переменную y через z
Пример 3.
обозначим в предикате Q переменную x через z
– ПНФ.
Пример 4.
последний предикат не зависит от переменной z 
два первых предиката не зависят от переменной u 
- ПНФ.
Пример 5.
