Колмогоров, Драгалин - Введение в математическую логику, страница 13

Например, если в формуле ЗуР(х, у, г) мы решим заменить переменную у на переменную х, то получится фор. мула ~хР(х, х, г), которая имеет совершенно иной смысл, чем исходная формула. Прежде всего, ~хР(х, х, й) зависит уже лишь от одного параметра г, а не от двух, и' задает всегда истинный предикат от г. Причина неприятности -состоит в том, что после неудачного переименования связанной переменной у первое вхождение переменной х,' которое раньше было свободным, стало связанным.

Указанное явление мы назовем коллизией переменных при переименовании связанных переменных. Коллизия переменных недопустима. По существу, эта ситуация хорошо известна и в обыденной математике. В сумме !о ~, ау переменная ! связана «квантороы суммы» Х, а переменная 1 остается свободной — параметром суммы. Вместо 1 мож- бз но подставить конкретное значение и рассмотреть сумм ~о например ~~, а„, в то время как вместо ( бессмысленн к=~' подставлять конкретные значения. Переменную ! можно з го менить на другую, например, ~, аы — это будет, в су о-! ности, та же самая сумма (иногда говорят, что индекс «немой» и допускает переименование). Однако если вмест ( подставить /, то произойдет коллизия переменных — сум ы ма ~' ап имеет уже совсем другой смысл (говорят, что пе с-з ременная ) «уже занята» и нельзя вместо г' подставить )).

Аналогично,,в интеграле ~ хоуйх о переменная у во всех вхождениях свободна, а переменная х связана «кванторной приставкой» йх. Переменную х мож- но заменить на переменную х — интеграл от этого не изме- нится, но отнюдь не на переменную у! !2. Уточним теперь, что именно означает ситуация, ког- да две формулы А и А' отличаются друг от друга лишь пра. вильным (т. е. без коллизий переменных) переименованием связанных переменных. В этом случае мы будем говорить, что формулы А и А' коигруэнтны, или, что формула А' яв- ляется вариантом формулы А, и писать А-А'. Рассмотрим некоторую формулу, например, 'р'х(Р(~(х) ) Л ~ хЯ(х, х) =э~ у)т(х, у) ) ~/Я(х, у). Отметим линиями связанные переменные этой формулы и кванторы, от которых происходит связывание: 1 1 1 1 Чх( (Пх)) ЛЭ.()(.,г) Эуя(х,у)) Л(г,у).

