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

Теорема 2.8. Пусть В{х) и С{х) - произвольные формулы ло­ гики предикатов, которые, может быть, содержат свободные вхожде­ ния переменнойi, тогда имеют место следующие равносильности: ViJ3(x)=>VxC(x) - Зу\/2{В(у):=>С{г)); (2.38) Vx5(x)=i>3xC(x) ~ Зх{В(х)=>С(х)); (2,39) Зх5(х)=>ЗхС(х) ~ V>'3z(i?(y)=>C(z)); (2.40) ЗхВ(х)=>\/хС{х) ~ yy\/z{B(y)=>C(z)), (2.41) где г и > - переменные, отличные от всех свободных переменных формул В(х) и С(х), а В(у) и C{z) - формулы, полученные из В(х) и С{х) соответственно при переименовании связанной перемен­ ной X на J и Z. Доказательство. Рассмотрим формулу \/хВ{х)=>\/хС(х). (2.42) Пусть у и Z - переменные, отличные от всех свободных пере­ менных формулы (2.42). Проведем переименование связанной переменной х в посылке этой формулы на переменную а в заключе­ ние - на г . Получим равносильную формулу: yyB(y)=>\fzC(z). (2.43) По построению в формуле (2.43) выражение \fzC{z) не содержит свободных вхождений переменной у, тогда по равносильности (2.35) можно вынести за скобки кваетор V>', причем он сменится на двойст­ венный, т.е. получим 3y(B(y)=:>\fzC(z)). Так как формула В(у) не содержит свободных вхождений z, то, используя равносильность (2.34), получим требуемое соотношение (2,38). Для доказательства соотношения (2.39) выразим импликацию в левой части соотношения (2.39) через 1 и v : VxB(x)=^aiC(x) ~ 1 (Vxi?(jc))v3xC(x) ~ (3x1 i?(x))v3xC(x). 74