Математическая логика и теория алгоритмов. Для изучающих компьютерные науки

VxB(x)^VxC(x) ~ Vz3y(B(y)^C(z)). (2.44) Так как левые части равносильностей (2.38) и (2.44) совпадают, то имеем: 3yVz (B (y)^(z)) ~ Vz3y (B (y)^(z)). (2.45) Известно, что в общем случае разноименные кванторы не перестановочны, а в частном случае (2.45) разноименные кванторы оказались перестановочны­ ми. Таким образом, в равносильности (2.38) в правой части порядок кванторов несуществен. Можно показать, что и в правых частях равносильностей (2.40) и (2.41) порядок кванторов несуществен. Замечание 2. Равносильности (2.38), (2.40) и (2.41) показывают, что при вынесении кванторов за скобками получили не один квантор, как это было ра­ нее, а уже два квантора. Для рассмотренного выше примера, проведя переименования переменных, а затем используя равносильность (2.41), легко получить (VxB(x))vVxC(x) ~ VzVy(B(y)vC(z)). (2.46) Также нетрудно получить (ЗхВ(х))&ЗхС(х) ~ 3z3y(B(y)&C(z)). (2.47) Таким образом, из формул (VxB(x))vVxC(x) и (ВхВ(х))&ВхС(х) мы все же вынесли кванторы за скобки, но за скобками оказались уже два квантора с раз­ личными переменными. Сравнивая равносильности (2.46) и (2.47) с равносиль- ностями (2.27) и (2.28), видим, что в последних кванторы вынесены без всякого изменения и удвоения их. Из равносильностей (2.33) - (2.36) и (2.38)-(2.41) очевидным образом сле­ дует, что для любой формулы можно добиться, чтобы сначала были записаны кванторы, а затем формула, не имеющая кванторов, т.е. "вынести" кванторы за скобки. Здесь применены кавычки, так как для получения равносильных фор­ мул кванторы выносятся за скобки, возможно, оставаясь неизмененными, либо меняясь на двойственные, либо выносятся за скобки только после переимено­ вания связанных переменных (в самом кванторе и области его действия). При этом переименование переменных осуществляется по правилам, описанным в предыдущем параграфе. Формула вида: QiQ2 ...QnB, где Qi,Q2, -,Qn - любая совокупность кванто­ ров, а формула В не содержит кванторов, называется формулой в предваренной нормальной форме или в пренексной нормальной форме. Для формулы Л ~ QiQ2 - QnB совокупность кванторов Qi,Q2, -,Qn называ­ ется префиксом формулы А, а формула В -матрицей формулы А. Из доказанных теорем легко следует следующая теорема. Теорема 2.9. Для каждой формулы логики предикатов су­ ществует равносильная ей формула в предваренной нормальной форме. 49