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


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

60 ИСКЛЮЧЕНИЕ СВЯЗАННЫХ ПЕРЕМЕННЫХ [ГЛ ! *
такие постоянные термы t1( ... , tc, для которых формула
a(tb .... tc)
будет истинной.
Это выгекает из доказанного нами обобщения первой е-тео-ремы. Будучи применено к нашему случаю, оно утверждает, что, ' исходя из вывода формулы
i ..... 5Г),
с помощью нашей процедуры исключения связанных переменных можно получить некоторую формулу
которая выводится из аксиом формализма F средствами элементарного исчисления и в которой fi", ..., f^ суть термы, не со-
держащие е-символа и, следовательно, построенные из одних только свободных переменных, индивидных символов и функциональных знаков формализма F.
Если вместо всех встречающихся в этой формуле свободных •; индивидных переменных мы подставим один и тот же индивидный символ, то у нас снова получится выводимая в F формула, , которая теперь будет постоянной, а потому и истинной. Значит, по крайней мере один из членов нашей дизъюнкции будет истинной формулой и эта формула будет иметь вид
где tb . . . , tc — некоторые постоянные термы. 3. Если какая-нибудь формула вида
не содержащая никаких переменных, кроме ?ь . . . , ?п, *?ь . . . , tyr выводима в F, то по выводу этой формулы для всякой системы постоянных термов аь . . . , а„ можно будет найти такие постоянные термы blt . . . , bt., для которых формула
«(аь .... а„, bi ..... bc)
является истинной.
Это следует из добавления 2 с учетом того, что для каждой •' системы термов аь . . . , ап из формулы
V?i . . . Vsn3^ . . . Э?СЯ (?ь . . . , ?„, рь . . . , 9С)
с помощью основной формулы (а) исчисления предикатов может быть выведена формула

 

1 10 20 30 40 50 60 61 62 63 64 65 66 67 68 69 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


Математика