Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 17
Текст из файла (страница 17)
Аксиомы равенства а=Ь-~-((а)* ((Ь), соответствующие различным аргументам всех вновь вводимых функциональных знаков (если они не я ляютс димымн уже сами по себе). вляются выво- 3 а м е ч а н и е. Рекурсивные равенства для сложения и умножения, фигурирующие среди аксиом системы (Г), можно специально и ие вводить, так как они включаются в п.
6, а аксиомы а'чь О а'=Ь'- а=Ь о помощью схемы примитивной рекурсии могут быть выведены из формулы О'чьО, как было показано ране А). Дл ее нахож ения и Д я описанного таким образом формализма мы имеем спос об д я истинностных значений его постоянных формул. этот способ состоит в последовательном вычислении истин иностных знаформул по значениям их составных частей и он слагается из: а) истолкования связок исчисления высказываний как истинностных функций; б) распределения истинностных значений для равенств между цифрами; при этом равенство такого рода считается истинным, если обе его части одинаковы, и ложным если о они различны; в) процедуры вычисления значений функциональных знаков с аргументами в виде цифр, связанной с введением этих знаков по схемам, упомянутым в п.
5. описан С учетом этого распределения истннностных значений о анного нами формализма оказываются верными (ввиду спра, для Ведливости нп-теоремы) следующие утверждения: 1. Всякая выводимая постоянная формула этого формализма является истинной. Отсюда, в частности, следует, что формула О'=О невыводима и что не могут оказаться одновременно выводимыми какие-либо две формулы т1 н ) 8(. г) См. т. 1, гл.
Н11, с. 368 — 369. 2. Всякая выводимая формула, не содержащая ни формульных переменных, ии связанных индивидных переменных, является верифицируемой. 3. Если выводима какая-либо формула вида Зй," Зй.й((8„", 8.), не содержащая никаких переменных, кроме х,, ..., Яи, то по ее выводу могут быть найдены такие цифры 1, ..., 1„, что будет истинной формула 8((1Ы "° > 1и) 4. Если выводима какая-либо формула вида 1Уит 1(йтиВРд ''' -)РАВ(йн '''~ $т' Ри '~ Ри)~ не содержащая никаких переменных, кроме указанных явно, то для любой системы цифр т, ..., т можно указать такие цифры йм ..., 8и, что будет истинной формула 8( (тт тм зп ° зи) Если мы примем во внимание, что во всех утверждениях 1 — 4 речь идет о выводимости формул без формульных переменных, то у нас получится еще один результат, касающийся сферы действия этих утверждений.
В самом деле, замену общей аксиомы равенства ()и) соответствующими специальными аксиомами при переходе от системы (Е) к системе (2') мы с самого начала произвели с учетом того, что при исследовании вопроса о непротиворечивости эта замена не накладывает на результат никаких ограничений, так как по отношению к выводимости формул без формульных переменных общие аксиомы равенства равносильны этим специальным. В связи с вопросом о том, будет ли эта равносильность оставаться в силе в случае расширенного формализма, мы, прежде всего, заметим, что специальные аксиомы равенства для функциональных знаков, добавившихся из-за включения соответствующих схем по п.
5, включены в наш формализм по п. 6. Что же касается логической части формализма, то мы должны принять во внимание, что доказанная в гл. НП т. 1 теорема о равнозначности общей аксиомы равенства соответствующим специальным аксиомам' ) справедлива для теорий, формализованных с помощью исчисления предикатов, в то время как в нашем формализме содержится еще и е-символ с относящейся к нему е-формулой. Для таких формализмов соответствующая теорема о равносильности не только не доказана, но и вообще, как это можно ') См.
т. 1, с. 458. 88 исслндовлнин лоифмнтики пги помощи е.символа 1гл. и 4 21 включнник аксиомы пп в пнввню е.тковкмн 83 показатьа), не имеет места. Но в гл. Ч1Н т. 1 было показано, что при добавлении мправила общая аксиома равенства продолжает оставаться равносильной специальным аксиомам'); а сдругой стороны, как уже упоминалось, прн использовании е-формулы е-правило является производным и, значит, содержится в рассматриваемом формализме. Таким образом, утверждения 1 — 4 сохранятся, если мы изменим ограничения на наш формализм, условившись, что он содержит: 1) исчисление предикатов; 2) (-правило; 3) символы =., 0 и штрих-символ, а также аксиомы а а, а = Ь -)- (А (а) -)- А (Ь)), 0'~О; 4) схему индукции рекурсивной арифметики (как прежде); б) схемы для введения функциональных знаков (как прежде). Следует еще раз подчеркнуть, что в данной ситуации добавление мправила не опирается на приведенное в гл.
ЧИ1 т. 1 доказательство устранимости е-правила. Мы используем здесь лишь возможность замены общей аксиомы равенства (Хз) (или соответственно обшей схемы для равенства), а также сводимость е-правила к в-формуле. Известным недостатком нашего подхода может показаться то обстоятельство, что общая аксиома равенства (Лз) вновь вовлекается нами в рассмотрение окольным путем, в то время как первая е-теорема пока что доказана без учета этой аксиомы. В этом заключается также и причина того, что в последней версии нашего результата а-формализм пришлось сократить до ь-формализма. Но на самом деле имеется возможность доказать первую е-теорему — а также и ее обобщение — с включением аксиомы ()а), в чем мы вскоре убедимся. й 2.
Распространение первой в-теоремы на общую аксиому равенства а) Подготовительные соображения; основной тип; формулы в-равенства. Напомним формулировку первой е-теоремы а). В ней речь идет о произвольном формализме Р, получающемся из фор- з) Н дальнейшем доказательство этого факта мы еще приведем. См. ври~ мечанне на с, 87 — 88, з) См. т. 1, Добавление, с. 547. э) См. с. 36. мализма исчисления предикатов в результате добавления к нему в качестве символов каких-либо индивидных, функциональных и предикатных символов, а также е-символа, а в качестве исходных формул — е-формулы и каких-либо собственных аксиом $, ..., 5)1, не содержащих связанных переменных. Утверждение этой е-тео- ремы гласит, что из любого осуществляемого средствами форма- лизма Р вывода формулы (2, не содержащей связанных перемен- ных, использование связанных переменных может быть полностью исключено.
Впоследствии ') мы обобщили эту теорему до утверждения о том, что по любому осуществляемому средствами формализма Р выводу какой-либо формулы ц вида Врз ":-(р,й(5, ".~ 5,)> не содержащей никаких связанных переменных, кроме 5,, ..., 5„ можно получить осуществляемый без использования связанных переменных вывод некоторой формулы 6з вида )й(1((), ..., 1(")17...175((1(е), ..., 1(е)), где 1(1), ..., 1(0 (1=1, ..., 8) суть какие-либо термы, построен- ные из свободных переменных, индивидных символов и функцио- нальных знаков. Теперь мы должны доказать зти теоремы и для того случая, когда рассматриваемый формализм Р содержит общие аксиомы равенства () ) а=а я () з) а=Ь-)-(А (а)-е.
А (Ь)), вторая из которых не является собственной. Для доказательства мы снова воспользуемся рассуждением, с помощью которого в гл. Ч11 т. 1 в применении к рассмотренному там формализму мы показали '), что в выводе любой формулы, не содержащей формульных переменных, аксиома (Ле) может быть заменена рядом собственных аксиом. Из этого рассуждения получается, что для любой бескванторной формулы 6 (а), элементарные подформулы которой строятся из индивидных переменных, а также индивидных, функциональных и предикатных символов, вывод формулы а = Ь -~ (81 (а) -е л (Ь)) ())" Ф ))")у ц"" ~(Л,) ( ж з) См.
с. 54. е) См. т. 1, с. 456 — 458. 84 исслвдоВАние Апиометики пги пОМощи в-симВолА 1гл и ВКЛЮЧЕНИЕ АКСИОМЪ1 ПЛ1 В ПЕРВУЮ в-ТЕОРЕМУ 86 ных аксиом можно получить без испопьзования кванторов, а значит, в рамках элементарного исчисления со свободными пере-' менными. Однако сказанное нельзя немедленно применить к рассматриваемому здесь формализму Г, поскольку в этом формализме присутствует е-символ. Чтобы уяснить себе, какую модификацию нашего утверждения придется произвести нз-за появления е-термов, мы проведем сейчас некоторое вспомогательное рассмотрение, касающееся структуры е-термов. В этом рассмотрении речь будет, идти только о термах, не содержащих формульнвех переменных, причем иногда это обстоятельство мы не будем оговаривать явно.
Как правило, е-терм содержит в качестве составных частей другие термы. Составную часть з-терма е, которая является термом, но не находится внутри какого-нибудь другого терма, являющегося составной частью е, мы будем называть п р я м ы м п о д-, з е рмом е-терма е*). Пусть е — какой-либо е-терм, у которого число всех прямых подтермов (рассматриваемых с учетом не голы!о их вида, ио и расположения в е) равно(. Тогда основным типам') е-терма е с аргументными переменными В,, ..., и! Мы будем называть терм, который получается из е, если вместо прямых подтермов этого терма подставить в порядке их очередности слева направо свободные переменные пп ..., Ве. Основным типом е-терма е, не со-, держащего в качестве составных частей никаких других термов, будет считаться сам этот терм е.
Из сказанного ясно, что основной тип данного е-терма определяется однозначно с точностью до обозначений аргументных переменных, причем степень основного типа всегда равна единице, так как в нем не содержится никаких вложенных в него е-термов. С другой стороны, основной тип е-терма е имеет тот же. самый ранг, что и е, так как в том случае, когда он не совпа- ' дает с е, он получается из е путем замены определенных термов, фигурирующих в качестве составных частей терма е, некоторыми, другими термами ').
Среди прочих в-термов основные типы могут быть охарактеризованы как такие е-термы, у которых в качестве составных частей нет никаких других термов„кроме свободных индивидиых переменных, и в которых ни одна свободная переменная не встре- ') Здесь полезно обратить внимание читателя нв то, что прямые подтермы в-тсрмз могут не быть в-термами. — Прим. Лед.
'1 Понятие основного типа в-тсрмв восходит и одному аналогичному понятию, введенному Дж. фон Неймзном в работе: Ы е и т и пп 2. ч. 2нг Н!1Ьехы всЬеп Веже!з!Ьеог!е.— Майн 2., 1927, 26. 3. 28. ь) Иногда, отвленвясь от обозначений аргументных переменных, мы будем говорить об основном тине двиного в-тврмз, имея в виду какой-кабйдь вго основной тнп. чается дважды. Лва отличных друг от друга в-терма имеют одинаковые основные типы тогда и только тогда, когда один из этих термов получается из другого в результате замены некоторых термов, фигурирующих в ием в качестве составных частей, какими-либо другими термами. Процесс построения основных типов в-термов мы поясним на следующем примере.
Основным типом е-герма в„(е,(с+2=в,(у+1(г)) =е„(в,(г+е„(и=г)(г) (убеу „-х)) с аргументными переменными а и Ь является е-терм е„(а = е„(Ь (уй! у( х)). Из двух вложенных в исходный терм е-термов е„(с+2=в,(у+1(г)) и е, (г+ в„(и = г) ( г') первый в качестве основного типа имеет е терм ел (а = е, (у+ Ь(г)) с аргументными переменными а и Ь, а второй сам является своим собственным основным типом. Если с помощью явных определений мы введем какие-либо сокращающие символы для основных типов всех з-термов заданной формулы, а именно, иидивидные символы для основных типов без аргументов и функциональные знаки с аргументами и„..., пе для основных типов с этими аргументами, то с использованием этих символов каждый входящий в данную формулу е-терм изобразится как некоторое выражение, построенное из свободных переменных, индивидных символов и функциональных знаков.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
