Гильберт, Бернайс - Основания математики. Логические исчисления и формализация арифметики (947375), страница 106
Текст из файла (страница 106)
нерее.). В качестве новейших публикаций пс этому вопросу следует также уцомяяуть работы К. Шрэтера; Я с Ь г осе г К. ТЬеог)е йее Ье»Мшшсеа Агг!Ье!е.— Е. ша1Ь. ЬОЯ!Ь Огаай1. МасЬ., 1956, 2 — и Э. Мендельссвас М е а й е1 5 оп Е. А вешаэмс ргсо1 с1 1Ье е1!шшаЬ11Ву О1 йевсг1рс!оаэ.— 2. шасЬ. СОЯ!Ь Огцвй1.
МасЬ., 1960, 6, Я. 199— 208. е) В порядке псдгстсэкя к первоначальному доказательству устрани- мости с-сзыэслсэ вами было дскаээво одно дополнение к теореме ве гл. ЧП (с. 456 — 459) с воэможности замены ансясыы равенства (1,) влв сссгэетстэеяяс схемы равенства а = Ь -«(сд (а) 9! (5)) сабстэеякыыи аксиомами. Отяссящяеся к этому рассуждения следуют ниже э спецяальясм дополнении; сы.
с. 547 †5. 6 б. Следствия, вытекающие из устранимостн характеристик 1. Представимость рекурсивных функций в системе (Х). Из полученного нами результата мы можем, в частности, вывести как следствие сформулированную в гл. УП теорему о представимости рекурсивных функций в еистлеме (Х) '). Пусть 1(а, Ь,, Й) — функция, получаемая, исходя из штрих-функции, применением примитивных рекурсий и подстановок.
Как мы знаем э), внутри той системы, которая возникает из системы (Х) в результате присоединения функции )с 4 (х) и формул ()51), ()с») и ()се), такую функцию можно изобразить посредством некоторого герма 6(а, Ь,..., Й), который не содержит никаких свободных переменных, кроме а, Ь,..., Й; при этом отношение герма 6 (а, Ь,..., Й) к функции 7 (а, Ь,..., Й) таково, что всякая формула, выводимая в рекурсивной арифметике и содержащая функцию 1 (а, Ь,...,.Й), в результате замены 1 (а, Ь,..., Й) посредством 6 (а, Ь,..., Й) перейдет в формулу, выводимую средствами системы (Х), дополненной формулами ()сс), ()с») и ()сэ).
Как известно, применение функции )с А (х) и формул ()сс), ()с») и ()55) здесь может быть сведено к применению с-правила »). г'ели вместо встречающихся в 6 (а,..., Й) выражений )с„Я (х) мы подставим их определения при помощи с-символа, то у нас получится некоторый терм 9(а, ..., Й), построенный с помощью с-снмволов; этот терм снова находится к 1 (а,..., Й) в таком отношении, что каждая формула, выводимая в рекурсивной арифметике и содержащая функцию ! (а,..., Й), в резуль-.
тате замены 7 (а,..., Й) посредством 9 (а,..., Й) перейдет в некоторую формулу, выводимую средствами системы (Х) с добавлением 1-правила. Поэтому, в частности, если а,Ь, ...,1,1 суть какие-либо цифры, то в системе (Х) с добавленным с-правилом выводимо равенство 9(а, Ь, ° ° ., 1) =1 или же его отрицание 9(а, Ь, ...,1)Ф1 в зависимости от того, совпадает или не совпадает с ! значение функции 7 (а, Ь,..., 1), получающееся в результате рекурсивного вычисления. ') Сы.
с. 455 я далее. ») См. с. 499 и далее. «) См. с. 481 — 482. 534 понятие «тот, котОРын» и егО устРАнимОсть сгл. ч111 $ Ы следствия иэ устРАнимости хАРАктеРистик 535 Теперь рассмотрим равенство 3(а,..., сс) =! с переменными а, ..., »с, !. Редукцией этого равенства является не содержащая 1-символов формула 6(а,..., !с, (), для которой выводима эквивалентность (6) 6(а,..., «с, () 3 (а, ..., «с) = !.
Так как в эту эквивалентность вместо переменных а, ..., сс, с мы можем подставить любые цифры, то в соответствии с ранее сказанным получается, что в зависимости от того, совпадает или не совпадает с ! значение ! (а,..., 5), средствами системы (Е) в сочетании с д-правилом может быть выведена либо формула 6(а, ...,д,!), либо ве отрицание. Из доказанной нами теоремы об устранимости 1-символов теперь вытекает, что из вывода формулы св(а, ..., д, !), соответственно формулы ! 6(а, ..., д, !), поскольку в ней не содержится д-символов, применение 1-правила может быть устранено.
Поэтому средствами самой системы (Е) может быть выведена либо формула 6(а, ...,5,!) либо ее отрицание в зависимости от того, совпадает или нв совпадает с ! значение ! (а,..., г). Поэтоыу функция ! (а,..., «с) действительно оказывается представимой в системе (Е) в смысле нашего более раннего определения 1): в самом деле, равенство !(а,..., «с) =! оказывается представленным формулой 6(а,..., сс, с). Однако представимость рекурсивных функций в системе (Е) имеет вдесто не только в смысле указанного определения в), но и в некотором более сильном смысле. Действительно, основываясь на выводимости эквивалентности (6), мы можем заключить о выводнмости формул единственности 356 (а, ..., сс, 5), !уй чд)(6(а, ..., сс, 5) «Г«6(а, ..., «с, 5)».5 ='у) '! Сы.
с. 433. ») Для целей проводившихся тогда рассметрвялй условие «лредставнмости» функции лря формулировке этого определения было выбрано чрезвычайно слабым. См. примечание ла с. 433. (с подходящими связанными переменными 5 и 5). В соответствии с этим можно будет ввести 1-терм 1 6 (а... «с, 5) н мы получим формулу 6(а, ...,«ц»6(а, ...,»С,й)) равно как и эквивалентность ся (а, ..., «с, !) С =1 6 (а, ..., сс, 5). Подставив 3 (а, ..., »с) вместо си воспользовавшись эквивалент- ностью (6) и аксиомой (3»), мы придем к равенству б (а, ..., )с) = 1 6 (а, ..., «с, 5).
Тем самым терм б (а,..., Й), а значит, и функция ! (а,, я) оказываются изображенными посредствоы некоторого д-герма, получившегося в результате применения»-символа к некоторой формуле системы (Е). Итак, этим способом можно изобразить любую рекурсивную функцию, и данная изобразимость основы- вается на добавлении к системе (Е) рассмотренного нами 1-пра- вила. При помощи этого способа, позволяющего изобразить любую рекурсивную функцию посредством некоторого 1-герма ддс((а,..., сс„й), мы можем теперь перейти от равенств, пред- ставляющих собой рекурсивное построение какой-либо функции ! (а,..., «с), к формулам без д-сиыволов, характеризующим пре- дикат 6(а,..., )с, !) в системе (Е). Пусть, например, функциональный знак ф (а, Ь) вводится рекурсивными равенствами ф(а, 0)=а(а), ф(а, и') = Ь(а, и, ф(а, и)), где а (а) и Ь (а, и, с) — рекурсивные термы, и пусть функции ф(а, Ь), а(а) и Ь(а, и, с) изображаются 1-термами 1„6(а, Ь, х), дв»а'(а, У) и 1»3(а, и, с, з), где 6(а, Ь, сс), Я(а, Ь) и !!)(а, и, с, с!) — формулы системы (Е).
Тогда вместо этих рекурсивных равенств мы сначала получим равенства 1,6 (а, О, х) = двн (а, у), 1„6 (а, и',х) = д,ц)(а, и, 1 6 (а, и,х), л). Затем из первого равенства с помощью выводимых эквивалентностей 6 (а, О, с) с = св6 (а, О, х), д (а, с) с = свею (а, У) 536 ПОНЯТИЕ»ТОТ, КОТОРЫЙ» И ЕГО УСТРАНИМОСТЬ >ГЛ.
УП1 и формулы а=Ь-«(с=а с=Ь), получающейся из аксиомы равенства (1г), мы получим эквива- лентность 6 (а, О, с) Я (а, с). Из второго равенства с помощью выводимой формулы 6 (а, и, Ь) — >-Ь= 1„6 (а, и, х) и аксиомы равенства (гг) мы получим формулу 6 (а, и, Ь) ->- г»6 (а, >г', х) = г,й (а, и, Ь, з), а из нее с помощью эквивалентностей 6(а, >г', с) с=г»6(а, и', х), В(а, и, Ь, с) с=1,й(а, и, Ь, з) и аксиомы равенства (гг) мы получим, далее, формулу 6 (а, и, Ь) «(6 (а, >г', с) В (а, и, Ь, с)).
Тем самым для характеризации предиката 6(а, и, с) мы получаем две формулы без г-символов: 6 (а, О, с) Я (а, с), 6 (а, и, Ъ) -«(6 (а, и', с) В (а, и, Ь, с)), которые заменяют в системе (Е) рекурсивное определение функции >у (а, Ь). Обратим внилгание на то, что из этих формул и вз формул единственности для Я(а, с) по второму аргументу и для В(а, и, Ь, с) по четвертому аргументу нндукцией по и могут быть выведены формулы единственности для 6 (а, и, с) по третьему аргументу. Далее, если функция >", является комбинацией уже построенных рекурсивных функций, то из предикатов, представляющих в системе (Е) участвующие в атой комбинации функции, мы получим характеризацию предиката, представляющего функцию Пусть, например, функция ь (а) определяется, исходя из функций гр (а, Ь), г(> (а) и т (а), при помощи функционального соотношения ь (а) = >р (ф (а), Е (а)), н пусть >р(Ь, с) = г„Я (Ь, с, х), ф (а) = г„й (а, у), т (а) = 1,6 (а, з), ь (а) = г„.й (а, х), где Я(Ь, с, гг), В(а, >К), 6(а, >К) и Я(а, а>) — формулы из системы (Е), представляющие эти функции.
Тогда в качестве опреде- 1 Ы СЛЕДСТВИЯ Из УСТРАНИМОСТИ ХАРАКТЕРИСТИК 537 ляющего равенства мы получим сначала г„й (а, х) = г,Я (глй (а, у), 1,6 (а, з), х). Из него, опираясь на эквивалентности В(а, Ь) Ь= ггй(а, у), гл (а, с) с=гггл (а, г), мы получим при помощи аксиомы равенства (гг) формулу В (а, Ь) бг 5 (а, с) — «г„й (а, х) = 1„Я (Ь, с, х), а затем из нее — опираясь на эквивалентности Я (Ь, с, г() д = г„Я (Ь, с, х), й'(а, А) г( = г„й (а, х) и используя аксиому (г г) — формулу З(а, Ь)бган(а, с) — «(И(а, с>) Я(Ь, с, д)), посредством которой предикат Й(а, д) характеризуется в системе (Е). Из этих формул и из формул единственности по последнему аргументу для формул В(а, Ь), 6(а, Ь) и Я(Ь, с, д) могут быть выведены формулы единственности для к(а, Ь) по второму аргументу.
Втот способ позволяет нам шаг за шагом получать для каждого состоящего из примитивных рекурсий и подстановок определения какой-либо рекурсивной функции 1(а, „ Ь) характеризацию некоторого предиката, представляющего ее в системе (Е). Только что проведенное нами рассуждение может быть обобщена в том смысле, что относительно рассматриваемой нами функции ) (а,..., Ь) мы можелг н не предполагать, что все использованные для ее построения рекурсии являются примитивными; более того, будет достаточно, чтобы все этя рекурспи обладали следующими двумя свойствами: 1.
Онн дают возможность вычислять значения этой функции при произвольной фиксации аргументов, причем оказывается возможной формализация этого вычисления, т. е. вывод равенства 7(а, ..., 1)=( в том случае, если 1 является аначением ) (а,..., 1). 2. В рамках системы (Е) они допускают сведение к явному определению при помощи функции )г„А (х). В проведенном нами доказательстве представимости рекурсивных функций мы совершили два рааличных перехода: во-первых, арифметическое сведение рекурсивных функций к сложению и умножению при помощи функции И„А (х) и, во-вторых, устранение г-символа, с помощью которого вместо функциональных равенств (построенных с участием г-символов) мы получаем соответствующие представляющие формулы. 533 понятие «тОт, кОтОРый» и его устРАнимость (гл„у|11 $51 СЛЕДСТВИЯ ИЗ УСТРАНИМОСТИ ХАРАКТЕРИСТИК 539 Эти два шага можно было бы объединить в один и таким образом избежать использования г-символов; однако с помощью г-символов этот прием принимает более прозрачный вид.
2. Общий способ исключения функциональных знаков путем введения предикатных символов; исключение индивидных символов. Вообще, введение г-символов представляет собой удобный способ перехода от функциональных знаков к соответствующим (т. е. представляющим функциональные равенства) предикатным символам. В самом деле, имеет место некоторая общая представимость ') функциона.гьных знаков посредством предикатных символов, которую можно очень легко уяснить с помощью теоремы об устранимости г-сиыволов. Соответствующее рассуждение достаточно провести для какого-нибудь типичного примера. Пусть нам дан формализм (Е, получающийся из исчисления предикатов путем добавления к нему аксиом равенства, тех или иных собственных аксиом вместе с встречающимися в них символами, а также, быть может, аксиомы индукции или, соответственно, равносильной ей схемы индукции.