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

40 — 43. 48 исключение сВязАнных пеРеменныР' (ГЛ ! случай. Как мы уже знаем, этот метод с9г1оит в том, что по данному нам нормированному доказательстгзф формулы ч: с критическими формулами 6 (1,) - 6 (е 6 (~)), 6 (1„) Л (.;6 (х)) сначала строятся выводы формул 6 (11) -~6, 6(1„)-~6, а затем вывод формулы ! 6 (1 ) ее... й ") 6 (1„) -э ~, который вместе с указанными и формулами средствами исчисления высказываний дает нам вывод формулы 6.

Построение этих и+! частичных доказательств по заданному нормированному доказательству происходит на основе дедукционной теоремы путем импликативного добавления соответствующих посылок и включения необходимых фрагментов доказательства, состоящих в надлежащем применении исчисления высказываний. Но, кроме этого, для получения вывода формулы 6 (1,) — 6 (в=1, ..., и) терм е 6(к) всюду, где он встречается в данном нормированном доказательстве, мы должны заменить на 1, Теперь мы будем пытаться применить сходный метод и в том случае, когда в рассматриваемом доказательстве кроме критических формул (й)„относящихся к данному терму ег6(х), встречаются другие критические формулы.

Здесь мы сталкиваемся со следующими двумя трудностями. Во-первых, может случиться, что при заменах, которые мы будем выполнять в ходе исключения формул (Й), другие критические формулы перестанут быть формулами, получающимися в результате подстановки в е-формулу; в этом случае данный метод может вообще не дать никакого вывода формулы ц. Но даже если этого и не случится, мы все равно должны будем считаться с тем, что вследствие производимых замен могут возникать новые критические формулы, и это делает совершенно не очевидным тот факт, что рассматриваемая процедура исключения критических формул после конечного числа шагов оборвется. Следовательно, нам необходимо более детально заняться рассмотрением тех изменений, которым может подвергнуться критическая формула 6 (1) 6(з,6 (й)) докАзхтельстзо пеевои леоеемы вследствие замены какого-то отличного от е„6(х) з-герма 1какимлибо другим термом 1*.

Здесь имеются следующие возможности: !. Терм 1 входит в рассматриваемую кригическую формулу только внутри терма 1. (Мы включаем сюда и случай, когда 1 совпадает с 1.) Тогда и после выполнения укаэанной замены эта формула будет по-прежнему критической формулой, связанной с е-термом ег6(х). 2. Терм 1 входит в формулу 6(с), а, кроме того, может быть, и в 1, но ни один из термов 1 и з„й((х) не является составной частью 1. Тогда наша критическая формула может быть более подробно записана в виде 6(1(1), 1)- 6(е,Л(х, 1), 1), В этом случае терм 1 является составной частью е-герма е 6 (х, 1), с которым связана данная критическая формула, и потому степень 1 меньше степени этого терна.

В данном случае замена терма 1 приводит к тому, что эта критическая формула переходит в другую критическую формулу, связанную с термом з 6(~, Р), который в силу замечания о ранге е-выражений' ), имеет тот же самый ранг, что и терм е„6(х, 1). 3. Один из термов 1 и вг6(х) содержится в 1 в качестве составной части. Тогда 1 имеет вид Е(1) или соответственно д(е„й((г)), а формула 6(с) имеет вид 3(д(с)), гдее(с) — вполне определенный е-терм, который имеет тот же самый ранг, что и 1, Терм е„6(х), с которым связана рассматриваемая критичсская формула, в этом случае записывается в виде е,'В (Е (Ь)). Значит, он подчиняет себе е-выражение з(у), и потомУ его Ранг выше ранга этого выражения. Но з(х) имеет тот же самый ранг, что и д(с), а ранг з(с), как мы только что установили, равен Рангу 1.

Следовательно, ранг терма г 6(х) больше ранга терма 1. Ввиду этого, если условиться в первую очередь производить ~амены тех связанных с критическими формулами е-термов, котоРь'е имеют ранг, наибольишй из числа встречающихся, то можно будет исключить разбор случая 3. Если мы будем придерживаться такого порядка замен, то У "ас будут встречаться только случаи 1 и 2. Зто говорит, во"ервых, о том, что любая критическая формула, если она вообще будет претерпевать какие-либо изменения, будет снова переходить ~) См. е, 4В исключение связанных пеееменньп, и'л. ! доказательство певвоп а-теоремы в некоторую критическую формулу, причем эта последняя будет связана либо с тем же самым е-термом, что и начальная критическая формула (случай 1), либо с нека'горым новым е-термом, имеющим тот же самый ранг.

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

Это рассуждение дает нам возможность следующим образом устранить нз любого наперед заданного нормированного доказательства какой-либо формулы К все его критические формулы. Среди чисел, являющихся рангами термов, с которыми связаны какие-либо критические формулы, имеется наибольшее. Ранг того е-терма, с которым связана какая-либо критическая формула, мы для краткости будем называть рангом этой формулы, а степень этого е-терма мы будем называть степенью этой критической формулы. Пусть ш — наибольший из рангов критических формул, фигурирующих в данном доказательстве, и пусть и — наибольшая из степеней критических формул, имеющих ранг ш. Пусть 1— один из тех е-термов, имеющих ранг ш и степень и, с которыми связаны какие-либо критические формулы.

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

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

Таким образом, у нас имеется способ, позволяющий уменьшать количество различных фигурирующих в нашем рассмотрении рангов критических формул. Повторив его нужное число раз, мы полностью исклю- чим все критические формулы, входящие в рассматриваемое доказательство. Это рассуждение и доказывает нашу первую н-теорему. Рассмотрение общего случая с помощью понятия ранга восходит к Вильгельму Аккерману. д) Обобщение результата.

