Гильберт, Бернайс - Основания математики. Теория доказательств (Гильберт Д. - Основания математики и прочие работы), страница 9

а ) 6 (1В), дОЕАВАтелъство пеРВой е.теоРемы 43 то получим доказательство формулы ц, в котором ии одна критическая формула ие фигурирует в качестве исходной. Но из ~~ого доказательства по дедукционной теореме мы можем получить вывод формулы ~ Л (1г) ~г ° ° ° 'г ) Л(1В) «~- ° в котором формула )6(1,)й...з )11(1а) уже не используется в качестве исходной, так что в этом выводе, кроме средств элементарного исчисления со свободными перемен- ными, используются только аксиомы»4)„..., г))1. Теперь формула ) 6 (1~) Ег...зг ) 6(1„)-«6, которая может быть преобразована в )(6(1т) Ч" Ч6(1,)) вместе с полученной перед этим формулзй 6(1,) ~/...

~/6(1,)-~-~ А) Сгь е. 1, ч. 472» позволяет нам получить средствами исчисления высказываний формулу ц. Таким образом, в итоге мы получаем вывод формулы ц без использования формул (К) в качестве исходных и без добавления каких бы то ни было новых исходных формул. Значит, действительно, из нашего нормированного доказательства формулы 6 удается устранить применение всех упомянутых критических формул в качестве исходных. в) Типы комбинирования е-символов; степень и ранг е-терма.

Теперь речь пойдет о том, чтобы описанный нами метод, который в рассмотренном частном случае ведет к устранению всех критических формул, распространить и на общий случай. С этой целью мы более детально остановимся на вопросе о возможных способах комбинирования е-символов. Способы, с помощью которых образуются эти символы, совершенно аналогичны способам, которые применялись при комбинировании г-символов, и для их характеризации мы снова будем пользоваться понятиями вложения и подчинения' ).

Мы будем говорить, что один е-терм вложен в другой, если он является составной частью последнего. Что же касается отношения подчинения, то оно, вообще говоря, будет касаться е-выражений, т. е. Вйражений, либо являющихся е-термамн, либо получающихся из В-термов в результате превращения их свободных индивидных 45 ИСКЛЮЧЕНИЕ СВЯЗАННЫХ ПЕРЕМЕННЫХ игл 44 переменных в связанные пе МЫ ) переменные, не входившие в эти терМы б удем говорить, что одно В-вы ажение ~ другому е-выражению е 6 (Р), сражение 1 подчинено нию е„(Р), если оно является составной частью этого выражения и содержит перемени ю В; в будем также говорить, енную В; в этом случае мы ражение а.

ть, что выражение е 6(в) подч ни я е ет выЗа, мечание. В соответствии с ан ражение а, я данными определениями е-выа, являющееся составной частью е-те не быть вложенным в 1 или е-герма ц может и П ст, в или подчиненным этому терму. усть, например, 1 — терм вида е~й(Е, В 6(Е, Р, е гг(1й 1))) Тогда е-выражение ей(Р, 1) не в („,) не вложено в терм 1, так как оно ие является термом; но оно также и не анже не подчинено терму ~, так Некоторые примеры комбина~ и" чинения мы п аций отношений включения и под- торов всеобщности и я мы получаем, в частности, п оизво я сти и существования. р вводя устранение кван- Рассмотрим, наприме ст а р, у ранение кванторов существования ЭЕ=-й)й (Е;), и Зр.

не содержащего никаких других кванторов, кроме указанных ЛЕ Прежде всего здесь следует заменит 31й(, ) ь у (Е, р) выражением й (Е, е й (Е, Р)). Если мы сок а р щенно обозначим это выражение че ез 3 'ЗЕ=Ьй(Е, Р) надо будет заменить на Э 6( . В на Е,Е). Место того выра 6 (е,й (Е)), причем в связи с подстановкой е 6 ( ) в З ( ) в в ( ) во избежание коли между связанными переменными в по нии должна б и в подставляемом выражеыть переименована связанная пе е мы получим выражение ременная 1д Так й(е й(Е, е й(Е, 1)), В й(е й(Е, е й(Е, 1)), 1))), т.

е. выражение вида й(а, е), и ) величие между е-термами и е.выражеиивми Вежд е-термами Рвыр жеииими См т 1 4 31 ЛОКАЗАТЕЛЬСТВО ПЕРВОИ а-ТЕОРЕМЫ , й(Е В,й(, В), а Ь вЂ” выРажение ~в~(~* «). В частности, если й(а, б) представляет собой формулу, то а и е будут термами; при этом а вложен в (, в то время как и-выражение е,й(Е, 1), из которого е получается в результате замены переменной Е термом а с переименованием ~ в Э, подчинено терму Аналогичным образом можно убедиться, что в результате )сгранения с помощью з-символа кваиторов в выражениях ВЕ=й)11 (Е Э). ПЕ чуй (Е 9) ч Е~урй (Е Р) мы получим формулы вида й(а, е), где а и в — надлежащим образом выбранные е-выражения.

