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


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

510 ПРИЛОЖЕНИЕ [II
При этом рассматриваемая формула & в GI с применением только что упомянутой эквивалентности может быть переведена в формулу 3#(t0(;e) = n). Если предикатный символ, введенный вместо штрих-символа, обозначить через Sq(a, b), то формулу $ можно будет взять в виде
b Ея)&...&
Еп_2, Sn-.i)&Sq(sn_lf *)->
Здесь ?ь .. ., ?„_! — отличные друг от друга и от л: связанные переменные, а выражение К (х) не зависит от числа п, а значит, оно определяется уже рекурсивным определением функции |0 (п). Впрочем, формула & не содержит свободных переменных.
Наконец, — ввиду теоремы о представимости общей аксиомы равенства (J2) с помощью собственных аксиом 1) — здесь вместо формализма Ьг можно рассмотреть формализм G2, получающийся из G! в результате замены исходной формулы a = b-*-(A(a)->A(b)) специальными формулами равенства, относящимися к предикатным символам из GI (или к их различным аргументам), включая и формулу a = b->(a = c->b = t'). Это означает, что формула & выводима в G! тогда и только тогда, когда она выводима в G2.
Но по одной ранее доказанной теореме2) выводимость & в формализме G2, который получается из исчисления предикатов добавлением ряда предикатных символов и символа 0, равносильна выводимости в исчислении предикатов некоторой конкретной формулы 8, которая получается из &, если во всех аксиомах формализма G2 все свободные переменные заменить связанными (т. е. связанными соответствующими кванторами всеобщности), затем по так модифицированным аксиомам 31Ь . . . , 3lg построить формулу
и в ней заменить символ 0 переменной а, а различные предикатные символы — различными формульными переменными, причем для каждого предикатного символа нужно брать соответствующую формульную переменную с тем же числом аргументов.
Если мы теперь примем во внимание, что рекурсивное определение функции j0 (п) может быть задано в явном виде и что с помощью этого определения могут быть явно написаны аксиомы G, равно как и аксиомы G2, а потому и формулы 31г ..... 3lg, и что с помощью этого определения может быть также построено выражение К (х), то станет ясно, что номер, который при нашей
1) См. т. I, с. 456 — 459 или Приложение 1 к данному тому, с. 472—473. «} См. с. 188.

 

1 10 20 30 40 50 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 511 512 513 514 515 516 517 518 519 520 530 540 550 560 570 580 590 600 610 620 630 640 650


Математика