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


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

ПО ИССЛЕДОВАНИЕ АРИФМЕТИКИ ПРИ ПОМОЩИ 8-СИМВОЛА [ГЛ. II
1) е-симеола и к-формулы,
2) знака равенства и аксиом (Ji) и (J2),
3) некоторого числа индивидных, функциональных и предикатных символов и ряда содержащих эти символы собственных аксиом $i, ..., ^?f без связанных переменных.
Если средствами этого формализма выводима формула (2, не содержащая связанных переменных, то по любому ее выводу мы сможем построить такой вывод этой формулы, в котором будут отсутствовать связанные переменные, так что этот вывод будет укладываться в рамки элементарного исчисления со свободными переменными.
Далее, если средствами формализма F выводима формула
где ?1( . . . , ?п — все входящие в эту формулу связанные переменные, то по любому выводу этой формулы мы сможем получить, не прибегая к использованию связанных переменных, вывод некоторой ди ъюнкции формул, имеющих вид
где ti, . . . , tn — некоторые не содержащие г-символа термы.
Кроме того, можно доказать, что в обоих этих случаях применение аксиомы (J2) может быть заменено применением специальных формул равенства вида
а = 6-*- (О (а)-»- О (и))
относящихся к предикатным и функциональным символам формализма F. В число этих формул, в частности, должна быть включена формула (i) a = b-*-(a = c-*-b = c).
На самом деле этот дополнительный результат получается прямо из процедуры устранения, в которой указанная замена осуществляется по ходу дела.
Пусть теперь F0 обозначает формализм, который получается из F в результате замены аксиомы (J2), указанной выше, специальными формулами равенства. Тогда, согласно сказанному, всякая не содержащая переменных формула, выводимая средствами формализма F, будет выводима и средствами формализма F0, и для всякой выводимой средствами F формулы

 

1 10 20 30 40 50 60 70 80 90 100 110 111 112 113 114 115 116 117 118 119 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


Математика