Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 18
Текст из файла (страница 18)
Например, е-терм, только что рассмотренный нами в качестве примера, с использованием явных определений ф(а, Ь) =а (а=е„(Ь(убеу(х)), ф(а, Ь) =е„(а =е,(у+Ь(г)), сс = е, (г+ е„(и = г) ( г") изобразится выражением ер(ф(с+2, 1), сс). Общее доказательство высказанного утверждения легко получается финитной индукцией по степени рассматриваемого е-терма. Можно также убедиться, что в выражении, получающемся из какого-либо е-герма е в результате использования сокращающих символов для основных типов, встречаются те же самые термы без е-символа, которые входят в качестве составных частей В тчрМ Е. 87 88 ИССЛЕДОВАНИЕ АРИФМЕТИКИ ПРИ ПОМОЩИ з-СИМВОЛА [ГЛ.
П' ВКЛЮЧЕНИЕ АКСИОМЫ (3»[ В МЕРВУЮ е-ТЕОРЕМУ Рассмотрим, в частности, формулу вида а=Ь-» (Я(а)- 8[(Ь)), () [) ([) и формул вида а=а, а=Ь-ь(а=с-».Ь=с) а = Ь -ь (С (а) — 1- Я~ (Ь)), а = Ь ([ (а) = ( (Ь)) (в этих формулах Я~ всюду представляет собой некоторый входящий в формулу е»е (а значит, и в»з() предикатный символ, а 1 — некоторый входящий в Йч функциональный знак, т. е. или функциональный знак, входящий в Й, или знак, введенный в качестве сокращающего символа для основного типа какого- либо в-терма; при этом имеющиеся, но явно не указанные места для аргу[[[ентов предикатных и функциональных символов заполняются свободными индивидными переменными, отличными друг от друга и от переменных а и Ь). Теперь, чтобы из вывода формулы а = Ь-ь(йе (а):-ь»ле (Ь)) получить вывод формулы а = Ь вЂ” ь (8((а) -ь л (Ь)), достаточно всюду заменить введенные нами сокращающие символы определяющими их в-термами.
При этом вместо формулы а Ь-»-(((а) =((Ь)), где ((.) представляет собой вводимый для некоторого основного типа сокращающий символ, получится формула а = Ь -Р зр'3 (», а) = е»3 (», Ь), которая не содержит формульных переменных, но, быть может, содержит е-термы. Если для основных типов входящих в нее з-термов мы введем сокращающие их символы, то вместо рассматриваемой формулы мы получим некоторую новую формулу а=Ь-» [е[*(а) — ьбе(Ь)), в которой е-символов уже больше не будет (зато в ней появятся ранее не встречавшиеся иидивидные и функциональные символы). Эта формула может быть выведена средствами исчисления , преднкатов (а если формула 6 (а), а значит, и 8[а (а), не содержит кванторов, то уже средствами одного только элементарного исчисления со свободными переменными) из формул »торой фигурирующий в ней в-терм В,6(», а) будет основным типом.
Таким образом, всякая формула вида а = Ь -+ (»)[ (а) -»- И (Ь)), где 6 (а) — формула, не содержащая формульных переменных, которая, кроме символов исчисления предикатов, может содер- жать еще индивидиые, функциональные и предикатные символы, всегда может быть выведена из: 1) формул (),) и (1), 2) специальных аксиом равенства, имеющих указанный ранее вид и связанных с предикатными символами и функциональными знаками, входящими в'формулу 6(п), и 3) формул вида а=Ь-евра(», а) =вр5(», Ь)> где ер»Э(»„а) — какой-либо основной тип.
Этот вывод осуществляется средствами исчисления предикатов или, если формула [й(а) ие содержит кванторов, средствами эле- ментарного исчисления со свободными переменными. При этом могут также добавиться подстановки е-термов вместо свободных нндивидных переменных. Замечание. Отметим, что каждая формула вида а Ь-ье Е(», а)=е 5(», Ь) получается в результате подстановки (и, быть может, переиме- нования связанных переменных) из формулы а Ь-ь в,А (х. а) = Е,А (х, Ь), которая в свою очередь выводится из формул ([д) и (Юз) совер- шенно таким же образом, каким для функционального знака[(.) выводится формула а=Ь-»-((а) =((Ь)').
») Оя. т. 1, с. 237 — 238.— Здесь представляется удобный случай прнвеств обосноваыяе высказанного ранее (см. с. 82) утверждения о том, что равно. сильность обшей аксиомы равенства ([з) соответсвующнм спепнальным аксяомзм равенства пряменнтельно к выводам формул без формульных переменных, установленная ыамн для аксноматыческях теорий, формалнзованных средствами нсчвслеыяя преднкатов, перестает яме[в место прв добавления к этны теорням е-свмвола в в-формулы. В свмом деле, доказательство этого факта с использованием только что отмеченной выводнмостн формул вада а = Ь -ь ера (р, а) = ера (з, Ц вз аксном (з») в (Зз) может быть получено следующим образом.
Мы рассматриваем формализм, состонщяй нз исчисления преднкатов с добавлеынем к нему з-снмвола, з.формулы, а также символов н аксиом системы [2), но с опущенной аксиомой внхукыян. В этом формалнзме выводится формула 38 ИССЛЕДОВАНИЕ АРИФМЕТИКИ ПРИ ПОМОЩИ з-СИМВОЛА (ГЛ 11 а Ь-ьз„(хчьп) е (х чь Ь), из котоРой с помошью аксиомы а+О и выводится формула [в] е„(х чь О+ 0) = е„(х чь 0). Если бы в этом формализме тоже имелась возможность замены в выво. аах формул без формульных переменных аксиомы (зз) соответствующими специальными аксиомами Равеыства, то в вывоДе фоРмУлы [е] аксиомУ (1») можно было бы заменить этими специальными аксиомами.
В результате этой замены вместо аксиом системы (а) у нас появились бы аксиомы системы (х'), Поэтому из аксиом системы (Е') и из е-формулы средствамы исчисления предикатов должна была бы выводиться формула [з], Но формула [з], взятая совместно с формулами (. зх (х чь 0) 0', ех (х чь О+ 0) = 0" [в ) и аксиомами системы (л'), ведет к противоречию. Поэтому формализм Ры состоящий из начисления предикатов, символов и аксиом системы (Х')„е-сим. вала, взятого вместе с а-формулой, и двух принимаемых в качестве аксиом формул [е'), был бы противоречивым.
Однако это не так: в непротиворечивостн формализма Ед можно убедиться при помощи процедуры устранения е-символов. Необходимо только, принимая зо внимание наличие аксиом [е»], модифици овать эту процедуру следующим образам. рв устранении критических формул из какого-либо доказательства те критическве формулы, которые относятся к термам ех(х-ьО) и а„(хч»0+0), процедуре исключения не подвергаются. Так как эти формулы имеют ранг 1 и степень 1, то при заменах, производимых для устранения остальных криты. ческнх формул, они останутся без изменений. Когда все зги критические формулы будут полностью устранены, терм е,(хчьО) надо будет заменить термам 0', а терм ех(х„-ь 0+0) — термам 0'. Тогда связанные с этими в.термамн критические формулы перейдут в формулы вида 1 чь 0-» О' чь 0 ы 1 чь О+ О -» 0 чь О+ 0 и формулы [е»] перейдут в формулы 0' 0' и 0' 0'. Но все вти формулы выводимы из аксном системы (2') средствами злемен.
тарного исчисления со свободными перемеыными. Таким образом, по нормированному доказательству любой нумерической формулы 6, осуществляемому средствами формализма Ьь мы получаем вывод эгей формулы из аксиом сястемы (Е') средствами элементарного исчисления со свободнымн переменными. Так как аксиомы системы (л') являются вернфицируемыми формулами, отсюда следует, что формула 6 является истинной. Следовательно, формализм г, непротиворечие, н, значит, формула [е] не может быть выведена из аксиом системы (Е') с помощью исчисленна пра. дикатов и е-формулы.
з) См. с. 63. Полученный результат мы теперь используем для намеченного нами ') распространения первой и-теоремы иа формализм хт,„ содержащий аксиомы равенства (]х) и (]з). ВКЛЮЧЕНИЕ АКСИОМЫ 11»] В ПЕРВУЮ з-ТЕОРЕМУ 89 И в том случае, когда заключительная формула вывода не содержит связанных переменных, и в том случае, когда она начинается кванторами существования, но не содержит ни других кванторов, ни е-символов, мы начнем наше доказательство совершенно так же, как и раньше. Сначала мы покажем, что, не ограничивая общности, заключительную формулу 6 можно считать формулой без свободных переменных. Затем мы исключим из вывода кванторы, заменяя изнутри каждое выражение Вида 3п5(п) выРажением 11(ез5(п)) и каждое выРажение вида 'ба~(п) — выражением 5(е„] 1](п)). При этом во избежание коллизий между связанными переменными мы должны будем произвести необходимые переименования.
В процессе этих преобразований применения схем (а) и ([]) переходят, как мы уже знаем, в некоторые подстановки, основная формула (Ь) переходит в в- формулу, а основная формула (а) переходит в некоторую формулу, выводимую из в-формулы с помощью подстановки и контрапозиции. Мы добавляем вывод этой формулы к рассматриваемому выводу. В вопросе о влиянии этой операции исключения кванторов на заключительную формулу Сь мы должны различать наши два случая: случай, когда эта формула не содержит связанных пере. меиных, и случай, когда она имеет вид Ж~х... -]Е,л(Гх, ..., 8,). В первом случае формула (Р остается без изменений; во втором случае вместо нее появляется формула вида Й(п„..., а„), где и,, ..., и,— некоторые е-термы' ). Далее с помощью разложения доказательства на нити мы произведем возвратный перенос подстановок в исходные формулы, а после этого исключим свободные переменные').
При этом на месте исходных формул первоначального вывода формулы 6, содержащих свободные переменные, окажутся некоторые формулы, получающиеся из них в результате соответствующих подстановок. В частности, вместо аксиомы (]з), фигурирующей в качестве исходной формулы, мы получим исходные формулы вида п = Ь -»- (Я (и) -ь 9[ (Ь)), которые не будут содержать никаких свободных (и, в частности, формульных) переменных, а также не будут содержать и кван- ') См. с.
43, 45. ') См. с. 39. включниин аксиомы (л! в пнгвию е-твогвмг 9! 90 исслвдовднив дииомнтнки пои помощи .символа !гл. е 2! торов. Любая формула этого вида получается в результате по ' становки из соответствующей формулы а = Ь- (6 (а) -ь Я (Ь)), а эта последняя, как мы отметили выше, выводится из форму (4), специальных аксиом равенства и формул вида а=Ь-+ н„8(», а)=е„6(», Ь)„ причем этот вывод осуществляется средствами элементарного.
исчисления с допущением подстановок е-термов вместо свободных: индивидных переменных. Специальные аксиомы равенства, которыми нам придется пользоваться, принадлежат некоторому определяемому формализмом Р конечному запасу формул, а именно совокупности тех, формул равенства, имеющих вид а=Ь-ь(кь(а)-ьО(Ь)), а Ь (1(а)=!(Ь)), которые соответствуют предикатным символам и функциональным знакам из Р (точиее, их различным аргументам). «Формула (!),. т. е. формула а=Ь-ь(а=с-ьЬ=с), содержится в их числе.] Мы будем кратко называть эти фор- ' мулы формулами (!л).
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
