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


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

so
ИСКЛЮЧЕНИЕ СВЯЗАННЫХ ПЕРЕМЕННЫХ, fffl. I
в некоторую критическую формулу, причем эта последняя будет связана либо с тем же самым е-термом, что и начальная критическая формула (случай 1), либо с некоторым новым е-термом, имеющим тот же самый ранг. Далее /заметим, что при любой замене е-терма t всякая критическая формула, связанная с каким-либо е-термом а, имеющим степень, не большую степени терма t, снова переходит в некоторую критическую формулу, связанную с а. В самом деле, случай 2, как мы знаем, может иметь место лишь тогда, когда степень е-терма, с которым связана измененная в результате замены терма t критическая формула, больше степени терма t. А в случае 1 е-терм, с которым связана данная критическая формула, остается без изменений.
Это рассуждение дает нам возможность следующим образом устранить из любого наперед заданного нормированного доказательства какой-либо формулы (? все его критические формулы. Среди чисел, являющихся рангами термов, с которыми связаны какие-либо критические формулы, имеется наибольшее. Ранг того е-терма, с которым связана какая-либо критическая формула, мы для краткости будем называть рангом этой формулы, а степень этого е-терма мы будем называть степенью этой критической формулы. Пусть т —наибольший из рангов критических формул, фигурирующих в данном доказательстве, и пусть п —наибольшая из степеней критических формул, имеющих ранг т. Пусть t — один из тех е-термов, имеющих ранг m и степень п, с которыми связаны какие-либо критические формулы. Если мы применим нашу процедуру к связанным с термом t критическим формулам, то вследствие произведенных при процедуре исключения замен в пребразованном доказательстве формулы (? вместо одной не исключенной критической формулы может появиться несколько различающихся между собой формул; однако все они также будут критическими формулами (т. е. формулами, получающимися в результате подстановки из е-формулы); более того, все они будут связаны с одним и тем же е-термом.
Таким образом, в результате устранения связанных с термом t критических формул количество различных е-термов ранга т, с которыми связаны какие-либо критические формулы, уменьшится на единицу, причем никаких критических формул с новыми рангами не появится. Следовательно, если в начальный момент у нас было f различных е-термов ранга т, с которыми были связаны какие-либо критические формулы, то f-кратное применение нашей процедуры приведет к тому, что все критические формулы, имеющие ранг т, будут исключены, причем не появится никаких критических формул с новыми рангами. Таким образом, у нас имеется способ, позволяющий уменьшать количество различных фигурирующих в нашем рассмотрении рангов критических формул. Повторив его нужное число раз, мы полностью исклю-

 

1 10 20 30 40 50 51 52 53 54 55 56 57 58 59 60 70 80 90 100 110 120 130 140 150 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


Математика