Гильберт, Бернайс - Основания математики. Логические исчисления и формализация арифметики (947375), страница 93
Текст из файла (страница 93)
Пусть Я' — формула, возникающая таким образом из формулы сЯ. В выводе Я' аксиома (1,) может быть заменена формулой (1,) н рядом формул ($»), „(1и) вида а=Ь-+.($1(а)- ф~(Ь)) (1=2, ..., Д). Действительно, каждому из введенных предикатных символов и каждому из его аргументов соответствует некоторая формула такого рода. Эти формулы таковы, что у предикатных символов с несколькими аргументами не указанные в обозначении ф» (а) аргументы представляют собой свободные переменные, отличные друг от друга, от а и от Ь. Сопоставим каждой из этих отличных от а и от Ь свободных переменных какую-либо связанную переменную.
Пусть х,у,...,и представляет собой список всех этих связанных переменньсх, 30 Д. Гвльберт, П. Веряаае Г Л А В А Ч111 РЕКУРСЕВНЫЕ ОПРЕДЕЛЕНИЯ 466 1гл. У11 ') С»ь с. 455 и далее, н пусть )д1« (а) — выражение, получающееся иэ $1 (а) в реаультате замены каждой отличной от а свободной переменной сопоставленной ей связанной переменной. Рассмотрим формулу 'Ух)Уу ...)Уи((Ф»(а) — ))5;(Ь)) д ... д ()[5й(а) - д5й (Ь))).
В этой формуле, которую мы обозначим посредством 6 (а, Ь), а и Ь суть единственные входящие в нее свободные переменные. Легко убедиться, что формулы 6 (а, а), 6 (а, Ь) -1-(6 (а, с) -+ 6 (Ь, с)), 6 (а, Ь)-+. ()р1(а)-+.'4»1(Ь)) выводимы средствами исчисления предикатов. Но эти формулы получаются из формул (УД, (1,), (1»),..., ([в) в результате аамены равенства а = Ь формулой 6 (а, Ь). Таким образом, если мы в упоминавшемся выводе формулы 6' всюду произведем замену равенства а = Ь формулой 6 (а, Ь), то встречающиеся в ней вхождения формул (3,), ([,),..., (1в), добавленных в качестве аксиом к основным формулам исчисления предикатов, перейдут з такие формулы, которые могут быть выведены с помощью исчисления предикатов.
С другой стороны, при этой замене формула 6', в которую знак равенства не входит, останется без изменений. Таким образом, мы получаем вывод формулы 6' в рамках исчисления предикатов беа присоединения каких-либо дополнительных аксиом. Теперь мы можем снова вместо предикатных символов вставить в этот вывод первоначальные формульные переменные. Тем самым получится некоторый вывод формулы 6 в исчислении предикатов. Итак, любая формула исчисления иредикатов, выводимая с добавлением аксиом равенстви, будет вывод мой и в самом исчислении нредикатов.
После этих вспомогательных замечаний мы снова займемся нашей основной темой. Как мы уже говорили, нашей ближайшей аадачей является исследование понятия «тот, который», изображение которого в формализме необходимо в дополнение к формализации процесса вывода. Это исследование приведет нас, в частности, к уже упоминавшейся теореме об устранимости понятия «тот, который» и в связи с этим позволит нам убедиться, что в системе (Е) оказываются представимыми все рекурсивные функции' ). ПОНЯТИЕ «ТОТ, КОТОРЬ[Й» И ЕГО в'СТРАНИМОСТЬ з $. »-правило и оперирование с ним т.
Рааъяснения неформального характера; введение «-правила; предотвращение коллизий; иэображение функций посредством ь-термов. Наш логический формализм в том виде, как мы его до сих пор развивали, вполне достаточен для целей формализации акспоматических теорий и проводимых в них доказательств. Теы не менее в нем отсутствует изобрая«ение одной логической конструкции, часто используемой в повседневном мышлении, и в особенности в математике, хотя в доказательствах применения ее можно было бы и избежать. Логическая операция, о которой здесь идет речь, в языке выражается при помощи оборотов типа определенного артикля.
Примерами могут служить такие обороты, как «высочайшая вершина Альп», «мать Гете», «ко»шозитор, сочинивший данную оперу», «камень, который мы вчера нашли» *). Из области математики в качестве примеров можно привести «нанбольший общий делитель чисел 63 н 84» или «наибольшее значение функции х е-"*».
Здесь всякий раз некоторый объект характеризуется тем, что для пего и только для него выполняется некоторый вполне определенный предикат. В области рассматриваемых нами высказываний всякий такой предпкат изображается некоторой формулой ') и условие, по этот предикат выполняется для одного н только для одного объекта, выражается с помощью следующих двух формул: ехр[ (х), )е хну (Я (х) бе И (у) -» х = у), которые называются формулами единственности д л я р[ (а).
Разумеется, нам нужен специальный символ, который *) Все примеры в орпгппзве начинаются определенным артиклем, в русском языке отсутствувтпм.— Прим. верее. ') Пзрзывппвя в, подобно пвдпвпдпой в»ременной какой-либо пи»»пой Формы, слувепт здесь только для указания песта,яз котором стоит аргумент. зо- 4зз понятие «тот, котОРыпх и егО УстРАнимость [Гл. Уш 469 РПРАВИЛО И ОПЕРПРОВ «НИЕ С НИМ характеризовал бы сопоставление предикату Я(а) того единственного объекта, для которого Я(а) выполняется. Объект этот определяется пробегом значений предиката «1(а); а соответствии с этим, при формализации указанного сопоставления аргумент предиката Я играет роль связанной переменной.
Следуя Расселу и Уайтхеду, мы используем символ «хЯ (х) (читается: «тот объект х, для которого имеет место г1 (х)»). Выражение такого рода мы будем называть х а р а к т е р и с т ик о й. Рассел н Уайтхед, особенно настойчиво подчеркивавшие своеобразие рассматриваемой нами конструкции, содержательно истолковывают формулы вида 5 («„Я (х)), в которых вместо герма фигурирует некоторая характеристика, понимая под Ь (««Я (х)) следующее высказывание: «существует единственный объект, для которого имеет место Я(а), и для этого объекта имеет место также и )В (а)ы В соответствии с этим, формула, в которой встречается символ ьхЯ (х), всякий раз изображает лоп«ное высказывание уже в том случае, если для Я (а) не выполняются условия, изображенные соответствующими формулами единственности.
Это истолкование формул вида 5 (~„Я (х)) не носит характера явного определения для символа (~ -с и м в о л а) ьх Я (х); действительно, оно не дает для этого символа выражения, которое непосредственно определяло бы его, а лишь определяет формулы, в которые 1х Я (х) входит вместо некоторого герма как составная часть. Но все же мы можем извлечь нз этого истолкования некоторый подход к доказательству, с помощью которого мы установим устранимость характеристик (исимволов). Для того чтобы упорядочить применение «-символа в нашем исчислении, мы будем как можно ближе придерживаться фактически соблюдаемого в речевом обиходе, и в особенности в математике, правила, которое заключается в том, что выражение «тот объект, которыи обладает свойством Я» употребляется лишь в том случае, когда уже установлено, что существует один и только Один объект, обладающий этим свойством. В соответствии с этим, выражение «х Я(х) мы будем допускать в качестве герма только тогда, когда уже выведены соответствующие формулы единственности для Я (а).
Кроме того, мы должны выразить еще и то обстоятельство, что в упомянутом случае терм «хЯ (х) изображает как раз такойобъект, для которого Я (а) имеет место. Так мы приходим к формулировке следующего правила употребления ысимвола, которое мы для краткости будем называть «-правилом: Если длл формулы Я(а) выведены формулы единственности, то, начинал с этого момента, выражение ~хЯ(х) (или соответственно ««Я (у), «,Я (з)) будет считал«ьел термом, а формула Я (~ Я (х)) будет считаться формулой, выведенной по схеме ЛхЯ (х) «1х««у (Я (х) д«Я (у) -+.
х = у) Я( «Я(х)) Разумеется, это ыправило еще нуждается в уточнении в части, касающейся применения связанных переменных. В отношении входящей в «-символ связанной переменной, как и в отношении переменных, связанных кванторами всеобщности и существования, будет действовать правило их переименования. В случае кванторов всеобщности и существования это правило применялось для того, чтобы избежать коллизий между связанными переменными '). Теперь это требование отсутствия коллизий мы распространим и на связанные переменные, входящие в состав ысимволов. Это означает, что для того, чтобы какое-либо выражение могло считаться ф о р м у л о й или соответственно т е рм о м, мы будем требовать, чтобы ни один из кванторов существования и всеобщности и ни один из исимволов ке попадал в нем в область действия другого квантора нли «-символа с той же самой связанной переменной.
Так, например, ни один из символов «у, Зу, «У не должен находиться в области действия какого-либо другого из этих знаков в сочетании с той же сапой связанной переменной у. Наличие правила переименования связанных переменных всегда дает возможность избегать таких коллизий между связапнымн переменными.
11ри употреблении ~-символов мы постоянно должны будем пользоваться этими переименованиями. Уже при выводе формул единственности всякая связанная переменная. входящая в Я (а), должна получить наименование, отличное от х и от у. Кроме того, следует заметить, что образование выражения Я (~„Я (х)), если формула Я (а) содержит какую-либо связанную переменную, всегда дает повод к коллизии между связанными переменными. Во всех этих случаях «-правило должно пониматься таким образом, что в заключительной формуле схемы в выражении ьх Я (х) производится переименование всех входящих в я (а) связанных переменных, так что в получающемся выражении ~„Я«(х) нн ) См.
с. 133. 4ТО ПОНЯТИИ»ТОТ, КОТОРЫЙ» И ВГО УСТРАНИМОСТЬ 1ГЕЕ» ЧП1 ~ ПРАВИЧО И ОПСРИРОВАЕ1ИЕ С НИМ одна из этих переменных больше не встречается, и потому в Я (Е„Я*(х)) коллизий между свяаанными переменными не будет. Пусть, например, Я (а) представляет собой формулу Зг(г=боег=а), Формулы единственности для нее могут быть получены из аксиом равенства с помощью эквивалентности а = О Эг (г = О ое г = а). Тем самым 1-правило может быть применено к Я (а). Тем не менее при этом с самого начала имеется трудность, ааключающаяся в том, что в выражении Я (Е„Я (х)), которое записывается в виде Лг (г = О сч г = 13г (г = О А г = х)), имеет место коллизия между свяаанными переменными, так как в нем в области действия стоящего слева квантора существования Зг этот же самый квантор встречается еще раз.
Мы избежим этой коллизии, переименован внутри Е„Я(х) переменную г в какую-нибудь другую переменную, например в и. Измененный таким образом терм Е,Эи(и = Оапек =х) теперь можно будет подставить в формулу Я (а) вместо а, и при этом получится формула Зг (г = О бе г = Е,Ли (и = О бе и = х)), которая по схеме 1-правила следует иа формул единственности для Я (а). В дальнейшем это выполнение переименований в целях избежания коллизий между связанными переменными всегда будет рассматриваться как сосепавная часть применения Оправила и не всегда будет оговариваться специально. В дальнейшем простоты ради мы будем разрешать вались Я (Е„З (х)) и в тех случаях, когда подстановка терка Е„З (х) в формулу Я (а) требует переименования одной или нескольких связанных переменных н когда для указания этих изменений следовало бы более точно писать Я (Е„З' (х)).
В качестве простого примера на применение ыправила установим выводимость эквивалентности Я (а) а = 1„ Я(х) для формулы Я (с) с уеке выведенными формулами единственности, В самом деле, 1-правило дает нам формулу Я (1„Я (х)), а эта формула в сочетании с аксиомой равенства (з,) дает а= «„Я (х)«- Я(а). С другой стороны, импликация Я (а) -»- а = Е„Я (х)1 получается из формулы Я(Е„Я(х)) в сочетании со второй формулой единственности. После этих дополнений к е-правилу мьЕ сделаем также ряд аамечаний относительно содержательного понимания введенных при помощи 1-правила термов. Вводя 1-символ для целей формализации понятия «тот, который», мы исходили из рассмотрения таких формул Я(а), с помощью которых изображается вполне определенное свойство некоторого (подставляемого вместо переменной а) объекта.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
