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

Аналогичным образом, исходя из формулы Чх'ЗуЗЕЧЕЭЛРй(х, у, г, и, и, а, Ь), в которой не встречаются никакие переменные, кроме указанных, символьное Решение экзистенциАльных ФОРМУЛ 25 мы получим формулу 6(с, ((а, Ь, с), й(а, Ь, с), с(, () (а, Ь, с, р(), а. Ь). й и Ь вЂ” отличные друг от друга, ранее не встречавшиеся функциональные знаки, причем 1 и 3 зависят от трех аргумен- тов, а 1) — от четырех. Этот способ перехода от предваренных формул к формулам без связанных переменных мы можем применить, в частности, к формулам, составляющим некоторую систему аксиом, если эти аксиомы являются собственными аксиомами ').

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

1. Сг(а, а, Ь). 2. Сг(а, Ь, с)- Сг(Ь, а, с) ЬСг(а, с, Ь), 3. Сг (а, Ь, с) ср Сг (а, Ь, с() й ачь Ь-р-Сг (а, с, с(). 4. )Сг(а, (), Т). П. !. Хв(а, Ь, с)-р Сг(а, Ь, с). 2, ) Хв (а, Ь, Ь). 3. Хв(а, Ь, с) — Ев(а, с, Ь)й 12в(Ь, а, е). 4, ачьЬ Хв(а, Ь, Чр(а, Ь)). 5. ) Сг (а, Ь, с) 1)р 7в (р, а, Ь) Ер ) Сг (р), а, Ь) ср )Сг (с, р, р)) -~ Сг(р, у, ф(а, Ь, с, р, д)) Ер (Ъч(ф(а, Ь, с, р, р)), а, с))/Ев(ф(а, Ь, с, р, д), Ь, с). Такую систему, состоящую из собственных аксиом, в которых все кванторы существования устранены в результате применения операции символьного решения, а все входящие в них перемен- ные являются свободными индивидными, мы будем называть систе- мой аксиом в р а з р е ш е н н о м в и де. По любой системе собственных аксиом (3) со связанными переменными с помощью операций символьного решения и замены связанных переменных свободными мы можем построить соответ- ствующую ей систему (3') в разрешенном виде.

При этом фори рар рррр рр«р. » с, р,, р, „, ~,„„,, 1., аз ') См т. 1, с. !82 а далее. Р) С . т. 1, с, 2В. 26 ИСКЛЮЧЕНИЕ СВЯЗАННЫХ ПЕРЕМЕННЫХ 1ГЛ. 1 27 ГИЛЬБЕРТОВ е-СИМВОЛ И е.ФОРМУЛА дикатов из формул системы (В'). Отсюда, в частности, вытекает, что если будет доказана непрсвиворечивость системы (5'), то в1ем самым будет устиновлена и непротиворечивость сисгпемы (В). Кроме того, мы убедились, что если при переходе от (В) к (5') вводязся одни лишь ипдивидные символы, то системы ($) и (5') в некотором смысле равнозначны, а именно: каждая принадлежащая формализму системы (5) формула, выводимая средствами системы (5'), будет выводима и средствами ($). Отсюда, в частности, следует, что в этом случае непротиворечивость (5) совпадает с непротиворечивосзью (Б').

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

Этот вопрос имеет большое значение для изучения различных проблем, связанных с непротиворечивостью. Дейс1вительно, для установления непротиворечивости того или иного формализма, включающего в себя обычное исчисление высказываний, достаточно, как мы знаем, установить нсвыводимость какой-нибудь конкретной формулы. Ввиду этого обстоятельства непротиворечивость тех формализмов, которые включают в себя символ О и первую аксиому равенства, мы могли бы охарактеризовать как невыводимость в них формулы О ~ О.

В случае произвольного формализма вместо формулы О Ф О мы можем взять какую-нибудь формулу вида 21 4 ') 2(, причем в качестве 21 мы можем выбрать формулу без свободных переменных. Тем самым исследование непротиворечивости какого-либо формализма сводится к выяснению вопроса о том, является ли выводимой конкрезцая фогмула без связанных переменных. Допустим теперь, что нам удалось показать, что вывод любой выводимой формулы без связанных переменных из системы аксиом в разрешенном виде может быть осуществлен без использования связанных переменных. Тогда исследование непротиворечивости такой системы аксиом упростится коренным образом.

Действительно, вместо формализма, состоящего из этой системы аксиом, взятой в сочетании с исчислением предикатов, у нас появится гораздо более ограниченный формализм, состоящий из объединения этой системы аксиом о элементарным исчислением со свободными переменными '), х) См. т. 1, с. 660 алн 11рнложенне 1, с. 462. Весьма удобным средством для рассмотрения этих вопросов оказывается гильбертов е-символ, к введению которого мы теперь и перейдем. 6 2. Гильбертов е-символ и е-формула К гильбертову е-символу и к характеризующей этот символ формуле нас приводит рассмотрение уже упоминавшейся выше операции символьного решения экзистенциальных формул. Введение какого-либо функционального знака 1(а, ..., й) в результате символьного решения некоторой экзистенциальной формулы Лхй((а, ..., й, х) отличается от введения подобного функционального знака иа основе ь-правила лишь тем, что в первом случае опускается условие выводимости формулы чх17у (21(а, ..., в, х) й й (а, ..., й, у) -ьх = у).

Поэтому сама собой напрашивается мысль реализовать символьное решение в общем виде посредством такой модификации оправила, которая получится, если мы опустим в нем играющую роль посылки вторую формулу единственности. Если мы для четкого различения случаев возьмем вместо буквы ь букву ть то это модифицированное оправило будет выглядеть следующим образом: если формула ЭВ21 (н) либо выведена, либо является аксиомой, то выражение Ч„21(в) может быть введено в качестве терма, а формула 2( (т) „2( (н)) может быль взята в качестве исходной. При этом по аналогии с записью результирующей формулы схемы для осимвола в записи 21(з)ее((н)) подразумевается, что во внутреннем выражении 21(в) в целях избежания коллизий между связанными переменными нам, может быть, придется переименовать некоторое количество связанных переменных').

Замечание. Это Ч-правило по сравнению с рассмотренным выше методом символьного решения обладает двумя особенностями. Во-первых, оно распространяется и на тот случай, когда в формуле Знг((н) имеются формульные переменные. Во-втоРых, благодаря записи Ч„у((ч) здесь соотнесение вводимого сим- ') Сн.

отыосннхнесн к этому кругу вопросов замечания к ьправнлу в т. 1, 460-470, а также изложение ьнравала в Прнложеннн 1, с. 464.— Нам не сгонт рассматривать формалнзм Ч-сннвола более подробно, так как Ч.снмвол будет служить лишь длв перехода к е-снмволу. 29 ИСКЛЮЧЕНИЕ СВЯЗАННЫХ ПЕРЕМЕННЫХ 1гл. 1 ГИЛЬВЕРтОВ е-СИМВОЛ И е-ООРМРЛА вола самой формуле Л( ) становится явным, откуда, в частности, следует согласованность между функциями, возникающими в результате подстановок из разных введенных по отдельности я-символов. Пусть, например, Я(а, Ь, с) — формула, для которой можно вывести обе формулы ЗхЯ (О, Ь, х) и ЗхЯ(а, 1, х), хотя, может быть, и нельзя вывести формулу ЗхЯ(а, Ь, х). Тогда с помощью тгправила мы можем ввести символы чЯ(0, Ь, х) т1,Л(а, 1, х).

Если в первом из них мы подставим 1 вместо Ь, а во втором 0 вместо а, то в обоих случаях у нас получится т),;Я(0, 1, х). Если же вместо Ч„Я(0, Ь, х) ввести функциональный знак 1(Ь) и формулу Я(0, Ь, ((Ь)), а вместо т)„Я(а, 1, х) — функциональный знак 9(а) и формулу Я(а, 1, й(а)), то вместо одного выражения т) Л(0, 1, х) мы получим два различных выражения 1(1) и 9(0), причем может оказаться, что не удастся вывести равенство ((1) =9(О). В самом деле, формула в(хУу(Я(0, 1, х) б(91(0, 1, д)-»х=у) не обязана быть выводимой, хотя обе формулы Я(0, 1, 1(1)) и Я (О, 1, )1(0)) и имеются в нашем распоряжении.

В формулировке ))-правила требуется, чтобы образование терма чеЯ (о), подобно образованию герма тьй (о), связывалось с выполнением еще одного условия, касающегося выводимости некоторой формулы, а именно — формулы ЗРЯ(о). От этого ограничения можно б дет освободиться следующим образом. Из выводимой формулы ) ЗуА (у) ~l ЗхА (х) преобразованиями исчисления предикатов мы получим формулу Зх (ЗуА (д) -» А (х)). Опираясь иа выводимость этой формулы, мы можем, в соответствии с т1-правилом, ввести терм т), (:-1уА (у) -). А (х)) и взять формулу Зд А (у) — А (т)„(ЗдА (у) — А (х))) в качестве исходной.

Теперь мы явно определим символ е„А (х) посредством равенства а„А (х) = т)„(ЗуА (у) -» А (х)). Тогда из предыдущей формулы в результате переименования стоящей в посылке импликации переменной у в х получится формула ЗхА (х) — » А (е, А (х)). (о) Благодаря этой формуле, в которой связанную переменную х как в посылке, так и в заключении мы можем переименовать в любую другую, всякое дальнейшее использование ггсимвола становится излишним. Действительно, в случае выводимости какой-нибудь формулы ЗЕЛ (в) мы, используя формулу (о), о помощью подстановки') и схемы заключения получим формулу Я (е,Я (о)).

Поэтому напрашивается идея полностью исключить Ч-правило и вместо него в формализм ввести в качестве основного знака символ е,А (о) в сочетании с формулой (ве) ЗхА (х) -» А (е А (х)). Эта формула, если отвлечься от обозначения вводимого символа, совпадает с формулой (р,) для символа р„А(х)').