Гильберт, Бернайс - Основания математики. Логические исчисления и формализация арифметики (947375), страница 91
Текст из файла (страница 91)
Как мы знаем, великая теорема Ферма (для произвольных чисел 1 ) 2) не доказана, а также нет и метода, который позволял бы для любой ааданной цифры г выяснить, справедливо лн для нее утверждение атой теоремы. Процедура редукции для системы (Е) должна была бы дать нам такой метод. Эта процедура редукции должна была бы отвечать и па произвольный вопрос о разрешимости того или иного д и о ф а н т он а у р а в н е н и я, иначе говоря, она должна была бы отвечать на любые вопросы, касающиеся разрешимости в положительных целых числах любых алгебраических уравнений с одним нлн несколькими неизвестными и с целочисленными коэффициентами е). Кроме того, с помощью процедуры редукции мы могли бы получить ответ и на вопрос о том, обладает ли данное уравнение «бесконечным числом» решений, а также на вопрос о том, верно ли, что такое уравнение для произвольных значений одного из неизвестных (или соответственно для всех значений, превышающих некоторое заданное число) имеет решение (в остальных неизвестных).
Но все это — вопросы, от решения которых мы в математике очень далеки. Однако нам вовсе не нужно вдаваться в дискуссию по поводу отдельных примеров, так как в дальнейшем получится — и в атом проявляется существенное отличие системы (Е) от ранее рассмотренной системы,— что рассматриваемый нами формализм системы (Х) не только позволяет, как мы в атом только что убедились, формулировать те или иные трудные проблемы арифметики, но что он вообще дает нам определенную формализацию всей арифметики.
Именно, в этом формализме уже) оказываются представимыми все функции, которые вводятся при',е'помощи е) Как было установлено в работе: М в т и ив е в и ч Ю. В. Диофавтовость перечисвиыых множеств.— ДАН СССР, 1970, 191, с. 279 — 282, алгоритм, распозивющий реврешиместь диофавтовых уравнений, иевевиожеи.— Прим. ред. [ГЛ. Р[[ РЕКУРСИВНЫЕ ОПРЕДЕЛЕНИЯ 456 1 Ы допОлнительное РАссмотРение Аксиом РАВВнстВА 457 рекурсивных равенств, причем даже в том случае, если мы допустим ряд рассматриваемых В рекурсивной арифметике обобщений схемы рекурсии.
Этот материал мы изложим только в следующей главе в связи с рассмотрением понятия «тот, которыйз, так как в этой связи ему может быть придана более точная редакция и более четкий вид. По[[а же мы отметим, что в случае системы (У) метод установления непротиворечивости при помощи процедуры редукции не достигает своей цели. Тем не менее этот метод позволил вам убедиться в непротиворечивости таких систем аксиом, которые не выполнимы в конечном (правда, только при некоторых ограничениях па способы образования понятий). Кроме того, он содействовал установлению того факта, что система аксиом Пеано, если взять за основу исчисление предикатов и аксиомы равенства, оказывается недостаточной для построения арифметики и что добавление к этой системе аксиом рекурсивных равенств для сложения и умножения является существенным расширением формализма; только благодаря такому расширению и проявляется все богатство арифметических отношений.
3 б. Дополнитеиьное рассмотрение аксиом равенства 1. Замена второй аксиомы равенства аксиомами более специального характера. В заключение этой дискуссии мы рассмотрим одно замечание, относящееся ко второй аксиоме равенства. Эта аксиома () з) во всех рассмотренных нами системах занимает особое положение, потому что, если не считать аксиомы индукции, она является единственной аксиомой, содержащей формульную переменную. Достойно внимания, что этого появления формульной переменной мы могли бы и избежать, если бы интересовались выводимостью только таких формул, которые не содержат формульных переменных. Мы постараемся проиллюстрировать зту мысль на примере первой из обсуждавшихся в гл.
Ч) систем аксиом, которая кроме аксиом равенства содержит аксиомы ((з), («..з) («..з) (Оз) и (Рз) ) Если из атой системы аксиом оказывается выведенной какая-либо формула, то, как мы знаем, из ее вывода можно исключить формульные переменные, сначала разложив этот вывод на нити, затем выполнив перенос подстановок вместо формульных переменных в исходные формулы и совершив произвольные подстановки вместо оставшихся формульных переменных '). Тогда вместо формулы (3 з) у нас появятся исходные формулы вида а = Ь -» (Я (а) -» Я (Ь) ), ') См. с.
273. з) См. с. 273 и далее. где формула Я (с) (которую мы подставляем в () з) вместо именной формы А (с) ) пе содержит формульных переменных. Эта формула является либо равенством, либо неравенством, либо строится из равенств и неравенств с помощью связок исчисления высказываний и, быть может, связывания одной или нескольких переменных. В обеих частях любого равенства или неравенства стоят выражения а[1), где а представляет собой либо символ О, либо (свободную или связанную) переменную. То обстоятельство, что формула Я (с) устроена именно таким образом, позволяет нам заключить, что любая из рассматриваемых нами исходных формул а =- Ь-» (Я (а)-» Я (Ь)) может быть выведена с помощью исчисления предикатов из сле- дующих формул: (уз) а=а, (1) а = Ь -» (а = с -» Ь = с), (1«) а=Ь-»а'=Ь', ( з) а=Ь вЂ” »(а~с-» Ь(с), (1«) а = Ь -» (с ( а -» с «Ь).
Факт этой выводимости вытекает из того, что: 1. Из формул (з,) и (1,), как было показано ранее '), выводимы формулы а=Ь-» Ь=а а= Ь -» (с = а — » с = Ь). й. Из формулы (1,) для любого 6 выводима формула а = Ь-» а(" = Ь(1). 3. Из формулы а=Ь-»(6(а)-»6(Ь)), пользуясь формулой а=Ь вЂ” » Ь=а, можно вывести формулу а = Ь вЂ” » ( 1 6 (а) -» [ 6 (Ь)).
4. Если Ц вЂ” произвольная формула, то из формулы а = Ь-» (6 (а)-» 6 (Ъ))) з) См. гл, Ч, с. 212 — 213. 1гл, чп РЕКУР'.ПВНЫВ ОПРЕДЕЛЕНИЯ $ б1 ДОПОЛНИТЕЛЬНОЕ РАССМОТРЕНИЕ АКСИОМ РАВЕНСТВА 439 средствами исчисления высказываний выводимы формулы а= Ь вЂ” »-(6(а) ~/ В-~6(Ь) ~/ 11) и а=Ь-» (О ~/ 6(а) — »-)1 )/ 6(Ь)). 5. Иэ формулы а=Ь вЂ” ».(6(а, г)-»-6(Ь, г)) выводима формула л = Ь вЂ” »- (Эхб (а, х) -»- Зхб (Ь, х)). б. Всяка . Всякая формула рассматриваемого формализма переводима средствами исчисления предикатов в некоторую другую формулу, не содержащуго кванторов всеобщности и такую, что иэ числа свявок исчисления выскааываний в ней встречаются только отрицание и диэъюнкция.
Отсюда следует, что в процессе вывода формул, не содержащих формульных переменных, в рассматриваемой системе аксиом вторая аксиома равенства ()1) может быть заменена формулами ("1)~ (11)» (гэ) и (11). В этом рассуждении мы не польаовались какими-либо особыми свойствами отношения а «Ь или штрих-функции, нашедшими отРажение в аксиомах ((1), ((б)» (~э)» (Р„) и (Рб); поэтомУ полученный нами результат можно применить и к другим формализованным системам аксиом, возникающим в результате добавления к формалиэму исчисления предикатов тех или иных предикатных символов, индивидных символов и энаков для математических функций вместе с относящимися к ним аксиомами; только среди аксиом этой системы должен содержаться знак равенства с аксиомами (Хг) и (11).
Если внутри такого формализма рассматривать выводы формул, не содержащих формульпых переменных, то в атих выводах аксиому ((б) можно будет ааменить рядом формул, имеющих вид а = Ъ -»- ($ (а) ». »4б (Ь)) или а Ь-1- 1 (а) ( (Ь), где ))б означает какой-нибудь предикатный символ, а 1 — какой- нибудь функциональный анак. Как 3», так и 1 кроме обоаначенных аргументов могут иметь и какие-нибудь другие; тогда эти аргументы должны быть попарно раэличными переменными, отличными от а и от Ь. Среди формул а = Ь -»- (эб (а)-»- 3б (Ь)) находитсяформула (1,), а кроме того, каждому аргумент'у любого отличного от знака равенства предикатного символа соответствует по одной такой формуле и каждому аргументу любого функционального анака соответствует некоторая формула вида а = Ь-э 1(а) = 1(Ь).
Так, в случае только что рассбютренной системы аксиом двум аргументам предикатного символа ( соответствуют две формулы (11) и (11), а единственнному аргументу штрих-функции соответствует формула (1,). 2. Применение к системам (А), (В) и (Х). У некоторых систем аксиом те или иные представляющие формулы оказываются излишними. Рассмотрим с этой точки зрения системы (А) и (В).
Система (А), правда, непосредственно не попадает в сферу действия нашей общей теоремы, так как формула (11) в гнп среди аксиом не встречается. Тем не менее данное обстоятельство не препятствует применению атой теоремы, так как В системе (А) аксиома (11) может быть выведена иа аксиом («.,), а ( Ь-»- -»- ~(Ь ( а') и а чь Ь-» а ( Ь ~/ Ь ( а ). Здесь можно добиться некоторых упрощений.
Именно, в системе (А) вместо формул (1 ), (1э) и (11) достаточно взять формулу а= Ь вЂ” ~ ~(а«;.Ь) или же формулу а=Ь-э а<Ь', так что каждая иэ этих двух формул вместе с (1,) может ваменить в системе (А) аксиому (11). В самом деле, если мы в (А) эаменим (11) аксиомой (1,) и воспользуемся только что упоминавшимся выводом формулы ()1), то окажутся выводимыми формулы а = Ь вЂ” »- Ь = а и а = Ь -»- (Ь = с — »- а = с) 1). Привлекая формулу а = Ь-» 1(а( Ь), мы получим, с испольэованием аксиом (» ) и а ~ Ь-». а «д ~/ Ь с. а» формулы (1,) и (1,). Иа (1,) с помощью аксиомы ((,) мы получим, далее, формулу а = Ь-»- Ь«аб и, с учетом а = Ь-»- Ь = а, получим а = Ь-э а < Ь'.
1) См. гл. Ч1, с. 320, 322. б) См. с. 212 — 213. 460 РЕКУРСИВНЫЕ ОПРЕДЕЛЕНИЯ !ГЛ. Чы (') ) (1 ) (1э) ((э) а = Ь-э. 1(а « Ь), а=Ь-~а<Ь', аксиома индукции. а+ с = Ь+ с, с+ а = с+ Ь, ас=Ьс, с.а=с Ь. а = Ь-+- а = Ь-~ а = Ь-эа = Ь-э. а = Ь -1- а = Ь, 1) См. с. 321. ) См. с. 333 — 335. ') Об этом см. гл. У1, с. 332. и аксиому а' = Ь'-э а = Ь Две последние формулы, в сочетании с формулой ( Ь вЂ” '11' ', ыводимои в (А) беэ использования (11) '), дают формулу (1,) (с испольэованнем («-э), 1(а «а) и Ь' = а' — Р С другой стороны, если вместо а = Ь-+ )(а «Ь) добавить к системе (А) в качестве аксиомы формулу а=Ь вЂ” э-а(Ь', то можно будет получить формулу а = Ь вЂ” ~- Ь «.. а', а иэ нее с помощью аксиомы а ~ Ъ-~ 1(Ь а') м снова получить фо ь ормулу ( С а ) можно будет а = Ь-~ 1(а ~ Ь). В случае системы (В) мы вернемся к рассмотрению уже и и- водившегося хаэенъегеровского вывода ф 11а «Ь" В эт уже приэтом выводе аксиома равенства (э' ) исполь- эуется только для вывода след ющя у х трех формул: Я а' ( Ь'-~ а ~ Ь, а'.= Ь-+.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
