Гильберт, Бернайс - Основания математики. Теория доказательств (Гильберт Д. - Основания математики и прочие работы), страница 138

и Еч,р,у (при 1 = /е-г) вытекает, что разложения этих двух (щ+1)-списков на щ-списки соответствуют друг другу вплоть до Я;„, соответственно вплоть до Еыр„,. Кроме того, из предположений относительно индексов общйх замен в силу справедливости утверждения (3) для а-списков вытекает, что тот щ-список в первом (а+1)-списке, который содержит замену Ю;„, имеет больший индекс, чем щ-список во втором (щ+1)-списке, содержащий Ег+р„.

А из способа построения индексов получается, что предшествующие щ-спискн в этих двух (щ+1)-списках имеют соответственно одинаковые индексы. Но отсюда следует, что индекс первого щ-списка больше индекса второго. Таким образом, утверждения (1), (2) и (3) установлены для всех входящих в рассмотрение щ, и, в частности, получается, что в каждом (щ+1)-сниске индексы следующих друг за другом щ-списков образуют убывающую последовательность О-го-фигур и что тем самым каждый (щ+1)-список может содержать только конечное число а-списков.

Поэтому процесс последовательного построения общих замен, как мы отметили выше, после конечного числа шагов должен оборваться, т. е. привести к такой общей замене, при которой все критические формулы будут редуцироваться в значение «истинаж 3 а м е ч а н и е. Аккерман усилил изложенное здесь доказательство непротиворечивости; а именно, он указал некоторую верхнюю оценку для числа требующихся здесь общих замен. Оценка эта зависит от трех параметров: числа Аг основных типов, числа г различных е-термов, фигурирующих в критических формулах, и максимальной степени щ встречающихся термов, причем степень герма определяется рекурсивно таким образом, что цифра О и е-термы имеют степень, равную нулю, о' и 6(а) имеют степень, ббльшую степени а на единицу, а степень а+э и степень а о на единицу больше максимальной степени термов а и (е Функция, выражающая эту оценку, строится из примитивно рекурсивных функций и квазирекурсивных функций некоторого типа, причем рекурсия этого более общего типа (ордин альп а я рекурсия) заключается в том, что при возврате к меньшим значениям аргумента используется не обычный порядок натуральных чисел, а некоторый зависящий от значения р некоторого аргумента этой функции специальный порядок'), в соответствии с которым натуральные числа могут быть отображены с сохранением порядка на О-го-фигуры, не превосходящие некоторой конкретной О-го-фигуры, не зависящей от р.

Из второй теоремы т) В определенвн етого порядяз нспользуется не рззложенне натуральных чисел нз простые множнтеля, язя зто было в определении порядков в (см. с. 440 н далее), в нх двоичное рззложенне. 644 Б45 пРиложение Э5 Э5 Я(е "° 5) 1) См. с. 44 — 45. ~) См. т. 1, е. 510 — 51!. ') См.

с. 624 — Б25. ~) См. с. 79 — 81. Геделя следует, что при построении этой оценки нельзя обойтись одними примитивно рекурсивными функциями. Действительно, в противном случае изложенное доказательство непротиворечивости системы (Х) можно было бы формализовать в рамках рекурсивной арифметики, а тем самым и в рамках самой системы (Х). Следует также Отметить, что в случае добавления к основным функциям системы (2) каких-либо дополнительных вычислимых функций вместе с верифицируемыми аксиомами для них, аккермановская оценка будет нуждаться в соответствукицей корректировке. По поводу таких расширений нашей формальной системы в начале изложенного доказательства ') специально отмечалось, что они не составляют препятствий для применимости этого доказательства.

Приспособление упомянутой оценки к такого рода расширениям тоже не представляет принципиальных трудностей, но вновь добавляемые основные функции (или по крайней мере наиболее быстро растущие из них) будут участвовать в рекурсивном описании этой оценки, и определение максимальной степени терма должно быть соответственным образом измен;но. Что касается результата, даваемого аккермановским доказательством для рассматриваемого формализма, то следует особо подчеркнуть, что здесь верны все следствия, которые мы в гл. П вывели для арифметики из обобщенной е-теоремы (заметим, что там мы рассматривали формализм с ограничениями на применение схемы индукции)' ). Мы перечислим здесь еще раз соответствующие предложения вместе с кратким изложением рассуждений, с помощью которых они вытекают из аккермановского доказательства.

