Гильберт, Бернайс - Основания математики. Логические исчисления и формализация арифметики (947375), страница 74
Текст из файла (страница 74)
С помощью явного определения может быть введен какой-либо новый индивидный символ, предикатный символ или знак математической функции. Такое введение в формализм обычно производится при помощи какой-либо специальной аксиомы, которая в случае инднвидного символа или знака математической функции имеет вид некоторого равенства, а в случае предикатного символа — некоторой эевивалентпности; при этом в левой части определения стоит вводимый символ, аргументы которого (если таковые имеются) замещены отличными друг от друга свободными переменными, а в правой части стоит не содержащее вводимого символа (т. е.
построенное иэ ранее введенных эна- (гл. чп з $) некОтОРые пояснения пРинципиАльногО хАРАктеРА 359 358 РККРРСИВНЫЕ ОПРКДЕЛИИИЯ ков) выражение, такое что входящие в него свободные переменные совпадают с переменными, входящими в левую часть. В случае равенства оно является термом, а в случае эквнвалеытности— формулой. Так, например, с помощью явных определеыий мы можем ввести обычные еимво.зы для цифр, такие как 1 = 0', 2 = О", 3 =О". Далее, с помощью явных определений мы можем ввести принятые в математике символы (, ), ): а (Ъ а=Ь)/а(Ь, а)Ь Ь <а, а ) Ь а = Ь ')/ Ь ., а. В даз нейшем мы ые раз встретимся с различными примерами введения знаков тех или иных математических функций при помощи соответствующих явных определений ').
В случае такого явного определения всегда можно непосредственно убедиться в том, что принятие его не приводит ыи к какому противоречию, так как рассматриваемый новый символ всюду, где ьп встречается может быть заменен определяющим его выражением; при атом соответствующее определяющее равенство (или эквивалентность) переходит в выводимую формулу вида п=п (или а Я), Таким образом, получается, что если в некотором доказательстве какой-либо формулы )1, ые содернзащей данного явно определенного символа, этот символ встречается, то его можно устранить и в этом доказательстве, причем это можно сделать путем непосредственной замены нового символа определяющим его выражением.
Если мы теперь сравним рекурсивные определения с явнымн, то обнаружим некоторое сходство между ними, заключающееся ц зметвм, кстати, что в рзыкзх нашего формализма явное опрзязлзкз з фувкцковзльвого анака может быть прздстзвлоко к з виде язкоторой ракур- свв. Нзпряызр, зслк явное опрздзлзкяз имеет впд ф (а, л) = Ф (а, л), зо вместо него мы можая ввести рзкурсввпыз равенства ф (а, О) = 1 (а, О), ф (а, л') = Ф (а, л'), которые получаются подстановкой кз упомянутого выше опрзделяющзго равенства.
И обратно, зто явное опрздзлзввз с помощью схемы ккдукцяв может быть выводзво кз првзздзнпых взяв рзкурсввкых рзззяств. в том, что рекурсивные определения при помощи особой, допускающей определенную формализацию процедуры дают нам некоторую замену для любого из тех термов, которые получаются из какой-либо рекурсивно определенной функции при фиксации ее аргументов цифрами, а именно замену посредством той самой цифры, которая получается в результате вычисления соответствующего значения этой функции. Болев того, эта процедура дает нам некоторый терм-заменитель уже в том случае, если цифрой мы заменим только выделенную в данной рекурсии переменную.
Так, в качестве замены для а + 0" мы получим терм а", а для а 0" получим терм (а + а) + а. Эта замена обладает еще и тем свойством, что в результате ее выполнения рекурсивные равенства,' если в них вместо выделенной переменной и будет стоять какая- либо цифра, перейдут в равенства вида Действительно если ф (а,..., Й, и) — данная рекурсивно определенная функция, то рассматриваемые рекурсивные равенства после замены переменной и какой-либо цифрой Ь буду иметь вид ф (а, ..., Й, 0) = а (а, ..., Й), ф(а, ..., Й, 3') =Б(а, ..., Й, Ь, ф(а, ..., Й, 3)). В качестве терма, заменяющего ф (а,..., Й, 0), зти равенства непосредственно дают и (а,..., Й), а нахождение герма, заменяющего ф (а,..., Й, Ь'), происходит таким образом, что ф(а,..., Й, 35) с самого начала заменяется термом Ь (а,...
..., Й, 3, ф (а,..., Й, 3)). Уже в результате этого оба рекурсивные равенства перейдут в равенства вида и дальнейшие шаги замены больше не изменят указанного вида этих равенств. В только что рассмотренной процедуре замены аргументы-параметры а,..., Й остаются,' переменными. Если мы подставим цифры и вместо этих переменных, то процедура вычисления может быть продолжена далее, до тех пор пока все имеющиеся у нас рекурсивно введенные функциональные внаки ые будут исключены. При этом окончательном вычислении зыачений оба рассматриваемые рекурсивные равеыства, которые уже после первого шага процедуры приобрели вид должны будут перейти в нумерические равенства вида )гл. Уп РЕКУРСИВНЫЕ ОПРЕДЕЛЕНИЯ 3ВО 1 11 некотОРые пояснения ЛРинципиАльного ХАРАктеРА 332 И все же замена этого рода в том виде, в каком она получается при использовании рекурсивных равенств, ые дает нам никакого выражеыия, которым можно было бы заменить рекурсивно вве ен- ный функциональный знак с переменной на месте выделенного аргумента.
В этом и заключается существенное отличив рекурсивных опре- делений от явных, и с этим, в частности, связано то обстоятель- ство, что доказательство непротиворечивости результата добавле- ния рекурсивных определений к рассмотренным в гл. (21 системам аксиом с испольаованием процедуры замены мы сможем провести только при условии исключения из рассмотрения связанных пере- 'менных.
2. Доказательство непротиворечивости добавления рекурсывных определений в рамках элементарного исчисления со свободными пе- ременными; привлечение схемы индукции. Мы сейчас приведем это доказательство. Будут рассматриваться следующие, отличаю- щиеся друг от друга системы аксиом: во-первых, система ') (1,), (1,), (-= ), (<.), ( .), (Р,), (Р,), во-вторых, система (А) 2) и, в-третьнх, система (В) '); и и этом нам нужно будет исключить из рассмотреыия те аксиомы, которые содержат связанные переменные, т.
е. формулу а~Π— ~Эх(х =а) из системы (А) и аксиому индукции из (В). Все трн указанные системы формул обладают тем свойством, что за исключением второй аксиомы равенства (12) они содержат только такие формулы, в которых не встречается никаких пере- менных, кроме свободных иыдивидыых, причем все эти формулы являются верифицируемыми. Что к асается логического исчисления, которое мывозьмем, исключив из исчисления предикатов связанные переменные, то оно будет допускать в качестве исходных формул лишь тождественные формулы исчисления высказываний.
Будут также допускаться подстановки вместо формульных и вместо свободных индивидных переменных и применение схемы заключения. Это урезанное исчис- ленив мы для краткости будем ыазывать элементарным исчислением со свободными переменными. Иск м скомое доказательство непротиворечивости результата добав- ления рекурсивных определений к каждой из трех указанных систем аксиом с исключением связанных переменных будет полу- чено одновременно со следующей, болев общей теоремой: 2) См. с. 273. 2) См. с, 322. г) См.
с. 335. Пусть у нас имеется систпема аксиом, состоящая из формульг (12), т. е. а = Ь-э (А (а) -+-А (Ь)), и, кроме того, из некоторых других формул 11 'аг~ ° °" %1, которые: а) не содержат никаких переменных, кроме свободных индивидных, б) кроме логических символов содержат только символы =, (, О и символ штриха' и в) являются верифицируемыми, т. е. при любой подстановке цифр вместо свободных переменных переходят в истинные формулы.
Если мы к атил формулам дополнительно присоединим рекурсивные определения каких-либо функций и, значит, допустим в качестве термов вводимые этими определениями функциональные знаки (с аргументами), а соответствующие рекурсивные равенства допустим в качестве исходных формул (аксиом), то и тогда формула О Ф О будет невыводима средствами элементарного исчисления со свободными переменныии; более того, всякая выводимая нумерическая формула будет в этом случае истинной. Это утверждение легко установить методом исключения переменных.
Действительно, пусть 6 — нумерическая формула, для которой имеется доказательство, т. е. вывод из формул (12) а1~ ' ' '~ 61 и присоединенных к ним рекурсивыых равенств, проведенный средствами элементарного исчисления со свободными переменными. Тогда можно будет снова разложить это доказательство на нити '), и исключить из него переменные. разумеется, в получившейся в результате этого разложенной фигуре доказательства, не содержащей теперь переменных, в которой новые вхождения формул получаются из предыдущих посредством повторений или применений схем заключения, не все формулы обяааны быть нумерическими.
В них могут, ыапример, встречаться вводимые при помощи рекурсий функциональные анаки. Тем не менее все эти функциональыые знаки могут быть устранены соответствующими заменами, получающимися с помощью рекурсивных равенств. Действительно, у самых выутренних функциональных знаков в качестве аргументов фигурируют только цифры, так как переменные были нами исключены; значение, получаемое нами для такого функционального знака с цифрами при помощи процедуры вычисления, снова является цифрой.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
