Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 132
Текст из файла (страница 132)
Таким образом, формула 5(1)-~6 в модифицированном выводе получает то же самое порядковое число, которое первоначально получала формула 5(а)-+(3 При переходе от формулы 5(1)-э Е к формуле 5(1)-~-(3$5(й)-~-(3) при помощи схемы заключения, который происходит без изменения высоты, эта формула получает то же самое порядковое число, что и формула 5(1)-эа, т. е. число, которое первоначально получала формула 5(а)-~Е, в то время как нижняя формула схемы для квантора существования Эй5(г)-~Е получает порядковое число, ббльшее на единицу.
Таким образом, здесь в модифицированном выводе происходит уменьшение порядкового числа по сравнению с первоначальным. Это уменьшение сохраняется или даже усиливается при замене первоначальной, идущей от формулы Зй5(й)-~-Е к формуле Й нити вывода соответствующей ей нитью, идущей от формулы 5(1)- ()й5(ь)-+ 13) к формуле 5(1)-~Й. Это следует, с одной стороны, из монотонности натуральной суммы и показательной функции, а с другой стороны — из того, что при переходах по правилам исчисления высказываний, которые появляются на местах первоначальных схем заключения из-за добавляющейся (в одной или в обеих верхних формулах) посылки 5(1), разности высот могут, самое большее, уменьшаться. Рассматриваемая нами первоначальная нить вывода идет через одну из формул е и 9 ~Й.
В соответствующей формуле первого подвывода к этой формуле импликативно добавляется посылка 5(1); затем ее порядковое число уменьшается. Поэтому, если р' и ч' — порядковые числа формул, появляющихся здесь на месте формул е и $-+ Й, то р' 4Р ч' (р 4$ ч. На месте схемы е, й-~-Й Й здесь возникают две схемы заключения, которые (в зависимости от того, какой случай имеет место) имеют один из двух ранее указанных видов. В обоих случаях в первой схеме заключения разность высот равна нулю, а нижняя формула этой схемы имеет то же самое порядковое число, что и левая верхняя формула. Во второй схеме заключения разность высот представляет собой положительное число 1 1 — й+ 1, а порядковые числа обеих верхних формул суть (отвлекаясь от порядка) р' и а'.
Таким образом, заключительная формула этого подвывода имеет порядковое число ехРК (Р' ~ 4'). Теперь обратимся ко второму подвыводу. Здесь путем импли. кативного добавления к аксиоме 5(1)-~-)$5(й) посылки 15(1) получается формула ) 5 (1) -Р.Й. В результате этого вместо указан- ной аксиомы, имеющей порядковое число 1, получается истинная в логике высказываний формула с порядковым числом О.
Это понижение порядкового числа снова сохранится при замене первоначальной нити вывода, идущей от этой аксиомы для квантора существования к формуле Й, соответствующей ей нитью, ведущей к формуле ) 5(1)-~-Й. Одна из прежних формул е и Я-~.Й получит посылку )5(1) и ее порядковое число уменьшится. Таким образом, если р" и Ч" — порядковые числа указанных двух соответствующих формул, то будет иметь место неравенство Р" 444"( (РФ4, И теперь, совершенно аналогично тому, как это было в первом подвыводе, получается, что заключительная формула второго подвывода ~ 5 (1) — Й будет иметь порядковое число ехр1 (Р" 4Ф ч").
При переходе от заключительных формул обоих этих подвыводов к формуле Й, происходящем с помощью двух схем заключения, прирост высоты может иметь место, как уже было установлено, только во второй схеме; этот прирост равен д=й — 1— — й. После этого, в.силу нашего определения порядковых чисел для заключительных формул обоих этих подвыводов, получается, что в переработанном выводе порядковое число формулы Й будет равняться ехри (ехр, (р' 4Р Ч') 44 ехр1 (Р" 4Р р")). В первоначальном выводе формула Й имела порядковое число ехр~ А(рай).
но (-й=(1 — д+ 1)+(д — ) — й) =)+ ( 1~0, с(=-0, Р'44 6'(Р44 Ч Р'ФЧ'(РФЧ, а в силу определения отношения порядка для 0-а-фигур и монотонности показательной функции для с'(с, с" (г, 1>0 и б~О имеет место неравенство ехра (ехр1 (с') 4Р ехр1 (с")) ( ехрз+1 (с). Таким образом, в результате применения операции устранения квантора существования порядковое число формулы Й уменьшится, и это уменьшение продолжится вплоть до заключительной формулы всего нашего вывода.
Следовательно, в результате этой операции уменьшится и порядковое число нашего вывода в целом. Итан, мы можем констатировать, что операции устранения индукции и квантора существования, будучи применены к какому- либо выводу, уменьшают его порядковое число. С помощью этого факта искомое доказательство того, что любая последовательность применений операций устранения индукции и квантора существования должна оборваться, сводится к установлению того, что любая убывающая последовательность 0-н-фигур после конечного докАЕАтельство кАльмАРА 4И ПРИЛОЖЕНИЕ числа шагов обрывается, т. е. ведет к фигуре О.
Этот факт мы еще должны установить '). Для О-в-фигур нулевого и первого ярусов справедливость этого утверждения усматривается элементарно. Теперь мы покажем, как из справедливости этого утверждения для О-а-фигур ярусов до Й-го включительно вытекает справедливость его и для ярусов до (Й+ 1)-го включительно. Данную О-в-фигуру мы будем для краткости называть фигурой конечного спуска, если можно убедиться, что любой спуск (т.
е. любая убывающая последовательность О-в-фигур), начинающийся с этой фигуры, обрывается после конечного числа шагов'). После этого наша задача формулируется следующим образом. Пусть нам удалось показать, что любая О-в-фигура яруса не выше Й-го (Й~ 1) является фигурой конечного спуска, Требуется показать, что и любая О-а-фигура (Й+1)-го яруса тоже является фигурой конечного спуска. Сначала заметим, что достаточно провести доказательство для фигуры в«.
Действительно, если рассматривать фигуры с 1(Й+1)- го яруса1 вида а '+...+а ', где а,) аз).'..= а„то, как известно, фигура в'>+' больше любой из них и тоже является 'фигурой (Й+1)-го яруса, причем каждому спуску, начинающемуся с с, соответствует спуск с в' +', который состоит в том, что мы сначала с в">+' спускаемся на с, а затем повторяем рассматриваемый спуск, начинающийся с с. Сделаем еще одно вспомогательное замечание.
Если нам удастся установить, что степень в' является фигурой конечного спуска, то отсюда будет вытекать, что и каждая сумма а' +а' +... ... +в' тоже является фигурой конечного спуска. Действительно, если, пользуясь обычными обозначениями, записать такую сумму, >) Кальмар использует хлы »того рассуждение, с помощью хаторого Генц«и ы его работе: Сеп ! хе ц С. !»!е 'й<'!бес»рсмс!м!ге!!>е!! бе< ге!Ееп хз)>!ецс(>е>г!е.— Мзйь Аып., !930, с!2, 8. 555 н далее — цохззыызег зыхоннос>ь трзнсфнннтной ынц><наны Аля порядковых чисел, не превосходящих первого хзнт<>роысного с чнслз. Сзм Г.нцен тоже ссылается нз зто рассуждение з «заем более позднем дока.
ззтельстые ыепрцтн>юречыностн, однако здесь он говорит об »сом способе обоснования нзн о предварительном, с намеренным когда-нибудь вернуться к рассмотрению ы<ого запрос». (См. !4еце гзаццй дв '>ь>!бесзр<цсЫ<е!Ье!!«Ь«ы>е!вез !Ф сне ге!Ее хзшеыс)<ео<!е — Го<»с!шцееп хы< 1.ойж ццб хцг Ссццб!ейный де< ехзщыц Е>>!»зецзс)>з!сеп, )4еце го!Ее, !%8, № 4, 3.
44,) Мы ы дальнейшем зосцользуемсн рассуждением, нцтороы — з отлнчне от упомянутого рзссужденнн Генцеыз, з также от приведенного ы гл. >!, 4 3, ц. з) дохзззты«ьс>ыз цлы частной трзнсфынытной ынхухцын-<пыосытсн йеыосредствеыно х О-е-фигурам н н котором не ыснохьзуютсн ынкзнне представления о трзысфннытыой индукции. з) Выражение «конечный снуск» не хохжно наводить нзс нз мысль о т<>м, что ы данном случае речь идет о каком-либо сзойссыз О-е-фнгур, распознаваемом злзментзрнымн средствами. В самом деле, у любой фигуры ые ниже второго яруса возможных спусков бесконечно много н оыы не могут быть церыцро.
боззны ысы, состоящую из т+ 1 члена, в виде в' (т+ 1), то при любом спуске с а' (и>+ 1) первые т слагаемых будут оставаться без изменений, пока мы не дойдем до фигуры, которая меньше в' т. Если мы отвлечемся от этих т совпадающих слагаемых, то получится начинающаяся с а' последовательность спуска, а она, по нашему предположению, должна после конечного числа шагов оборваться Таким образом, за конечное число шагов мы приходим От а' (т+1) к а' т или к меньшей фигуре. Мы можем даже считать, что мы доходим до в' т, так как в любом случае эту фигуру можно включить в наш спуск, от чего Он только удли нится.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
