Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 27
Текст из файла (страница 27)
Теперь возникает задача развить этот метод так, чтобы его можно было применить к любому нормированному доказательству нашего арифметического формализма. Прежде всего мы сделаем одно общее упрощающее замечание. Оно состоит в том, что нам всегда будет достаточно позаботиться лишь о тех е-термах рассматриваемого нормированного доказательства, которые фигурируют в каких-либо критических формулах или формулах е-равенства. Действительно, если мы для этих термов укажем такие цифровые замены, в результате которых критические формулы и формулы е-равенства перейдут в истинные формулы, то оставшиеся е-термы мы сможем заменить цифрой О и при этом сохранятся схемы заключения и повторения формул.
Поэтому можно вообще отвлечься от рассмотрения нормированных доказательств как таковых, и наша задача попросту сводится к тому, чтобы для любой конкретно заданной совокупности критических формул и формул е-равенс1ва, принадлежащих рассматриваемому нами арифметическому формализму, найти такие замены для фигурирующих в них е-термов, в результате которых зтн формулы стали бы истинными. Набор таких замен !28 ИССЛЕДОВАНИЕ АрнфМЕтИКИ ПРИ ПОМОШИ е-СИМВОЛА !ГЛ, и.
первонАчАльныи гильБертОБскпи пОдхОд 129 мы будем называть резольвентой данной рассматриваемой, совокупности критических формул и формул е-равенства. В разобранном частном случае мы имели дело только с кри., тическими формулами, причем предполагалось, что в этих фор-, мулах встречается всего лишь один е-терм. Из рассмотрения: этого случая мы теперь извлечем способ, позволяющий строить:. резольвенты и для таких совокупностей критических формул, что все входящие в них формулы имеют степень 1 и ранг 1, и ни один из тех е-термов, с которыми связаны эти критические ' формулы, не содержит вложенных в него е-термов или подчинен- . ных ему е-выражений. В самом деле, если при указанном условии ( Е (е)) или соответственно 6 (1) - Б Я (й) чь 1' является одной из данных критических формул, то в формулу Я (с) не могут входить никакие Б-термы, и поэтому любой е-терм, .
отличный от терма е 6 (й), может встречаться в рассматриваемой формуле только внутри терма 1. Отсюда вытекает, что ни одна критическая формула не поте-, ряет своего вида, если мы заменим в них цифрой 0 те с-термы, с которыми не связаны никакие критические формулы. Этот прием сводит дело к рассмотрению случая, когда, кроме Б-термов, с которыми связаны какие-либо крчтические формулы, — мы обозначим их буквами с„..., с„, зафиксировав какой-либо порядок для них, — у нас вообще не будет встречаться никаких других е-термов. Мы должны теперь найти подходящие замены для термов сп ...
Набор, состоящий из каких-либо цифровых замен для термов с„, ..., с„, мы будем называть общей заменой. Мы начнем с общей замены, состоящей из 0-замен для каждого -' из термов с„..., с„. Если в результате этой 0-замены все критические формулы станут истинными, то она и будет искомой ! резольвентой. В противном случае для каких-либо термов из числа с„..., ср мы найдем экземплярные замены, а по ним определятся и минимальные.
Мы построим теперь новую общую замену, взяв '.;. вместо 0-замены минимальную для тех термов с„ для которых ' она будет найдена. Тогда все связанные с этими е-термами критические формулы станут истинными. Если окажется, что и все остальные критические формулы стали истинными, то мы получим искомую резольвенту. В противном случае мы найдем минимальные замены для некоторых других термов из числа см ... ,, е» и затем построим новую общую замену, взяв найденные минимальные замены вместо О-замен, Мы можем продолжать двигаться таким образом и дальше. Но этот процесс не позже чем после р-кратного изменения общей замены должен будет оборваться, так как на каждом шаге не МЕНЕЕ ЧЕМ ДЛЯ ОДНОГО тЕРМа, ВХОДЯЩЕГО В СПИСОК Ем ..., Ср, ОПРЕ- деляется минимальная замена и, найденная однажды, минимальная замена остается без изменений.
Поэтому, если резольвента еще не была получена раньше, то после р-й общей замены для каждого из термов е„..., с„будет найдена минимальная замена, а в результате (9+1)-й общей замены, в которой будут использоваться все эти минимальные замены, все критические формулы станут истинными. Таким образом следуя этому точно сформулированному предписанию, мы не позже чем через р+1 шаг придем к построению искомой резольвенты. Замечание. Отметим, что переход от экземплярной замены к минимальной необходим только для тех термов рп с которыми связаны какие-либо критические формулы второго рода; для остальных термов мы можем сохранить их экземплярные замены.
б) Подготовка к рассмотрению общего случая. Рассмотренный нами случай является пока очень частным, и мы теперь должны будем освободиться от ограничений, наложенных на степени и на ранги критических формул. Кроме того, нам нужно будет принять во внимание еще и тот факт, что в совокупности формул, для которой будет строиться резольвента, наряду с критическими формулами могут также содержаться и формулы Б-равенства.
В порядке подготовки к этому нам будет целесообразно составить более подробно представление о том, как на нашей процедуре замены могут сказаться вложенность и подчиненность е-термов. Дело в том, что при рассмотрении самого общего случая некоторые существенные Осложнения возникают именно из-за того, что свойство цифры 1 быть экземплярной или минимальной заменой для терма е 6(е), вообще говоря, зависит от замен тех е-термов, которые входят в Я (!) или соответственно в Я (0), 6(0'), ..., 6(1). Наличие же таких е-термов обусловливается степенью и рангом терма е 6(е), т. е. имеющими место в этом терме случаями вложений и подчинений. С отношениями вложенности и подчиненности мы уже познакомились раньше').
Здесь мы отме~им, в частности, следующие факты: е) Ом. с. 43 — 44. (! Д. Глльберп П. Берлейс — 149 1ЗО ИССЛЕЛОВАНИЕ АРИФМЕТИКИ ПРИ ПОМОШИ Ф.СИМВОЛА (ГЛ П * 1. Каждый и-терм, вложенный в терм и Я(у), входит в фор-. мулу Я(с), причем таким образом, что переменная с им не охва.' тывается. И обратно, каждый входящий таким образом в фор- .
мулу Я(с) е-терм вложен в терм е Я(у) и тем самым имеет более низкую степень, чем этот последний. 2, Каждому и-выражению, подчиненному и-терму е Я (у), в фор-: муле Я(с) соответствует некоторый е-терм, охватывающий переменную с и получающийся из этого выражения в результате замены переменной у переменной с.
И обратно, каждому входя- ' щему в формулу Я(с) и охватывающему переменную с и-терму, соответствует некоторое н-выражение, которое подчинено терму е Л(у) и из которого этот е-терм получается в результате замены переменной у переменной с; таким образом, этот и-терм имеет ранг, меньший ранга терма Б„Я(у). Согласно утверждению 1 мы можем заключить, что в случае и-терма, имеющего ранг, равный единице, ситуация, связанная с заменами, является достаточно простой. Действительно, в этом случае истннностное значение, получающееся для формулы Я(б), где й' — некоторая цифра, при какой-либо общей замене, зависит: только от замен тех Б-термов, которые вложены в терм е Я(у).
Таким образом, хотя экземплярная или минимальная замена для терма БЕЯ(р) и может перестать быть таковой, тем не менее это может случиться только тогда, когда будет найдена некоторая экземплярная замена для некоторого вложенного в и Я(к) и-терма (т. е. для терма, имеющего степень, меньшую степени терма е Я(у)). Если, в частности, степень терма е Р((у) равна единице, то найденная для этого терма экземплярная (соответственно минимальная) замена как таковая является окончательной. На этом пути мы получаем некоторый спуск, который, как мы увидим позже'), в том случае, когда имеются только критические формулы ранга 1, позволяет достаточно простым способом получить (после наперед оцениваемого числа общих замен) некоторую резольвенту.
Однако прежде чем проводить это рассуждение, будет полезно еще более детально познакомиться с тем, как мы предполагаем организовать нашу процедуру замены в случае критических формул высоких рангов, потому что рассмотрение критических формул, имеющих ранг, больший единицы, показывает, что наша процедура замены в ее нынешнем виде является неудовлетворительной. Мы сталкиваемся в ней со следующими трудностями. Если терм Б Я(у) имеет ранг, не меньший двух, то, согласно утверждению 2, переменная с находится в формуле Я(с) внутри л) См, п, в), с. 140 — 146. ПЕРВОНАЧАЛЬНЫН ГИЛЬБЕРТОВСКИЙ ПОДХОД некоторого е-терма Б„дл(с, и), т, е.
Л(с) имеет вид й(с, Б„Э(с, и))'). Поэтому любая связанная с з-термом и Я(у) критическая формула первого рода имеет вид Й (1, Б,8 (1, и)) — й (БЕЯ (у), Е„З (Б Я (р), и)). Допустим теперь, что, отправляясь от этой формулы, мы нашли— прн помощи некоторой общей замены, при которой эта формула становится ложной, — какую-либо экземплярную замену для терма и Я(р), т. е. указали соответствующую цифру 1, получающукся а из 1 на основе этих замен и значений некоторых постоянных термов. Тогда замена, которую прн этой общей замене получит терм еье)((, и), должна быть получена по некоторой замене для ТЕрма Еьб(й П).
ДЕйСтВИтЕЛЬНО, В ПрОтИВНОМ СЛуЧаЕ МЫ НИКаК НЕ смогли бы заклк1чить, что в результате рассматриваемой общей замены формула Я(1) оказывается истинной. Между тем терм Б,О(1, и) с самого начала мог и не встречаться в заданной иам совокупности формул. Таким образом, мы не можем обойтись заменами для Б-термов, непосредственно фигурирующих в заданной пал| совокупности формул. Тем не менее можно без труда указать путь, позволяющий удовлетворить перечисленным выше требованиям: выход будет заключаться в том, что необходимые замены для и-термов мы будем осуществлять в виде некоторой производимой изнутри шагаобразнай рсдукиии.
Рассмотрим следующий пример, поясняющий наш замысел, Пусть нам требуется найти замену для е-терма Б,Я(х„ек3(у, и,й(г)+3) 5, 2 1), в который не входят никакие и-символы, кроме явно указанных. Пусть в нем также не встречается в качестве составной части ни один терм, кроме указанных явно. Тогда наша замена «изнутри» будет происходить следующим образом. Сначала заменяется своим значением, т. е. цифрой О", постоянный терм 2.1.