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

Таким образом, при вынесении кванторов за скобки для указанных фор­ мул кванторы могут выноситься без изменения, либо меняться на двойствен­ ные. В общем случае, оказывается, нужно проводить еще и переименование пе- эеменных, прежде чем вынести квантор за скобки. Теорема 2.8. Пусть В(х) и С(х) - произвольные формулы логики предика­ тов, которые, может быть, содержат свободные вхождения переменной х, тогда имеют место следующие равносильности: VxB(x)^VxC(x) ~ 3yVz(B(y)^(z)); (2.38) VxB(x)^3xC(x) ~Зх(В(х)^С(х)); (2.39) ВхВ(х)^ВхС(х) ~ Vy3z(B(y)^(z))- (2.40) 3xB(x)^VxC(x) ~VyVz(B(y)^(z)), (2.41) где z и - переменные, отличные от всех свободных переменных формул В(х) и С(х), а В(у) и C(z) -формулы, полученные из В(х) и С(х) соответст­ венно при переименовании связанной переменной х на и z. Доказательство. Рассмотрим формулу VxB(x)^VxC(x). (2.42) Пусть 3^ и Z - переменные, отличные от всех свободных переменных фор­ мулы (2.42). Проведем переименование связанной переменной х в посылке этой формулы на переменную а в заключении - на z . Получим равносильную формулу: VyB(y)^VzC(z). (2.43) По построению в формуле (2.43) выражение VzC(z) не содержит свобод­ ных вхождений переменной у, тогда по равносильности (2.35) можно вынести за скобки квантор Vy, причем он сменится на двойственный, т.е. получим 3y(B(y)^VzC(z)). Так как формула В(у) не содержит свободных вхождений z, то, используя равносильность (2.34), получим требуемое соотношение (2.38). Для доказательства соотношения (2.39) выразим импликацию в левой час­ ти соотношения (2.39) через —i и v: VxB(x)^3xC(x) —\(VxB(x))v3xC(x) ~(3x~B(x))v3xC(x). Далее по доказанной равносильности (2.28) получаем Зх(^В(х) vC(x)), от­ куда и следует равносильность (2.39). Равносильности (2.40) и (2.41) доказываются, как и для соотношения (2.38). Замечание 1. При доказательстве равносильности (2.38) мы вынесли за скобки квантор из посылки, а затем из заключения, хотя, как легко видеть, можно сделать это и в обратной последовательности: сначала вынести квантор из заключения, а затем из посылки. В этом случае вместо (2.38) получим 48