Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 83
Текст из файла (страница 83)
Небольшой модификацией этой формулы мы получим также рекурсивное изображение двуместного предиката «число т яв- ляется номером одной из формул (14',) и (144), а и представляет собой номер формулы, получающейся из формулы с номером т в результате некоторой подстановки вместо формульной переменной этой формулы„быть может, вместе с переименованием одной или нескольких связанных переменных». А теперь мы можем приступить к построению требуемой в условии б,) формулы 8(т, а), посредством которой формализуется высказывание: «число т является номером списка формул, представляющего собой вывод в (У ) формулы, номером которой является л».
Это высказывание в точности означает следующее: Для любого числа х такого, что х(74(т), т(т, х) представляет собой номер некоторой формулы из (У ), причем т(т, ) (т)) = = и; а кроме того, имеет место одно из следующих утверждений а) — к): а) Р(т, х) является номером какой-либо тождественно истинной формулы исчисления высказываний; б) т (т, х) является номером одной из формул (а) и (Ь) исчисления предикатов или одной из аксиом формализма (ХР); в) Р(т, х) является номером явного определения какого-либо функционального знака или предикатного символа; г) хчьО, и формула с номером т(т, х) получается из формулы с номером Р(т, х — 1) в результате некоторой подстановки вместо какой-либо свободной индивидной переменной или вместо формульной переменной без аргументов; д) х~О, и формула с номером т(т, х) получается из формулы с номером Р(т, х — 1) в результате некоторой подстановки вместо какой-либо формульной переменной с одним или несколькими аргументами; е) хчьО, и формула с номером ч(т, х) получается из формулы с номером т(т, х — 1) в результате переименования одной или нескольких связанных переменных; ж) х~ О, т(т, х — 1) является номером одной из формул (р;) и (р,'), а формула с номером т(т, х) получается из этой формулы в результате некоторой подстановки вместо ее формульной переменной в сочетании с переименованием одной или нескольких связанных переменных; з) х~ О, и формула с номером Р(т, х) получается из формулы с номером Р(т, х †' 1) по одной из схем (с«) и (()); и) х) 1, и формула с номером Р(т, х) получается по схеме заключения из формул с номерами т(т, х — 1) и Р(т, х — 2); к) существует число у, меньшее х, такое, что формулы с номерами т(т, х) и Р(т, у) совпадают.
А теперь все десять членов этой альтернативы мы рассмотрим на предмет выяснения их рекурсивной изобразимости. По большей части мы сможем воспользоваться рекурсивными изображе- эя ФОРмАлизАция АРиФметическОГО ФОРмАлизмА 382 егл Р 380 выход зА Рхмки георгии докАзАтельств пнями соответствующих отношений, полученными в свое время для формализма исчисления предикатов с добавлением цифр и функциональных знаков, Только теперь потребуется всюду вместо старых определений внести новые, приспособленные к формализму (Х ) определения понятий формулы, тер ма и к в аз ит ерм а, а функцию 812(222, 72, 1) нужно будет заменить функцией 81'(т, й, !), Так мы получим изображения для членов а), г), д), з) и и).
Для членов в) и ж) их рекурсивные изображения были определены только что. Член е) изобразится выражением Х~Ойч(т, х) чьч(т, х — '1) й41'4(О(т(т, х), Р(т, х — ' 1))), член к) — выражением Зу(у(хйч(еп, х)=Р(т, у)), а член б) изобразится дизъюнкцией Р(Л2 х)=п2 У Р(т Х)=пе Ч ° Ч Р(т Х)=п2 * где и, и и, суть номера основных формул (а) и (Ь) исчисления предикатов, и, и и,— номера аксиом равенства, п„п, и и,— номера трех арифметических аксиом, п„п„п„и и„— номера рекурсивных равенств для сложения и умножения, и„и и„, — номера формул для символов ~ и (, а 222О е„и п2,— номера формул (14,), (12,) и (122). Если мы запишем полученные выражения для всех членов от а) до к) включительно, то в качестве формализации высказывания, изображаемого искомой формулой 6 (т, п), у нас сначала получится некоторая формула вида Р (т, Л(т)) = ай 42(х(х 4-Л(л2)-~ Ж(Р(т, х)) й 10 ! Р(т, х) й 2(т, х)), где Ж(т, 72) — дизъюнкция, не содержащая отличных от т и (е свободных переменных, члены которой переводимы в рекурсивные формулы.
По внешнему виду этой формулы, которую мы обозначим посредством 6* (т, п), ясно, что она может быть переведена в некоторую рекурсивную формулу, не содержащую переменных, отличных от т и и. Тем самым искомая формула 6(т, и) построена. Итак, мы убедились, что для формализма (ХР) условие бе) выполняется во всех его частях. Для дальнейшего мы также заметим, что фигурирующая в формуле 6*(т, и) дизъюнкция Ж(т, х) имеет вид Т2(Р(гп, х)) 12 (Х~ОйЖ,(Р(т, х), Р(т, х -' 1))) Л7 (О' «=хй'О,(ч(т, х), Р(т, х -- 1), Р(т, х — '2))) ~/ Ву(у(хйт(т, х) с ч(т, у)).
При этом ~2(а), Же(а, Ь) и 4'з(а, Ь, с) суть формулы из (7Р), допускаюецие перевод в рекурсивные формулы. формула Ч2,(а, Ь) содержит в качестве дизъюнктивного члена формулу ЗуЛЕ(у(Ьйг(айРг(у)й7(уйС(г)й 1 (10 ~ г) й а = 81* (Ь, 2 у, г) ), а формула Ж,(а, Ь, с) представляет собой равенство Ь=80 7' 11'. г) Проверка условий иа выводимость. Теперь мы еще должны. убедиться, что формализм (7„), а также введенная для него нумерация и построенная на основе этой нумерации формула 6(т, л) удовлетворяют нашим трем условиям на выводимость, фигурирующим во второй теореме Геделя о неполноте в качестве предположений ').
Рассмотрим сначала первые два из этих условий. В применении к формализму (ХР) они утверждают, что: 1) если из формулы с номером ! выводима формула с номером 1, то в (У„) выводима формула ЗХ6(х, !)-+ЧХ6(х, !) 2) формула ЗХ6(Х, Е (м) — РЗХ6(Х, Е(8(72, !))) выводима в (2„). При этом с учетом произведенной нами нумерации в качестве е(й) следует взять функцию З.й, а в качестве 8(72, !) — функцию 81*(й, !4, 2 ° 3')'). Установлению искомых выводимостей мы предпошлем следующие два замечания. Во-первых, мы заметим, что при рассмотрении упомянутых выводимостей в (2Р) формула 6(т, л) повсюду может быть заменена формулой 6*(т, и), так как она переводима в эту формулу.
Далее, мы заметим, что в результате небольшого видоизменения формулы 6*(т, и) может быть получено изображение высказывания «число т является номером списка формул, являющегося выводом в (2Р) формулы с номером и при добавлении формулы с номером й к числу исходных формул». Действительно„это высказывание изображается формулой т(т, Л(т)) = ай 4РХ(Х~Л(т)-РС(Р(т, х)) й 10!42(т, х) й(42(т, х) 2/ 4(т, х) =72)). Эта формула, которую мы обозначим посредством 6*(т, й, п), 9 См. с.
355. 4) См. с, 370 — 37ц (гл. и з82 $ з) ФОРМАЛИЗАЦИЯ АРИФМЕТИЧЕСКОГО ФОРМАЛИЗМА ЗЕЗ ВыхОд зА Рдмки теопии докдзлтельств тоже может быть переведена в некоторук' р ур у формулу 8(т, Й, и), которая не содержит переменных, отличных от т, )г и и. Рассмотрим теперь первое условие на выводимость. В нем предполагается, что из формулы с номером 1 может быть выведена формула с номером 1').
Пусть этот вывод представляет собой список формул с номером )и. В этом случае рекурсивная формула 8(ш, 1, 1) без переменных является истинным отношением между числами ш, 1 и 1, и потому эта формула выводима в (Хи). 1)(ы ищем вывод формулы Зх8 (х, 1) -« =1х8 (х, 1). Как было замечено выше, чтобы доказать выводимость этой формулы, достаточно установить выводимость формулы Зх8(х, 1)8(8(ш, 1, 1)- Зх8(х, 1) или же выводимость формулы Зх8е (х, 1) 8( 8' (ш, 1, 1) -)- Зх8' (х, 1).
Но выводима даже формула Зх8* (х, й) 8( 8* (т, )г, 1) -«Зх8* (х, 1) с переменными т, (г и 1 вместо цифр ш, 1 и 1. Действительно, эта формула получается средствами исчисления предикатов из формулы 8 (и, й)8 8*(т, й, 1)- 8ь~п П Рлч((„")+)., 1), к(Л (м) а эта последняя, имеющая вид 8*(п, )г)8(8е (т, )г, 1)-«8*(1(п„т), 1), Где 1(п„ т) обозначает терм к(кь к) 1 д )зл(к) + к', к ~ Л (пз) и свою очередь получается на основе определения формул 8* (т, и) и 8*(пг, й, и) с использованием выводимых формул а().(п)-«з)(1(п, т), а) =Р(п, а), а ~ й (т) - з) (( (и, т), Л (и) + а') = Р (т, а) и (1 (и, т)) = ). (и) + ()((т))' ') Под в ы в о д и м о с т ь ю и н е в ы в о д и и о с т ь ю в данных рассмотрениих, относяшихси к условиям иа выводнмость, всюду, где не оговорено противное, будет пониматься выводимость и соответственно неаыводимос)ь в формализме (ХР). с учетом вида выражения, сокращенно обозначенного через Ж(т, х)').
Тем самым первое из рассматриваемых нами условий на выводимость для формализма (Еи) оказывается выполненным. Что же касается выводимости формулы Зх8 (х, 3 й) -«Зх8 (х, 3. З1' (й, 14, 2 3')), то эта формула получается в результате подстановки и использования (выводимого из определения функции з1е(т, )г, 1)1 равенства з( е (3 т, й, 1) = 3 з(е (т, Уг, 1) из формулы Зх8(х, й) — «Зх8(х, з1а(Й, 14, 2 3')), а значит, и из формулы (1) Зх8Ф (х, й)-«.Зх8'(х, з(е ()г, 14, 2 3')). Эта формула в свою очередь выводится средствами исчисления предикатов из формулы 8Ф(п), й) 8'( Р,,(,,;, 9, з('(й, 14„2 3')), которая на основании вида формулы 8е(т, п), в частности, с учетом вида выражения Ж(т, х), получается с помощью выво- димых формул') 4к (2 3'), ~ (10 (2 3'), (а()г, и, 1)чьй - й и Я()г)8!0()г- Я(з(е(й, 14, 2.3())8(!О(з(к(й, 14, 2 3).
Таким образом, выполненным оказывается и второе условие на выводимость. Вместе с тем проведенное доказательство дает несколько более общий результат, так как фигурирующее на месте второго аргумента функции З1* число 14 в этом выводе может быть заменено номером любой свободной индивидной переменной, т. е. любым числом вида 2 р, где р — простое число, большее или равное 3. Так для любого простого числа р=-.=3 получается выводнмость формулы :-)х8(х, й)- Зх8(х, з(к (й, 2 р, 2 3')).
л) См. с. 880. з) дли вывода упомянутой формулы (1) надо вернуться от рекурсивных определений функции з(' и формулы Ж к тем дизъюнкциил) (альтернативам), из которых зги определении были получены. Оставшуюся часть вывода можно будет затем провести, вана за обравец неформальное теоретико-множественное Рассуждение. $2! ФОРМАЛИЗАЦИЯ АРИФМЕТИЧЕСКОГО ФОРМАЛИЗМА 335 ВЫХОД ЗА РАМКИ ТЕОРИИ ДОКАЗАТЕЛЬСТВ !гл ч Обратимся теперь к третьему условию на выводимость. В применении к формализму (2м) н к рассматриваемой нами нумерации оно утверждает следующее: Если ((и) — какой-либо рекурсивный терм, содержащий единственную переменную и, а и — номер равенства ((а) = О, то формула 1(и) =0-~-Эха(х, з(е (и, 14, 2 Зм)) выводима в (Хп).
Из этой формулировки мы прежде всего можем исключить функцию з1а. Это удается сделать с помощью следующего замечания: Для всякого выражения 6(а„..., а,) из (Еп), где а„..., а,— какие-либо отличные друг от друга свободные индивидные переменные, можно указать такое элементарно-арифметическое выражение 1(п,, ..., а,), что для любых цифр 1„..., !с значение 1(1„..., 1„) равно номеру выражения Л(1,, ..., !с). Действительно, каждая из переменных и„..., а„всюду, где она входит в 6 (пм ..., а,) — сама по себе илн с некоторым числом штрихов — фигурирует либо в качестве аргумента какой-либо формульной переменной или предикатного символа, либо в качестве аргумента функционального знака.