! 1 Сотрем теперь все связанные переменные, оставляя линии 1 1 1 !У(РЧ()) ~ЗЕ(, ) З)~(.»Ча(, р). 1' ) ! Полученную фигуру можно назвать скелетом исходной формулы. 64 Две формулы жонгруэнтны тогда В только тотда, когда ях скелеты совпадают. Упражнение. Укажите несколько вариантов формулы 'ух(Р(х)/~ ~ гЯ(х, х)~~уй(г, у))~/Я(х, х). Какие переименования связанных переменных ведут к коллизии? Можно дать и аккуратное математическое определение отношения А А' индукцией по логической сложности 1(А) формулы А.

А именно: А. Единственным вариантом атомарной формулы является она сама. Б. Если А имеет вид (ВАС), то всякий вариант А' формулы А имеет вид (В'АС'), где В~ В' и С С'. Если А имеет вид 1В, то всякий вариант А' формулы А имеет вид ~В', где В В'. В. Если А имеет вид ЯхВ, то всякий вариант А' формулы А имеет вид ЯуС, где у и С таковы, что для всякой новой переменной х '(т. е. не входящей ни свободно, ни связанно в формулы ЯхВ и ЯуС) имеем В, С",.

Здесь через В»» обозначен результат замещения всех свободных вхождений переменной х в В на переменную х. Аналогично понимается С«,. Предполагается еще, конечно, что все три переменные х, у, х имеют один и тот же сорт. Приведенное определение дает возможность точно доказывать различные свойства вариантов формулы А индукцией ~по логической сложности ((А) формулы А. Например; нетрудно доказать, что если Аж А', то !(А) =1(А'), Еч(А) = =Гч(А') и А н А' имеют один и тот же главный (т. е. последний в построении) логический символ. Отношение ж 'является отношением эквивалентности между формулами рассматриваемого языка„и с точки' зрения смысла формул конгруэнтные формулы можно считать «несущественно отличающимися друг от друга». Можно 'ска.

зать, что математическая логика изучает скорее не отдельные формулы, а классы конгруэнтных между собой формул. 5 2. О ПРАВИЛЬНОЙ ПОДСТАНОВКЕ,ТЕРМОВ В ФОРМУЛЫ Е Формальной подстановкой (или просто подстановкой) назовем функцию О, определенную на конечном (может быть, и пустом) множестве переменных языка (г и перерабатывающую каждую переменную х из областиопределения 0 в некоторый терм 0(х) языка, причем х и 0(х) имеют один и тот же сорт. Формальную подстановку можно изображать в виде дву мерной таблицы '('Хм Хм ..., Х») где в верхней строке указана область определения функции О: догп 0=(хь ..., х») и, кроме того, 0(х;) =(ь Здесь х; и г; имеют один и тот же) сорт. Порядок столбцов в двумерной таблице несуществен.", Таблица может.

быть и пустой, если функция О имеет пу-1 етую область определения, 2. Пусть Т вЂ” выражение языка (з (т. е. формула или, терм) и 8 — формальная подстановка ~"1 ''' ~"'). Через (ТО) мы обозначим результат одновременного замещения, всех-свободных вхождений переменных хь ..., х» в Т на тер-' мы 1ь ..., г» соответственно. Конечно, при этом некоторые х; могут и не входить свободно в Т. Тогда соответствующие 6~ никуда не подставляются и просто не играют никакой роли. Подчеркнем, что замещаются только свободные вхождения д в Т.

Вместо (ТО). будем иногда употреблять одно из следую= щих обозначений: . ТО, т Ч'"""') Т' к1 " ° к» п,....1»' Дадим теперь индуктивный рецепт для вычисления под- становки в формулу. Этот рецепт можно рассматривать и как самостоятельное индуктивное определение подстановки. Можно убедиться с помощью индукции, что оно эквивалент- но данному ранее определению. л. (ррь ..., ( ) О) =Р((,о, ..., (.8), Б. (Адв)е=(АОАВО), ( ~АО)=' 1(АО), В. (Вве) =а (в(8 — (г))). Здесь через 0 — (а) обозначен результат квыбрасывания» пе- ременной г из области определения О, т. е. 0 — (а) есть та- -кая подстановка О', что хогне'=скоте~(а) и 0'(х)=8(х) для всякой переменной хыдогп 0'.

3. Уп р а жн'е н не, Вычислите результаты подстановок: 1) (пуР(х,у, г)( " )); 2) (~УР(х, у, г) ( У )) ° 3) (~УР(х, у, г)) 4) (пг'УУР(х, У)=э(г(х))7(х г)' 5) (\ф УР (х, у) '-> Я (х)) б) (Р(х, у):э'у'У0(у)) )Р(х. У),г' 7) (~l уР (у, г)',4 и уй (х' у) ) р(х у) г' 4. Заметим теперь, что не все подстановки одинаково пригодны с точки зрения логики. Пусть, например, в некотором языке атомарная формула Р(х, у, г) выражает ~преднкат х+у=г, где переменные пробегают натуральные числа О, 1,-2, .... Формула 3 УР(х, у, г) выражает уже предикат от переменных х и г', а именно х~г, Пусть в этом же языке терм 7(х, у) задает операцию умножения натуральных чисел х у.

Теперь мы желали бы подставить )(х, у) в ~УР(х, у, г) вместо свободной переменной х с целью выразить предииат от трех переменных. х у<г. Однако ошибочно было.. бы рассмотреть с этой целью формулу Я УР (х, у, 'г) '( " ) ), т. е. формулу ((х, у)) П УР(7(х, у), у, г). Эта послсдняя формула выражает совсем,иную мысль (в частности, она зависит от двух параметров х и г, а не от трех).

Причина затруднения состоит в том, что переменная у была свободна в терме 1(х, у), а оказалась связанной в результирующей формуле. Как говорят, ~произошла коллизия переменных и ри подстановке. Правильный выход из положения состоит в том, что сна. чала следует переименовать связанную переменную у, например образовать формулу АР(х, и, г), которая выра. жает тот же предикат, а уже затем произвестл подстановку, так что в результате получим формулу ПиР(((х, у), и, г), которая,и выражает нужный предикат. 5.

Выделим теперь клясс подстановок, которые заведомо не приводят к коллизии переменных. Подстановка О называется свободной для выражения (или допустимой для выражения Т), если для всякой пере менной хыдотО любое свободное вхождение х в Т не по, падает в область действия кванторов:по переменным, сво бодно входящим в терм О(х). Упражне.нне. Выясните, какие;из подстановок п. ' свободны. Как всегда, мы укажем и индуктивное определение сво бодной подстановки: А.

Если Т вЂ” терм или атомарная формула, то всякан подстановка является допустимой для Т. Б. О свободна для (АЛВ)~=:-О свободна для А и О сво бодна для В. 0 свободна для 1А~=~О свободна для А. В. 8 свободна для ЯгВ с=~ подстановка 0 †(х) свободна' для В, и, кроме того, для всякой переменной хобот 0() ()Е»ЯхВ) терм 0(х) не содержит свободно переменной г.: б. Если для всех хыйотО выражение Т новое не содержит кваиторов по параметрам терма О(х), то О допустима для Т. Просто обстоит дело и в том случае, если для всякой переменной х~йош(О) терм О(х) является замкнутым.