Совершенно аналогично можно также показать, что любая формула ЧЕ,ЛЕ,."ЗЕей(Е„", Е1), не содержащая никаких связанных переменных, кроме Е,, ..., Еы в результате устранения из нее с помощью и-символа кванторов существования перейдет в формулу вида й(ам ..., а~), где а,, ..., а~ — некоторые конкретные термы. Отношения включения и подчинения В-термов позволяют устроить некоторую классификацию этих термов по степеня м, с одной стороны, и по р а и г а м, с другой. Степень выперла 1 определяется следующим образом. Мы рассматриваем всевозможные последовательности В-термов, начинающиеся термом 1 и такие, что за каждым их термом, в который вложен хотя бы олин другой е-терм, следует один из вложенных в него е-термов.

Может существовать только ограниченное число таких последоватсльностей, и в каждой из них количество е-термов ограничено общим числом е-термов, входящих в 1 (считая и сам терм 1). Число термов в максимальной по длине из этих последовательностей мы будем называть степенью терма 1. Это определение степени, как легко убедиться, равносильно следующему рекурсивному определению. Любой е-терм, не содержащий ни одного вложенного в него е-терма, имеет степень, Равную 1. Данный е-терм имеет степень 1+1, если любой вложенный в него е-терм имеет степень, не превосходящую 1, и по крайней мере один вложенный в него е-терм имеет степень, Равную 1. Гогласно этому определению всякий е-терм имеет ббльшую степень, чем любой вложенный в него В-терм. 1гл.

т исключение сВязАнных пеРеменнтух Подобно тому, как отношение вложения ведет к понятию, степени для е-термов, отношение подчинения ведет к понятию ранга для е-выражений. Пусть 1 — и-выуажение, т'(ы рассмотрим последовательности е-выражений, начинающиеся выражением 1 и такие, что за каждым их е-выражением, подчиняющим себе хотя бы одно отличное от него е-выражение, следует одно из подчиненных ему е-выражений. Существует только ограниченное число таких последовательностей, и внутри каждой из них имеется только ограниченное число следующих друг за другом е-выражений. Число е-выражений в максимальной по длине из этих последовательностей мы будем называть рангом е-выражения 1. Определению ранга также можно придать рекурсивный характер. Какое-либо е-выражение мы будем называть е-выражением ранга 1, если ему не подчинено никакое е-выражение; мы будем говорить, что данное и-выражение имеет ранг 1+1, если всякое подчиненное ему и-выражение имеет ранг, не превосходящий 1, и если по меньшей мере одно подчиненное ему е-выражение имеет ранг, равный 1.

Прежде всего, из данного определения получается, что любое е-выражение имеет ранг, ббльший, чем любое подчиненное ему е-выражение, а также что любое е-выражение, получающееся из какого-либо е-герма в результате превращения одной или нескольких свободных переменных в связанные '), имеет тот же самый ранг, что и исходный е-терм, рассматриваемый как е-выражение. Очевидно, что на ранг данного е-выражения не оказывают никакого влияния ни входящие в него в качестве составных частей е-термы, ни подчиненные таким е-термам е-выражения; в самом деле, е-терм вообще не может быть подчинен никакому а-выражению, и если какой-нибудь е-терм является составной частью какого-либо е-выражения а, которому подчинено другое е-выражение 6, то либо этот е-терм фигурирует внутри а только в качестве составной части о, либо он лежит совершенно вне (т, так как он не может содержать никакой переменной, которая связывалась бы каким-нибудь стоящим вне его е-символом.

Таким образом, ранг е-выражения не изменится, если находящийся внутри него е-терм (в одном илн нескольких местах, где он встречается) заменить каким-нибудь другим е-термом. В качестве примера на вычисление степени, а также ранга рассмотрим построенный из арифметических символов е-терм е„[[е„(0' = е, (г < у")) = е„(х )|,и, [0<еа((е. (г<и') <„) а, )И ') Особо отметим, что речь идет о тех иа иих, которые ис входит в даииый в-тсрм (см.

с. 44). 4т докхздтельство ПВРВСИ *'твоРЕМ 4й м соде жит в качестве которы мы обозначим буквой 1. Этот тер Р Вложет ого е-герма только терм е„(0' е,(г<у)) мов ольше уже не который, со свое сто т роны, вложенных е-термов б ь 2. содержит; те с мым 1 имеет степень 1 подчинены е-выражения ерму е„(х<у) и е„((е,(г<и')<и)сси<х), вое больше не содержит никаки - р х е-вы ажеиий и из которых первое о емя как второе, которому под- тем самым имеет ранг 1, в то время как чинено е-выражение е,(г -и'), ранг 2 Тем самым 1 имеет Ранг 3 имеет ра В качестве еще одного примеРа возьмем е-терм е„[е „(х < е, (х < г)) < У1 о с ст анения с помощью е-симк которому нас приводит процесс у р вола кванторов существования из формулы Зх)у (х < у). е жит ни одного подчиненного ему е-выра- 1 В качестве ~ю~ынож жения и, значит, ранг его равен е-терма этот терм содержит е-терм е„(х < е,(х< г)).

же не содержит вложенных в него е-термов последни уже не и, значит, имеет степень 1, то весь рассматр степень 2. - е м может иметь меньший этом р~~ере м д, - м ви им, что е-терм м й е-те м, вложенный в него. ей Ругон е Р сматриваемый е-терм имеет ранг, а в х входящих в них кри тических мул. г) Устранение критических формул в Речь пойдет о том, чтобы гильбер о у р е товскую процедуру у л из но мированиых доказательств, «Рнтических формул из нор ом ' ~ы~<кщан~л~ на бщий сл чая, когда все критичес ~вязаны с одним и тем же е-термом, расп о ) Ом, и. 6), с.