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

Действительно, в каждом из первых и частичных доказательств происходит некоторая замена терма е '3 (х), а именно, з 1-м частичном доказательстве терм е Ф(х) заменяется гермом Вследствие этих замен формула 6, которая, может быть, содержит заменяемый терм егЗ(~), может подвергнуться каким-либо изменениям. Лишь относительно (и+1)-го частичного доказательства, которое проводится без каких бы то ни было замен, мы можем быть уверены, что формула 6 останется в нем без изменений. В соответствии со сказанным, заключительные формулы этих частичных доказательств в общем случае будем иметь вид 6(11)- 6ы Е ((и) -1-6», ) 3 (11) й... й ) 3 (Еи) -»-6, 1) СМ С.

43, причем формулы 6„..., 6«, возможно, будут отличаться от 6 тем, что в 6, (г=1, ..., и) вместо е Е(г) будет стоять соответственно терм 1, Хотя из этих п+1 формул формула 6, вообще говоря, и не выводитсг, но средствами исчисления высказываний из них можно вывести формулу 6 Ч 61 Ч " Ч 6и. Действительно, обозначим эту дизъюнкцию посредством 2.

Тогда формулы 61 '"~~ 6и +' ~ будут выводимы средствами исчисления высказываний. Поэтому из заключительных формул указанных и + 1 частичных доказательств при помощи исчисления высказываний мы получим формулы 6 ((1) — »Ь, З (Еи)-~-5>, ) Е (11) й... й ) Е (1»)- Х, которые, будучи взяты совместно друг с другом, дадут нам формулу Ь. На этом пути мы получаем некоторую простую модификацию нашей процедуры исключения крииических формул. Единственное различие по сравнению со случаем, когда заключительная формула не содержала е-символов, заключается в том, что здесь на каждом шаге процесса исключения, приводящем к исключению критической формулы, связанной с каким-либо определенным е-термом, может происходить некоторое дизъюнктивиое раацепление заключительной формулы; именно, на каждом таком шаге вместо данной заключительной формулы (х может появиться некоторая дизъюнкция 6 ~/ (ь1~/ ...

~/6„где каждый ее член 6, получается из 6 в результате некоторой замены одного из входящих в Ф е-термов (всюду, где этот последний входит в 6). Если теперь эту модифицированную процедуру применить к рассматриваемому нами нормированному доказательству формулы л(а„..., а,), то у нас получится вывод некоторой формулы Ж*„не содержащий вхождений критических формул. Если в результате применения нашей процедуры формула Е(а1, а,) будет подвергаться каким-либо изменениям, то формула 6* будет получаться из «((а1, ..., А,) в результате одного или нескольких расщеплений на дизъюикции. ИСКЛЮЧЕНИЕ СВЯЗАННЫХ ПЕРЕМЕННЫХ 1гл 1 Рассмотрим более детально вопрос о виде этой формулы.

В результате однократного расщепления на дизъюнкции у нао получается заключительная формула аа 'ч' аз 'ч' ° ° 1» а», где аа представляет собой формулу а(аз, ..., е,), а остальные члены дизъюикции могут отличаться от нее лишь тем, что вместо термов а„..., а„в них стоят какие-нибудь другие термы. В самом деле, как мы знаем, в формуле а(аз, ..., в,) вне тернов а„..., а, никаких в-символов не встречается. Тем самым формула а, '11' а, '1/ ...'1/ а„представляет собой дизъюнкцию членов вида а (ь„ ..., ь»), где Ь„..., Ь, суть некоторые термы. Это свойство заключительной формулы будет сохраняться и при всех дальнейших расщеплениях; действительно, из дизъюнктивного члена, имеющего вид а(Ь„ ..., Ь„), в результате замены одного входящего в него етерма другим может снова получиться только член а (сд, ..., с,) с некоторыми термами сд, ..., с„, а дизъюнкция таких дизъюнк- ций сама является дизъюнкцией, состоящей из таких членов.

Указанное свойство заключительной формулы сохранится и в том случае, если мы после устранения всех критических фор- мул заменим каждый из оставшихся е-термов конкретной пере- менной а, за исключением тех из них, которые являются состав- ными частями каких-либо объемлющих их е-термов. Таким образом, мы получим вывод некоторой формулы вида а(1,2>, ..., 1,"') Ч... Ч а(1(е), ..., 1(е)) /» где 11 ~, ..., 1~.'1, ..., 1(а) суть некоторые термы; причем этот вывод будет производиться, исходя из аксиом ч)м,..., ф1, сред- ствами элементарного исчисления, т. е. с использованием под- становок вместо свободных переменных, входящих в ф„ ..., ч)1, и с применением средств исчисления высказываний. Тем самым мы получаем следующее обобщение первой в-л»горгмы: Пусть нам дан вывод некоторой формулы зу,...зу„а(у,, ..., у,), не содержащей, кроме у„.„з хм никаких других связинных перв- ДОКАЗАТЕЛЬСТВА НЕПРОТИВОРЕЧИВОСТИ данных.

Пусть этот вывод производится, исходя из некоторых аксиом '~зм ..., 71, средствами исчисления предика»Лог и, быть Азолсгт, с использованием е-формулы. Тогда можно построить токой вывод некоторой формулы а(1)-, ..., 1,-)Ч...Ча(11а), ..., 1(6)) гдг 1',", °, 12, ..., 1(Е) суть термы без е-символов, в котором используются люлько аксиомы А)„..., 'л)1 и средства элементарного исчисления со свободными переменными.

Заслуживает внимания тот факт, что от этой заключительной формулы к первоначальной заключительной формуле :-)у,... =)и,а(у„..., у,) можно без труда вернуться с использованием основной формулы (Ь) исчисления предикатов и средств исчисления высказываний. $ 4. Доказательства непротиворечивости а) Одна общая теорема о непротиворечивости. Мы прп 2еним теперь нашу первую е-теорему к исследованию проблематики, связанной с непротиворечивостью. Ради этих применений мы и занялись доказательством нашей теоремы').

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

Л первого тома '). Мы имеем в виду формализм, который получается в результате добавления к исчислению пре- дикатов двух предикатных символов и <, индивидного сим- вола О и штрих-символа в качестве функционального знака, а также следующих аксиом: аксиомы равенства: (51) а .а, (аз) а Ь-~(А (а) -з. А (Ь)), аксиомы порядка: (<2) ~(а<а), (~ 2) а< Ьг»Ь<с»-а<о, (<з) а<а' '1 См. с.

25 — 26. 2) См. т. 1, с. 273 я далее. ИСКЛЮЧЕНИЕ СВЯЗАННЫХ ПЕРЕМЕННЫХ и аксиомы Пеано: (рз) (Ре) а' = Ь' -+. а = Ь. Доказательство непротиворечивости этой системы — мы обозначим ее посредством (Я) — было проведено в два этапа: сначала мы рассмотрели выводы, обходящиеся без использования связанных переменных, а затем перешли к общему случаю, основанному на использовании всего исчисления преднкатов в целом. Это разбиение доказательства иа две части в то время носило только эвристический характер, Но теперь, применяя нашу е-теорему, рассмотрение упомянутого частного случая можно будет достроить до нового доказательства непротиворечивости.

