Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 22
Текст из файла (страница 22)
в ез льтате подстаДействительно, в первом случае из (5 в реву новки и импликативного добавления формулы а =6 получаегся формула а =6-е-(1=6-с-е„сВ(», с) =е„'3(»„а)); зта последняя с помощью формулы Е=Ъ-е.(с=Ь- с=а), которая может быть получена из ((1) и (1), выводится из формулы с= а-е.з„Е(», с) =Е„Е(», а). В ором случае формула, получающаяся из Е в результате подстановки и импликативного добавления пасы сывается в виде а = ( -~ (с = 6 -~ е„6 (», Ь, с) = е„З (»„ а, 6)), из (5 ) и,1) а эта последняя получается с помощью выводимых формул а = 6 -~- 6 = а, е 6(» Ь с)=е 6(», а, с)6се.'В(», а, 1)=е»3(», а, 6)-1- е, »,, с — е, Е„Е (», 6, с) = е„6 (», а, 6) 100 исследовхние Аеифметики пеи помоши -символА 1гл.
и и следующих формул е-равенства: Ь=а',— «Е„З(», Ь, г) =е„о(», а, г), =Е- е,е)(», 1, ) е,6(», а, 0). Но сказанное еще не устраняет всех трудностей. Правда, при построении первого частичного доказательства мы можем после выполнения замены 1 на 1 и импликативного добавления посылки а = 0 вставить только что указанные выводы для формул, полу- чающихся вместо отличных от 5 связанных с 1 формул е-равен- ства,— точно так же, как мы должны были включить выводы, для формул, получающихся вместо связанных с 1 критических формул, — и таким образом придем к некоторому нормированному доказательству формулы а=Ь-«СУ.„ где 6, — формула, получающаяся из Й в результате замены..
Однако используемые при этом формулы е-равенства г = а -«е„В (», г) = е,о (», а) или соответственно Ь=а-«е Е(», Ь, г) =е„о(», и, г) и г=д-«е„6(», а, г) =е„б(», а, О), которые, как мы знаем, имеют основной тип 1 вовсе не об за ы . и и 1 я. н ринадлежать совокупности 6 ). Таким образом, вместо устраненной формулы 5 могут появиться новые формулы е-равенства с основным типом 1, и, следовательно, число формул е-равенства, связанных с основным типом 1, в результате устранения формулы 5 может и не уменьшиться.
Теперь наша задача заключается в том, чтобы показать, что каждый такой шаг процедуры устранения, направленный на исключение какой-либо формулы е-равенства с основным типом 1, при подходящем выборе этой формулы непременно будет осуществлять некоторую редукцию нашей проблемы, так что после ° с наперед оцениваемого числа шагов все формулы е-ранено ва т рассматриваемым основным типом будут устранены, и тем самым ' число имеющихся основных типов формул е-равенства ранга ш уменьшится. С этой ой целью мы рассмотрим совокупность ь всех тех е-термов, с которыми связаны какие-либо формулы из 6, или, точнее, с которыми в заданном нормированном доказательстве (после А) См. с.
100. 1Я Включение Аксиомы сш в пеРВую е.теоеему шт исключения имеющихся несобственных формул е-равенства с основным типом 1) связаны какие-либо формулы е-равенства, имеюшие основной тип 1. Эта совокупность ~ определяет собой совокупность Я:~ тех е-термов, которые получаются из основного типа 1 в результате замены каждого из его аргументов каким-либо из тех термов, которые заменяют тот же самый аргумент в каком-либо терме совокупности ч.. Согласноэтому определениюч, является частью ~~. Совокупность ~' может быть явным образом построена по совокупности !ь. Мы можем также легко указать оценку для количества элементов в Й~. В самом деле, если и — число аргументов основного типа 1, а 1 — число всех термов, которые по крайней мере в одном из термов совокупности ч.
заменяют некоторый аргумент у основного типа 1 (эти термы мы будем кратко называть аргументными термами в Й), то Ф*, как легко убедиться, содержит не более 1" элементов, Теперь мы установим для термов из ®* некоторую очередность. С этой целью мы выберем какую-либо очередность для аргументных термов в ч„ подчиненную единственному условию, что из двух е-термов различной степени терм 0 меньшей степенью предшествует терму с большей степенью и что термы, не являюгциеся е-термами (термы нулевой степени), предшествуют всем е-термам. Затем мы зафиксируем какую-нибудь очередность аргументов в 1.
Элементы совокупности ч.* мы упорядочим по возрастающей степени, а в остальном — лексикографически, т. е. так, чтобы для двух термов одинаковой степени предшествование определялось по аргументным термам, подставляемым в первый из аргументов основного типа 1, в результате замешения которого эти термы становятся отличными друг от друга. В нашей процедуре теперь в качестве терма 1, замена которого будет производиться, мы будем брать тот из е-термов, принадлежащих совокупности ч., который в установленной нами очередности термов из Й~ является самым последним, т. е. не предшествует никакому другому.
В соответствии с этим выбором терм 1 среди е-термов, о которыми связаны какие-либо формулы из 6, будет иметь ранг, максимальный из числа имеющихся. Пусть теперь 5 — та из числа связанных с термом 1 формул из 6, которую мы должны устранять первой. Для устранения 6 мы произведем замену ! посредством 1 и импликативно добавим формулу а = Ь. Чтобы получить таким образом нормированное доказательство (первое «частичиое доказательство»), нам может быть придется, как только что было установлено, ввести в качестве исходных новые, т. е.
не содержащиеся в совокупности 6, формулы е-равенства с основным типом 1. Присоединение такого рода вспомогательных формул приведет к тому, что после произведенного устранения формулы 8 совокупность 6А исполь- 108 исследование а»и»мвтики п»и помощи»-символа 1гл, и. зуемых теперь в качестве исходных формул в-равенства с основ-:: ным типом ! не будет являться частью совокупности 0 и что тем самым и совокупность Т, тех е-термов, с которыми связаны, какие-либо формулы нз б„не обязательно будет являться частью ' совокупности ч..
Однако мы можем легко убедиться, что переход от ч. к ~, в определенном смысле слова является редукцией. Для этого нужно отдельно рассмотреть два случая, которые мы различали '), когда принимали во внимание возможность того, . что формула в-равенства 9 в результате замены терма 1 переста-, нет быть формулой е-равенства. Этим случаям соответствуют выводы двух типов, с помощью которых, вводя одну или соответственно две формулы е-равенства в качестве исходных, мы получаем формулу, возникающую в результате этой замены и нмпликативного добавления посылки в = ». Эти два случая в терминах в-термов, с которыми связаны формулы 5, 9 и формулы в-равенства, добавляемые в качестве вспомогательных, будут выглядеть следующим образом: Первый случай.
Если термы ! и 1, с которыми связана фор-, мула 5, записать в виде е„6(», а) и е,6(», »), то формула 9 будет связана с термом 1 и с некоторым термам е 6 (», с). В этом случае нам будет нужно ввести в качестве вспомогательной формулы только одну формулу е-равенства, причем она будет свя- ' зана с термами е„6(», с) и е„6(», а). Значит, в этом случае к совокупности ~ не добавляется нн одного нового терма. Между ' тем терм 1 в этой совокупности уже встречаться не будет. Второй случай. Если термы 1 и 1 записать в виде е,6(», а, 6) и в„6 (», 8, 6), то формула 9 будет связана с 1 и с некоторым термом е„6 (», !, г). В этом случае нам нужно будет ввести в качестве вспомогательных формул две формулы е-равенства, из ' которых одна связана с термами е 6(», », с) и з»6(», а, г), а другая — с термами »„6(», а, г) и а»6(», а, 6).
Значит, по сравнению с ч. в ~, добавляется терм е,6(», а, г), 'в то время как терм 1 выбрасывается. Но терм е„6(», в, г) непременно принадлежит к -'*, потому что в этом терме все аргументы терма 1, в том числе и унаследованные от терма в, замещены в точности так же, как и в терме ' е„6(», », г) из ®, а терм в стоит в терме е„6(», в, 6), также, принадлежащем ч,, на месте того же самого аргумента, что и в терме з„6(», в, г). Кроме того, можно доказать, что терм »,6(», а, г) в очеред-: ности термов из ~» предшествует терму !. Действительно, терм 1, г) См. с. !04. включение аксиомы ыв в ив в»го»-тво»вм» 6(» 5 6), по определению в очередности элементов сово- т.
е. е„ ( , купности р асположен позже содержащихся в ч. термов 6) и в„6(» 8» г). Отсюда прежде всего вытекает, что те м е„6(», 5, 6) имеет степень, не меньшую степени каждого из терм е„», этих двух термов. Далее, если степень терма е»6(,, ) е 6(»» 6) совпа- дает со степенью терма е„6(», а, 6), то терм а в очередности ых термов из ь должен находиться раньше 5; с дру- гой стороны, если в„6(», 8, 6) имеет более высокую степе нь чем е,6(», в, 6), то» должен иметь степень более высокую, чем а, ы в в очередности аргументных термов из ч. должен и тем самым в те м в в оче едностн находиться раньше $.
Таким образом, терм в в р аргументных термов из ® находится раньше герма 6 и потому имеет степень, не превосходящую степени тер пень терма е„6 (», а, г) тоже не превосходит степени терма в„6(», 8, г) и, значит, в очередности термов, входящих в сово- купность ч.», терм в„6 (», а, г) располагается раньше герма е„6 (», », г). Так как этот терм опять-таки располагается раньше 1, то е,6(», в, г) располагается раньше 1, что и утверждалось. Таким об азом, разбор обоих этих случаев показывает, что ервом нз них совокупность Тг получается из ч.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
