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

\/уА()!)-=>ЗхВ(х)=:>С(х). Из формулы (2.21) переименованием можно получить формулу У xA{x)=>3zB{z)=>C(x) или \/хА(х)=>ЗуВ(}')=>С(х) (при этом каждая полученная формула будет равносильна исходной формуле (2.21)). Отметим еще раз, что переименовываются только связанные пе­ ременные, а свободные не трогаются. Так, в формуле (2.21) последнее вхождение зс свободно, поэтому при любых переименованиях пере­ менная X остается неизменной. Рассмотрим еще один пример. Пусть задана формула Vx(3yP(x,y)z:^\/yQ(x,y)z:^R{x)). (2.22) Переименовывая в этой формуле переменную х, нужно заменить ее одинаковым образом всюду, где она входит, ибо х в формуле (2.22) является либо переменной квантора, либо находится в области действия квантора. Например, переименовав х на г, получим следующую формулу, равносильную исходной; Vz(3yP(z,y)^VyQ(z,y)z:^R(z)). В формуле (2.22) переменную у можно переименовать в первой посылке, например, на переменную v; а во второй оставить без изме­ нения, либо заменить, например, переменной и. В последнем случае получим формулу: Vx(3vF(x,v)=>VtiQ(x,ti)=>I^(x)). Если учесть enie реименование перемешюй х, то имеем: Vz(3vP(2,v)=>VtiQ(z,!i)=:>If(z) Полученные формулы толсе равносильны исходной формуле (2.22). § 10. Правила вынесения кванторов за скобки. Предваренная нормальная форма Выясним, каким образом выносятся кванторы за скобки, при этом получим и правила внесения кванторов под скобки. 70