Гильберт, Бернайс - Основания математики. Логические исчисления и формализация арифметики (947375), страница 98
Текст из файла (страница 98)
С другой стороны, ранее мы вывели формулу п ~ 0 А а ) п 81 Ь ! п -«- р (и, шп11 (а, Ь)) пш11 (а, Ь); тем самым мы получаем и~О Аа (иАЬ (п — »р(п, шп11(а, Ь)) = 0 и, значит, ввиду эквивалентности а(Ь вЂ” р(Ь,а) =О, имеем и~О Аа (иАЬ (и — »шп11(а, Ь) (и. Наконец, из-за шо11 (а, Ь) ( О, здесь еще можно будет опустить в посылке член и ~ О, так что в итоге мы приходим к формуле а ( п А Ь ) и -« шп1С (а, Ь) (п.
Итак, мы получили для функции шп11 (а, Ь) следующие формулы: а ( шп11 (а, Ь) А Ь ( шп11 (а, Ь), а ! п А Ь ! п -«- шп11 (а, Ь) ! и. Формулы атн достаточным образом характеризуют рассматриваемую нами функцию. Для дальнейшего нам потребуется также наименьияее общее кратное конечной последовательности чисея, задаваемой с помощью т последовательных значений какаго-либо терма 1(а). Мы получим его с помощью следующего определения: шп1С„(1 (х); т) = рв (х ~ 0 А Ру (у «- и-«-1(у) ( х). Из этого определения получаются формулы, совершенно аналогичные тем, которые мы получили выше для функции шп11 (а, Ь), а именно 'уу (у ( т — «-1 (у) Ф О) -» шпИв (1 (х); т) ~ О, 'йу(у(т — 1(у) / пшИв(1(х); т)), «уу (у ( т -«-1 (у) / и) — » 1пп11„(1 (х); т) / и.
Вывод этих формул протекает аналогично выводу соответствующих формул для шп11 (а, Ь); надо будет только индукцией по т вывести формулу, которая теперь замепяет формулу а ~ 0 А Ь ~ 0 -«Лх (х ~ 0 А а ( х А Ь ( х) и которая записывается в виде УУ (У «п — «-1 (У) ~ О)-«Зх (х ~ 0 А ((у (у ( т -»1 (у) ~ х)) В связи с этим выводом следует обратить особое внимание на тот факт, что с его помощью удается обойтись бег использования рекурсивного определения.
Вывод этот протекает следукяцнм обрааом. Если мы сокращенно обозначим доказываемую формулу посредством Я (т)-» й) (т,), то формула м«(0), т. е. Зх (х т«0 А Ч у (у ( 0 — 1(у) ~ х)), может быть получена из формулы 0' =~ 0 А «Уу (у ( 0-«1(у) ( 0'); а пз й)(0) мы получим Я (О) -«- (В (0). Теперь для того, чтобы применить схему индукции, нам остается только вывести формулу (Я (т)-» й) (т))-«(Я (т')-«(В (т')). Так как Я (т) имеет внд «уу (у <- т -«- 1(у) 4.- 0).
то мы можем получить Я (т')-«-Я (т) А1(т) ~ О. Поэтому достаточно вывести формулу (Я (т)-«З (т)) -«(Я (т) А 1(т) Ф О-«й«в(т')), для чего в свою очередь будет достаточно средствами исчисления высказываний вывести формулу (6(т) 8: 1(т) Ф 0 -«- й(т').
Но эта формула, которая в подробной записи имеет вид Зх (х Чь 0 А Чу (у ( т -» 1 (у) ( х)) А 1 (т) 5Ь О вЂ” » Вх (х ~ 0 А «((у (у ( т' — «-1 (у) / х) ), ДЕДУКТИВНОЕ ПОСТРОЕНИЕ АРИФМЕТИКИ [ 2[ 497 49б ПОНЯТИЕ «ТОТ, КОТОРЫЙ» И ЕГО УСТРАНИМОСТЬ [ГЛ, Ч1П средствами исчисления предикатов получается иа выводимой формулы а чь 0 А чеу (у . т -+.
1 (у) [ а) А 1 (т) чь 0 -эа 1(т) ~0&»чу (у(и'-+1(у) [а 1(т)). Иэ получающихся таким образом формул для функции шп11„(1(х); и) мы теперь можем вывести еще одну формулу: 'Рх (х .-, и — Ргпа (1(х), а)) » Рпш (шп11„(1(х); т), а). Эта формула также может быть получена индукцией по т. Мы опять сокращенно запишем ее в виде 91(т) -«3(и). 3(0) представляет собой формулу Ргпп (ши11„(1(х); 0), а); ее можно получить из выводимого равенства шп11„(1(х); 0) = 1 в сочетании с формулой Рпш (1, а). Тем самым оказывается выведенной и формула Я(0) — 3(0).
Теперь требуется еще вывести формулу Я (т) — 3 (и)) (Ч (и') — 3 (и'И. Для этого, ввиду формулы е[(т') -«. Я(т) А Рпш(1(т), а), достаточно вывести формулу 3(т) А Рпш(1(т), а) -+. 3(т'), т. е. в подробной записи: Рг!ш (шп11„(1(х); т), а) А Рпш (1(т), а) -э Рг[ш (шп[С (1(х); т ), а). Эта формула может быть получена с помощью имеющихся для шп11„(1(х); т) формул 'уу (у (т -~- 1(у) ) шп11„(1(х); т)) 1[у (у "т — >- 1(у) ~ и) -ь шп11„(1(х); т) ) и.
Действительно, ив первой формулы мы получаем еуу (у ( т — ь 1(у) ~ (шп11„(1(х); т) ° 1(т))). Из второй формулы подстановкой т' вместо и и шп11„(1 (х); т) ° 1(т) вместо и получаем формулу, которая вместе с предыдущей дает пш11„(1(х); и') ! шп1С„(1(х); т).1(т). В силу этой формулы вывод формулы Рпш (шп11„(1(х); т), а) А Ргпп (1(т), а) — ь Рпш (шп11„(1(х); т'), а) сводится к применению формулы Ргпа (ке а) А Рг[ш ([, а) А г ( тс 1-ь Рпш (т, а), которую можно получить из формул Ргпп (а, и) А Ргпп (д, и)-ь Рпш (а Ь, и) Рпш (а, Ь) А с ~ а-ь Ргпп (с, Ь).
Ввиду скааанного, схема индукции дает нам искомую формулу 'эх (х (т-«Рпш (1(х), а)) -е Ргпп (шп11„(1(х); т), а). Мы применим эту формулу некоторым специальным обрааом, взяв в качестве 1(х) термх' Ь + 1 ') и подставив вместо атерми' Ь+ 1. В результате этого мы получим формулу Чх (х «т -е- Рпш (х' Ь + 1, т' Ь + 1)) -ь Рпш (шп11„(х'.Ь + 1; т), и' Ь + 1).
Посылку этой импликацин можно заменить посредством Чх (х ( т -«- х' ( Ь); действительно, мы можем вывести формулу 'чх (х (и-ь х' ! Ь) — »[[х (х -т — Рпш (х' те+ 1, и' й + 1)). Наметим вкратце план этого вывода. Достаточно будет вывести чх (х <" т-»-х' ) те) -ь (г с'и — ь Рпш (т' й + 1, т'.Ь + 1)). Для этого мы будем исходить из двух выводимых формул г «" т -э Лх (х чь 0 А г' + х = т') и з ~ 0 &- г' + з = т' -«- Вх (з = х' & х ( т).
'] Мы пользуемся записью х'.Ь + 1 вместо (х' Ь)' для уменьшения числа скобок. З2 д Гвльеерт и Гера»ее 498 ПОНЯТИЯ »ТОТ, КОТОРЫЙ» И ЕГО ГСТРАНИМОСТЬ ИГЛ. УГЫ » 3) СВИДКНИК К ЯВНЫМ ОПРКДКЛКНняМ 499 Из второй формулы мы получим 'Ух (х - т -» х' ) й) -». (г =~ О дс г' + в = и' -»- в ) й), а отсюда, в сочетании с первой формулой, получим гсх (х ( т — ~- х' ! й) -э (г ( т -». Зх (х 1 й дс г' + х = и')). После этого для вывода искомой формулы будет достаточно вывести формулу Вх (х ) й А- г' + х = т') -».
Рпш (Г й + 1, и'.й + 1), которая в свою очередь дедуктивно равна формуле а ) й дс г' + а = т' — Рпш (Г .й + 1, и' й + 1). Но эта формула может быть получена следующим образом. Так как мы имеем г'+а=и'- г' й+1+а й=т' й+1, то выводима формула г'+а=и'-»-т' й+1=а й(шог)(г' й+1)). Далее, из определения Ргпп (а, Ь) мы получим Рпш(г' й+ 1, й) и Рг1ш (й, г' й + 1) а также а ) й †»- Рпш (а, г' й + 1); две последние формулы совместно друг с другом дают а )й-»-Рпш(а й,г' й+1).
Основываясь на приводившейся выше формуле г' + а = и' -»- и' й + 1 = а й (шог) (г'.й + 1)), мы теперь можем получить а ) й дс г' + а = и' -»- Рг)ш (т' й + 1, г' й + 1), а отсюда и требующуюся нам формулу а | й сч г' + а = т' — Рг)ш (Г й + 1, т' й + 1). Тем самым формула 'ух (х т -+ х' ) й) — ~ Рпш (ши!с, (х' й + 1; и), т' й + 1) окааывается выведенной. Наконец покажем, как при помощи фуннции р„А (х) может быть определен максимум аначений какого-либо терма г(а) для а - и. Соответствующее определение записывается в виде шах1(х) =Рх)УУ(У(п-+1(У)~(х).
В дальнейшем от этой функции нам потребуется лишь то ее свой- ство, которое изображается формулой 'чу (у ( и-э г (у) ( шах 1(х)). я<х Формулу эту мы можем получить, применив формулу (рг) в со- четании с формулой Зх'уу (у(я — »-$(у)~(х), которая выводится индукцией по и. 5 3. Сведение примитивных рекурсий к ввиым опРеДелениЯм посРеДством фУнкЦии )Ах А (ю) иа основе аксиом системы (Е) 1.
Эвристический подход. Теперь мы продвинулись настолько, что можем показать, каким образом с помощью функции рхА (х) всякое рекурсивное определение может быть ваменено подходящ м явным определением, в котором в качестве основнмх функций кроме штрих-функции используются только сложение и умножение. Рекурсивные определения вводятся, как мы помним, в определенной очередности, и функции, введенные к настоящему моменту, могут быть использованы в последующих рекурсивных определениях. Наша аамена рекурсивных определений явными также будет протекать шаг за шагом с учетом этой очередности. Все дело теперь сводится к тому, чтобы показать, что если до определенного места рекурсивные определения — не считая таковых для сложения и умножения, которые в системе (Х) берутся в качестве аксиом, — уже заменены явными определениями, то и непосредственно следующее аа ними рекурсивное определение также может быть заменено явным.
Пусть эта очередная рекурсия (адесь речь идет только о рекурсиях в узком смысле слова, т. е. о примитивных рекурсиях) имеет вид г) ц>(а, ...,й,О)=о(а,...,й), ср (а, ..., й, и') = Ь(а,..., й, и, ~р (а, ..., й, и)). ') Согласно раяее доказанному (гл. ЧП, с. 398), ыы могли бы адеоь ограяячяться рекурсиями с яе более чеы одним явраыотроы, яо наше рассуждение ог этого яе стало Вы проще. эг* 501 1(0) =а, 1(и')> й(и> 1(и)), ае> аа> ° аа» ~„(х') = 5(х, Д„(х)).