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

ерна ию П. Бе найс снова взял на себя на- назад. По моему желанию П. ерна с с го а ю его за тщательность и точность Ф б й он восп оизвел моп взгляды, в разра о б . Генцен, А. Шмидту и Г. ШольГосподам В. Аккерману, Г. Генцену, ект цу я благодарен за их дру ружеское участие в чтении коррек ур. Ги гьберт Геттиквея, март 1939 е. В настоящей книге дается ся детальное изложение современо ии доказательств.

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

оэт у, в. оэтом, независимо от регильбе товской школы ального интереса этих исследований, у ги имеется научный долг подтвердить сделан анные в азличных местах сообщения о существовании тех или или иных доказательств фактическим их изложением. В данном случае э р чае эта пот ебность тем более неотложна, что первое время (во с у во всяком случае, до 19ЗО г.) имелись различные заблуждения относительно границ ПРЕДИСЛОВИЯ АВТОРОВ К ПЕРВОМУ ИЗДАНИЮ применимости доказательств Аккермана и фон Неймана, асио. ванных на одной из упомянутых идей Гильберта, Эти до сих пор не публиковавшиеся доказательства подробно излагаются в главах 1 и П; при этом четко указывается ограниченне, которое здесь требуется наложить на арифметический формализм для установления его непротиворечивости. С помощью одного из изложенных здесь методов получается также некоторый подход к целому ряду теорем, удачно завершающих исследование исчисления предикатов средствами теории доказательств и имеющих замечательные приложения в области аксиоматического метода.

В центре этих рассмотрений стоит одна впервые сформулированная и доказанная Ж.Эрбраиом теорема математической логики, для которой на указанном пути получается естественное и простое доказательство. Разбор приложений этой теоремы дает удобный повод рассмотреть ряд вопросов, связанных с проблемой разрешимости. На этой основе в гл. !А~ мы доказываем одно сформулированное уже в т. 1 усиление теоремы Геделя о полноте исчисления предикатов, выдержанное в духе теории доказательств. Вторая основная тема — это критический анализ обстоятельств, вызывающих необходимость расширения (по сравнению с описанной ранее «финитной точкой зрения») способов содержательных рассуждений, которые допускаются при рассмотрении теории доказательств. Здесь в центре внимания находится обнаруженный Геделем факт дедуктивной неполноты любых четко очерченных и обладающих достаточными выразительными возможностями формализмов. Мы подробно разбираем обе выражающие этот факт теоремы Геделя как с точки зрения их связи с семантическими парадоксами, так и с точки зрения анализа условий их применимости.

Мы приводим также их доказательства (доказательство второй из этих теорем Гедель только наметил) и рассматриваем вопрос о их применимости к формализму арифметики. Дискуссия по поводу расширения финитной точки зрения заканчивается рассмотрением генценовского доказательства непротиворечивости арифметического формализма. Правда, из этого доказательства детально излагается и разбирается лишь то, что составляет методическое нововведение Генцена, а именно использование некоторого частного типа канторовской «трансфинитной индукции».

Тот факт, что это доказательство излагается в неполном виде, вызван главным образом внешней причиной, заключающейся в том, что к моменту подготовки данного тома к печати новое, по-настоящему прозрачное изложение генценовского доказательства еще не было опубликовано. Впрочем, генценовское доказательство не имеет прямого отношения к формализ- ПРЕДИСЛОВИЯ АВТОРОВ К ПЕРВОМУ ИЗДАНИЮ мат иваемого в данной книге тип .

а. Но недавно Л, КальмаРу удалось модифицирова ассматриваемому в нашей книге гл. формализму, расс получить еще и некоторые упэтом оказалось возможным получит ри э в емя В. Аккерман намеревается применить с ользованном Генценом трансфинитную ду ин кцию в виде, исполь ложенного в гл. П на- для распростр анения своего прежнего, изл ж ь арифметический форма- стоящего т тома доказательства на вес лизм. итывать на это имеются все осЕсли у это дастся — а рассчитыв й мысел Гильберта в части, ка- пова ния,— р ,— то пе воначальны замы , б ет реабилитирован. Однако, сающеис " я его э ективности, уд т тво, можно высказать убеж- учитывая генценовское д оказательство, в еменная неудача теории доказат ление что Р .

т ебования Впрочем окончательный з-за того, что к этой ком высокие методические тре ования. вынести лишь с ьбе теории доказательств может вын с ПРОТИВОРЕЧИВОСТИ ЗНЗЛНЗЗ. азвиваемому в гл. 1 — Ъ' настоящего тома кругу идей е за ачи становлении неп ва П нложения дополняют мате П ассматривается уточнение понятия вы- гл. у'. в Пр ложении рзссмзтрн мой ф нкции, полученное в последнее вр . числимо у осящиеся к этому кругу вопро- способзми, н пр д Осящ иво ятся те относящ СОВ фаКТЫ, КО~ОРЫЕ ЛЕГК Мо~у~ ЫТЬ а егося в данной книге. частно материала, содержащег дится теорема .

