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


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

390 ВЫХОД ЗА РАМКИ ТЕОРИИ ДОКАЗАТЕЛЬСТВ [ГЛ. V
Но для этой формулы вывод получается в силу определения
формулы 53* (т, я), которая, как мы знаем, переводима в Ъ(т, п).
Тем самым мы получаем некоторую выводимую схему формул
8 <{@ -*$})-* (8 ({@}) -ч. 8 ({$})),
которую мы кратко будем называть первой S-схемой.
Из этой схемы с помощью нашей леммы тут же получается в качестве производной схемы следующая вторая 23-с х е м а:
В самом деле, согласно лемме, по выводу формулы <Е>-»-§! может быть получен вывод формулы $({©-»-$:}), а отсюда с помощью первой Ш-схемы и схемы заключения мы получаем формулу
» 8 ({$}).
Из второй S-схемы мы сначала выведем следующее утвержде-.ние:
Если f (m) и fx (m) — термы и если равенство
а также формула
Ыт) = 0-
выводимы в (Z^), TO формула
тоже выводима в (7Ц).
В самом деле, из равенства
с помощью аксиомы равенства (J2) получается формула
fi(/n) = 0-vf(m) = 0,
которая по второй S -схеме дает формулу
8({fi(m) = 0})-^ а эта формула вместе с формулой
выводимость которой мы предполагаем, по правилу силлогизма дает формулу

 

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 391 392 393 394 395 396 397 398 399 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


Математика