Доказательство это легко получается с учетом следующих фактов: 1. Утверждение о непротиворечивости системы (5) нам удалось усилить до позитивного утверждения об истинности всякой выводимой в (В) нумерической формулы. При этом нумерической формулой мы назвали формулу, которая либо является равенством цифр, либо неравенством ') между цифрами, либо строится из формул этого рода с помощью связок исчисления высказываний, а разбиение нумерических формул на истинные и ложные мы произвели в соответствии с арифметическим пониманием нумерических элементарных формул и с пониманием связок исчисления высказываний как истииностных функций'). 2.

Аксиомы системы (В) не содержат связанных переменных. Все они, за исключением аксиомы (),), являются собственными аксиомами, а аксиома равенства ()а), как было показано в гл. ЧИ первого тома'), может быть заменена следующими собственными аксиомами: а=Ь вЂ” Р(а=с-РЬ к В), а=Ь-+-а'=Ь', Д) а = Ь -+ (а < с -+ Ь ( с), а=Ь-+(с(а-а.с<Ь). Получающуюся из (В) в результате этой замены систему аксиом мы обозначим посредством (В*). Она равносильна системе (Я). После эзого искомое доказательство сводится к тому, чтобы показать, что всякая выводимая в системе (В") нумерическая формула является истинной.

Так как все аксиомы системы (Ба) являются собственными аксиомами без связанных переменных, з) Неравенствами мы назвали формулы вида е(й см. т. 1, с, 283. з) См. т. К с. 283 — 284. а) См. т. 1, с. 456 — 459, ДОКАЗАТЕЛЬСТВА НЕПРОТИВОРЕЧИВОСТИ то, со~ласно нашей е-теореме, из вывода любой нумерической формулы, проводимого в рамках системы (В*), связанные переменные могут быть исключены, и поэзому нам достаточно показать, что всякая нумерическая формула, выводимая из аксиом системы (В') средствами элементарного исчисления со свободными переменными, является истинной'). Тем самым сведение общего случая к случаю, когда вывод осуществляется средствами элементарного исчисления, закончено.