Это доказательство непосредственно дает следующий результат: 1) С учетом определений, данных нами для вычисления значений арифметических функций, а также истинностных значений равенств между цифрами и значений нстинностных функций, всякая выводимая формула без переменных является истинной. Отсюда также получаются следующие предложения: 2) Всякая выводимая формула без связанных индивидных и без формульных переменных, но со свободными индивидными переменными является верифицируемой.

Действительно, всякая формула, получающаяся из формулы такого рода в результате замены индивидных переменных цифрами, является выводимой, а следовательно, в силу предложения 1), и истинной формулой. 3) Для любой выводимой формулы вида эп ДОКАЗАТЕЛЬСТВО АККЕРМАНА в котоРой нет Отличных от 5м ..., 5, пеРеменных, можно так подобрать цифры !м ..., )„что формула Я(м, 1,) будет истинной.

Действительно, рассматриваемая формула с использованием е-формулы может быть переведена' ) в формулу Я(1„..., 1,), где 1,— некоторые е-термы. Значит, для этой формулы тоже может быть получен вывод в рамках рассматриваемого формализма, а из этого вывода, с помощью подготовительных операций аккермановского доказательства, — и некоторое нормированное доказательство.

Если к нему применить метод построения общих замен, то при каждой общей замене на месте термов 1„..., )„появятся некоторые цифры 1„..., 1,. При окончательной общей замене эти термы могут быть заменены указанными цифрами. Так как при этой замене все критические формулы перейдут в истинные, то мы получим некоторый вывод формулы Я(1„..., )„) из истинных формул с помощью схемы заключения. Поэтому формула Я(1„... ..., !,) тоже будет истинной.

4) Если выводима формула 75,... У5,-)!),... 39,Я (хм ..., 5„9Н ..., 9,), в котоРой нет отличных от 5„..., 5„9м ..., !) пеРеменных, то для любых цифр 1„..., 1, (которые подставляются вместо переменных 5м ..., 5,) могут быть найдены такие цифры и„..., и,, для которых формула Я(1„..., 1„п„..., п,) будет истинной. Это получается из предложения 3), так как из вывода рассматриваемой формулы мы для любого г-членного набора цифр 1„..., 1Р можем получить вывод формулы :-)9„...394Я(1м ..., 1„9м ..., !)4). Таким образом, перечисленные в предложениях 3) и 4) выводимые теоремы существовании истинны в эффективном смысле. Все эти утверждения справедливы для формализма (Х) с добавленной к нему е-аксиомой, а потому и для (2) с добавленным к нему ыправилом, а также для формализма (2 ) и для (Х) с добавлением рекурсивных определений, причем всякий раз без использования теоремы об устранимости характеристик '). Эти утверждения остаются справедливыми и при добавлении каких- 546 пРилОжение АЛФАВИТНЫЙ УКАЗАТЕЛЬ ') См.

с, 340 н след. Бернайс (Вегпауз Р.) 9 — 12, 14, 16, 418, 439 Бет (Ве!Ь Е. »»».) 203 Брауэр (Вгончгег 1.. Е. 3.) 216, 438 Бюхи (Вйсы 3. Н.) 262 Вайсберг (Ъ'а)зьегй М.) 544 Ван Хао (Ъ'апй Нао) 262 Вариант именной формы 291, 460, 548 Верифицируемость 58, 599 Верхняя формула схемы 601 Ветвление 607 Вложение 43, 626 Возвратный перенос подстановок 473 Вторая теорема Геделя о неполноте 357 либо верифицируемых формул в качестве исходных (возможно, в сочетании с введением новых вычислимых функций). Заслуживает специального упоминания также следующее использование предложения 3): если Я(пт) — рекурсивная формула с единственной входящей в нее переменной пт и если для каждой цифры 1 формула Я(!) выводима, то формула Зх ) Я(х), а потому и формула ) ЧхЯ(х), не может оказаться выводимой.

Действительно, в противном случае в силу предложения 3) можно было бы указать такую цифру»ы что формула )Я(»») была бы истинной, а тогда Я(»,) была бы ложной, в то время как, согласно предложению 1), формула Я (»,) должна быть истинной. Таким образом, рассматриваемые нами формализмы ш-непротиноречивы — по крайней мере относительно рекурсивных формул. Значит, построив для любого из этих формализмов соответствующую формулу ~6(п»„й) из первой теоремы Геделя' ) [которая, как мы знаем, является рекурсивной формулой) такую, что сама она не выводима в этом формализме, но для каждой цифры ! выводима формула ) 6 (», й), мы получим, что ни формула »7х )6(х, й), ни ее отрицание не выводимы в этом формализме.

