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

бранного нами квантора и в области действия этого квантора. Это значит, что одинаковые переменные, для которых связывающие их кванторы имеют раз­ личные области действия, могут переименовываться разным образом или одна из них может переименовываться, а другая нет. Рассмотрим действие приведенного правила на примерах. Пусть имеем формулу VxA(х) ^ЗхВ(х) =^(х). (2.21) Переименовав связанную переменную х на в первой посылке получим формулу, равносильную исходной: \/уЛ(у)^ЗсВ(х)^>С(х). Из формулы (2.21) переименованием можно получить формулу VxA(x) ^3zB(z) ^>С(х) или \/хЛ(х)^ВуВ(у)^>С(х). При этом каждая полученная формула будет равносильна исходной формуле (2.21). Отметим еще раз, что переименовываются только связанные переменные, а свободные не трогаются. Так, в формуле (2.21) последнее вхождение х свобод­ но, поэтому при любых переименованиях переменная х остается неизменной. Рассмотрим еще один пример. Пусть задана формула Vx(3yP(x,y)^ VyQ(x,y)^R(x)). (2.22) Переименовывая в этой формуле переменную х, нужно заменить ее оди­ наковым образом всюду, где она входит, ибо х в формуле (2.22) является либо переменной квантора, либо находится в области действия квантора. Например, переименовав х на z , получим следующую формулу, равносильную исходной: Vz(3yP(z,y)^ VyQ(z,y)^R(z)). В формуле (2.22) переменную у можно переименовать в первой посылке, например, на переменную v, а во второй оставить без изменения либо заменить, например, переменной и. В последнем случае получим формулу: Vx(BvP(x,v) ^VuQ(x,u) ^R(x)). Если учесть еще переименование переменной х, то имеем: Vz(3vP(z,v)^VuQ(z,u)^R(z)). Полученные формулы тоже равно­ сильны исходной формуле (2.22). Переименование переменных удобно делать не только для формул. Ино­ гда это упрощает визуальные проверки программ. В параграфе 3 данной главы была приведена программа на Паскале, в которой локальная и глобальные пе­ ременные были обозначены через X. Если в качестве локальных и глобальных переменных ввести разные символы, то меньше вероятность запутаться в про­ грамме. 45