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