Таким образом, в каждом из этих рассматриваемых нами формализмов имеются формально неразрешимые формулы. Абсурдность 438 Аккерман (Асйеппапп %.) !1 †!3, 15, 51, 93, !24, 157, 250, 260 †2, 338, 454, 546, 624, 630, 634, 643 Аксиома для квантора существования 600 — индукции 468 — свертывания 591 Аксиомы геометрические 67 — конгруэнтностн 62 — Пеано 468, 589 — равенства 464 Антецедент 454 Антиномия лжеца 321 Аргумент выделенный 104 Аргументная переменная 460, 626 Арифметизация 265, 276 — понятия герма 278 — — формулы 276, 281 — явных определений 368 Арифметическая модель системы аксиом 320 Арифметическое функциональное выражение, сопоставленное формуле 385 Вывод в исчислении предикатов 459— 464 — — обобщенном смысле 39, 91 — — формализмах аксиоматическнх теорий 462 — 464 — при дедуктивных ограничениях в исчислении высказываний 512 — равенства нз системы равенств прн вычислении каазирекурсивных функций 490 — редуцированный 611 †, рекурсивное изображение 295, 166, 379, 380 — средствами исчисления высказываний 462 Выделенное распределение значений для равенства 1!2 Выполнимость 231 — эффехтивная 245 Высота формулы 604 Вычисление значений термов в концевом фрагменте вывода 604 — формализованное 605 Вычислимость 478 — регулярная 479 Гейтинг (Неуцпй А.) 428, 436, 544, 545 Генкин (Непрбп 1..) 238 Генцен (Сеп!хоп С.) 11, 13, 203, 2!2, 437, 439, 450, 454, 455, 544, 612, 622, 624 Геометрические ахсиомы в разрешенном виде 67 Геометрия аналитическая 68 — элементарная 6! Гермес (Неппез Н.) 266, 534 Герц (Негра Р.) 454, 455, 520, а также т.

1, с. 77, 100 Гессенберг (НеглепЬегй С.) 6!3 Гедель (Соде! К.) 9, 12, 16, 78, 238, 260, 261, 264 — 266, 320, 321, 400— 402, 417, 418, 421, 437, 491, 507 АЛФАВИТНЫЙ УКАЗАТЕЛЬ 649 648 АЛФАВИТНЫЙ УКАЗАТЕЛЬ 3! Гильберт (Н|1Ьег1 О.) 9 — 14, 16, 17, 36, 40, 62, 63, 70, !24, 266, 454, 605, 546, 624, 629 Гливенко В. И. 437 Дедекинд (ОебеМпд К.) 468, 554, 593 Дедуктивное равенство 471 Дедукционная теорема 472 Дентов (Оеп(оп 3.) 212 Дизъюнктивное расщепление 53, 95 Дизъюнктивные члены первого н второго рода 197 Диэъюнкция 457 Дорро (ОоггоЬ 3. 1..) 63 Дребен ((угеЬеп В.) 203, 212 Замена минимальная 127 — общая !28, !38, 629 — примером 634 — свободных переменных связанньпэи 471 — связанных переменных свободными 472 — функциональная 134 — функциональных знаков предикатными символамн !83 — цифрамн 123 — экземплярная 126 — эффехтивная !26 Заменимость !9 — рекурсивных функций в (Е) 470 — экзистенциальных аксиом 19 Заменитель именной формы 291, 460, 548 Зифкес (Б!ейгез О.) 16 Именная переменная 480 — форма формульной переменной 290, 460, 548 Импликатнвная формула 5!2 — †, непосредственно тождественная 516 †!7 — †, позитивно тождественная 512 Импликацня 457 — в формализме (3) 437 †4 Индекс замены 144, 152 — в-списха 638 Ипдивидные переменные 457 Индивидный символ 463 Индукция трансфинитная 440, 576 Исключение излишних свободных переменных 600 Истинностные функции 459 Истинные формулы 598 Исходные формулы 600 Исчисление высказываний, связки 457 — —, формулы 457 — предикатов 457 — Кэ Шютте 211 йогансон (ЗоЬапзэоп !.) 428, 544 Кальмар (Ка!шйг 1..) 13, !5, 16, 259— 261, 454, 552, 593, 598, 599, 604, 622 Кантер (Капйег 31.) 203 Кантор (Сап!ог О.) 332, 439, 450 — 452, 503, 573, 576, 578 Канторовское е-число первое 452, 612 Кар (КаЬг А.