Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 104
Текст из файла (страница 104)
31), здесь между свявяяяымв оервцв 480 приложение !и В качестве исходных формул в выводах допускаются: !. Рекурсивные равенства, построенные по схеме примитивной рекурсии, и, значит, в частности, рекурсивные равенства для сложения и умножения, а также рекурсивные равенства для функций зйп(п) и ваап(а): зип(0) =О, зйп(а') =0', здп (0) = О', зйп (п') = О. 2.
Явные определения вида ((п„..., а„)=1(а„..., пг), где ! — некоторый г-местный (ранее не использовавшийся) функциональный знак, а 1(п„..., п,) — терм с единственными свободными переменными а„..., и. 3. Формулы вида )ь,(1(х), а) =здп(1(а)) Рх(1(х), а')+зап(1(а)) а и рх1(х) = р„(1(х), 0), где 1(а) — какой-либо рекурсивный терм !схема формул (й)) Разрешаются следующие способы перехода от уже имеющихся формул к новым: 1. Подстановка какого-либо терма вместо всех вхождвний данной свободной инднвидиой переменной в данную формулу. 2. Схема замены п=в, Я(п) Я (5) где Я(п) означает формулу, получающуюся из выражения Я(у) в результате замены буквы (именной переменной) у термом о, а Я (В) получается из Я (у) в результате замены у термам о. 3 а м е ч а н и е.
Эту именную переменную мы не причисляем к свободным индивидным переменным, которые у нас считаются термами. Она используется лишь для описания схемы замены. Описанный нами формализм (2з) не содержит ии логических символов, ни формульных переменных. В качестве единственной не формулируется. Это ограниченые в рвссмлтривземом формализме онззывзется нз самом деле ненужным, тян езн не разрешается в качестве операции построения термоз применять й-еимвол н какому-либо терму, в котором уже содержигся некоторый й-символ, и поззому терм вида й„! (х, Кх! (х, х)) может возникнуть лишь в результате замены изной-нибудь индивидиой переменной термом !г,)(х, х).
Это обстоятельство позволяет нзм обходиться здесь перемен. ной х в качестве единственной связанной переменной. зь 48! р и РЕГУ ГУЛЯРНО ВЫЧИСЛИМЫЕ ФУНКЦИИ. ФОРМАЛИЗМ ! ) связанной пер м еременной в нем фигурирует относящаяся к р-символу пе емеииая х. Схема замены, примененная к формуле а+О =а (при зто м качестве Я (у) берется выражение у= а), дает нам формулу й формулы и схемы замены от равенства а= а. С помощью этои О м п=й можно переити к р к равенству В= о. В сочетании с этим перео ом схема замены позволяет для любой рекурсивной функции й авенств, представляющих собой рекурсивное опр де,„у п е еление ф нкЧтобы прокомментировать схему формул (р), м с помощью втой схемы для любого рекурсивного терма 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(х), п)=1.
Таким образом, для любого рекурсивного терма 1(а) на основе ) " (1(х) и) формально представляет некоторую т а значение которой для любого числа и, д ля кото- 1)п и 1(!)=О, равно рого может быть указано ! такое, что . и наименьшему среди чисел зтого род, а а в том случае, когда для всех ! ==:п значение терма 1(1) отлично от О, значения зто функ, ббл ших цли равных и, определены лишь с точностью до совпадения '). иссе тенин: К ! ее не В, С, А !Ьеогу о! розн!че 3 Мз!Ь )933 57 № ! 9 показал что т явное определение в поет~~мне лшбзя функция такого родо допускает явное п А.
Черчем фо р из ли зме енонверсийэ. !6 д. Гяльоерп П, Вервзве 482 ПРИЛОЖЕНИЯ й и Регтляпно вычислимые етнкции. мопмализм 1г»1 ЛЯЗ Схема (ь 1(л) = )ь (1 (х), 0) представляет собой явное определение символа " 1(х). Е какой-либо рекурсивный те м, л а ерм, для которого может быть указана цифра ц такая, что имеет место равенство 1(п) = О, и е является наименьшей с еди циф (и) =, и если 1 ию после указания цифры ц она может быть най е вычисления термов 1(0), 1(0'), ..., 1 и — ! то и р щ в ого в сочетании со схемои м ВыВести раВенство )ь 1(х) =1. В том случае, когда значение терма 1(а) отлично от 0 для позволяют о маль всех цифр п, определяющее равенство ля ( о для (1,1(л) и схема ()ь) не формально вычислить значение терма р 1( ) ').
Что же касается тиво ечиво ется вопроса о непротиворечивост (Хе), р сть в смысле невозможности однов е и ( ), то неп о- какой-ниб дь фо м лы и е у ф р улы и ее отрицания имеет место тривиальным образом, так как этот формализм вообще не соде жит от и от ассмат ечивости еще не вытекает — в отличие р м ривавшихся до сих пор арифметических фо что каждое выводимое н их формализмов,— нумерическое равенство является в равенством н что, следовательно б верным ство между двумя различными циф ами.
Это , не может ыть выведено ав равен- азывать й В е форма Еэ ческо непротиво е лнзм ( ) удовлетворяет этому условию. В этом мы сможем убедиться, рассмотрев некоторый фо мализм к ней )ь-символа и относящих я ной ари мегики путем добав хся к нему формул') ут лепна (р') А (а) -ь А (Р„А (л)), (ь) А (а) -ь (ь„А (л) ( а, (р~) ) А (рлА (л)) — ь р А (л) = 0 с соблюдением следующих соглашений. ') С ледовательяо, в этом отношении имеется с ест вынется ущ~~м~ю~ Рымчн ежду ренном гл У д нного том Фо „..„..,2) Ф...,..7.„,..0.' л ' - н-м.-у--- ) ) помощью ~ыю~~ (р,) можщ быть р (1(л) = О) ') Обозначения этих формул выб аны в с приведенными на с. 164.
вы раны в соответствии с обозначениями, Если т((с) — формула, не содержащая связанной переменной г, то выражение )ь Я(х) считается термом. Относящаяся к какому- либо )ь-символу (ь,й(й) связанная переменная р может быть переименована в какую-нибудь другую; при этом переименование должно производиться во всей области действия рассматриваемого р-символа. Подстановки вместо свободных переменных, как и переименования связанных, должны производиться таким образом, чтобы в результате их выполнения нн один р-символ не попадал в область действия другого, снабженного той же самой связанной переменной (условие недопущения коллизий между связанными переменными).
Употребление формул ((ь',), ((ьа) и (р,') в качестве исходных формул выводов должно подчиняться таму условию, что ни в одной из формул, которые при возвратном переносе подстановок в исходные формулы будут подставляться в формулы ()ь',), (ц,) и (р;) вместо именной формы А(с), переменная с не должна находиться в области действия какого-либо из (ь-символов 1). 3 а меч а н не. С учетом только что наложенного условия, в формализме (Хх) — так же, как это было сделано при описании формализма (Хе),— можно было бы сэкономить правило недопущения коллизий между связанными переменными, так что мы и здесь могли бы обойтись одной-единственной связанной переменной х. Однако мы этого не делаем, так как хотим, чтобы формализм (Р) представлял собой подфорж лизм рассмотренного в гл.
У формализма (ХР), чем, в частности, мы достигаем того, что всякая выводимость, установленная в формализме (ет), автоматически будет иметь место и в (Х ). Непротиворечивость же формализма (Хт) — а тем самым и его нумерическая непротиворечивость — вытекает из рассуждений, проведенных нами в конце гл. 11'). С другой стороны, мы можем показать, что каждое числовое равенство, выводимое в (хе), выводимо также и в (ет). ') Условие это нацелено на то, чтобы прн замене формул К), (р,) н (р() соответствующими схемами формул в ходе применения зтнх схем р-снмволов не возникало ннкакнх подчинений вида рак (р16(т, 1)) нлн ргк(рггв (г.
0 1). ') См. с. 163-168. По сравнению с формализмом, непротнворечнвосп, которого была там установлена, формалнзм (Е') существенно более узок, так как, во-первых, в нем отсутствуют кванторы, а во.вторых, ограничительное условие, которое в формализме, рассмотренном в гл. П, было наложено на применения формулы (рэ), в (с») распространяется также н на применения Формул (р,) в (р,) Ввиду этой особенности формализма (Х') процедуру построення общнх взамен н получення резольвенты прн установлении его непротиворечивости необходнмо применять лншь в случае, когда все крнтнческне формулы (в том числе н Формулы в-равенства) имеют ранг 1, так что процедурой функцнональных замен здесь можно н не пользоваться, ограннчнвшнсь одними лишь цифровыми ааменамн 16» пгиложенив 484 4 П ЕЕГГЛЯЕНО ВЫЧИСЛИМЫЕ ФГНКЦИИ.
ЭОЕМЛЛИЗМ сгп 488 Н1 а~Ь81А(Ь) А(р (А(х), а)), а ~ Ь 81 А (Ь) -~ а ~ р (А (х), а), а(Ь81А(Ь) р (А(х), а)~ р (А (х), а) ~ 0-э А (р (А (х), а)), р„(А(х), а) ФО-~а(р (А (х), а), (2) а затем с помощью формул а(а, а(Ь81Ь(а- а=Ь, аФ08са~Ь-~Ь~О, а(Ь8са~Ь-~а'(Ь, а'(Ь-+ а(Ь, а'(Ь-~Ь~О, аксиомы равенства (Ю,) и средств исчисления высказыва ий— ни ( 3) А (а) -~ р„(А (х), а) = а, 1 А (а) -~ р„(А (х), а) = р„(А (х), а'), дизъюнкцией причем для вывода второй из этих формул нужно о о воспользоваться р„(А(х), а)=0~/р,(А(х), а)ФО. Если мы теперь добавим еще определяющую схему р (1(х), и)=р,»(1(х) О, и), применение которой ограничим рекурсивными термами 1(а), то р ы (с) входящей в (3) о- подставив в (3) вместо именной формы А (с) мульной переменной какую-либо рекурсивй ф ( ую формулу 1(с)=0, Действительно к роме тех дедуктивных средств, которые содержатся непосредственно в (21), формализм (Е') содержит только явные определения функциональных знаков, явное определение функции р„1(х), схему замены и схему (р).
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