р а А. Че ча о невозможности о бщего решения проредикатов. В Приложе- блемы разрешимо сти для исчисления пре ые воп осы дедуктивной логи- нии П1 рассматриваются некоторые вопросы . т также ряд дополнени ки высказываний Оно содержит й в гл. П1 т. 1 «позитивной логике». изложенно в гл. азличные дедуктивные фор- В Приложении 1Аг приведены разли я анализа и показано, как с помощью этих орма- мализмы для анализа и п ействительных чисел и тео- лизмов можно изложить теорию де ст Рию чисел втор ого числового класса. бзо п авил исчисления предика- Приложение 1 содержит обзор правил и тов, а также применений этого исчисления к вопросам оме того в нем содержится ряд лизации систем аксиом, роме т, я замечаний, касающихся возможности и некото ых мод акже конспективное из- исчисления предикатов. Проводится также з льтатов, содержащихся ложение различных понятий и резуль в т.! К сожалению, из-за сильно разросшегося о ося обьема книги мы м, относящихся к теории не смогли коснуться в ней ряда тем, отно щ !4 ПРЕДИСЛОВИЯ АВТОРОВ К ПЕРВОМУ ИЗДАНИЮ Цюрих, феврали 1939 г.

Пауль Бернайс доказательств. В частности, нерассмотренным осталось мно- сертацни Э б ана и госортное исчисление предикатов, впервые поя р рана и недавно более подробно исследованное Арнольдом Шмидтом (см. Ма)Ь. Апп., 115). гивавшиеся в л В книге ие изложены также и некоторые вопросы, р , затра- с ним, но либо ост . екциях Гильберта и обсуждавшиес б я в еседах оставшиеся в разрозненных заметках, либо во- обще пока ие азоб лений чисел вто о р равные.

Таковы, например, наброски опре р го числового класса с помощью обычных т. е. не трансфинитных) рекурсий, а также наброски, каса- ющиеся использования символов для видов (6 11 Ьо!е) — в част ности, символов, вводимых при помощи явных илн рекурсивных определений. Настоящий том написан как продолжение пе в г . М численные отс ылки к тем или иным страницам первого тома стороны, приведен- сщс более усиливают связь с ним.

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

1. ч Читателю яастоящего тома было бы целесооб тением гл. 1 ознакомиться с Приложением 1, а о разно пе ед отдельным ст а ением, а отсылками к ког раницам т. 1 он может пользоваться лиш лишь тогда, этом. да у него будет возникать действительна б я потре ность в К сделанном в гл. П у . 1 указанию иа возможность некоторо- го пропуска при чтении мы добавим, что довольно утомитель- ный $2 гл. 1Ч также может быть пропущен. Что касается упоминаний глав, то номера 1 — Ч, циально н е оговорено противное, будут относиться к р —, если спе- т. 11, а номе а Ч1 — ! с к данному с т. 1.

ра — Ч П будут упоминаться только в связ а — . связи ПРЕДИСЛОВИЕ КО ВТОРОМУ ИЗДАНИЮ В дополнение к сказанному в предисловии к первому изда иию хотелось бы заметить следующее. Ввиду плодотворного развития теории доказательств, имевшего место за время, истекшее после первого издания, настоящая книга, разумеется, уже не может претендовать на всесторонний охват современного состояния данной теории. Об этом специально говорилось в предисловии ко второму изданию первого тома. Нам остается лишь вкратце указать, чем второе издание второго тома отличается от первого его издания, Наиболее существенным добавлением является Приложение Ч, в котором приводятся упомянутые в предисловии к первому изданию доказательства Л. Кальмара и В. Аккермана.

В качестве нефинитиого средства, используемого в этих доказательствах, фигурирует лишь некоторая обобщенная индукция, относящаяся к так называемым «О-со-фигурам», которые составляют допускающий финитное описание начальный отрезок канторовского второго числового класса. Применимость этого обобщенного принципа индукции устанавливается при помощи специального арифметического перевода [см. гл.

Ч, $3, п. в)1. В большинстве своих применений — в том числе н в обоих упомянутых доказательствах — этот обобщенный принцип индукции может быть заменен эквивалентным ему в рамках канторовской теории множеств предложением о том, что всякая убываюгцая последовательность О-ы-фигур после конечного числа шагов обрывается. В Приложении Ч дается также прямое и относительно простое доказательство этого утверждения.