Метод, примененный в только что изложенном доказательстве, дает еще один важный для применений результат. Результат этот мы получим, применив рассмотренную процедуру исключения к выводу формулы 6 вида :-)й,...=)Е,6(у,, ..., ~,), не содержащей никаких других кванторов, кроме стоящих в ее начале кванторов существования Зй,, ..., Бй„а также не содержащей и е-термов. При этом предположения относительно формализма Р я аксиом ь4),, ..., 4)1 будут прежними.

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

е. формула Эй,...Зт,ь' й ..., Ед. перейдет в формулу вида й((а,, ..., а,), где а,, ..., а,— некоторые термы'). Заметим, что термы эти не будут содержать свободных переменных, так как сама формула (Ч их не содержит, а при замене любого выражения Зйб(х) выражением ьВ(е„б (г)) никаких новых свободных переменных появиться не может. Остальные подготовительные операции из числа упомянутых выше оставят формулу !?1(а,, ..., и„) без изменений. Внутри этой формулы е-символы будут встречаться только в термах а,, ..., а„ так как по условию выражение 91 (й,,..., г,) е-символов не содержит.

Теперь у нас будет нормированное доказательство' ) формулы аеы".,) Н а ° ь - ° ° *ь- ь ) См. и. а), с. 37 и далее е) См. Вассужление на с. 44 — 45, сде мы произвели ато устранение для случая ь 4 В а) См, с. 39 — 40. ИСКЛЮЧЕНИЕ СВЯЗАННЫХ ПЕРЕМЕННЫХ !ГЛ 1 «1! докхзхтельство пеивоп теоиемы процедуру устранения критических формул оп»«санным выше способом, так как в ней существенным образом используется то обстоятельство, что заключительная формула рассматриваемого нормированного доказательства не содержит е-символов. Однако эту процедуру легко модифицировать таким образом, чтобы она давала результат и в том случае, когда в заключительной формуле содержатся е-термы. В этом можно убедиться путем следующего рассуждения, Г1усть дано нормированное доказательство с заключительной формулой 6.

Пусть среди е-термов, с которыми в этом доказательстве связаны какие-либо критические формулы, терм е„б(х) является термом с максимальным рангом, и пусть среди термов, обладающих этим свойством, он имеет наибольшую степень. Пусть с этим е-термом связаны критические формулы ( Е~ (~))~ 6(ЕК) ~6(а 6(г)). Действуя совершенно аналогично предыдущему,' мы можем применить гильбертовский метод для получения и+1 «частичного доказательства» '). Но в данном случае эти доказательства, вообще говоря, уже могут и не оканчиваться формулами вида 5 (11) -э 6, З(1«) — ~6, ) 6 (11) й... й ) Е (1,) 6.