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