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