Логика булевых функций

Определение 2.6. Приведенная формула называется нормальной, если она не содержит символов кванторов или все символы кванторов стоят впереди.
Пример 2.14.

1. 
   xy(A(x)  B(x, y)) – нормальная формула.
   
2. 
   x(A(x)) & yB(x, y) – приведенная формула, не являющаяся нормальной.
   

Теорема 2.2. Для каждой приведенной формулы существует равносильная ей нормальная формула.
Строгое доказательство теоремы 2.2 приведено в [6].
Алгоритм, позволяющий из приведенной формулы получить равносильную ей нормальную формулу, основан на правиле переименования связанных переменных и использовании равносильностей (2.3) – (2.8), (2.14) и (2.17).
Пусть Q – любой из кванторов , .
Воспользуемся равносильными преобразованиями (см.предыдущий раздел):
QxA(x)  B  Qx(A(x)  B) (2.18)
QxA(x) & B  Qx(A(x) & B). (2.19)
В тождествах (2.18), (2.19) формула B не зависит от x.
Q₁xA(x) & Q₂xB(x)  Q₁xQ₂z(A(x)&B(z (2.20)
Q₁xA(x)  Q₂xB(x)  Q₁xQ₂z(A(x)B( (2.21)
Тождества (2.18) и (2.19) есть обобщенная запись равносильных преобразований (2.3) – (2.6), а тождества (2.20) и (2.21) обобщают равносильности (2.14) – (2.17).
Мы видим, что тождества (2.18) – (2.21) позволяют поместить кванторы впереди формулы, что и требуется для нормальной формулы.
Пример 2.15.
Найти равносильную нормальную формулу для приведенной формулы: xyA(x, y) & xu(x, u).
В формуле yA(x, y) переменная y связана, поэтому yA(x, y) не зависит от y. Обозначим D(x) = yA(x, y).
В формуле uB(x, u) переменная u связана, поэтому uB(x, u) не зависит от u . Обозначим F(x) = uB(x, u).
Тогда
xyA(x, y) & xuB(x, u) = xD(x) & xF(x). (2.22)
Применим равносильность (2.20), имея в виду, что Q₁x есть x, а Q₂x есть x. Получим
xD(x) & xF(x) xz(D(x) & F(z)). (2.23)
Рассмотрим формулу D(x) & F(z) = yA(x, y) & uB(z, u). Применив два раза равносильность (2.19), получим
yA(x, y) & uB(z, u) y(A(x, y) & uB(z, u)) yu (A(x, y) & B(z, u)). (2.24)
Учитывая (2.21), (2.22), (2.23), получим окончательно
xyA(x, y) & xuB(x, u) xzyu(A(x, y) & B(z, u)). (2.25)
В тождестве (2.25) в левой части – исходная формула, а в левой части ее нормальная формула.