Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 124
Текст из файла (страница 124)
Тогда может быть выведено равенство (Л„е (»)) (а) е (а), а потому н формула =К(Л(х) й х (а) (Л„е (»)) (а)), Из этой формулы, взятой в сочетании с без труда выводимой в К формулой У«(Ф(с (1) =«(1))-Я(«)) йЯ(Ь) й Ь(а) = = (Л„е (»)) (а) -+- с (а) = (Л„е (а)) (а), мы получаем формулу 'е«(71(1 (3) «(1)) Я («)) с (а) = (Л„е (»)) (а), а затем 'ес«(Ч1(<(1)-«(1))-Я(«))- Ча(с'(1)=(Л„е(»))(1)), а также формулу 1<«('ч'1 (< (1) = «(1)) Я («))-~ Я (Л„е (»)) Но эта формула вместе с формулой, выводимость которой предполагается, дмт нам формулу Я (Л„е (»)). Таким образом, роль, которую в формализме Н по отношению к рассматриваемой формуле Я (с) играет фуНкционал а Я (х), в формализме К играет функционал Л„е(»). Этим методом использованное в Н явное определение для а+Ь в формализме К может быть заменено определением а+ Ь = <,ЛХ (х (0) = а й Чг (х (г') (х (г))') й (х (Ь) = и)) с предварительным введением по <-правилу <-терма, стоящего в правой части определяющего равенства.
При этом мы должны воспользоваться аксиомой индукции, аксиомами равенства н схемой для Л-символа. В частности, первая формула единственности получается нндукцией по а, а вторая — нндукцией по Ь. Аналогично, умножение может быть явно определено с помощью равенства а Ь <„ЭХ(х(0) ОйУг(х(г')=Х(г)+а)йх(Ь)=и), причем формула =)хУг (х (г) = 0), которая используется для получения первой из двух необходимых для применения с-правила формул, может быть выведена с помощью формулы <,(и=п йг=О) =О. Вслед за определением а+Ь мы можем, как и в Лс, ввести определение для ==, и тогда можно будет сформулировать явное определение для р-символа, нз которого получатся формулы (1<1), ПРИЛОЖЕНИЕ МОДИФИКАЦИИ ФОРМАЛИЗМА ИСКЛЮЧЕНИЕ Е.СНИВОЛА 686 (р,) и (р,) ') . Теперь р-символ может играть роль, которую в фор- мализме Н играет е-символ, так как прн замене е-символа Ьд-сим- волом формулы, оказывающиеся на месте первых двух е-формул, могут быть выведены из формул (р,) и (рв).
Теперь, аналогично тому, как это делается в Н , могут быть введены функции т (а, Ь), т, (п) и т, (и), а определение функции, универсальной для рекурсивных функций, может быть дано сле- дующим образом '): р (а, Ь, и) = д,йх (х (0) = а й ддгЬЕ и-д-х(е')=Ь(т(г,.т(г)))]йх(п)=и) ° Из этого определения выводятся равенства р(а, Ь, 0)=а и р(а, Ь, и')=Ь(т(п, р(а, Ь, п))).
Изображение рекурсивных функций при помощи этой универсаль- ной функции производится с использованием )д-символа. Например, функция 6(п) изображается в виде 6(п)=р(0, Ьд тд(х), п), а функция ( ) в виде (".— э)=р(0 )~ р(тд(х), Ь;(тх(г))', тд(х)), и). Метод замены функционала е;Я(у) соответствующим ему функционалом Ь дв'=Ь$ (Я (у) й у («) = и), применимый, как мы внаем, в случае выводимости формулы :-ЬйдУ«(УЬ(Й(Ь) =«(Ь)) И(«)) может быть распространен и на некоторые более общие случаи, часто встречающиеся в дедуктивной практике.
Пусть ад, ..., а,— свободные индивидные или функциональные переменные, и пусть формула 4)(а„..., а,)- ЗудтдЬ(дтд(у(Ь) =«(Ь)) И(«, а„..., ат)) выводима. Если мы обозначим посредством И*(Ь, ад, ..., а„) формулу (4) (а„..., а,) й И (ь, а„..., а,)) Ь/ ( щ (а„..., а,) й дйЬ (т (Ь) 0)) ') См. Приложение 1> с, 469, д) Обрвшвем вннмвнве нв то, что ввиду соглвшеннй, прннятых немн отио. сительно явных определений в формвлевме К, винись р» (а, Ь (х), л) недопустима. (где т представляет собой какую-либо не входящую в РЬ(дЬ, а,,...
..., а,) свободную функциональную переменную), то будут выводимы формулы =Ьедр«(дг)(в(Ь)=«(Ь)) И*(«, а„..., а,)) и Ь)(адт ..., ад)-д (Ив(т, а„..., а,) Я(т, а„..., а,)). Если теперь свободная индивидная переменная а и связанная индивидная переменная н не входят в И(д), ам ..., ат), то выражение д Д«(И* («, а„.. „а,) й «(а) = и) может быть взято в качестве терма. Пусть т(а) — этот терм или получающийся из него в результате переименования каких-либо связанных переменных терм, не содержащий связанных переменных, входящих в Ив(т, а„..., а,), и пусть « — какая-либо связанная переменная, не встречающаяся ни в этом терме, нн в Ив(«, а„..., а,).
Тогда указанным ранее методом можно будет вывести формулу Ив ()две («), а„..., а,), а потому и формулу др(а„..., ат)-в И(две(«), а„..., а,). Этим способом можно, например, заменить в формализме К определение функционала а: Ь, которое в Н записывается в виде') й: Ь'=еЬ(6*(х) йЬЭ.«-й), — после предварительного введения символов -д-, чь, О, 6* и 00 †определени дЬ Ь вЂ” ' Л»д»Бу (Ь(6» (а) й 6 в (Ь) й Ь ~ 0 й Ь бр у ='дЬ ) у' (( ) 6* (дЬ) д/ ) 6* (Ь) ~/ Ь вЂ” ' О) й у =' 0)1 й у (г) =* х), на основе которого может быть выведена формула 6 (а) й 6" (Ь) й Ь О - 6* (а': Ь) й Ь 8 (й' Ь) — ' а.
ь, помощью этого метода может быть заменено соответствующим определением в К и явное определение функционала $ (у, с, а), д) См. с, 570. ПРИЛОЖЕНИЯ использованное') при формализации в Н трансфинитной рекурсии. Но этого уже не удается сделать для следующего за ним определения функционала Е„.И (Ф, д), с помощью которого строится функционал ((б). И все же при формализации в К теории первого и второго числовых классов можно воспользоваться тем обстоятельством, . что функции, определенные трансфинитной рекурсией, представимы в К аналогично тому, как рекурсивные функции арифметики были представимы в формализме (2): вместо функционала ((б), для которого выводимы формулы ((6)), в К можно построить формулу (5(д, Ь), которая формализует отношение, изображаемое в Н формулой ((й) с. Наконец, если внимательно посмотреть, в какой степени указанные методы позволяют повторить в К выполненное средствами формализма Н дедуктивное построение анализа и теории полных упорядочений натурального ряда, то оказывается, что все это удается проделать почти в полном объеме, за исключением только тех, представляющих собой применение принципа выбора способов умозаключения, которые формализуются формулой (7а) или (7Ь).
Взяв формализм К за основу, мы можем изобразить и этот способ умозаключения, если добавим в качестве аксиомы формулу Ухну А (х, у) -ь. Эу ч1хА (х, Х,у (т (х, г))), при этом, чтобы в данной аксиоме не нужно было ссылаться на определение функции т(а, Ь), надо будет взять функциональные знаки т, и, и т, в качестве основных знаков, а формулы т(т,(п), т,(н))=п, тх(т(а, Ь))=а, тз(т(а, Ь))=Ь в качестве аксиом. Исследование непротиворечивости естественно начать с самого формализма К. При этом могут быть также произведены следующие редукции: может быть опущено правило введения явных определений, так как любой введенный явным определением символ в К, равно как и в Н, устраним из вывода любой формулы, не содержащей этого символа, а значит, и из вывода любой нумерической формулы. Затем, как и в ранее рассмотренных формализмах, в формализме К, ввиду осуществимости возвратного переноса подстановок в исходные формулы, имеется возможность исключить с помощью схем формул формульные переменные и сделать ненужными правила подстановки.
Тогда, в частности, на месте исходных формул х) См. с, 576, З Е1 Мопноихдции ОормдЛНЭМд, ИсКЛЮчяния е.СИМВОЛД 687 для кванторов появятся схемы формул 1аЬЯ(у)-~Я((), Я(()е- оЬЯ(Ь) чууЯ (х) -ь. И (9, И (() -~ ВуЯ Щ, причем в первых двух схемах вместо у надо будет брать какую- нибудь связанную индивидную переменную, а вместо 1 — какой- нибудь терм, а в следующих двух схемах вместо у- какую-нибудь связанную функциональную переменную, а вместо( †как-нибудь функционал. При этом теряется исключительный характер переменных а и х и д и х в схемах для кванторов.
Правила подстановки вместо свободных индивидных и функциональных переменных, равно как и правило переименования связанных переменных, становятся производными правилами. Кроме этой, возможной редукции формализма К, могут быть произведены и другие его модификации. Так, например, можно устранить связанное с ь-правилом усложнение понятия терма, условившись, что любое выражение вида )зИ (у) считается термом всякий раз, когда Я(с) — формула, содержащая свободную индивидную переменную < и не содержащая связанной индивидной переменной у, и, кроме того, взяв в качестве аксиомы формулу') ЗхА (х) й Ухну (А (х) й А (у) -а.
х = у) -~- А (ь„А (х)). Схема 1-правила в этом случае оказывается производной. Разумеется, в этом случае не всегда можно будет интерпретировать ь-символ как формализацию понятия «тот, который». Но во всяком случае в результате этой модификации формализма К никакая формула, не содержащая вхождений ь-символа, не станет выводимой, если она раньше не была выводима в К. В самом деле, это следует из того, что — как нетрудно сообразить — любая 'выводимая в модифицированном формализме формула после замены каждого выражения вида ь Я (у) соответствующим выражением )ь И(у) переходит в формулу, выводимую в формализме К.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
