Избранное
ЭБ Нефть
и Газ
Главная
Оглавление
Поиск +
Еще книги ...
Энциклопедия
Помощь
Для просмотра
необходимо:


Книга: Главная » Гильберт Д.N. Основания математики Теория доказательств
 
djvu / html
 

150 ИССЛЕДОВАНИЕ АРИФМЕТИКИ ПРИ ПОМОЩИ е-СИМВОЛА [ГЛ. II
появляется некоторая другая цифровая замена, либо (в случае функциональной замены) функция замены для некоторых (в конечном числе) систем значений аргументов вместо старого значения, равного 0, приобретает некоторое новое значение. Отсюда также следует, что все фигурирующие в рассмотрении функции замены получают отличные от 0 значения лишь для конечного числа значений (или соответственно систем значений) аргументов.
Замечание. Если исходный список формул SR имеет ранг 2, то списки 3ftb 3ft2, ... суть списки ранга 1. Поэтому при получении резольвент для этих списков можно обойтись без метода функциональных замен, т. е. можно ограничиться одними цифровыми заменами. Значит, в этом случае, не меняя нашей процедуры в прочих отношениях, можно ограничить применение основных типов для замен выражениями ранга 1. Такая процедура целесообразна, в частности, тогда, когда все имеющиеся е-термы ранга 2 имеют степень, равную единице; в этом случае построение резольвент для списков ЪЛЪ SR2, ••• удается осуществить рассмотренным вначале прямым способом.
д) Построение резольвенты в случае, когда все критические формулы являются формулами первого рода. Описанный метод построения общих замен пока еще не приводит нас к поставленной цели. Все еще остается нерешенной существенная задача — показать, что применение указанного метода всегда приводит к обрыву процесса. Такое доказательство удается получить лишь для случая, когда все критические формулы второго рода, входящие в рассматриваемый список, имеют ранг 1.
Прежде чем проводить доказательство при этом предположении, целесообразно сначала рассмотреть случай, когда выполняется еще более сильное предположение; а именно, мы потребуем, чтобы в рассматриваемом списке формул все критические формулы были формулами первого рода. Тогда ситуация упростится в том смысле, что при построении общих замен можно будет не переходить от экземплярных замен к минимальным, а всякий раз для построения новой общей замены непосредственно использовать экземплярные замены. Для такой упрощенной процедуры построения общих замен действительно удается показать, что после некоторого, заранее оцениваемого сверху числа шагов всегда получается резольвента.
Эта оценка строится рекурсивным образом. Как мы уже знаем*), для любого списка формул, имеющего ранг 1, количество общих замен, требующихся для построения резольвенты, не превышает 2", где п —число различных е-термов, входящих в данный список формул.
См, с. J45 и далее.

 

1 10 20 30 40 50 60 70 80 90 100 110 120 130 140 150 151 152 153 154 155 156 157 158 159 160 170 180 190 200 210 220 230 240 250 260 270 280 290 300 310 320 330 340 350 360 370 380 390 400 410 420 430 440 450 460 470 480 490 500 510 520 530 540 550 560 570 580 590 600 610 620 630 640 650


Математика