Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 87
Текст из файла (страница 87)
Схема явного определения не включается. Так как формализм (Е) содержит только такие символы и переменные, которые имеются н в (Е„), то нз нумерации выражений, входящих в (Е„)'), немедленно получается нумерация и для выражений, входящих в (Е). Опираясь на эту нумерацию, можно построить рекурсивную функцию д(й, 1), которая номеру всякого выражения Й из (Е) и всякой цифре 1 ставит в соответствие номер выражения, получающегося из К в результате замены переменной а цифрой 1 Можно также построить рекурсивную фомулу 9(т, и), изображающую отношение между номером списка формул и номером формулы, для которой этот список является ее выводом в формализме (Е). Хотя функция 8(й, 1) в формализме (Е) и неизобразима, она в нем все же представима; именно, оказывается, что можно указать некоторую формулу Я(а, Ь, с) формализма (Е), не содержащую отличных от а, Ь и с свободных переменных, переводимую в рамках (Еи) в равенство 8(а, Ь) =с.
Точно так же по формуле ез(т, и) можйо построить формулу е)з(т, и) формализма (Е), не содержащую отличных от т и п свободных переменных, такую, что в рамках (Е„) она переводима в формулу 3(пт, и). Исходя из этого, мы теперь покажем, как путем некоторой модификации вышеприведенного доказательства, относящегося к формализму (Е„), вторая теорема Геделя о неполноте может быть распространена на формализм (Е). При этом мы можем воспользоваться тем обстоятельством, что любая формула, выводимая в формализме (Е„), выводима и в том формализме, который получается из (Е) путем присоединения к нему ь-правила и общей схемы явного определения'). По теореме об устранимости ь-правила отсюда следует, что каж- О для первого и второго условий зто даже может бить усмотрено непосредственно из выводов для формул, приведенных на с.
382 в строке 21 и на с. 383 в строке 17. О Ом. с. 367 и далее. ') Относительно соотношения между формализмами (2 ) н (2) см. с. 362 — 366. 4 11 ФОРМАЛИЗАЦИЯ АРИФМЕТИЧЕСКОГО ФОРЛ1АЛИЗМА 4ОЗ 402 ВЫХОД ЗА РАМКИ ТЕОРИИ ДОКАЗАТЕЛЬСТВ дая формула формализма (Е), выводимая в (Е„), выводима также н в (Е). Сказанное дает нам возможность по выводам в (Е„) получать соответствующие выводы в (Е), и поэтому нам нужно будет лишь слегка модифицировать рассуждения, потребовавшнеся для дока- зательства второй теоремы Геделя и ее применения к форма- лизму (Е„). Первая модификация будет заключаться в том, что вместо формулы 3 (т, 8(а, а)) мы будем рассматривать формулу '»Ух(Я(а, а, х)-»- 161(т, х)).
Пусть р — номер этой формулы, а « — значение терма 8(р, р), т. е. номер формулы Чх(«б(Р, р, х)-~)»61(т, х)), которая с помощью выводимых в (Е) формул Я(р, р, «) и С(а, Ь, с)81(О(а, Ь, д)- с=д переводима в формулу 16,(т, «). Пусть г — номер формулы 6,(а, «), а Г,— номер ее отрицания. В качестве е(и) можно снова взять функцию 3 и. Выражение З.и является термом и в (Е). Поэтому утверждение о непротиворечивости формализма (Е) может быть изображено формулой :-(х61(х, и)». ) =(х61(х, 3 и), которую мы и на этот раз возьмем в качестве формулы »а. Для искомого доказательства невыводимости в формализме (Е)— в предположении непротиворечивости этого формализма — формулы 6 достаточно показать, что из 5 средствами формализма (Е) выводима формула ) 6,(т, «).
Действительно, если это будет установлено, то из предположения о выводимости 6 в формализме (Е) будет следовать выводимость в (Е) формулы с номером «, и значит, истинность 6(1, «) для некоторой конкретной цифры 1, а тем самым и выводимость в (Е) формулы 6,(1, «), которая вместе с формулой ) 6,(т, «) дает противоречие. А теперь, чтобы убедиться в выводимости в формализме (Е) формулы ) 6, (т, «) из формулы»з, — что по дедукционной теореме равносильно выводимости формулы е»и(Зх61(х, и)-+ ~Чх61(х, 3 и))-л 1З,(т, «), — согласно сделанному выше замечанию достаточно установить выводимость этой формулы в формализме (Уи), а это в свою очередь равносильно выводимости в рамках формализма (Е„) формулы )61(т, «) из формулы пх61(х, и)-» ) ЗХ61(х, 3'и). В этой выводимости можно убедиться, рассуждая аналогично тому, как при рассмотрении формализма (Е„) для построенной применительно к этому формализму формулы 6(т, и) доказывалась выводимость ~6(т, «) из формулы ВхЗ (х, и) - 13х6 (х, 3 и).
При этом на месте тех трех условий на выводимость, выполнимость которых мы установили для формализма (Е„), теперь появляются следующие три условия: 1. По заданному выводу формулы с номером 1 средствами формализма (Е), к которому добавлена формула с номером в качестве исходной, можно построить вывод в (Е„) формулы =(х»61 (х, 1) -».
Чх61 (х, 1). 2. Формула Эх61(х, 3 й)-Ф=1хЗ,(х, 3 8(/г, 1)) выводима в (Е„). 3. Если ( (т) — рекурсивный терм с единственной переменной т, а г — номер равенства 1(а) =О, то формула ((т) =О- Вх61(х, 8 (г, т)) выводима в (Е„). (Заметим, что во всех этих трех предположениях речь идет о построении некоторого вывода в (Е„).) Проверка условий 1 и 2 может быть произведена в точности так же, как проверка выполнения первых двух условий в случае формализма (Е„).
Утверждение 3 можно свести (сначала введя рекурсивную функцию з1* (т, й, 1), а затем устранив ее ')) к следующему предложению: Если ( (т) — какой-либо рекурсивный терм с единственной переменной т, Е(т) — формула из (Е) с единственной свободной переменной т, переводимая средствами формализма (Е„) в равен. ство ((т) О, а «(т) — арифметическое функциональное выражение, сопоставленное этой формуле Ж(т) относительно переменной т, то формула 9(т)-~=(х61(х, й(и1)), а потому и формула 1(т) =О-л:-(х61(х, й(т)), выводима в (Е„). ') См.
рассуждение на с. 384 — 385, выход ЗА ~Амки теогии докАзАтельств [ГЛ. Р зя ФОРмАлизАция АРВФметическОГО ФОРИАлизмА 405 Доказательство этого предложения совершенно аналогично проведенному нами для формализма (ем) доказательству выводи- мости формулы ( (т) = 0 -«6 ((( (т) = 0)) для случая рекурсивного терма ((т) с единственной переменной т. Используя соответствующие сокращенные обозначения '), можно доказать следующий аналог нашей леммы'): Если формула й выводима в (Х), то формула 6, Щ) выводима в( ). $ авным образом, пвименительно к формуле 6,(т, и) действуют соответствующие 6,-схемы, аналогичные двум рассмотренным ранее Е-схемам').
А вот два последних утверждения из утверждений') 1 — 4 должны быть модифицированы в соответствии с содержанием доказываемого предложения. Нам достаточно привести эту модификацию для утверждения 4 и притом для случая двуместной рекурсивной функции. Мы должны здесь воспользоваться представимостью в (Е) рекурсивных функций. Любой паре рекурсивных равенств ( (а, 0) а (а), ((а, и') = Ь (а, и, ( (а, п)) в (Е) соответствует пара выводимых формул $(а, О, с) Й(а, с), $(а, и, Ь)-«(7(а, п', с) 2(а, и, Ь, с)), где а„п, и с суть все свободные переменные в формуле ~3 (а, и, с), а и с суть все свободные переменные в Й(а, с), а а, и, Ь и с суть все свободные переменные в с(а, и, Ь, с), причем в (УР) выводимы эквивалентности Й (а, с) а (а) = с, г (а, и, с, 40 Ь (а, п, с) = д, 7 (а, и, с) ( (а, и) = с.
Кроме того, опираясь на выводимую формулу Лг$(а, и, г), из формулы $(а, п, Ь)- (6(а, п', с) 2(а, и, Ь, с)) можно получить эквивалентность (Р(а, и', с) (г(143(а, и, г)й2(а, п, г, с)). 1) См. с. 388. В) См. с. 390. а) См. с, 394. Поэтому утверждение, которое должно быть доказано вместо утверждения 4, имеет вид: Пусть в (Е„) выводимы формулы Й (а, с) — 3, ((Й (а, с))) 2 (а, п, с, 40 -« 6,((е (а, п, с, й))). Пусть, кроме того, в (Х) выводимы эквивалентности $(а, О, с) Й(а, с) и 6(а, и', с) =1г(6(а, и, г)йй(п, а, г, с)). Тогда в (ХР) выводима формула 6(а, и, с)-«6,((6(а, и, с))). Это утверждение будет доказано, если мы покажем, что пол- ной индукцией по п может быть выведена формула УхС(п, х), где А4(п, с) обозначает формулу $(а, п, с)-«6Г((6(а, и, с))).
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
