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


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

450 ВЫХОД ЗА РАМКИ ТЕОРИИ ДОКАЗАТЕЛЬСТВ [ГЛ, V
поэтому выражение 33,, (с, О (у, а, п, К), п — k') имеет вид
* !(*, с, п, )&z/(m2*, у, п, )-+(y, а, п, ->-
Чу(®*(х-р„ У, п, k)-+a(y, а, п,
где чЙ! (а, Ь, п, k) и 2Я2 (а, Ь, п, k) — некоторые рекурсивные формулы, и может быть преобразовано в формулу
У*{-]2«г(х, с, п, *)V3y(3t,(*, у, п, k)&~]?l(t/, а, п, *)) V
Vy ПИ, (*•!»„ у, п, k)\j?l(y, a, n, k))}.
Таким образом, рекурсивное определение символа Q (с, а, п, k) аналогично тому, с помощью которого мы ввели символ М (п, k) при определении истинности для формализма (Z)1).
Относительно введения символа М (п, k) мы выяснили, что оно выводит как за пределы формализма (Z), так и за пределы (Z^) 2). В связи с этим в высшей степени правдоподобно, что приведенная выше схема, определяющая предикатный символ JQ (с, а, п, k), окажется средством, не укладывающимся в рамки формализма (Z^), т. е., вообще говоря, не будет заменяться явными определениями в (Z^).
То, что этот способ введения предикатных символов, а тем самым и доказательство рассмотренного частного случая трансфинитной индукции, выводит за пределы формализма (Z^), следует из того, что применение этого способа умозаключений вместе с рассуждениями, которые формализуются в (Z^), позволяет провести генценовское доказательство непротиворечивости формализма (Z)3).
Мы приведем здесь — хотя бы в схематическом виде — ход этого доказательства, причем в новой его редакции4). С этой целью к проведенному рассмотрению данного частного случая трансфинитной индукции мы добавим еще одно дополнительное рассуждение.
Каждый из порядков -3, если отвлечься от конкретного уст-
п
ройства упорядочиваемых им элементов (в данном случае являющихся числами), по терминологии Кантора, изображает некоторый
1) См. с. 411. ») См. с. 415.
3) Это рассуждение использует вторую теорему Гёделя. В одной более поздней работе: Gentzen G. Beweisbarkeit und Unbeweisbarkelt von An-fangsfallen der transfiniten Induktion in der reinen Zahlentheorie. — Math Ann., 1943, 119, S. 140—161, Генцен показал, что с помощью некоторой модификации доказательства непротиворечивости можно и без ссылки на эту теорему Гёделя убедиться в том, что обобщенный принцип индукции существенным образом не укладывается в рамки арифметического формализма.
4) См. сноску на с. 439.

 

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 451 452 453 454 455 456 457 458 459 460 470 480 490 500 510 520 530 540 550 560 570 580 590 600 610 620 630 640 650


Математика