Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 36
Текст из файла (страница 36)
А для входящих в нее критических формул и формул е-равенства мы можем построить резольвенту. Если извлекаемые из этой резольвенты эффективные замены мы внесем в упомянутое нормированное доказательство, а затем заменим все оставшиеся е-термы цифрой О. то исходные формулы, а тем самым и все остальные формулы этого нормированного доказательства перейдут в истинные формулы. Следовательно, и формула 6(1„..., 1„), получающаяся из заключительной формулы 6 (е,, ..., е„) в результате внесения цифровых замен 1,, ..., ), вместо е-термов е,, ..., е„ является истинной формулой. Таким образом, для каждой формулы ЛГ " ° =(В«Л (Г, " ° Г,), обладающей указанными свойствами, мы можем найти такие цифры 1,, ..., 1„для которых формула Л(1,, ..., 1„) является истинной. Тем самым для рассматриваемого формализма выполняются все утверждения нашей нп-теоремы.
Этот метод доказательства ип-теоремы сохраняет силу и при некоторых расширениях рассмотренного арифметического формализма. Так, во-первых, можно, не меняя доказательства, расширить наш формализм путем добавления функциональных знаков, для которых задан способ вычисления их значений для цифровых значений их аргументов, а также путем добавления собственных аксиом без связанных переменных при условии, что эти аксиомы являются верифицируемыми.
Так снова получается непротиворечивость тех арифметических формализмов, которые мы рассматривали в 9 ! этой главы»). Рассмотренное доказательство сохранит свою силу и в том случае, если мы присоединим к нашему формализму р-символ и В См. с. 74 — В2. 6» 16з 1й(!)-~а И(х) (Е 164 нсслгдовднне АРифметнки пги помощи е-символд 1гл.ч1 формулы (рз) (р ) (р ) ()ьз) :-)хА(х)- А(р А(х)), (ре) А (а) — р„А (х) «=а, (рз) Чх ) А (х) -ь р, А (х) = О при условии, что в формулу (рз) вместо именной формы А (с) будут подставляться только такие формулы 'Л (с), у кото(ых переменная с не будет попадать в область действия какого-либо квантора или в-символа'). В самом деле, формула (ре) с помощью формулы Оьз) и средств исчисления предикатов может быть переведена в формулу (р') ! А (р„А (х)) -ь р,А (х) = О, а формула (р,) дедуктивно равна формуле (рз) А(а)-+ А (р А(х)), если пользоваться средствами исчисления предикатов.
Поэтому добавление формул (рх), (ре) и (ре) равносильно добавлению формул Оь,') (р,) и (р,'). А эти формулы можно без особого труда включить в процедуру построения резольвенты. Действительно, если каждое выражение р Й(») заменить выражением езЛ(»), то формула (р,') совпадет с е-формулой. Формулы (ря) и (р,') хоть и приведут (после исключения кванторов и свободных переменных) к крит и ч е с к и м ф о р м у л а м нового типа, а именно к формулам вида Я (!)-ье зЛ(х) (! и 1$(е 'Л(х))- е Л(х) =О, но эти формулы не требуют каких-либо новых способов их рассмотрения; действительно, формула )й(еяй(х))-э и е((х) =О переходит в истинную формулу в результате любой общей замены, при которой е-терм е Я (Л) или соответственно появляющийся вместо него (в результате подстановок вместо вложенных е-термов) а-терм получает О-замену или какую-нибудь экземплярную замену, а формула ') Этп ограничение должно распространяться и нв все те промежуточные подстановка в формулу (из,', которые 6удут производиться прн вовврвтнем переносе подствновок в исходные формулы.
ПЕРНОНАЧАЛЬНЫЙ ГИЛЬБЕРТОПСКИЙ ПОДХОД переходит в истинную формулу в результате любой общей замены, при которой е-терм е с( (х) или соответственно появляющийся вместо него е-терм получает О-замену или минимальную замену. Мы знаем '), что наша процедура построения резольвенты всегда приводит к цели, если минимальные замены требуются только для е-термов ранга !. Но в данном случае для выполнения этого условия достаточно, чтобы переменная с не попадала в область действия какого-либо квантора или ц-символа ни в одной из тех формул 'Л (с), которые при возвратном переносе подстановок в исходные формулы будут подставляться вместо именной формы А (с) формульной переменной в формуле (р,). Действительно„ нетрудно убедиться, что вследствие этого ограничения любая критическая формула, получающаяся из формулы (р,), будет иметь ранг !. Таким образом, при указанном ограничении на применение фоРмУлы (Ре) наши фоРмУлы ()ьз), (Р,) и (Р,) действительно могУт быть включены в доказательство нп-теоремы, которое получается применением метода резольвент.
Указанный метод может быть применен и к другим формализмам, отличным от формализма арифметики. На самом деле специфическая роль, которую в процедуре построения резольвенты играют цифры, проявляется лишь в связи с рассмотрением критических формул второго рода, а эти формулы появляются лишь в связи с формализацией принципа полной индукции. Если будут отсутствовать критические формулы второго рода,— а значит, и возникающие из-за них минимальные замены, — то в доказательстве можно будет заменять е-термы не цифрами, а какими-либо термами без переменных; в частности, роль цифры О при этом может быть отдана какому-нибудь специально выделенному для этой цели индивидному символу. Так с помощью метода резольвент мы убеждаемся, что нптеорема справедлива для любого формализма, состоящего из исчисления предикатов, е-формулы, общей аксиомы равенства и тех или иных собственных аксиом без связанных переменных, которые становятся верифицируемыми при каком-либо распределении истинностных значений для элементарных формул без переменных, причем для равенств без переменных это распределение должно представлять собой выделенную оценку для равенства').
Последнее условие может быть заменено другим, более слабым. 'г!менно его можно заменить условием, что любая элементарная формула без переменных сохраняет свое истинностное значение, з) См. с. !60. ') Не универсальный характер этого предположения с самого начала ойрвтил вннмвпие Дж, фон Нейман в своем уже цитировавшемся выше докаввтельстве непротиворечивости (Мв1Ь. л:! 26). 166 исслРПОВАние АРифметики пРи помоши».сил[ВОЛА [Гл и если некоторый входящий в нее терм без переменных с заменить в одном или нескольких местах, где он встречается, каким-либо термом 3, «равносильным» ему, т. е. таким, что равенство «=3 является истинной формулой. В этом несколько более общем случае, когда наличие выделенной оценки для равенства не предполагается, процедуру построения резольвенты придется немного модифицировать, так как при построении функций замены нужно будет следить за тем, чтобы значения этих функций при одинаковых значениях аргументов также были одинаковыми.
Однако основная цель, которой должна была послужить процедура построения резольвенты, все-таки остается недостигнутой: непротиворечивость арифметического формализма в его полном объеме на этом пути остается недоказанной. Но прежде чем продолжать рассмотрение этой проблемы, нам будет уместно довести до конца начатый в гл.
1 ход мыслей: мы все еще не привели обещанного доказательства') второй а-теоремы. ») См. с. 37. ГЛАВА 11! ИСПОЛЬЗОВАНИЕ е-СИМВОЛА В ИЗУЧЕНИИ ЛОГИЧЕСКОГО ФОРМАЛИЗМА й 1. Вторая е-теорема Результаты предыдущих глав группируются вокруг одной из двух задач, поставленных нами в связи с введением е-символа, а именно — вокруг задачи, касающейся возможности исключения связанных переменных из выводов, осуществляемых средствами исчисления предикатов (возможно, с применением е-формулы), при условии, что используемые в этих выводах аксиомы, а также результирующие формулы выводов не содержат связанных переменных.
Эта возможность устанавливается первой е-теоремой'). Теперь остается вторая задача, относящаяся к символьному решению экзистенциальных формул'). Мы намеревались показать, что применение этой операции в рамках формализма какой-либо системы аксиом Я первой ступени не подвергает расширению совокупность выводимых формул, построенных из символов системы Я. Мы воспользовались е-символом и е-формулой, дающими общую формализацию операции символьного решения экзистенциальных формул, и задачу установления этого факта свели к задаче установления второй е-теоремы, которая содержит в себе только что упомянутую теорему о символьном решении и является ее обоб[цен нем ').
Напомним формулировку второй е-теоремы. В этой теореме речь идет о формализме Р, получающемся из исчисления предикатов в результате добавления к нему е-формулы, а также некоторого числа собственных аксиом, не содержащих вхождений е-символа. (Разумеется, к символам исчисления предикатов должны быть добавлены входящие в эти аксиомы индивидные, функциональные и предикатные символы.) Утверждается, что любая выводимая средствами формализма г формула ш, не содержащая вхождений а-символа, может быть выведена в г н без использования е-символа. Доказательство мы начнем с двух предварительных упрощений.
Во-первых, мы заметим, что без ограничения общности можно ") См. с, 26. ») См. с. 23 а 25. ») См. с. 35 н д«лес, 169 ВТОРАЯ е ТЕОРЕМА Е-СИМВОЛ И ЛОГИЧЕСКИП ООРМАЛИЗМ 1гл. п1 считать, что в выводе формулы СР аксиомы не используются. Действительно, допустим, что такой частный случай второй е-теоремы уже доказан. Пусть ~6 — какая. нибудь формула, не содержащая вхождений е-символа, и пусть нам дан вывод этой формулы средствами формализма тс, использующий аксиомы й(ы ..., 911 Согласно предположению, сделанному относительно формализма г', эти аксиомы являются собственными, и если мы заменим входящие в них свободные индивндные переменные связанными ') (соответствующие кванторы всеобщности проставляются при этом в начале формул), то гюлучим некоторые формулы й(' ..., 91" зе ° 1 без свободных переменных, дедуктивно равные соответственно формулам Яы ..., 61. Эти формулы «1;, ..., 6~, кроме того, не содержат е-символов.
Согласно дедукционной теореме средствами формализма г" может быть получен вывод формулы г1;б ...ай(1'- Е, не использующий аксиоме). Так как формула 91~+ бе... й Р(ь'-и~6 не содержит вхождений е-символа, то, согласно нашему допущениюг е-символ из этого вывода, не использующего аксиом, может быть исключен, так что получится вывод этой формулы, использующий средства одного только исчисления предикатов.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
