Математическая логика и теория алгоритмов

Далее по доказанной равносильности (2.28) получаем: Зх(1 B(x)vC(x)), откуда и следует равносильность (2.39). Равносильности (2.40) и (2.41) доказываются, как для соотноше­ ния (2.38). Замечание 1. При доказательстве равносильности (2.38) мы вынесли за скобки квантор из посылки, а затем, из заключения, хотя, как легко видеть, можно сделать это и в обратной последова­ тельности; сначала вынести квантор из заключения, а затем из посылки. В этом случае вместо (2.38) получим УхВ(х)^УхС(х) ~ yz3yiB(y)=^C(z)). (2.44) Так как левые части равносильностей (2.38) и (2.44) совпадают, то имеем: 3y\/z(B(y)=^C(z)) ~ yz3y(B(y)=^C(z)). (2.45) Известно, что в общем случае разноименные кванторы не перестановочны, а в частном случае (2.45) разноименные кванторы оказались перестановочными. Таким образом, в равносильности (2.45) в правой части порядок кванторов несущественен. Можно показать, что и в правых частях равносильностей (2.40) и (2.41) порядок кванторов не существенен. Замечание 2. Равносильности (2.38), (2.40) и (2.41) показывают, что при вынесении кванторов за скобками получили не один квантор, как это было ранее, а уже два квантора. Проведя переименования переменных, а затем используя равно­ сильность (2.41), легко получить: (VxB(x))vVxC(x) ~ VzVy(B(y)vC(z)). (2.46) Таюке нетрудно получить: (ЭхВ(х))&ЭхС(х) ~ 3s3y(B(y)&C(z)). (2.47) Таким образом, из формул (VxB(x))vVxC(x) и (ЗхВ(х))&БхС(х) мы все же вынесли кванторы за скобки, но за скобками оказались уже два квантора с различными переменными. Сравнивая равносильности (2.46) и (2.47) с равносильностями (2.27) и (2.28), видим, что в последних кванторы вынесены без всякого изменения и удвоения их. 75