Гильберт, Бернайс - Основания математики. Логические исчисления и формализация арифметики (947375), страница 104
Текст из файла (страница 104)
Тогда формула 1чх (Ж (Я (х))— Ж (3(х))) после элементарных преобразований ее средствами исчисления предикатов запишется в виде (1) Ухчх! ... ~ь$ (Ж(Я (х)) &Ж(Я (Х1)) & Ж(52(х2)) & ." & Ж(5~ (х~)) -«)р(х, ХО ..., Х~)). Формула Й(2„Я (х)), т.е. ф (22Я (х), 2,, 52 (х2) ° ° 2х~5$(хд) по принятому нами соглашению должна ваписываться в виде З2*(2,Я(х), 2,252(х,), ..., 2, 5~(ху)), где )р*(с, сз, ..., С~) представляет собой формулу ~З2(с, с, с2, ..., с~).
Тем самым редукция Ж(3(2„Я (х))) есть формула (2) з'х'Фхз ... 'Фх~(Ж(Я(х))&Ж(52(хз)) & ... & Ж(5~(ху)) 'д1(х, х, х2, ..., Х~)). Чтобы убедиться, что в этом случае формула (Ж Я 3) выводима без использования 2-символов, согласно теореме о дедукции, достаточно установить, что формула (1) может быть переведена с помощью формулы ЗХФу (Ж(Я(у)) у = х) в (2). УСТРАНИИОСТЬ ХАРАКТЕРИСТИК О-СИМВОЛОВ) 525 534 понятие «тот, кОтОРый» и его устРАнимОсть 1гл.
чш 5 4) Как мы знаем, ив формулы Лх»»»у (Ж(а(у)) — у = х) при помощи аксиомы равенства (4 ) можно получить вторую формулу единственности для Ж(Я(с)), а тем самым и Ж (Я (а)) А Ж (Я (а»)) -ь а = а,. С другой стороны, снова польауясь аксиомой (3т), мы получим формулу а = а, — »- (д5(а, а„ат,..., а1) )р (а, а, ат,..., а])); эти две формулы совместно друг с другом дают Ж (Я (а)) А Ж (»Л (а)))-+. ()[5 (а, а„аю ..., а)) ф (а, а, аю..., а))) '). При помощи этой формулы формула (1) может быть переведена в формулу 'тхтх» ...
'Ух~(Ж(о[(х))АЖ(Я (х»))АЖ(Яе(хв)) А... АЖ($1 (х»)) $( ° . " '1) а эта последняя может быть переведена в (2) согласно выводимой схеме формул »эх»ех, (6 (х)1& 6 (х,) — ь ф (х))»тх (6 (х) — ь А) (х)). Рассмотрим теперь вторую из упомянутых вьппе возможностей, а именно тот случай, когда переменная с встречается по крайней мере в одном из»-термез, входящих в нашу элементарную формулу ц](с). Переменная с в этом случае может встречаться в й](с) еще и помимо этих»-термов. Предположим, что это последнее места не имеет. Тогда й](с) имеет вид ф()»я,(х„с), ..., »„,Яс(хс с), »е,6»(у») "Р,66(уз)) (здесь переменная с не входит в выражения 6,(у»)» ..., 65(ус)); впрочем, число б может быть и нулем). В рассматриваемо») случае )»х (Ж (Я (х)) — ь Ж (й (х))) ивображается формулой [1] 'Фх[Ж(Я(х))-».»ух) .. ~»хс'5»У» ...
»УУВ(ЖЯ»(х»» х) А ... А Ж(5т(х„х))АЖ(6,(у,))А ... &Ж(6,(ув))- »41 (х„..., х, У„..., Ус))], ') Чтобы избежать нежелательных совпадении, быть может, следует в этих формулах вместо о, а, ..., а~ веять навис-нибудь другие свободные переменные. а Ж()О(» Я (х))) — формулой ]2] )У ° ° ° 'Ухе)Уу ° ° ](уз(Ж(6 (х, ло] (х))) 8 ... & Ж (5т (хс, » Я (х))) & Ж (6, (у,)) & ... & Ж (65 (уз)) -»- чу(х» ° ° ° хв» У» ° ° » Уз)) Чтобы в этом случае установить, что формула (Ж, Й, )О] выводима без использования»-символов, в силу теоремы о дедукции достаточно показать, что, испольвуя формулу Зх))»у (Ж()1(у)) у = х), можно без использования»-символов перевести друг в друга формулы [1] и [2] при помощи исчисления предикатов и с применением аксиомы равенства (ее). Кроме того, мы можем воспользоваться индукционным предположением. Его можно будет применить к формуле Яг (сн с) &... А $т (с, с) (с именными переменными с, сю..., с,) '), где сг, ..., сс мы рассматриваем как параметры; вта формула содержит по крайней мере на один логический символ меньше, чем формула ц](с), так как число добавляемых знаков конъюнкции на единицу меньше числа упраздненных»-символов», ..., )„.
Мы сокращенно запишем эту конъюнкцию в виде й(сю..., с, с). Таким образом, для нашего вывода мы располагаем формулой Эх)УУ (Ж(Ж(у)) у = х) -». [»Ух (Ж(й (х)) -»- Ж(й(сю..., сс, х))) - Ж(й(с„..., с, » „о] (х)))]. Так как формулу Зх))у (Ж()Х(у)) у = х) мы используем в качестве вспомогательной, то по схеме заключения получим эквивалентность 'ух(Ж(21 (х))-»-Ж(й(сж ..., с„х)))-Ж(й(с„..., с„»„р((х))), согласно которой мы можем оба ее члена заменять друг другом. С этими вспомогательными средствами мы приступим к переводу формулы [1] в формулу [2].
Формула [1] средствами исчисления предикатов может быть преобразована в УХ7х, ... Ух 'Уу, ... )Уув[Ж(о](х)) АЖ(й(х„..., х, х)) 8с Ж (6» (У»»)) & ' А Ж (65 (Уз)) )»»5 (х ° . хю У! Ув)] и далее в формулу [1'] 'Ух) ... УхсГУу) ... ](Уз[ЗХ(Ж(Я(х)) &Ж(й(х„...,х, х)))8с Ж(6)(У»)) 8с ... АЖ(65(УЕ))'-»»45(ХО ...» Х„У„..., У )]. ') При етом мы должны будем воспольеоваться тем обстоятельством, что редунция воныонвции каких-либо формул, по определению, есть вонъювнция редукций ее членов. попятив «тот, котогыи«н иго РОТРАнимость Хтл. Рпг РстРАниыОсть хАРАктвРистик (Рсимволов) Теперь воспользуемся установленной нами переводимостью формулы Лхэ)у (А (у) у = х) в конъюнкцию формул ЗхА(х) и 'Фх Чу (А (х) & А (у) — Р х = у). Отсюда следует, что из нашей вспомогательной формулы Эх)гу (й (Я (у)) ° у = х) можно вывести формулы единственности для й(Я(а)) (а играет роль именной переменной); из этих последних при помощи исчис- лениЯ пРеДикатов и аксиомы Равенства (А г) можно полУчить эквивалентность Зх(й(Я(х)) &В(х)) ° ]))х(Й(Я(х))-РВ(х)).
Подставив в нее вместо В (с) формулу И([т' (с„..., см с)« мы получим тем самым формулу Лх (Я (Я (х)) & Я (1[ (с), ..., с, х))) ]Ух (й (2[ (х)) -Р Й(К(сп ..., сг, х))). Части этой эквивалентности можно заменять друг другом. Но вместо второй иэ них можно, как мы установили выше, написать Й(Й(,,; «Я())). Поэтому формулу [1'] мы можем перевести в формулу ][х, ... Х))хг)УУ, ... 'г)уг [И(И(хм ... х, г„Я (х))) & й(6,(у,)) & ...
&Я(6,(уг)) — Я(х„..., х„у,, уг)]. Но это и есть формула [2], так как Я([1(с„..., с, с)) совпадает с Я(5)(сы с)) &... & Я 9 (с, с)). Тем самым искомый перевод осуществлен. Заметим, что в нем отсутствуют ~-символы. В самом деле, все редукции свободны от ~-символов (даже тогда, когда ~-символы встречаются в их обоаначениях). Аналогичным образом мы поступим и тогда, когда в элементарной формуле В(с) переменная с будет встречаться и вне ~-терман, так что Е(с) будет иметь вид ф(с, г,)5,(хо с), ..., г„т5,(х„с), ~ю6,(у)), ..., г„6З(уг)), где с снова не входит в 6,(уг),..., 6 (УА).
Аналогично предыдущему, адесь формула )Ух (И(Я(х)) «- Я(д](х))) с использованием сокращения [г(с„..., с, с) можег быть записана в виде [1х] У [й(Я(х))- Ъ~х, ... УхгУу, ... ](УА(й(1[(х„..., х„х)) & Я(6)(у))) & &Я(6г(уг)) — $(х, хо ..., х„УО, Уг))] Но теперь )«2[(х) фигурирует в В(г„Я(х)) в качестве внешнего ~-терна, и тем самым редукция Я(В()„Я(х))) может быть записана в виде х) [2х] ]ух'Фх . ° . Тух Уу, ... ][Уз(й(2[ (х)) & Я (й (хм ..., х„~„Я (х))) & й (6) (у,)) & ...
&'„й (6г (у„)) -«- $ (х«х)« ° ° «хю Ум ° «Уг)) Для установления того, что формула (Й, Я, В) может быть выведена без использования ~-символов, достаточно перевести— без использования ~-символов — формулу [1х] в [2х], используя прн этом в качестве вспомогательного средства формулу Лх)) у [й (Я (у)) у = х), которую мы кратно ооозначим посредством 0(Я(Я)). Для этого мы применим наше индукционное предположение к формуле й(с„..., сг, с) (где с„..., сг) — параметры). Это даст нам возможность заменить формулу )«г [Я (Я (г))-+-й (й (с„..., с„г))] формулой Я (К(с» ..., сг, ~«Я (г))). С другой стороны, из формулы Х[(Я(Я)) могут быть выведены формулы единственности для Я(Я(а)). Применяя вторую из них, а также аксиому равенства (г г), мы получим средствами исчисления предикатов формулу И(Я(с)) &В(с) й(Я(с))&Чг(й(Я(г))-э-В(г)).
Подставив в нее вместо В (с) формулу й([г(см ..., с, с)), мы получим переводимость формулы Я (Я (с)) & 3; (й (с„..., с, с)) в )Х)ормулу Я(2[ (с)) &'))г(И(Я (г)) — ~')А](й'(с„..., с„г))), которая, другой стороны, как было укааано выше, заменима формулой Я (Я (с)) & Я (й (с„..., с, ),Я (г))). Но тем самым мы имеем перевод [1х] в [2х], не использующий ~-символов, так как [1х] допускает преобразование в тух)ух, ... Чхгуу) ... Чуг(Я (Я (х)) & Я ([[(хм ..., хг, х)) & Я(6,(у,))& ... &И(6г(уг)) -«. ф(х, х„..., х, у„' ..., Уг)).
') Следует обратить внимание ва необходимость пвревменоваввя переменной х эо вложенном «-терке )„ Н (л). УСТРАНИМОСТЬ ХАРАКТБРИСТИК О-СИМВОЛОВ> 529 523 поннтин атота которыие и Бго УстРАнимость П'л ч>п Остается еще рассмотреть случай, когда в элементарную формулу 3(с) наряду с а-термами, содержащими переменную с, входит а-терм, совпадающий с а Я(х).
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
